Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrE5M..
/
57bda..
PUSyL..
/
f94c0..
vout
PrE5M..
/
b4e2a..
19.99 bars
TMHDV..
/
47fb0..
ownership of
1bdc8..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMZMM..
/
a8ee2..
ownership of
87aa1..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMPeo..
/
d05b9..
ownership of
321de..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcXn..
/
72b02..
ownership of
1115a..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVoE..
/
a1f9f..
ownership of
c0058..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMYJn..
/
fcf89..
ownership of
8eb80..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMaSr..
/
caa53..
ownership of
8745b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbsT..
/
e4c15..
ownership of
339a9..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTDM..
/
bad70..
ownership of
2c340..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNYs..
/
f5db2..
ownership of
562b8..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJxi..
/
80eb8..
ownership of
4d5b3..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJM5..
/
d9649..
ownership of
fd76e..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVbk..
/
531fe..
ownership of
19dcc..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMd2a..
/
62ef1..
ownership of
23535..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKro..
/
0d63c..
ownership of
6265f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGZC..
/
b0895..
ownership of
42525..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbws..
/
d209f..
ownership of
a6fb8..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMX2W..
/
3027e..
ownership of
a08a1..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMc2E..
/
cdb64..
ownership of
11204..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMW62..
/
27a20..
ownership of
8ddf3..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQQD..
/
3c88f..
ownership of
96773..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRGn..
/
eccd7..
ownership of
ed3e7..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMLz7..
/
7ddd1..
ownership of
f367d..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMMA7..
/
ce069..
ownership of
480dd..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMZgZ..
/
fbe29..
ownership of
2b76d..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQ5H..
/
c5092..
ownership of
0b753..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMK8N..
/
679f2..
ownership of
ffd8b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMXxW..
/
b7a79..
ownership of
63ba9..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVVe..
/
f1a75..
ownership of
dab9e..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMT9n..
/
7e6ee..
ownership of
b1337..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGNV..
/
532a3..
ownership of
9df8b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMda4..
/
b10f5..
ownership of
f3deb..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKfc..
/
5a027..
ownership of
091e4..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMaPc..
/
34f1b..
ownership of
54a97..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcXm..
/
a7efe..
ownership of
e6e93..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcmK..
/
9674c..
ownership of
1a54f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMdZL..
/
55cae..
ownership of
2b0c1..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHkh..
/
03260..
ownership of
014f3..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRxp..
/
f9b0a..
ownership of
26de2..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVTr..
/
7e86b..
ownership of
326d2..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJPt..
/
ce2e4..
ownership of
b51a0..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMLTg..
/
7ad44..
ownership of
8be1f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcu2..
/
f45df..
ownership of
75cb5..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMN5J..
/
f8542..
ownership of
dc4de..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKrs..
/
19b26..
ownership of
f387b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQhp..
/
4df06..
ownership of
1ff91..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbve..
/
87492..
ownership of
565cc..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMPY7..
/
0d1e3..
ownership of
1626d..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJtf..
/
91347..
ownership of
95492..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMR2U..
/
f960d..
ownership of
8e6af..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbjL..
/
c4296..
ownership of
dfae7..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRuc..
/
b6bf7..
ownership of
d223e..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNfh..
/
3bf6a..
ownership of
6172f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMG5G..
/
36314..
ownership of
38fd3..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMb4k..
/
3ff3c..
ownership of
912ff..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMLaz..
/
8146f..
ownership of
af9fb..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQKk..
/
a982f..
ownership of
d7558..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTen..
/
a3848..
ownership of
a5347..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcvY..
/
5ac1b..
ownership of
2dc52..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJrB..
/
14983..
ownership of
3444c..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGkE..
/
6dc63..
ownership of
e106e..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMdD8..
/
88e11..
ownership of
ee746..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMax1..
/
92c13..
ownership of
26e35..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJS3..
/
db4b2..
ownership of
424f0..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMaGw..
/
9d555..
ownership of
0b544..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMMnm..
/
adecf..
ownership of
a9f23..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRea..
/
5d4f5..
ownership of
152f8..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcp9..
/
5ba70..
ownership of
31b73..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJcv..
/
51390..
ownership of
f6a5c..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMSV8..
/
ea828..
ownership of
88fb9..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMYmj..
/
ed541..
ownership of
200f9..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHYm..
/
8694c..
ownership of
f0459..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVYj..
/
406f8..
ownership of
fa15a..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMLEX..
/
d508a..
ownership of
1eba3..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMdPc..
/
6e8d9..
ownership of
710e0..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMFqd..
/
f9894..
ownership of
7648d..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTJC..
/
10e0d..
ownership of
a86e4..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMUGo..
/
a429c..
ownership of
2a532..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMK5m..
/
2b042..
ownership of
f9399..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJbi..
/
37de6..
ownership of
d87f1..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHyR..
/
5d5e8..
ownership of
807c4..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGPX..
/
a2a58..
ownership of
4acd4..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMZ5n..
/
fdb90..
ownership of
c4639..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMF86..
/
01587..
ownership of
3e4ce..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcwg..
/
5f952..
ownership of
3e84b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHnk..
/
2db95..
ownership of
3ef06..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJ7w..
/
cac26..
ownership of
5d12f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMasa..
/
947b3..
ownership of
c3c64..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMEnR..
/
cc882..
ownership of
c0e34..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNfC..
/
f7be2..
ownership of
f97d4..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNLW..
/
b87f0..
ownership of
bed93..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMdGm..
/
30783..
ownership of
d5698..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbu6..
/
e4d4d..
ownership of
dc738..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMSy1..
/
55e55..
ownership of
99365..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHRn..
/
88b58..
ownership of
f95ec..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMSb2..
/
14392..
ownership of
b424f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMd7q..
/
9ceb3..
ownership of
29c9c..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMapG..
/
ad38b..
ownership of
25fc3..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcNq..
/
9e338..
ownership of
e1ab0..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJqC..
/
be057..
ownership of
4d7be..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKCW..
/
753b1..
ownership of
72eef..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQ1C..
/
d0cde..
ownership of
cdddc..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMFRx..
/
f8770..
ownership of
54c27..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMK4v..
/
dc55b..
ownership of
094e7..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMUT2..
/
24173..
ownership of
6e87c..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMYqv..
/
fc663..
ownership of
c5e73..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTSp..
/
c7b8b..
ownership of
14f80..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGxH..
/
5d776..
ownership of
ca4bc..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMLYV..
/
b63ba..
ownership of
18f73..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVyK..
/
55fd6..
ownership of
f7184..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMJMJ..
/
20e70..
ownership of
4209f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHhh..
/
a0a52..
ownership of
e9032..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMaYZ..
/
62c21..
ownership of
892c4..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMckD..
/
57d41..
ownership of
7de75..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRka..
/
2c2ab..
ownership of
98c22..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQPM..
/
c7d21..
ownership of
d5d02..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMZpK..
/
483ed..
ownership of
31254..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMPCp..
/
4967c..
ownership of
d1683..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNM1..
/
079cb..
ownership of
9d312..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMZSf..
/
538fe..
ownership of
4160b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMSPy..
/
b6b54..
ownership of
0a605..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbM2..
/
c3a22..
ownership of
a0f0f..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKZb..
/
2fc0b..
ownership of
4cd0b..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbsX..
/
0577e..
ownership of
67747..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTz5..
/
21766..
ownership of
c5a9d..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMHBz..
/
88f47..
ownership of
812a5..
as prop with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVQv..
/
18e94..
ownership of
ead2c..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMPim..
/
d85a1..
ownership of
8b980..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMdQH..
/
c3e96..
ownership of
0ccdf..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMFsC..
/
ab958..
ownership of
5eaf9..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNPe..
/
8854b..
ownership of
a42b7..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcbp..
/
2c20d..
ownership of
19cb9..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMF8e..
/
24bf5..
ownership of
89a26..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMS8d..
/
8fd1c..
ownership of
98f4e..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMYcx..
/
e3bbf..
ownership of
ee004..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKUw..
/
84297..
ownership of
57b37..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRrK..
/
bf3fe..
ownership of
c2616..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMcmB..
/
b65cc..
ownership of
4f282..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMFih..
/
6fccc..
ownership of
95551..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMR2t..
/
da0f9..
ownership of
c1fc8..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMRGP..
/
51790..
ownership of
c748f..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMPZm..
/
59f25..
ownership of
f9f7a..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMUhw..
/
f5d9f..
ownership of
f1b6a..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGe5..
/
9e1a3..
ownership of
e81ec..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMV73..
/
87ed6..
ownership of
9f09b..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTfT..
/
3d097..
ownership of
b9355..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMVFQ..
/
9e8a1..
ownership of
31bb2..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMXuu..
/
0dc60..
ownership of
4809f..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMXYX..
/
e6ff8..
ownership of
d7ab0..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMNEB..
/
c9e75..
ownership of
b4a64..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMYC2..
/
f9f1f..
ownership of
cab0f..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMEh8..
/
56c9a..
ownership of
3a8be..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMc22..
/
81f8f..
ownership of
4b512..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMQk7..
/
a2b17..
ownership of
ac880..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMbDW..
/
2de7a..
ownership of
b2d12..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMX3Z..
/
41933..
ownership of
06053..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTk3..
/
3da15..
ownership of
b942b..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMdst..
/
1e8db..
ownership of
c1215..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMYe3..
/
7edca..
ownership of
7084d..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMKjD..
/
caf8d..
ownership of
c4696..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMTXe..
/
35b95..
ownership of
5773e..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMc6f..
/
7512c..
ownership of
fa593..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMZgZ..
/
91977..
ownership of
743c9..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMGEK..
/
7f0c7..
ownership of
b2f97..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMF5G..
/
ea724..
ownership of
9ed63..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
TMSS4..
/
f433c..
ownership of
d3520..
as obj with payaddr
Pr6Pc..
rightscost 0.00 controlledby
Pr6Pc..
upto 0
PUgzH..
/
923e7..
doc published by
Pr6Pc..
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
encode_c
encode_c
:
ι
→
(
(
ι
→
ο
) →
ο
) →
ι
Param
encode_b
encode_b
:
ι
→
CT2
ι
Definition
pack_c_b
:=
λ x0 .
λ x1 :
(
ι → ο
)
→ ο
.
λ x2 :
ι →
ι → ι
.
lam
3
(
λ x3 .
If_i
(
x3
=
0
)
x0
(
If_i
(
x3
=
1
)
(
encode_c
x0
x1
)
(
encode_b
x0
x2
)
)
)
Param
ap
ap
:
ι
→
ι
→
ι
Known
tuple_3_0_eq
tuple_3_0_eq
:
∀ x0 x1 x2 .
ap
(
lam
3
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
x1
x2
)
)
)
0
=
x0
Theorem
pack_c_b_0_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ι
.
x0
=
pack_c_b
x1
x2
x3
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_c_b_0_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ι
.
x0
=
ap
(
pack_c_b
x0
x1
x2
)
0
(proof)
Param
decode_c
decode_c
:
ι
→
(
ι
→
ο
) →
ο
Known
tuple_3_1_eq
tuple_3_1_eq
:
∀ x0 x1 x2 .
ap
(
lam
3
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
x1
x2
)
)
)
1
=
x1
Known
decode_encode_c
decode_encode_c
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ο
.
(
∀ x3 .
x2
x3
⟶
x3
∈
x0
)
⟶
decode_c
(
encode_c
x0
x1
)
x2
=
x1
x2
Theorem
pack_c_b_1_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ι
.
x0
=
pack_c_b
x1
x2
x3
⟶
∀ x4 :
ι → ο
.
(
∀ x5 .
x4
x5
⟶
x5
∈
x1
)
⟶
x2
x4
=
decode_c
(
ap
x0
1
)
x4
(proof)
Theorem
pack_c_b_1_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ι
.
∀ x3 :
ι → ο
.
(
∀ x4 .
x3
x4
⟶
x4
∈
x0
)
⟶
x1
x3
=
decode_c
(
ap
(
pack_c_b
x0
x1
x2
)
1
)
x3
(proof)
Param
decode_b
decode_b
:
ι
→
ι
→
ι
→
ι
Known
tuple_3_2_eq
tuple_3_2_eq
:
∀ x0 x1 x2 .
ap
(
lam
3
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
x1
x2
)
)
)
2
=
x2
Known
decode_encode_b
decode_encode_b
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
decode_b
(
encode_b
x0
x1
)
x2
x3
=
x1
x2
x3
Theorem
pack_c_b_2_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ι
.
x0
=
pack_c_b
x1
x2
x3
⟶
∀ x4 .
x4
∈
x1
⟶
∀ x5 .
x5
∈
x1
⟶
x3
x4
x5
=
decode_b
(
ap
x0
2
)
x4
x5
(proof)
Theorem
pack_c_b_2_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
x4
=
decode_b
(
ap
(
pack_c_b
x0
x1
x2
)
2
)
x3
x4
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Theorem
pack_c_b_inj
:
∀ x0 x1 .
∀ x2 x3 :
(
ι → ο
)
→ ο
.
∀ x4 x5 :
ι →
ι → ι
.
pack_c_b
x0
x2
x4
=
pack_c_b
x1
x3
x5
⟶
and
(
and
(
x0
=
x1
)
(
∀ x6 :
ι → ο
.
(
∀ x7 .
x6
x7
⟶
x7
∈
x0
)
⟶
x2
x6
=
x3
x6
)
)
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
=
x5
x6
x7
)
(proof)
Param
iff
iff
:
ο
→
ο
→
ο
Known
encode_b_ext
encode_b_ext
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x1
x3
x4
=
x2
x3
x4
)
⟶
encode_b
x0
x1
=
encode_b
x0
x2
Known
encode_c_ext
encode_c_ext
:
∀ x0 .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
(
∀ x3 :
ι → ο
.
(
∀ x4 .
x3
x4
⟶
x4
∈
x0
)
⟶
iff
(
x1
x3
)
(
x2
x3
)
)
⟶
encode_c
x0
x1
=
encode_c
x0
x2
Theorem
pack_c_b_ext
:
∀ x0 .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x0
)
⟶
iff
(
x1
x5
)
(
x2
x5
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
=
x4
x5
x6
)
⟶
pack_c_b
x0
x1
x3
=
pack_c_b
x0
x2
x4
(proof)
Definition
struct_c_b
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
(
ι → ο
)
→ ο
.
∀ x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
x2
⟶
∀ x6 .
x6
∈
x2
⟶
x4
x5
x6
∈
x2
)
⟶
x1
(
pack_c_b
x2
x3
x4
)
)
⟶
x1
x0
Theorem
pack_struct_c_b_I
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
x4
∈
x0
)
⟶
struct_c_b
(
pack_c_b
x0
x1
x2
)
(proof)
Theorem
pack_struct_c_b_E2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ι
.
struct_c_b
(
pack_c_b
x0
x1
x2
)
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
x4
∈
x0
(proof)
Known
iff_refl
iff_refl
:
∀ x0 : ο .
iff
x0
x0
Theorem
struct_c_b_eta
:
∀ x0 .
struct_c_b
x0
⟶
x0
=
pack_c_b
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_b
(
ap
x0
2
)
)
(proof)
Definition
unpack_c_b_i
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ι
)
→ ι
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_b
(
ap
x0
2
)
)
Theorem
unpack_c_b_i_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ι
)
→ ι
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ι
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
x3
x6
x7
=
x5
x6
x7
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_b_i
(
pack_c_b
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
unpack_c_b_o
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ι
)
→ ο
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_b
(
ap
x0
2
)
)
Theorem
unpack_c_b_o_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ι
)
→ ο
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ι
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
x3
x6
x7
=
x5
x6
x7
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_b_o
(
pack_c_b
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
pack_c_u
:=
λ x0 .
λ x1 :
(
ι → ο
)
→ ο
.
λ x2 :
ι → ι
.
lam
3
(
λ x3 .
If_i
(
x3
=
0
)
x0
(
If_i
(
x3
=
1
)
(
encode_c
x0
x1
)
(
lam
x0
x2
)
)
)
Theorem
pack_c_u_0_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ι
.
x0
=
pack_c_u
x1
x2
x3
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_c_u_0_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ι
.
x0
=
ap
(
pack_c_u
x0
x1
x2
)
0
(proof)
Theorem
pack_c_u_1_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ι
.
x0
=
pack_c_u
x1
x2
x3
⟶
∀ x4 :
ι → ο
.
(
∀ x5 .
x4
x5
⟶
x5
∈
x1
)
⟶
x2
x4
=
decode_c
(
ap
x0
1
)
x4
(proof)
Theorem
pack_c_u_1_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
(
∀ x4 .
x3
x4
⟶
x4
∈
x0
)
⟶
x1
x3
=
decode_c
(
ap
(
pack_c_u
x0
x1
x2
)
1
)
x3
(proof)
Known
beta
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
Theorem
pack_c_u_2_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ι
.
x0
=
pack_c_u
x1
x2
x3
⟶
∀ x4 .
x4
∈
x1
⟶
x3
x4
=
ap
(
ap
x0
2
)
x4
(proof)
Theorem
pack_c_u_2_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x2
x3
=
ap
(
ap
(
pack_c_u
x0
x1
x2
)
2
)
x3
(proof)
Theorem
pack_c_u_inj
:
∀ x0 x1 .
∀ x2 x3 :
(
ι → ο
)
→ ο
.
∀ x4 x5 :
ι → ι
.
pack_c_u
x0
x2
x4
=
pack_c_u
x1
x3
x5
⟶
and
(
and
(
x0
=
x1
)
(
∀ x6 :
ι → ο
.
(
∀ x7 .
x6
x7
⟶
x7
∈
x0
)
⟶
x2
x6
=
x3
x6
)
)
(
∀ x6 .
x6
∈
x0
⟶
x4
x6
=
x5
x6
)
(proof)
Known
encode_u_ext
encode_u_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
lam
x0
x1
=
lam
x0
x2
Theorem
pack_c_u_ext
:
∀ x0 .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
∀ x3 x4 :
ι → ι
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x0
)
⟶
iff
(
x1
x5
)
(
x2
x5
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
x3
x5
=
x4
x5
)
⟶
pack_c_u
x0
x1
x3
=
pack_c_u
x0
x2
x4
(proof)
Definition
struct_c_u
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
(
ι → ο
)
→ ο
.
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
x2
⟶
x4
x5
∈
x2
)
⟶
x1
(
pack_c_u
x2
x3
x4
)
)
⟶
x1
x0
Theorem
pack_struct_c_u_I
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x0
)
⟶
struct_c_u
(
pack_c_u
x0
x1
x2
)
(proof)
Theorem
pack_struct_c_u_E2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ι
.
struct_c_u
(
pack_c_u
x0
x1
x2
)
⟶
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x0
(proof)
Theorem
struct_c_u_eta
:
∀ x0 .
struct_c_u
x0
⟶
x0
=
pack_c_u
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
ap
(
ap
x0
2
)
)
(proof)
Definition
unpack_c_u_i
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ι
)
→ ι
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
ap
(
ap
x0
2
)
)
Theorem
unpack_c_u_i_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ι
)
→ ι
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ι
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x3
x6
=
x5
x6
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_u_i
(
pack_c_u
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
unpack_c_u_o
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ι
)
→ ο
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
ap
(
ap
x0
2
)
)
Theorem
unpack_c_u_o_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ι
)
→ ο
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ι
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x3
x6
=
x5
x6
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_u_o
(
pack_c_u
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Param
encode_r
encode_r
:
ι
→
(
ι
→
ι
→
ο
) →
ι
Definition
pack_c_r
:=
λ x0 .
λ x1 :
(
ι → ο
)
→ ο
.
λ x2 :
ι →
ι → ο
.
lam
3
(
λ x3 .
If_i
(
x3
=
0
)
x0
(
If_i
(
x3
=
1
)
(
encode_c
x0
x1
)
(
encode_r
x0
x2
)
)
)
Theorem
pack_c_r_0_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ο
.
x0
=
pack_c_r
x1
x2
x3
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_c_r_0_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 x3 :
ι →
ι → ο
.
x3
x0
(
ap
(
pack_c_r
x0
x1
x2
)
0
)
⟶
x3
(
ap
(
pack_c_r
x0
x1
x2
)
0
)
x0
(proof)
Theorem
pack_c_r_1_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ο
.
x0
=
pack_c_r
x1
x2
x3
⟶
∀ x4 :
ι → ο
.
(
∀ x5 .
x4
x5
⟶
x5
∈
x1
)
⟶
x2
x4
=
decode_c
(
ap
x0
1
)
x4
(proof)
Theorem
pack_c_r_1_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
(
∀ x4 .
x3
x4
⟶
x4
∈
x0
)
⟶
x1
x3
=
decode_c
(
ap
(
pack_c_r
x0
x1
x2
)
1
)
x3
(proof)
Param
decode_r
decode_r
:
ι
→
ι
→
ι
→
ο
Known
decode_encode_r
decode_encode_r
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
decode_r
(
encode_r
x0
x1
)
x2
x3
=
x1
x2
x3
Theorem
pack_c_r_2_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ο
.
x0
=
pack_c_r
x1
x2
x3
⟶
∀ x4 .
x4
∈
x1
⟶
∀ x5 .
x5
∈
x1
⟶
x3
x4
x5
=
decode_r
(
ap
x0
2
)
x4
x5
(proof)
Theorem
pack_c_r_2_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
x4
=
decode_r
(
ap
(
pack_c_r
x0
x1
x2
)
2
)
x3
x4
(proof)
Theorem
pack_c_r_inj
:
∀ x0 x1 .
∀ x2 x3 :
(
ι → ο
)
→ ο
.
∀ x4 x5 :
ι →
ι → ο
.
pack_c_r
x0
x2
x4
=
pack_c_r
x1
x3
x5
⟶
and
(
and
(
x0
=
x1
)
(
∀ x6 :
ι → ο
.
(
∀ x7 .
x6
x7
⟶
x7
∈
x0
)
⟶
x2
x6
=
x3
x6
)
)
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
=
x5
x6
x7
)
(proof)
Known
encode_r_ext
encode_r_ext
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
iff
(
x1
x3
x4
)
(
x2
x3
x4
)
)
⟶
encode_r
x0
x1
=
encode_r
x0
x2
Theorem
pack_c_r_ext
:
∀ x0 .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
∀ x3 x4 :
ι →
ι → ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x0
)
⟶
iff
(
x1
x5
)
(
x2
x5
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
iff
(
x3
x5
x6
)
(
x4
x5
x6
)
)
⟶
pack_c_r
x0
x1
x3
=
pack_c_r
x0
x2
x4
(proof)
Definition
struct_c_r
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
(
ι → ο
)
→ ο
.
∀ x4 :
ι →
ι → ο
.
x1
(
pack_c_r
x2
x3
x4
)
)
⟶
x1
x0
Theorem
pack_struct_c_r_I
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι →
ι → ο
.
struct_c_r
(
pack_c_r
x0
x1
x2
)
(proof)
Theorem
struct_c_r_eta
:
∀ x0 .
struct_c_r
x0
⟶
x0
=
pack_c_r
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(proof)
Definition
unpack_c_r_i
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ο
)
→ ι
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
Theorem
unpack_c_r_i_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ο
)
→ ι
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ο
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
iff
(
x3
x6
x7
)
(
x5
x6
x7
)
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_r_i
(
pack_c_r
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
unpack_c_r_o
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ο
)
→ ο
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
Theorem
unpack_c_r_o_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι →
ι → ο
)
→ ο
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
ι → ο
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
iff
(
x3
x6
x7
)
(
x5
x6
x7
)
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_r_o
(
pack_c_r
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Definition
pack_c_p
:=
λ x0 .
λ x1 :
(
ι → ο
)
→ ο
.
λ x2 :
ι → ο
.
lam
3
(
λ x3 .
If_i
(
x3
=
0
)
x0
(
If_i
(
x3
=
1
)
(
encode_c
x0
x1
)
(
Sep
x0
x2
)
)
)
Theorem
pack_c_p_0_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ο
.
x0
=
pack_c_p
x1
x2
x3
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_c_p_0_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ο
.
x0
=
ap
(
pack_c_p
x0
x1
x2
)
0
(proof)
Theorem
pack_c_p_1_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ο
.
x0
=
pack_c_p
x1
x2
x3
⟶
∀ x4 :
ι → ο
.
(
∀ x5 .
x4
x5
⟶
x5
∈
x1
)
⟶
x2
x4
=
decode_c
(
ap
x0
1
)
x4
(proof)
Theorem
pack_c_p_1_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 x3 :
ι → ο
.
(
∀ x4 .
x3
x4
⟶
x4
∈
x0
)
⟶
x1
x3
=
decode_c
(
ap
(
pack_c_p
x0
x1
x2
)
1
)
x3
(proof)
Param
decode_p
decode_p
:
ι
→
ι
→
ο
Known
decode_encode_p
decode_encode_p
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
decode_p
(
Sep
x0
x1
)
x2
=
x1
x2
Theorem
pack_c_p_2_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ο
.
x0
=
pack_c_p
x1
x2
x3
⟶
∀ x4 .
x4
∈
x1
⟶
x3
x4
=
decode_p
(
ap
x0
2
)
x4
(proof)
Theorem
pack_c_p_2_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
x2
x3
=
decode_p
(
ap
(
pack_c_p
x0
x1
x2
)
2
)
x3
(proof)
Theorem
pack_c_p_inj
:
∀ x0 x1 .
∀ x2 x3 :
(
ι → ο
)
→ ο
.
∀ x4 x5 :
ι → ο
.
pack_c_p
x0
x2
x4
=
pack_c_p
x1
x3
x5
⟶
and
(
and
(
x0
=
x1
)
(
∀ x6 :
ι → ο
.
(
∀ x7 .
x6
x7
⟶
x7
∈
x0
)
⟶
x2
x6
=
x3
x6
)
)
(
∀ x6 .
x6
∈
x0
⟶
x4
x6
=
x5
x6
)
(proof)
Known
encode_p_ext
encode_p_ext
:
∀ x0 .
∀ x1 x2 :
ι → ο
.
(
∀ x3 .
x3
∈
x0
⟶
iff
(
x1
x3
)
(
x2
x3
)
)
⟶
Sep
x0
x1
=
Sep
x0
x2
Theorem
pack_c_p_ext
:
∀ x0 .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
∀ x3 x4 :
ι → ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x0
)
⟶
iff
(
x1
x5
)
(
x2
x5
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
iff
(
x3
x5
)
(
x4
x5
)
)
⟶
pack_c_p
x0
x1
x3
=
pack_c_p
x0
x2
x4
(proof)
Definition
struct_c_p
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
(
ι → ο
)
→ ο
.
∀ x4 :
ι → ο
.
x1
(
pack_c_p
x2
x3
x4
)
)
⟶
x1
x0
Theorem
pack_struct_c_p_I
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ο
.
struct_c_p
(
pack_c_p
x0
x1
x2
)
(proof)
Theorem
struct_c_p_eta
:
∀ x0 .
struct_c_p
x0
⟶
x0
=
pack_c_p
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_p
(
ap
x0
2
)
)
(proof)
Definition
unpack_c_p_i
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ι
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_p
(
ap
x0
2
)
)
Theorem
unpack_c_p_i_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ι
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ο
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
iff
(
x3
x6
)
(
x5
x6
)
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_p_i
(
pack_c_p
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
unpack_c_p_o
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
decode_p
(
ap
x0
2
)
)
Theorem
unpack_c_p_o_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι → ο
.
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
∀ x5 :
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
iff
(
x3
x6
)
(
x5
x6
)
)
⟶
x0
x1
x4
x5
=
x0
x1
x2
x3
)
⟶
unpack_c_p_o
(
pack_c_p
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
pack_c_e
:=
λ x0 .
λ x1 :
(
ι → ο
)
→ ο
.
λ x2 .
lam
3
(
λ x3 .
If_i
(
x3
=
0
)
x0
(
If_i
(
x3
=
1
)
(
encode_c
x0
x1
)
x2
)
)
Theorem
pack_c_e_0_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 .
x0
=
pack_c_e
x1
x2
x3
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_c_e_0_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 .
x0
=
ap
(
pack_c_e
x0
x1
x2
)
0
(proof)
Theorem
pack_c_e_1_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 .
x0
=
pack_c_e
x1
x2
x3
⟶
∀ x4 :
ι → ο
.
(
∀ x5 .
x4
x5
⟶
x5
∈
x1
)
⟶
x2
x4
=
decode_c
(
ap
x0
1
)
x4
(proof)
Theorem
pack_c_e_1_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 .
∀ x3 :
ι → ο
.
(
∀ x4 .
x3
x4
⟶
x4
∈
x0
)
⟶
x1
x3
=
decode_c
(
ap
(
pack_c_e
x0
x1
x2
)
1
)
x3
(proof)
Theorem
pack_c_e_2_eq
:
∀ x0 x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 .
x0
=
pack_c_e
x1
x2
x3
⟶
x3
=
ap
x0
2
(proof)
Theorem
pack_c_e_2_eq2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 .
x2
=
ap
(
pack_c_e
x0
x1
x2
)
2
(proof)
Theorem
pack_c_e_inj
:
∀ x0 x1 .
∀ x2 x3 :
(
ι → ο
)
→ ο
.
∀ x4 x5 .
pack_c_e
x0
x2
x4
=
pack_c_e
x1
x3
x5
⟶
and
(
and
(
x0
=
x1
)
(
∀ x6 :
ι → ο
.
(
∀ x7 .
x6
x7
⟶
x7
∈
x0
)
⟶
x2
x6
=
x3
x6
)
)
(
x4
=
x5
)
(proof)
Theorem
pack_c_e_ext
:
∀ x0 .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
∀ x3 .
(
∀ x4 :
ι → ο
.
(
∀ x5 .
x4
x5
⟶
x5
∈
x0
)
⟶
iff
(
x1
x4
)
(
x2
x4
)
)
⟶
pack_c_e
x0
x1
x3
=
pack_c_e
x0
x2
x3
(proof)
Definition
struct_c_e
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
(
ι → ο
)
→ ο
.
∀ x4 .
x4
∈
x2
⟶
x1
(
pack_c_e
x2
x3
x4
)
)
⟶
x1
x0
Theorem
pack_struct_c_e_I
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 .
x2
∈
x0
⟶
struct_c_e
(
pack_c_e
x0
x1
x2
)
(proof)
Theorem
pack_struct_c_e_E2
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 .
struct_c_e
(
pack_c_e
x0
x1
x2
)
⟶
x2
∈
x0
(proof)
Theorem
struct_c_e_eta
:
∀ x0 .
struct_c_e
x0
⟶
x0
=
pack_c_e
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
ap
x0
2
)
(proof)
Definition
unpack_c_e_i
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
ι → ι
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
ap
x0
2
)
Theorem
unpack_c_e_i_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
ι → ι
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 .
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
x0
x1
x4
x3
=
x0
x1
x2
x3
)
⟶
unpack_c_e_i
(
pack_c_e
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)
Definition
unpack_c_e_o
:=
λ x0 .
λ x1 :
ι →
(
(
ι → ο
)
→ ο
)
→
ι → ο
.
x1
(
ap
x0
0
)
(
decode_c
(
ap
x0
1
)
)
(
ap
x0
2
)
Theorem
unpack_c_e_o_eq
:
∀ x0 :
ι →
(
(
ι → ο
)
→ ο
)
→
ι → ο
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
∀ x3 .
(
∀ x4 :
(
ι → ο
)
→ ο
.
(
∀ x5 :
ι → ο
.
(
∀ x6 .
x5
x6
⟶
x6
∈
x1
)
⟶
iff
(
x2
x5
)
(
x4
x5
)
)
⟶
x0
x1
x4
x3
=
x0
x1
x2
x3
)
⟶
unpack_c_e_o
(
pack_c_e
x1
x2
x3
)
x0
=
x0
x1
x2
x3
(proof)