Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrJAV..
/
d2852..
PUep9..
/
6613d..
vout
PrJAV..
/
c9982..
6.57 bars
TMTNa..
/
9aab8..
ownership of
0c548..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKwA..
/
460ce..
ownership of
baacc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMG3J..
/
5224a..
ownership of
880bf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYed..
/
54d7e..
ownership of
7a756..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEyP..
/
0ba19..
ownership of
fa3b1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TManV..
/
e7250..
ownership of
7e28f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKQ1..
/
5757b..
ownership of
08a8a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGVN..
/
eeb79..
ownership of
1014a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaHz..
/
26a1e..
ownership of
c1030..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ9Y..
/
c917c..
ownership of
3b7ab..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcAD..
/
dfbfa..
ownership of
d5832..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TML6E..
/
cd5b5..
ownership of
76e0c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMdZ..
/
4847d..
ownership of
d0102..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMF4R..
/
f17aa..
ownership of
332ce..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNxz..
/
b1fba..
ownership of
8d10c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMn4..
/
1b346..
ownership of
3ee73..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQRL..
/
e956d..
ownership of
36ee1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWA1..
/
cd963..
ownership of
2fcf8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGMZ..
/
4a4c3..
ownership of
4bb51..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMagr..
/
9f368..
ownership of
2de6d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGGu..
/
7e16b..
ownership of
29558..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLTi..
/
1f0b7..
ownership of
87a4a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMRn..
/
c09b5..
ownership of
9103b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTTD..
/
e6c21..
ownership of
19cd9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVLM..
/
e2718..
ownership of
15b71..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMczy..
/
da834..
ownership of
2a894..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGxX..
/
0c76f..
ownership of
79c62..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTQk..
/
c3baf..
ownership of
b2e26..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRji..
/
c4268..
ownership of
94f11..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJAC..
/
a5c9c..
ownership of
0d995..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMH6h..
/
f70aa..
ownership of
405a7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTsA..
/
fbb08..
ownership of
a6055..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJd1..
/
ed1de..
ownership of
4367f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJxK..
/
58990..
ownership of
a6a9b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMS5W..
/
62aae..
ownership of
379ab..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJnp..
/
73078..
ownership of
5bc2e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRNN..
/
c391f..
ownership of
b637c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTb1..
/
0c8f0..
ownership of
aa8d9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQam..
/
a3cf7..
ownership of
0df0e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKEJ..
/
ec841..
ownership of
d38ea..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEw2..
/
7b4cb..
ownership of
f8932..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbEY..
/
36c40..
ownership of
c5ad5..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYo6..
/
e543c..
ownership of
f094f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMMF..
/
a7a2f..
ownership of
aca0d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYNA..
/
ae2d1..
ownership of
35493..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZdg..
/
f2848..
ownership of
f2dd7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNHa..
/
7d0dc..
ownership of
2c0ad..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ9i..
/
5b12a..
ownership of
59656..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMmX..
/
64124..
ownership of
ad903..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQ8n..
/
695a7..
ownership of
42d45..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNPC..
/
7f7f4..
ownership of
8feac..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFbq..
/
26fce..
ownership of
5a5be..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZ49..
/
89d94..
ownership of
c69df..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMNk..
/
83f0a..
ownership of
2907d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYB1..
/
6d0aa..
ownership of
de381..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTxD..
/
6bb28..
ownership of
d4a9d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQyW..
/
52fed..
ownership of
ed37d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQLy..
/
523ae..
ownership of
b02df..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXWQ..
/
dc46c..
ownership of
9bd10..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZ1A..
/
cd685..
ownership of
9ca3e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFnU..
/
6df01..
ownership of
08bc8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZQy..
/
2f62a..
ownership of
afabf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQb6..
/
81e8b..
ownership of
fcbe2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMK7g..
/
7838b..
ownership of
895d7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFXJ..
/
b70b8..
ownership of
cb962..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXNo..
/
6c25a..
ownership of
7c361..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMR7x..
/
f37cb..
ownership of
3733f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMK1t..
/
fa0ce..
ownership of
c0b88..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJq3..
/
dc0c6..
ownership of
e80f9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLoc..
/
87492..
ownership of
aee68..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNmP..
/
bd375..
ownership of
c6a19..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQsw..
/
bc570..
ownership of
e900d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWx4..
/
ddcb5..
ownership of
1f8f6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHGz..
/
86be8..
ownership of
2b7ef..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUTE..
/
d1b19..
ownership of
18198..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNGG..
/
ba79a..
ownership of
c122f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX5V..
/
f04ef..
ownership of
f8f97..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRXK..
/
2a463..
ownership of
98214..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPDL..
/
e60eb..
ownership of
4ab8c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMa7P..
/
e4a85..
ownership of
edb4f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVJ3..
/
0b1f0..
ownership of
cda5c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMpb..
/
91ed8..
ownership of
e93eb..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUhx..
/
99152..
ownership of
f6693..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJUp..
/
b53f8..
ownership of
e4b35..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPcM..
/
6127a..
ownership of
8f2fd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJoD..
/
61bb3..
ownership of
06d9a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKB8..
/
3e210..
ownership of
520af..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQ3N..
/
7eb02..
ownership of
ad3bf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUBP..
/
acafb..
ownership of
1affc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKRf..
/
181d3..
ownership of
861a7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMapL..
/
dfa64..
ownership of
6a36d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJvh..
/
982e5..
ownership of
aa4c5..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFmH..
/
e9737..
ownership of
cce3d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSs4..
/
fce04..
ownership of
2274f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPNW..
/
c4c43..
ownership of
bb047..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVVc..
/
dbdc7..
ownership of
ac34b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRaY..
/
b90b3..
ownership of
2328b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNoH..
/
2f7f8..
ownership of
d116b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSgB..
/
6897b..
ownership of
d4f35..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYCX..
/
31ec5..
ownership of
588f3..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFBw..
/
ef651..
ownership of
475c2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMc9M..
/
0cb97..
ownership of
3bb43..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUK7..
/
bd213..
ownership of
b5182..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMW5S..
/
932ec..
ownership of
95991..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSiU..
/
ade15..
ownership of
bd396..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZQ7..
/
35cd3..
ownership of
4c9d6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNq9..
/
cf729..
ownership of
c0856..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMM47..
/
04ee7..
ownership of
85693..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPak..
/
f3c2a..
ownership of
77081..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZLP..
/
011da..
ownership of
64667..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYMe..
/
c507f..
ownership of
4e83a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTFx..
/
598ef..
ownership of
50179..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSWu..
/
05dd9..
ownership of
92b4c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKaL..
/
0ec66..
ownership of
107e9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVQE..
/
8d2ba..
ownership of
afe85..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMHA..
/
75d5e..
ownership of
f6765..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQGs..
/
83c4b..
ownership of
f7a51..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbvs..
/
033c5..
ownership of
51062..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJCX..
/
6e115..
ownership of
1dd49..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMP1c..
/
b82b1..
ownership of
f55ea..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZYU..
/
4e5ab..
ownership of
889ba..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTUP..
/
73b74..
ownership of
7a3ae..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVez..
/
39855..
ownership of
8a20d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHxE..
/
98b15..
ownership of
8f6c6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMG1i..
/
e3a17..
ownership of
0c39e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHvd..
/
3c1d2..
ownership of
9b3fb..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMS4j..
/
d4426..
ownership of
a8add..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYSa..
/
f86f9..
ownership of
425a2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUV6..
/
69f6c..
ownership of
e7bf4..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXKo..
/
15599..
ownership of
49886..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHvz..
/
8d667..
ownership of
8ecfa..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKZh..
/
8a3ad..
ownership of
5b1bd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWdj..
/
ef8ae..
ownership of
81d8b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMuk..
/
b5ea2..
ownership of
c294a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRJQ..
/
d8eee..
ownership of
481fd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMa5x..
/
4eb25..
ownership of
c4b41..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFMA..
/
be2fe..
ownership of
d7991..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaYk..
/
081af..
ownership of
553db..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWkP..
/
e3c60..
ownership of
50686..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGDa..
/
fea36..
ownership of
ae12a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX4C..
/
2dae1..
ownership of
f30f7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJH9..
/
2d7dd..
ownership of
8b31c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMY1G..
/
534eb..
ownership of
77ba8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWpz..
/
c0800..
ownership of
afe96..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaVj..
/
6eac7..
ownership of
1456c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TML8f..
/
83de4..
ownership of
0d864..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKMb..
/
39456..
ownership of
3edd4..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdFV..
/
e7b7d..
ownership of
abcb4..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPoU..
/
f8b7a..
ownership of
02824..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGH5..
/
75f38..
ownership of
b93a6..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUxU..
/
39604..
ownership of
f2f91..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaAg..
/
800e7..
ownership of
e6e31..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVAv..
/
ecefc..
ownership of
17bc9..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEnX..
/
638de..
ownership of
e9507..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdai..
/
e097c..
ownership of
3b93e..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLJX..
/
cb40f..
ownership of
1024f..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEom..
/
2fe4f..
ownership of
28572..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEnk..
/
1c83a..
ownership of
4c89a..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMULG..
/
fc3be..
ownership of
a4d82..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRkK..
/
1c43e..
ownership of
c7aaa..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMS2X..
/
ab2a5..
ownership of
d64bc..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMDL..
/
bfb4a..
ownership of
8acbb..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFfL..
/
56334..
ownership of
1af26..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYPt..
/
7a7e9..
ownership of
f73bd..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGXX..
/
4dc53..
ownership of
fd6f8..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUjS..
/
1b94b..
ownership of
f0b1c..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYXW..
/
189d4..
ownership of
fc03e..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJBz..
/
1b0ae..
ownership of
b86d4..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMDi..
/
8effd..
ownership of
021ae..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdMK..
/
82056..
ownership of
1de7f..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMb8z..
/
10032..
ownership of
a7b1b..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMms..
/
1d305..
ownership of
40f1c..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSwu..
/
96d30..
ownership of
7b913..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPQR..
/
40ae0..
ownership of
83d48..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbuq..
/
7526a..
ownership of
5c8a3..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSvX..
/
ecd39..
ownership of
ade2b..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFyV..
/
c53c9..
ownership of
107b6..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX5i..
/
e8461..
ownership of
fc0b6..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
PUdQg..
/
70ebf..
doc published by
Pr6Pc..
Param
famunion
famunion
:
ι
→
(
ι
→
ι
) →
ι
Param
setsum
setsum
:
ι
→
ι
→
ι
Definition
lam
Sigma
:=
λ x0 .
λ x1 :
ι → ι
.
famunion
x0
(
λ x2 .
prim5
(
x1
x2
)
(
setsum
x2
)
)
Known
famunionI
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
x0
⟶
x3
∈
x1
x2
⟶
x3
∈
famunion
x0
x1
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
lamI
lamI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
x2
⟶
setsum
x2
x3
∈
lam
x0
x1
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
proj0
proj0
:
ι
→
ι
Param
proj1
proj1
:
ι
→
ι
Known
exandE_i
exandE_i
:
∀ x0 x1 :
ι → ο
.
(
∀ x2 : ο .
(
∀ x3 .
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 .
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
proj0_pair_eq
proj0_pair_eq
:
∀ x0 x1 .
proj0
(
setsum
x0
x1
)
=
x0
Known
proj1_pair_eq
proj1_pair_eq
:
∀ x0 x1 .
proj1
(
setsum
x0
x1
)
=
x1
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
famunionE
famunionE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
∈
x1
x4
)
⟶
x3
)
⟶
x3
Theorem
Sigma_eta_proj0_proj1
Sigma_eta_proj0_proj1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
and
(
and
(
setsum
(
proj0
x2
)
(
proj1
x2
)
=
x2
)
(
proj0
x2
∈
x0
)
)
(
proj1
x2
∈
x1
(
proj0
x2
)
)
(proof)
Known
and3E
and3E
:
∀ x0 x1 x2 : ο .
and
(
and
x0
x1
)
x2
⟶
∀ x3 : ο .
(
x0
⟶
x1
⟶
x2
⟶
x3
)
⟶
x3
Theorem
proj_Sigma_eta
proj_Sigma_eta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
setsum
(
proj0
x2
)
(
proj1
x2
)
=
x2
(proof)
Theorem
proj0_Sigma
proj0_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
proj0
x2
∈
x0
(proof)
Theorem
proj1_Sigma
proj1_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
proj1
x2
∈
x1
(
proj0
x2
)
(proof)
Theorem
pair_Sigma_E0
pair_Sigma_E0
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
setsum
x2
x3
∈
lam
x0
x1
⟶
x2
∈
x0
(proof)
Theorem
pair_Sigma_E1
pair_Sigma_E1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
setsum
x2
x3
∈
lam
x0
x1
⟶
x3
∈
x1
x2
(proof)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
lamE
lamE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x1
x4
)
(
x2
=
setsum
x4
x6
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
(proof)
Definition
iff
iff
:=
λ x0 x1 : ο .
and
(
x0
⟶
x1
)
(
x1
⟶
x0
)
Known
iffI
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Theorem
lamEq
lamEq
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
iff
(
x2
∈
lam
x0
x1
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x1
x4
)
(
x2
=
setsum
x4
x6
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
)
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Theorem
Sigma_mon
Sigma_mon
:
∀ x0 x1 .
x0
⊆
x1
⟶
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
⊆
x3
x4
)
⟶
lam
x0
x2
⊆
lam
x1
x3
(proof)
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Theorem
Sigma_mon0
Sigma_mon0
:
∀ x0 x1 .
x0
⊆
x1
⟶
∀ x2 :
ι → ι
.
lam
x0
x2
⊆
lam
x1
x2
(proof)
Theorem
Sigma_mon1
Sigma_mon1
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
⊆
x2
x3
)
⟶
lam
x0
x1
⊆
lam
x0
x2
(proof)
Param
ordsucc
ordsucc
:
ι
→
ι
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Known
In_0_1
In_0_1
:
0
∈
1
Known
setsum_0_0
setsum_0_0
:
setsum
0
0
=
0
Param
Sing
Sing
:
ι
→
ι
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
Subq_1_Sing0
Subq_1_Sing0
:
1
⊆
Sing
0
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Theorem
Sigma_Power_1
Sigma_Power_1
:
∀ x0 .
x0
∈
prim4
1
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim4
1
)
⟶
lam
x0
x1
∈
prim4
1
(proof)
Definition
setprod
setprod
:=
λ x0 x1 .
lam
x0
(
λ x2 .
x1
)
Theorem
pair_setprod
pair_setprod
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
⟶
setsum
x2
x3
∈
setprod
x0
x1
(proof)
Theorem
proj0_setprod
proj0_setprod
:
∀ x0 x1 x2 .
x2
∈
setprod
x0
x1
⟶
proj0
x2
∈
x0
(proof)
Theorem
proj1_setprod
proj1_setprod
:
∀ x0 x1 x2 .
x2
∈
setprod
x0
x1
⟶
proj1
x2
∈
x1
(proof)
Theorem
pair_setprod_E0
pair_setprod_E0
:
∀ x0 x1 x2 x3 .
setsum
x2
x3
∈
setprod
x0
x1
⟶
x2
∈
x0
(proof)
Theorem
pair_setprod_E1
pair_setprod_E1
:
∀ x0 x1 x2 x3 .
setsum
x2
x3
∈
setprod
x0
x1
⟶
x3
∈
x1
(proof)
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Definition
ap
ap
:=
λ x0 x1 .
ReplSep
x0
(
λ x2 .
∀ x3 : ο .
(
∀ x4 .
x2
=
setsum
x1
x4
⟶
x3
)
⟶
x3
)
proj1
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Theorem
apI
apI
:
∀ x0 x1 x2 .
setsum
x1
x2
∈
x0
⟶
x2
∈
ap
x0
x1
(proof)
Known
ReplSepE_impred
ReplSepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
ReplSep
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
x5
∈
x0
⟶
x1
x5
⟶
x3
=
x2
x5
⟶
x4
)
⟶
x4
Theorem
apE
apE
:
∀ x0 x1 x2 .
x2
∈
ap
x0
x1
⟶
setsum
x1
x2
∈
x0
(proof)
Theorem
apEq
apEq
:
∀ x0 x1 x2 .
iff
(
x2
∈
ap
x0
x1
)
(
setsum
x1
x2
∈
x0
)
(proof)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Theorem
beta
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
(proof)
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
Empty_eq
Empty_eq
:
∀ x0 .
(
∀ x1 .
nIn
x1
x0
)
⟶
x0
=
0
Theorem
beta0
beta0
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
nIn
x2
x0
⟶
ap
(
lam
x0
x1
)
x2
=
0
(proof)
Known
proj0E
proj0E
:
∀ x0 x1 .
x1
∈
proj0
x0
⟶
setsum
0
x1
∈
x0
Known
proj0I
proj0I
:
∀ x0 x1 .
setsum
0
x1
∈
x0
⟶
x1
∈
proj0
x0
Theorem
proj0_ap_0
proj0_ap_0
:
∀ x0 .
proj0
x0
=
ap
x0
0
(proof)
Known
proj1E
proj1E
:
∀ x0 x1 .
x1
∈
proj1
x0
⟶
setsum
1
x1
∈
x0
Known
proj1I
proj1I
:
∀ x0 x1 .
setsum
1
x1
∈
x0
⟶
x1
∈
proj1
x0
Theorem
proj1_ap_1
proj1_ap_1
:
∀ x0 .
proj1
x0
=
ap
x0
1
(proof)
Theorem
pair_ap_0
pair_ap_0
:
∀ x0 x1 .
ap
(
setsum
x0
x1
)
0
=
x0
(proof)
Theorem
pair_ap_1
pair_ap_1
:
∀ x0 x1 .
ap
(
setsum
x0
x1
)
1
=
x1
(proof)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
pairE
pairE
:
∀ x0 x1 x2 .
x2
∈
setsum
x0
x1
⟶
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
setsum
0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x1
)
(
x2
=
setsum
1
x4
)
⟶
x3
)
⟶
x3
)
Known
pair_inj
pair_inj
:
∀ x0 x1 x2 x3 .
setsum
x0
x1
=
setsum
x2
x3
⟶
and
(
x0
=
x2
)
(
x1
=
x3
)
Known
In_0_2
In_0_2
:
0
∈
2
Known
In_1_2
In_1_2
:
1
∈
2
Theorem
pair_ap_n2
pair_ap_n2
:
∀ x0 x1 x2 .
nIn
x2
2
⟶
ap
(
setsum
x0
x1
)
x2
=
0
(proof)
Theorem
ap0_Sigma
ap0_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
0
∈
x0
(proof)
Theorem
ap1_Sigma
ap1_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
1
∈
x1
(
ap
x2
0
)
(proof)
Definition
pair_p
pair_p
:=
λ x0 .
setsum
(
ap
x0
0
)
(
ap
x0
1
)
=
x0
Theorem
pair_p_I
pair_p_I
:
∀ x0 x1 .
pair_p
(
setsum
x0
x1
)
(proof)
Param
UPair
UPair
:
ι
→
ι
→
ι
Known
UPairE
UPairE
:
∀ x0 x1 x2 .
x0
∈
UPair
x1
x2
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
Known
pairI0
pairI0
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
setsum
0
x2
∈
setsum
x0
x1
Known
pairI1
pairI1
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
setsum
1
x2
∈
setsum
x0
x1
Known
Subq_2_UPair01
Subq_2_UPair01
:
2
⊆
UPair
0
1
Theorem
pair_p_I2
pair_p_I2
:
∀ x0 .
(
∀ x1 .
x1
∈
x0
⟶
and
(
pair_p
x1
)
(
ap
x1
0
∈
2
)
)
⟶
pair_p
x0
(proof)
Theorem
pair_p_In_ap
pair_p_In_ap
:
∀ x0 x1 .
pair_p
x0
⟶
x0
∈
x1
⟶
ap
x0
1
∈
ap
x1
(
ap
x0
0
)
(proof)
Definition
tuple_p
tuple_p
:=
λ x0 x1 .
∀ x2 .
x2
∈
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
∀ x5 : ο .
(
∀ x6 .
x2
=
setsum
x4
x6
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
Known
pred_ext_2
pred_ext_2
:
∀ x0 x1 :
ι → ο
.
(
∀ x2 .
x0
x2
⟶
x1
x2
)
⟶
(
∀ x2 .
x1
x2
⟶
x0
x2
)
⟶
x0
=
x1
Theorem
pair_p_tuple2
pair_p_tuple2
:
pair_p
=
tuple_p
2
(proof)
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Theorem
tuple_p_2_tuple
tuple_p_2_tuple
:
∀ x0 x1 .
tuple_p
2
(
lam
2
(
λ x2 .
If_i
(
x2
=
0
)
x0
x1
)
)
(proof)
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Theorem
tuple_pair
tuple_pair
:
∀ x0 x1 .
setsum
x0
x1
=
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
(proof)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Definition
Pi
Pi
:=
λ x0 .
λ x1 :
ι → ι
.
{x2 ∈
prim4
(
lam
x0
(
λ x2 .
prim3
(
x1
x2
)
)
)
|
∀ x3 .
x3
∈
x0
⟶
ap
x2
x3
∈
x1
x3
}
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
UnionI
UnionI
:
∀ x0 x1 x2 .
x1
∈
x2
⟶
x2
∈
x0
⟶
x1
∈
prim3
x0
Theorem
PiI
PiI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
(
∀ x3 .
x3
∈
x2
⟶
and
(
pair_p
x3
)
(
ap
x3
0
∈
x0
)
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
ap
x2
x3
∈
x1
x3
)
⟶
x2
∈
Pi
x0
x1
(proof)
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Theorem
PiE
PiE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
Pi
x0
x1
⟶
and
(
∀ x3 .
x3
∈
x2
⟶
and
(
pair_p
x3
)
(
ap
x3
0
∈
x0
)
)
(
∀ x3 .
x3
∈
x0
⟶
ap
x2
x3
∈
x1
x3
)
(proof)
Theorem
PiEq
PiEq
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
iff
(
x2
∈
Pi
x0
x1
)
(
and
(
∀ x3 .
x3
∈
x2
⟶
and
(
pair_p
x3
)
(
ap
x3
0
∈
x0
)
)
(
∀ x3 .
x3
∈
x0
⟶
ap
x2
x3
∈
x1
x3
)
)
(proof)
Theorem
lam_Pi
lam_Pi
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
x3
)
⟶
lam
x0
x2
∈
Pi
x0
x1
(proof)
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
Theorem
ap_Pi
ap_Pi
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
Pi
x0
x1
⟶
x3
∈
x0
⟶
ap
x2
x3
∈
x1
x3
(proof)
Theorem
Pi_ext_Subq
Pi_ext_Subq
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
Pi
x0
x1
⟶
∀ x3 .
x3
∈
Pi
x0
x1
⟶
(
∀ x4 .
x4
∈
x0
⟶
ap
x2
x4
⊆
ap
x3
x4
)
⟶
x2
⊆
x3
(proof)
Theorem
Pi_ext
Pi_ext
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
Pi
x0
x1
⟶
∀ x3 .
x3
∈
Pi
x0
x1
⟶
(
∀ x4 .
x4
∈
x0
⟶
ap
x2
x4
=
ap
x3
x4
)
⟶
x2
=
x3
(proof)
Theorem
Pi_eta
Pi_eta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
Pi
x0
x1
⟶
lam
x0
(
ap
x2
)
=
x2
(proof)
Definition
setexp
setexp
:=
λ x0 x1 .
Pi
x1
(
λ x2 .
x0
)
Theorem
pair_tuple_fun
pair_tuple_fun
:
setsum
=
λ x1 x2 .
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x1
x2
)
(proof)
Theorem
tuple_2_Sigma
tuple_2_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
x2
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
x2
x3
)
∈
lam
x0
x1
(proof)
Theorem
lamE2
lamE2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x1
x4
)
(
x2
=
lam
2
(
λ x8 .
If_i
(
x8
=
0
)
x4
x6
)
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
(proof)
Theorem
tuple_2_inj
tuple_2_inj
:
∀ x0 x1 x2 x3 .
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x0
x1
)
=
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x2
x3
)
⟶
and
(
x0
=
x2
)
(
x1
=
x3
)
(proof)
Theorem
tuple_2_0_eq
tuple_2_0_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
0
=
x0
(proof)
Theorem
tuple_2_1_eq
tuple_2_1_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
1
=
x1
(proof)
Definition
Sep2
Sep2
:=
λ x0 .
λ x1 :
ι → ι
.
λ x2 :
ι →
ι → ο
.
{x3 ∈
lam
x0
x1
|
x2
(
ap
x3
0
)
(
ap
x3
1
)
}
Theorem
Sep2I
Sep2I
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x1
x3
⟶
x2
x3
x4
⟶
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x3
x4
)
∈
Sep2
x0
x1
x2
(proof)
Theorem
Sep2E
Sep2E
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
x3
∈
Sep2
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
∀ x6 : ο .
(
∀ x7 .
and
(
x7
∈
x1
x5
)
(
and
(
x3
=
lam
2
(
λ x9 .
If_i
(
x9
=
0
)
x5
x7
)
)
(
x2
x5
x7
)
)
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
(proof)
Theorem
Sep2E'
Sep2E
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 x4 .
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x3
x4
)
∈
Sep2
x0
x1
x2
⟶
and
(
and
(
x3
∈
x0
)
(
x4
∈
x1
x3
)
)
(
x2
x3
x4
)
(proof)
Theorem
Sep2E'1
Sep2E1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 x4 .
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x3
x4
)
∈
Sep2
x0
x1
x2
⟶
x3
∈
x0
(proof)
Theorem
Sep2E'2
Sep2E2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 x4 .
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x3
x4
)
∈
Sep2
x0
x1
x2
⟶
x4
∈
x1
x3
(proof)
Theorem
Sep2E'3
Sep2E3
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 x4 .
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x3
x4
)
∈
Sep2
x0
x1
x2
⟶
x2
x3
x4
(proof)
Definition
set_of_pairs
set_of_pairs
:=
λ x0 .
∀ x1 .
x1
∈
x0
⟶
∀ x2 : ο .
(
∀ x3 .
(
∀ x4 : ο .
(
∀ x5 .
x1
=
lam
2
(
λ x7 .
If_i
(
x7
=
0
)
x3
x5
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
Theorem
set_of_pairs_ext
set_of_pairs_ext
:
∀ x0 x1 .
set_of_pairs
x0
⟶
set_of_pairs
x1
⟶
(
∀ x2 x3 .
iff
(
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
x2
x3
)
∈
x0
)
(
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
x2
x3
)
∈
x1
)
)
⟶
x0
=
x1
(proof)
Theorem
Sep2_set_of_pairs
Sep2_set_of_pairs
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
set_of_pairs
(
Sep2
x0
x1
x2
)
(proof)
Theorem
Sep2_ext
Sep2_ext
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 :
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x1
x4
⟶
iff
(
x2
x4
x5
)
(
x3
x4
x5
)
)
⟶
Sep2
x0
x1
x2
=
Sep2
x0
x1
x3
(proof)
Theorem
lam_ext_sub
lam_ext_sub
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
lam
x0
x1
⊆
lam
x0
x2
(proof)
Theorem
encode_u_ext
encode_u_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
lam
x0
x1
=
lam
x0
x2
(proof)
Theorem
lam_eta
lam_eta
:
∀ x0 .
∀ x1 :
ι → ι
.
lam
x0
(
ap
(
lam
x0
x1
)
)
=
lam
x0
x1
(proof)
Theorem
tuple_2_eta
tuple_2_eta
:
∀ x0 x1 .
lam
2
(
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
)
=
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
(proof)
Definition
lam2
lam2
:=
λ x0 .
λ x1 :
ι → ι
.
λ x2 :
ι →
ι → ι
.
lam
x0
(
λ x3 .
lam
(
x1
x3
)
(
x2
x3
)
)
Theorem
beta2
beta2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x1
x3
⟶
ap
(
ap
(
lam2
x0
x1
x2
)
x3
)
x4
=
x2
x3
x4
(proof)
Theorem
lam2_ext
lam2_ext
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x1
x4
⟶
x2
x4
x5
=
x3
x4
x5
)
⟶
lam2
x0
x1
x2
=
lam2
x0
x1
x3
(proof)
Definition
lam
Sigma
:=
lam
Definition
ap
ap
:=
ap
Definition
encode_b
encode_b
:=
λ x0 .
lam2
x0
(
λ x1 .
x0
)
Definition
decode_b
decode_b
:=
λ x0 x1 .
ap
(
ap
x0
x1
)
Definition
decode_p
decode_p
:=
λ x0 x1 .
x1
∈
x0
Definition
encode_r
encode_r
:=
λ x0 .
Sep2
x0
(
λ x1 .
x0
)
Definition
decode_r
decode_r
:=
λ x0 x1 x2 .
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x1
x2
)
∈
x0
Definition
encode_c
encode_c
:=
λ x0 .
λ x1 :
(
ι → ο
)
→ ο
.
{x2 ∈
prim4
x0
|
x1
(
λ x3 .
x3
∈
x2
)
}
Definition
decode_c
decode_c
:=
λ x0 .
λ x1 :
ι → ο
.
∀ x2 : ο .
(
∀ x3 .
and
(
∀ x4 .
iff
(
x1
x4
)
(
x4
∈
x3
)
)
(
x3
∈
x0
)
⟶
x2
)
⟶
x2
Theorem
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
(proof)
Theorem
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
(proof)
Known
prop_ext_2
prop_ext_2
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
x0
=
x1
Theorem
decode_encode_p
decode_encode_p
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
decode_p
(
Sep
x0
x1
)
x2
=
x1
x2
(proof)
Theorem
encode_p_ext
encode_p_ext
:
∀ x0 .
∀ x1 x2 :
ι → ο
.
(
∀ x3 .
x3
∈
x0
⟶
iff
(
x1
x3
)
(
x2
x3
)
)
⟶
Sep
x0
x1
=
Sep
x0
x2
(proof)
Theorem
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
(proof)
Theorem
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
(proof)
Known
Sep_In_Power
Sep_In_Power
:
∀ x0 .
∀ x1 :
ι → ο
.
Sep
x0
x1
∈
prim4
x0
Theorem
decode_encode_c
decode_encode_c
:
∀ x0 .
∀ x1 :
(
ι → ο
)
→ ο
.
∀ x2 :
ι → ο
.
(
∀ x3 .
x2
x3
⟶
x3
∈
x0
)
⟶
decode_c
(
encode_c
x0
x1
)
x2
=
x1
x2
(proof)
Theorem
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
(proof)