Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr7pr..
/
77a92..
PUQ3g..
/
b05de..
vout
Pr7pr..
/
67f01..
19.96 bars
TMWw8..
/
cdd77..
negprop ownership controlledby
Pr6Pc..
upto 0
TMP2e..
/
dbcbd..
negprop ownership controlledby
Pr6Pc..
upto 0
TMdM7..
/
7e4ef..
ownership of
94cbe..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbQG..
/
3b8ec..
ownership of
5b4c3..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZNw..
/
4d398..
ownership of
109f1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMaN..
/
98fbf..
ownership of
c2447..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYJs..
/
89eb7..
ownership of
15c58..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYpo..
/
e267d..
ownership of
7558b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLop..
/
2f154..
ownership of
c9a73..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdSZ..
/
66710..
ownership of
72c5e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX6t..
/
828e1..
ownership of
ced78..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKf8..
/
8e6b4..
ownership of
e37d0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMay..
/
258ee..
ownership of
51ee4..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMW5w..
/
71f8d..
ownership of
94579..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMd5j..
/
6172c..
ownership of
fea5f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZ8s..
/
0fd34..
ownership of
56f8b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMe1K..
/
8f0eb..
ownership of
1eea3..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMV1V..
/
a0a8a..
ownership of
ac39b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGZE..
/
e61a1..
ownership of
d6f8b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMF7T..
/
d80c7..
ownership of
ba974..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJYn..
/
8f72b..
ownership of
12998..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcVb..
/
7a208..
ownership of
bd4a2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRnf..
/
8c94c..
ownership of
8ca37..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUeM..
/
bdc91..
ownership of
ac957..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMa2t..
/
379c6..
ownership of
0dfd1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMda5..
/
ed82e..
ownership of
217cf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKdF..
/
c3cc0..
ownership of
52934..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQdt..
/
0581c..
ownership of
33cf6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFDX..
/
fbb92..
ownership of
5aa0a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLE3..
/
ca233..
ownership of
26efc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMY25..
/
98545..
ownership of
5345a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSdM..
/
58a8c..
ownership of
fa323..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQty..
/
b0d00..
ownership of
76562..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWGx..
/
b4c6f..
ownership of
b353a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXbE..
/
29b53..
ownership of
73bbf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZZk..
/
2a995..
ownership of
b7b86..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMH2y..
/
788e5..
ownership of
c8f8e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQd3..
/
eee5d..
ownership of
d41d3..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbYC..
/
09b3a..
ownership of
7754e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWHK..
/
d8583..
ownership of
4731f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQc8..
/
c596d..
ownership of
f6661..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQED..
/
acfc8..
ownership of
c1078..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMU9R..
/
93162..
ownership of
42373..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNRF..
/
fd929..
ownership of
bb8cd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKQr..
/
d72a6..
ownership of
8362f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGpK..
/
6a959..
ownership of
b52eb..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPBd..
/
beacb..
ownership of
7c3d1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdih..
/
8b5a6..
ownership of
9161d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcuZ..
/
8a734..
ownership of
4bca1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKfL..
/
1f261..
ownership of
984a3..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMkf..
/
fd0ee..
ownership of
ae46e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNKa..
/
2ffeb..
ownership of
9621a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZQ7..
/
ff1a0..
ownership of
dc927..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMbZ..
/
a65bb..
ownership of
3cc36..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSrH..
/
f8e7f..
ownership of
383e8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTPF..
/
1e48e..
ownership of
97693..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMV17..
/
bed93..
ownership of
4f3d0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFWN..
/
09a77..
ownership of
ddd91..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJz3..
/
4da90..
ownership of
e13f4..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ2p..
/
c2124..
ownership of
98051..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPHF..
/
1a645..
ownership of
ded78..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLcR..
/
b2009..
ownership of
6e3a2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUsP..
/
5452d..
ownership of
7dca0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbsB..
/
19fe0..
ownership of
efca0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYKc..
/
ff77f..
ownership of
7ccd8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZmX..
/
877fa..
ownership of
cead4..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVyV..
/
7f7d7..
ownership of
7aba5..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQrz..
/
85c1d..
ownership of
52486..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbma..
/
a39ce..
ownership of
8efb8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMW8w..
/
334e4..
ownership of
a9ba1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZeU..
/
54969..
ownership of
d5dbd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFyX..
/
93ea2..
ownership of
ab85f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMb5f..
/
5da28..
ownership of
62b49..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRab..
/
93a05..
ownership of
deb03..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUES..
/
84207..
ownership of
f48d4..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPvN..
/
8e0e5..
ownership of
fbb46..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcJg..
/
7e73b..
ownership of
d928b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUi6..
/
15723..
ownership of
6828e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKRK..
/
ceb84..
ownership of
b4042..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ7H..
/
9901b..
ownership of
7a14c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKCt..
/
e746d..
ownership of
04f24..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMNh..
/
20c53..
ownership of
f5227..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTy8..
/
abc9a..
ownership of
bb731..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRdG..
/
f562b..
ownership of
970ce..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMdd..
/
41522..
ownership of
66456..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMU2S..
/
dae0e..
ownership of
9398b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSzf..
/
e2c04..
ownership of
6196d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXkN..
/
4da62..
ownership of
11b6e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNDv..
/
9d2ea..
ownership of
53516..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMG8B..
/
7a431..
ownership of
6e122..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXGg..
/
25e09..
ownership of
8965d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQDj..
/
fcd42..
ownership of
f595a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXd8..
/
ed1ff..
ownership of
03198..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKoi..
/
628fa..
ownership of
a0c5c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMK9r..
/
93904..
ownership of
4a77a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLec..
/
08b16..
ownership of
b2178..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWXy..
/
4c204..
ownership of
ba854..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFeQ..
/
eee3f..
ownership of
3bc66..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMew..
/
b97db..
ownership of
3abee..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdEq..
/
f6298..
ownership of
f9f75..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKJt..
/
4be1d..
ownership of
83bd2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWbE..
/
9c61d..
ownership of
c940c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TML6q..
/
c2876..
ownership of
ccfdf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMddk..
/
b824a..
ownership of
ac0e2..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdyk..
/
e778e..
ownership of
8ad05..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdfG..
/
eb393..
ownership of
35a4c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFNg..
/
09e0a..
ownership of
06fac..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbVe..
/
39b71..
ownership of
d5ecf..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX95..
/
b0ed1..
ownership of
938f6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ4V..
/
e0f95..
ownership of
006af..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTsv..
/
dbeeb..
ownership of
82b82..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSSV..
/
bcc5c..
ownership of
282b0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMScx..
/
78e97..
ownership of
d12fc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQaP..
/
980a2..
ownership of
95871..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKhJ..
/
cc496..
ownership of
246d0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZPd..
/
6e9ff..
ownership of
f756d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWvC..
/
4478b..
ownership of
92ef0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMR8s..
/
96800..
ownership of
23cc4..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKZj..
/
ccb4c..
ownership of
1c9c6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWx2..
/
3a68e..
ownership of
f0983..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcpC..
/
e4b83..
ownership of
c0fef..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXZ1..
/
10bd6..
ownership of
bf4ac..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMaw..
/
1f9dd..
ownership of
b08bd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMG63..
/
b5260..
ownership of
95a70..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTis..
/
92a63..
ownership of
06351..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKUK..
/
8d3f6..
ownership of
c702b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcZ2..
/
1f1de..
ownership of
76c08..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQV9..
/
8c70b..
ownership of
fdcb7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVu9..
/
3837e..
ownership of
a428a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZCR..
/
cd074..
ownership of
a244d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMH87..
/
ba918..
ownership of
9c489..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMS4B..
/
b3abd..
ownership of
07f1e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPZ6..
/
d9c7f..
ownership of
8c787..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTaG..
/
6abb6..
ownership of
6ffef..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHMi..
/
88767..
ownership of
49cd5..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMF7H..
/
a4be6..
ownership of
4a103..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNg3..
/
00d5b..
ownership of
f0e9f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYpW..
/
9ea3f..
ownership of
7cacc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTeC..
/
b2834..
ownership of
21761..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEuZ..
/
09b8f..
ownership of
a8afc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdvM..
/
26e6c..
ownership of
5d96d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaDQ..
/
03444..
ownership of
68f71..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUMC..
/
f9cb8..
ownership of
65843..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJjy..
/
6b205..
ownership of
2ca11..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUJv..
/
5f57d..
ownership of
a5934..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMDu..
/
b1fe6..
ownership of
929b7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdU6..
/
51f13..
ownership of
63011..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcuW..
/
03233..
ownership of
1642a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUdw..
/
f8e5d..
ownership of
f03db..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHEH..
/
c3a2b..
ownership of
96e4e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWKe..
/
baeb1..
ownership of
68851..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZtD..
/
abf95..
ownership of
c12e0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYbW..
/
bcb55..
ownership of
85961..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcnJ..
/
e9e5e..
ownership of
49a08..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUFg..
/
e9320..
ownership of
e7ff3..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMEiG..
/
24bf3..
ownership of
7f35b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTYB..
/
b5ae2..
ownership of
70c25..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNf9..
/
871d2..
ownership of
a1d43..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYDs..
/
8dd97..
ownership of
ec160..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKi9..
/
7f356..
ownership of
1f7dc..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdBj..
/
31bd6..
ownership of
ef37f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTWK..
/
25508..
ownership of
cf032..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVoj..
/
8a687..
ownership of
c0e2c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFQr..
/
33df7..
ownership of
b603b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVBk..
/
01777..
ownership of
aaf6e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSUb..
/
d8620..
ownership of
f9488..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKxs..
/
03848..
ownership of
db797..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUKB..
/
016aa..
ownership of
99a3f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWGS..
/
59564..
ownership of
be9a7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJBs..
/
84dc2..
ownership of
8f2d6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQVo..
/
44c47..
ownership of
8c551..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKMd..
/
1ed1e..
ownership of
464e4..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbS5..
/
a6634..
ownership of
ff416..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQCh..
/
5b51f..
ownership of
997d9..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMH8P..
/
e86e0..
ownership of
0cfe8..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSvK..
/
215c1..
ownership of
73b2b..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGV9..
/
80370..
ownership of
48bcf..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUvM..
/
2da77..
ownership of
8cd81..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMS7R..
/
e3203..
ownership of
4680c..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYei..
/
e416a..
ownership of
d5069..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMF5e..
/
fdc7c..
ownership of
77512..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdYB..
/
f635b..
ownership of
c083d..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMP7d..
/
bfb35..
ownership of
295bc..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRuD..
/
25947..
ownership of
ec849..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcgc..
/
1b3f8..
ownership of
54f40..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKo9..
/
439e1..
ownership of
ddf7d..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKc4..
/
171e3..
ownership of
8c8aa..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQeB..
/
3f1f4..
ownership of
46e7e..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPsS..
/
9639a..
ownership of
12b5f..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUZT..
/
fa96e..
ownership of
83dce..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLgH..
/
364b3..
ownership of
293b7..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMcKk..
/
b3daf..
ownership of
116b7..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMN8j..
/
f7481..
ownership of
11faa..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMTsR..
/
1a8da..
ownership of
0a835..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYCs..
/
63890..
ownership of
3657a..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQpD..
/
fa65e..
ownership of
c16a7..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWTZ..
/
7fbcb..
ownership of
4ab7e..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX8t..
/
d8d49..
ownership of
6f0c3..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMchc..
/
60c73..
ownership of
c0ec7..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
PUUwp..
/
cb4ae..
doc published by
Pr6Pc..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Definition
TransSet
TransSet
:=
λ x0 .
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Param
Sing
Sing
:
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Known
neq_0_1
neq_0_1
:
0
=
1
⟶
∀ x0 : ο .
x0
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
In_0_1
In_0_1
:
0
∈
1
Theorem
not_TransSet_Sing1
not_TransSet_Sing1
:
not
(
TransSet
(
Sing
1
)
)
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Definition
ordinal
ordinal
:=
λ x0 .
and
(
TransSet
x0
)
(
∀ x1 .
x1
∈
x0
⟶
TransSet
x1
)
Theorem
not_ordinal_Sing1
not_ordinal_Sing1
:
not
(
ordinal
(
Sing
1
)
)
(proof)
Param
binunion
binunion
:
ι
→
ι
→
ι
Definition
SetAdjoin
SetAdjoin
:=
λ x0 x1 .
binunion
x0
(
Sing
x1
)
Known
ordinal_Hered
ordinal_Hered
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordinal
x1
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Theorem
tagged_not_ordinal
tagged_not_ordinal
:
∀ x0 .
not
(
ordinal
(
SetAdjoin
x0
(
Sing
1
)
)
)
(proof)
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Theorem
tagged_notin_ordinal
tagged_notin_ordinal
:
∀ x0 x1 .
ordinal
x0
⟶
nIn
(
SetAdjoin
x1
(
Sing
1
)
)
x0
(proof)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Theorem
tagged_eqE_Subq
tagged_eqE_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
SetAdjoin
x0
(
Sing
1
)
=
SetAdjoin
x1
(
Sing
1
)
⟶
x0
⊆
x1
(proof)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Theorem
tagged_eqE_eq
tagged_eqE_eq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
SetAdjoin
x0
(
Sing
1
)
=
SetAdjoin
x1
(
Sing
1
)
⟶
x0
=
x1
(proof)
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Theorem
tagged_ReplE
tagged_ReplE
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
SetAdjoin
x1
(
Sing
1
)
∈
{
SetAdjoin
x2
(
Sing
1
)
|x2 ∈
x0
}
⟶
x1
∈
x0
(proof)
Theorem
ordinal_notin_tagged_Repl
ordinal_notin_tagged_Repl
:
∀ x0 x1 .
ordinal
x0
⟶
nIn
x0
{
SetAdjoin
x2
(
Sing
1
)
|x2 ∈
x1
}
(proof)
Definition
SNoElts_
SNoElts_
:=
λ x0 .
binunion
x0
{
SetAdjoin
x1
(
Sing
1
)
|x1 ∈
x0
}
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
SNoElts_mon
SNoElts_mon
:
∀ x0 x1 .
x0
⊆
x1
⟶
SNoElts_
x0
⊆
SNoElts_
x1
(proof)
Param
exactly1of2
exactly1of2
:
ο
→
ο
→
ο
Definition
SNo_
SNo_
:=
λ x0 x1 .
and
(
x1
⊆
SNoElts_
x0
)
(
∀ x2 .
x2
∈
x0
⟶
exactly1of2
(
SetAdjoin
x2
(
Sing
1
)
∈
x1
)
(
x2
∈
x1
)
)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Definition
PSNo
PSNo
:=
λ x0 .
λ x1 :
ι → ο
.
binunion
(
Sep
x0
x1
)
{
SetAdjoin
x2
(
Sing
1
)
|x2 ∈
x0
,
not
(
x1
x2
)
}
Definition
iff
iff
:=
λ x0 x1 : ο .
and
(
x0
⟶
x1
)
(
x1
⟶
x0
)
Definition
PNoEq_
PNoEq_
:=
λ x0 .
λ x1 x2 :
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
iff
(
x1
x3
)
(
x2
x3
)
Known
iffI
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
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
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Theorem
PNoEq_PSNo
PNoEq_PSNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 :
ι → ο
.
PNoEq_
x0
(
λ x2 .
x2
∈
PSNo
x0
x1
)
x1
(proof)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
exactly1of2_I2
exactly1of2_I2
:
∀ x0 x1 : ο .
not
x0
⟶
x1
⟶
exactly1of2
x0
x1
Known
exactly1of2_I1
exactly1of2_I1
:
∀ x0 x1 : ο .
x0
⟶
not
x1
⟶
exactly1of2
x0
x1
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Theorem
SNo_PSNo
SNo_PSNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 :
ι → ο
.
SNo_
x0
(
PSNo
x0
x1
)
(proof)
Known
exactly1of2_E
exactly1of2_E
:
∀ x0 x1 : ο .
exactly1of2
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
not
x1
⟶
x2
)
⟶
(
not
x0
⟶
x1
⟶
x2
)
⟶
x2
Theorem
SNo_PSNo_eta_
SNo_PSNo_eta_
:
∀ x0 x1 .
ordinal
x0
⟶
SNo_
x0
x1
⟶
x1
=
PSNo
x0
(
λ x3 .
x3
∈
x1
)
(proof)
Definition
SNo
SNo
:=
λ x0 .
∀ x1 : ο .
(
∀ x2 .
and
(
ordinal
x2
)
(
SNo_
x2
x0
)
⟶
x1
)
⟶
x1
Theorem
SNo_SNo
SNo_SNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNo
x1
(proof)
Definition
SNoLev
SNoLev
:=
λ x0 .
prim0
(
λ x1 .
and
(
ordinal
x1
)
(
SNo_
x1
x0
)
)
Known
exactly1of2_or
exactly1of2_or
:
∀ x0 x1 : ο .
exactly1of2
x0
x1
⟶
or
x0
x1
Theorem
SNoLev_uniq_Subq
SNoLev_uniq_Subq
:
∀ x0 x1 x2 .
ordinal
x1
⟶
ordinal
x2
⟶
SNo_
x1
x0
⟶
SNo_
x2
x0
⟶
x1
⊆
x2
(proof)
Theorem
SNoLev_uniq
SNoLev_uniq
:
∀ x0 x1 x2 .
ordinal
x1
⟶
ordinal
x2
⟶
SNo_
x1
x0
⟶
SNo_
x2
x0
⟶
x1
=
x2
(proof)
Known
Eps_i_ex
Eps_i_ex
:
∀ x0 :
ι → ο
.
(
∀ x1 : ο .
(
∀ x2 .
x0
x2
⟶
x1
)
⟶
x1
)
⟶
x0
(
prim0
x0
)
Theorem
SNoLev_prop
SNoLev_prop
:
∀ x0 .
SNo
x0
⟶
and
(
ordinal
(
SNoLev
x0
)
)
(
SNo_
(
SNoLev
x0
)
x0
)
(proof)
Theorem
SNoLev_ordinal
SNoLev_ordinal
:
∀ x0 .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
(proof)
Theorem
SNoLev_
SNoLev_
:
∀ x0 .
SNo
x0
⟶
SNo_
(
SNoLev
x0
)
x0
(proof)
Theorem
SNo_PSNo_eta
SNo_PSNo_eta
:
∀ x0 .
SNo
x0
⟶
x0
=
PSNo
(
SNoLev
x0
)
(
λ x2 .
x2
∈
x0
)
(proof)
Theorem
SNoLev_PSNo
SNoLev_PSNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 :
ι → ο
.
SNoLev
(
PSNo
x0
x1
)
=
x0
(proof)
Theorem
SNo_Subq
SNo_Subq
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
⊆
SNoLev
x1
⟶
(
∀ x2 .
x2
∈
SNoLev
x0
⟶
iff
(
x2
∈
x0
)
(
x2
∈
x1
)
)
⟶
x0
⊆
x1
(proof)
Definition
SNoEq_
SNoEq_
:=
λ x0 x1 x2 .
PNoEq_
x0
(
λ x3 .
x3
∈
x1
)
(
λ x3 .
x3
∈
x2
)
Theorem
SNoEq_I
SNoEq_I
:
∀ x0 x1 x2 .
(
∀ x3 .
x3
∈
x0
⟶
iff
(
x3
∈
x1
)
(
x3
∈
x2
)
)
⟶
SNoEq_
x0
x1
x2
(proof)
Theorem
SNoEq_E
SNoEq_E
:
∀ x0 x1 x2 .
SNoEq_
x0
x1
x2
⟶
∀ x3 .
x3
∈
x0
⟶
iff
(
x3
∈
x1
)
(
x3
∈
x2
)
(proof)
Theorem
SNoEq_E1
SNoEq_E1
:
∀ x0 x1 x2 .
SNoEq_
x0
x1
x2
⟶
∀ x3 .
x3
∈
x0
⟶
x3
∈
x1
⟶
x3
∈
x2
(proof)
Theorem
SNoEq_E2
SNoEq_E2
:
∀ x0 x1 x2 .
SNoEq_
x0
x1
x2
⟶
∀ x3 .
x3
∈
x0
⟶
x3
∈
x2
⟶
x3
∈
x1
(proof)
Known
PNoEq_antimon_
PNoEq_antimon_
:
∀ x0 x1 :
ι → ο
.
∀ x2 .
ordinal
x2
⟶
∀ x3 .
x3
∈
x2
⟶
PNoEq_
x2
x0
x1
⟶
PNoEq_
x3
x0
x1
Theorem
SNoEq_antimon_
SNoEq_antimon_
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
∀ x2 x3 .
SNoEq_
x0
x2
x3
⟶
SNoEq_
x1
x2
x3
(proof)
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Known
iff_sym
iff_sym
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
iff
x1
x0
Theorem
SNo_eq
SNo_eq
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
=
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
x0
=
x1
(proof)
Param
PNoLt
PNoLt
:
ι
→
(
ι
→
ο
) →
ι
→
(
ι
→
ο
) →
ο
Definition
SNoLt
SNoLt
:=
λ x0 x1 .
PNoLt
(
SNoLev
x0
)
(
λ x2 .
x2
∈
x0
)
(
SNoLev
x1
)
(
λ x2 .
x2
∈
x1
)
Definition
PNoLe
PNoLe
:=
λ x0 .
λ x1 :
ι → ο
.
λ x2 .
λ x3 :
ι → ο
.
or
(
PNoLt
x0
x1
x2
x3
)
(
and
(
x0
=
x2
)
(
PNoEq_
x0
x1
x3
)
)
Definition
SNoLe
SNoLe
:=
λ x0 x1 .
PNoLe
(
SNoLev
x0
)
(
λ x2 .
x2
∈
x0
)
(
SNoLev
x1
)
(
λ x2 .
x2
∈
x1
)
Known
PNoLeI1
PNoLeI1
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
PNoLt
x0
x2
x1
x3
⟶
PNoLe
x0
x2
x1
x3
Theorem
SNoLtLe
SNoLtLe
:
∀ x0 x1 .
SNoLt
x0
x1
⟶
SNoLe
x0
x1
(proof)
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Theorem
SNoLeE
SNoLeE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
or
(
SNoLt
x0
x1
)
(
x0
=
x1
)
(proof)
Known
PNoEq_ref_
PNoEq_ref_
:
∀ x0 .
∀ x1 :
ι → ο
.
PNoEq_
x0
x1
x1
Theorem
SNoEq_ref_
SNoEq_ref_
:
∀ x0 x1 .
SNoEq_
x0
x1
x1
(proof)
Known
PNoEq_sym_
PNoEq_sym_
:
∀ x0 .
∀ x1 x2 :
ι → ο
.
PNoEq_
x0
x1
x2
⟶
PNoEq_
x0
x2
x1
Theorem
SNoEq_sym_
SNoEq_sym_
:
∀ x0 x1 x2 .
SNoEq_
x0
x1
x2
⟶
SNoEq_
x0
x2
x1
(proof)
Known
PNoEq_tra_
PNoEq_tra_
:
∀ x0 .
∀ x1 x2 x3 :
ι → ο
.
PNoEq_
x0
x1
x2
⟶
PNoEq_
x0
x2
x3
⟶
PNoEq_
x0
x1
x3
Theorem
SNoEq_tra_
SNoEq_tra_
:
∀ x0 x1 x2 x3 .
SNoEq_
x0
x1
x2
⟶
SNoEq_
x0
x2
x3
⟶
SNoEq_
x0
x1
x3
(proof)
Param
binintersect
binintersect
:
ι
→
ι
→
ι
Definition
PNoLt_
PNoLt_
:=
λ x0 .
λ x1 x2 :
ι → ο
.
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
and
(
and
(
PNoEq_
x4
x1
x2
)
(
not
(
x1
x4
)
)
)
(
x2
x4
)
)
⟶
x3
)
⟶
x3
Known
PNoLtE
PNoLtE
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
PNoLt
x0
x2
x1
x3
⟶
∀ x4 : ο .
(
PNoLt_
(
binintersect
x0
x1
)
x2
x3
⟶
x4
)
⟶
(
x0
∈
x1
⟶
PNoEq_
x0
x2
x3
⟶
x3
x0
⟶
x4
)
⟶
(
x1
∈
x0
⟶
PNoEq_
x1
x2
x3
⟶
not
(
x2
x1
)
⟶
x4
)
⟶
x4
Known
PNoLt_E_
PNoLt_E_
:
∀ x0 .
∀ x1 x2 :
ι → ο
.
PNoLt_
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
PNoEq_
x4
x1
x2
⟶
not
(
x1
x4
)
⟶
x2
x4
⟶
x3
)
⟶
x3
Known
binintersectE
binintersectE
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
and
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
PNoLtI3
PNoLtI3
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
x1
∈
x0
⟶
PNoEq_
x1
x2
x3
⟶
not
(
x2
x1
)
⟶
PNoLt
x0
x2
x1
x3
Known
PNoLtI2
PNoLtI2
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
x0
∈
x1
⟶
PNoEq_
x0
x2
x3
⟶
x3
x0
⟶
PNoLt
x0
x2
x1
x3
Theorem
SNoLtE
SNoLtE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
SNo
x3
⟶
SNoLev
x3
∈
binintersect
(
SNoLev
x0
)
(
SNoLev
x1
)
⟶
SNoEq_
(
SNoLev
x3
)
x3
x0
⟶
SNoEq_
(
SNoLev
x3
)
x3
x1
⟶
SNoLt
x0
x3
⟶
SNoLt
x3
x1
⟶
nIn
(
SNoLev
x3
)
x0
⟶
SNoLev
x3
∈
x1
⟶
x2
)
⟶
(
SNoLev
x0
∈
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
SNoLev
x0
∈
x1
⟶
x2
)
⟶
(
SNoLev
x1
∈
SNoLev
x0
⟶
SNoEq_
(
SNoLev
x1
)
x0
x1
⟶
nIn
(
SNoLev
x1
)
x0
⟶
x2
)
⟶
x2
(proof)
Theorem
SNoLtI2
SNoLtI2
:
∀ x0 x1 .
SNoLev
x0
∈
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
SNoLev
x0
∈
x1
⟶
SNoLt
x0
x1
(proof)
Theorem
SNoLtI3
SNoLtI3
:
∀ x0 x1 .
SNoLev
x1
∈
SNoLev
x0
⟶
SNoEq_
(
SNoLev
x1
)
x0
x1
⟶
nIn
(
SNoLev
x1
)
x0
⟶
SNoLt
x0
x1
(proof)
Known
PNoLt_irref
PNoLt_irref
:
∀ x0 .
∀ x1 :
ι → ο
.
not
(
PNoLt
x0
x1
x0
x1
)
Theorem
SNoLt_irref
SNoLt_irref
:
∀ x0 .
not
(
SNoLt
x0
x0
)
(proof)
Known
PNoLt_trichotomy_or
PNoLt_trichotomy_or
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
ordinal
x0
⟶
ordinal
x1
⟶
or
(
or
(
PNoLt
x0
x2
x1
x3
)
(
and
(
x0
=
x1
)
(
PNoEq_
x0
x2
x3
)
)
)
(
PNoLt
x1
x3
x0
x2
)
Known
or3I1
or3I1
:
∀ x0 x1 x2 : ο .
x0
⟶
or
(
or
x0
x1
)
x2
Known
or3I2
or3I2
:
∀ x0 x1 x2 : ο .
x1
⟶
or
(
or
x0
x1
)
x2
Known
or3I3
or3I3
:
∀ x0 x1 x2 : ο .
x2
⟶
or
(
or
x0
x1
)
x2
Theorem
SNoLt_trichotomy_or
SNoLt_trichotomy_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
or
(
SNoLt
x0
x1
)
(
x0
=
x1
)
)
(
SNoLt
x1
x0
)
(proof)
Known
PNoLt_tra
PNoLt_tra
:
∀ x0 x1 x2 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
x2
⟶
∀ x3 x4 x5 :
ι → ο
.
PNoLt
x0
x3
x1
x4
⟶
PNoLt
x1
x4
x2
x5
⟶
PNoLt
x0
x3
x2
x5
Theorem
SNoLt_tra
SNoLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
(proof)
Known
PNoLe_ref
PNoLe_ref
:
∀ x0 .
∀ x1 :
ι → ο
.
PNoLe
x0
x1
x0
x1
Theorem
SNoLe_ref
SNoLe_ref
:
∀ x0 .
SNoLe
x0
x0
(proof)
Known
PNoLe_antisym
PNoLe_antisym
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 x3 :
ι → ο
.
PNoLe
x0
x2
x1
x3
⟶
PNoLe
x1
x3
x0
x2
⟶
and
(
x0
=
x1
)
(
PNoEq_
x0
x2
x3
)
Theorem
SNoLe_antisym
SNoLe_antisym
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
SNoLe
x1
x0
⟶
x0
=
x1
(proof)
Known
PNoLtLe_tra
PNoLtLe_tra
:
∀ x0 x1 x2 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
x2
⟶
∀ x3 x4 x5 :
ι → ο
.
PNoLt
x0
x3
x1
x4
⟶
PNoLe
x1
x4
x2
x5
⟶
PNoLt
x0
x3
x2
x5
Theorem
SNoLtLe_tra
SNoLtLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLt
x0
x2
(proof)
Known
PNoLeLt_tra
PNoLeLt_tra
:
∀ x0 x1 x2 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
x2
⟶
∀ x3 x4 x5 :
ι → ο
.
PNoLe
x0
x3
x1
x4
⟶
PNoLt
x1
x4
x2
x5
⟶
PNoLt
x0
x3
x2
x5
Theorem
SNoLeLt_tra
SNoLeLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
(proof)
Known
PNoLe_tra
PNoLe_tra
:
∀ x0 x1 x2 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
x2
⟶
∀ x3 x4 x5 :
ι → ο
.
PNoLe
x0
x3
x1
x4
⟶
PNoLe
x1
x4
x2
x5
⟶
PNoLe
x0
x3
x2
x5
Theorem
SNoLe_tra
SNoLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLe
x0
x2
(proof)
Theorem
SNoLtLe_or
SNoLtLe_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
SNoLt
x0
x1
)
(
SNoLe
x1
x0
)
(proof)
Known
PNoEqLt_tra
PNoEqLt_tra
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 x3 x4 :
ι → ο
.
PNoEq_
x0
x2
x3
⟶
PNoLt
x0
x3
x1
x4
⟶
PNoLt
x0
x2
x1
x4
Known
PNoLtEq_tra
PNoLtEq_tra
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 x3 x4 :
ι → ο
.
PNoLt
x0
x2
x1
x3
⟶
PNoEq_
x1
x3
x4
⟶
PNoLt
x0
x2
x1
x4
Theorem
SNoLt_PSNo_PNoLt
SNoLt_PSNo_PNoLt
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
ordinal
x0
⟶
ordinal
x1
⟶
SNoLt
(
PSNo
x0
x2
)
(
PSNo
x1
x3
)
⟶
PNoLt
x0
x2
x1
x3
(proof)
Theorem
PNoLt_SNoLt_PSNo
PNoLt_SNoLt_PSNo
:
∀ x0 x1 .
∀ x2 x3 :
ι → ο
.
ordinal
x0
⟶
ordinal
x1
⟶
PNoLt
x0
x2
x1
x3
⟶
SNoLt
(
PSNo
x0
x2
)
(
PSNo
x1
x3
)
(proof)
Param
PNo_bd
PNo_bd
:
(
ι
→
(
ι
→
ο
) →
ο
) →
(
ι
→
(
ι
→
ο
) →
ο
) →
ι
Param
PNo_pred
PNo_pred
:
(
ι
→
(
ι
→
ο
) →
ο
) →
(
ι
→
(
ι
→
ο
) →
ο
) →
ι
→
ο
Definition
SNoCut
SNoCut
:=
λ x0 x1 .
PSNo
(
PNo_bd
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
PSNo
x2
x3
∈
x0
)
)
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
PSNo
x2
x3
∈
x1
)
)
)
(
PNo_pred
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
PSNo
x2
x3
∈
x0
)
)
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
PSNo
x2
x3
∈
x1
)
)
)
Definition
SNoCutP
SNoCutP
:=
λ x0 x1 .
and
(
and
(
∀ x2 .
x2
∈
x0
⟶
SNo
x2
)
(
∀ x2 .
x2
∈
x1
⟶
SNo
x2
)
)
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
Param
famunion
famunion
:
ι
→
(
ι
→
ι
) →
ι
Definition
PNoLt_pwise
PNoLt_pwise
:=
λ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
∀ x2 .
ordinal
x2
⟶
∀ x3 :
ι → ο
.
x0
x2
x3
⟶
∀ x4 .
ordinal
x4
⟶
∀ x5 :
ι → ο
.
x1
x4
x5
⟶
PNoLt
x2
x3
x4
x5
Definition
PNo_lenbdd
PNo_lenbdd
:=
λ x0 .
λ x1 :
ι →
(
ι → ο
)
→ ο
.
∀ x2 .
∀ x3 :
ι → ο
.
x1
x2
x3
⟶
x2
∈
x0
Definition
PNo_strict_upperbd
PNo_strict_upperbd
:=
λ x0 :
ι →
(
ι → ο
)
→ ο
.
λ x1 .
λ x2 :
ι → ο
.
∀ x3 .
ordinal
x3
⟶
∀ x4 :
ι → ο
.
x0
x3
x4
⟶
PNoLt
x3
x4
x1
x2
Definition
PNo_strict_lowerbd
PNo_strict_lowerbd
:=
λ x0 :
ι →
(
ι → ο
)
→ ο
.
λ x1 .
λ x2 :
ι → ο
.
∀ x3 .
ordinal
x3
⟶
∀ x4 :
ι → ο
.
x0
x3
x4
⟶
PNoLt
x1
x2
x3
x4
Definition
PNo_strict_imv
PNo_strict_imv
:=
λ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
λ x2 .
λ x3 :
ι → ο
.
and
(
PNo_strict_upperbd
x0
x2
x3
)
(
PNo_strict_lowerbd
x1
x2
x3
)
Definition
PNo_least_rep
PNo_least_rep
:=
λ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
λ x2 .
λ x3 :
ι → ο
.
and
(
and
(
ordinal
x2
)
(
PNo_strict_imv
x0
x1
x2
x3
)
)
(
∀ x4 .
x4
∈
x2
⟶
∀ x5 :
ι → ο
.
not
(
PNo_strict_imv
x0
x1
x4
x5
)
)
Known
PNo_bd_pred
PNo_bd_pred
:
∀ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
PNoLt_pwise
x0
x1
⟶
∀ x2 .
ordinal
x2
⟶
PNo_lenbdd
x2
x0
⟶
PNo_lenbdd
x2
x1
⟶
PNo_least_rep
x0
x1
(
PNo_bd
x0
x1
)
(
PNo_pred
x0
x1
)
Known
and5I
and5I
:
∀ x0 x1 x2 x3 x4 : ο .
x0
⟶
x1
⟶
x2
⟶
x3
⟶
x4
⟶
and
(
and
(
and
(
and
x0
x1
)
x2
)
x3
)
x4
Known
PNoLt_trichotomy_or_
PNoLt_trichotomy_or_
:
∀ x0 x1 :
ι → ο
.
∀ x2 .
ordinal
x2
⟶
or
(
or
(
PNoLt_
x2
x0
x1
)
(
PNoEq_
x2
x0
x1
)
)
(
PNoLt_
x2
x1
x0
)
Param
PNo_rel_strict_imv
PNo_rel_strict_imv
:
(
ι
→
(
ι
→
ο
) →
ο
) →
(
ι
→
(
ι
→
ο
) →
ο
) →
ι
→
(
ι
→
ο
) →
ο
Definition
PNo_rel_strict_split_imv
PNo_rel_strict_split_imv
:=
λ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
λ x2 .
λ x3 :
ι → ο
.
and
(
PNo_rel_strict_imv
x0
x1
(
ordsucc
x2
)
(
λ x4 .
and
(
x3
x4
)
(
x4
=
x2
⟶
∀ x5 : ο .
x5
)
)
)
(
PNo_rel_strict_imv
x0
x1
(
ordsucc
x2
)
(
λ x4 .
or
(
x3
x4
)
(
x4
=
x2
)
)
)
Known
PNo_rel_split_imv_imp_strict_imv
PNo_rel_split_imv_imp_strict_imv
:
∀ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
∀ x2 .
ordinal
x2
⟶
∀ x3 :
ι → ο
.
PNo_rel_strict_split_imv
x0
x1
x2
x3
⟶
PNo_strict_imv
x0
x1
x2
x3
Known
PNoEq_rel_strict_imv
PNoEq_rel_strict_imv
:
∀ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
∀ x2 .
ordinal
x2
⟶
∀ x3 x4 :
ι → ο
.
PNoEq_
x2
x3
x4
⟶
PNo_rel_strict_imv
x0
x1
x2
x3
⟶
PNo_rel_strict_imv
x0
x1
x2
x4
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
iff_trans
iff_trans
:
∀ x0 x1 x2 : ο .
iff
x0
x1
⟶
iff
x1
x2
⟶
iff
x0
x2
Known
PNo_extend0_eq
PNo_extend0_eq
:
∀ x0 .
∀ x1 :
ι → ο
.
PNoEq_
x0
x1
(
λ x2 .
and
(
x1
x2
)
(
x2
=
x0
⟶
∀ x3 : ο .
x3
)
)
Known
PNo_strict_imv_imp_rel_strict_imv
PNo_strict_imv_imp_rel_strict_imv
:
∀ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
∀ x2 .
ordinal
x2
⟶
∀ x3 .
x3
∈
ordsucc
x2
⟶
∀ x4 :
ι → ο
.
PNo_strict_imv
x0
x1
x2
x4
⟶
PNo_rel_strict_imv
x0
x1
x3
x4
Known
ordinal_ordsucc_In
ordinal_ordsucc_In
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
PNo_extend1_eq
PNo_extend1_eq
:
∀ x0 .
∀ x1 :
ι → ο
.
PNoEq_
x0
x1
(
λ x2 .
or
(
x1
x2
)
(
x2
=
x0
)
)
Known
ordinal_ordsucc
ordinal_ordsucc
:
∀ x0 .
ordinal
x0
⟶
ordinal
(
ordsucc
x0
)
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Known
PNo_bd_In
PNo_bd_In
:
∀ x0 x1 :
ι →
(
ι → ο
)
→ ο
.
PNoLt_pwise
x0
x1
⟶
∀ x2 .
ordinal
x2
⟶
PNo_lenbdd
x2
x0
⟶
PNo_lenbdd
x2
x1
⟶
PNo_bd
x0
x1
∈
ordsucc
x2
Known
famunionI
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
x0
⟶
x3
∈
x1
x2
⟶
x3
∈
famunion
x0
x1
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Known
ordinal_linear
ordinal_linear
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
⊆
x1
)
(
x1
⊆
x0
)
Known
Subq_binunion_eq
Subq_binunion_eq
:
∀ x0 x1 .
x0
⊆
x1
=
(
binunion
x0
x1
=
x1
)
Known
binunion_com
binunion_com
:
∀ x0 x1 .
binunion
x0
x1
=
binunion
x1
x0
Known
ordinal_famunion
ordinal_famunion
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
ordinal
(
x1
x2
)
)
⟶
ordinal
(
famunion
x0
x1
)
Theorem
SNoCutP_SNoCut
SNoCutP_SNoCut
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
and
(
and
(
and
(
and
(
SNo
(
SNoCut
x0
x1
)
)
(
SNoLev
(
SNoCut
x0
x1
)
∈
ordsucc
(
binunion
(
famunion
x0
(
λ x2 .
ordsucc
(
SNoLev
x2
)
)
)
(
famunion
x1
(
λ x2 .
ordsucc
(
SNoLev
x2
)
)
)
)
)
)
(
∀ x2 .
x2
∈
x0
⟶
SNoLt
x2
(
SNoCut
x0
x1
)
)
)
(
∀ x2 .
x2
∈
x1
⟶
SNoLt
(
SNoCut
x0
x1
)
x2
)
)
(
∀ x2 .
SNo
x2
⟶
(
∀ x3 .
x3
∈
x0
⟶
SNoLt
x3
x2
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
x2
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
x2
)
)
(proof)
Definition
SNoS_
SNoS_
:=
λ x0 .
{x1 ∈
prim4
(
SNoElts_
x0
)
|
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
SNo_
x3
x1
)
⟶
x2
)
⟶
x2
}
Theorem
SNoS_E
SNoS_E
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
SNo_
x3
x1
)
⟶
x2
)
⟶
x2
(proof)
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Known
Subq_tra
Subq_tra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
x1
⊆
x2
⟶
x0
⊆
x2
Theorem
SNoS_I
SNoS_I
:
∀ x0 .
ordinal
x0
⟶
∀ x1 x2 .
x2
∈
x0
⟶
SNo_
x2
x1
⟶
x1
∈
SNoS_
x0
(proof)
Theorem
SNoS_I2
SNoS_I2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
∈
SNoLev
x1
⟶
x0
∈
SNoS_
(
SNoLev
x1
)
(proof)
Theorem
SNoS_Subq
SNoS_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
x0
⊆
x1
⟶
SNoS_
x0
⊆
SNoS_
x1
(proof)
Theorem
SNoLev_uniq2
SNoLev_uniq2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNoLev
x1
=
x0
(proof)
Theorem
SNoS_E2
SNoS_E2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
∀ x2 : ο .
(
SNoLev
x1
∈
x0
⟶
ordinal
(
SNoLev
x1
)
⟶
SNo
x1
⟶
SNo_
(
SNoLev
x1
)
x1
⟶
x2
)
⟶
x2
(proof)
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Theorem
SNoS_In_neq
SNoS_In_neq
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoS_
(
SNoLev
x0
)
⟶
x1
=
x0
⟶
∀ x2 : ο .
x2
(proof)
Theorem
SNoS_SNoLev
SNoS_SNoLev
:
∀ x0 .
SNo
x0
⟶
x0
∈
SNoS_
(
ordsucc
(
SNoLev
x0
)
)
(proof)
Definition
SNoL
SNoL
:=
λ x0 .
{x1 ∈
SNoS_
(
SNoLev
x0
)
|
SNoLt
x1
x0
}
Definition
SNoR
SNoR
:=
λ x0 .
Sep
(
SNoS_
(
SNoLev
x0
)
)
(
SNoLt
x0
)
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
SepE1
SepE1
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x2
∈
x0
Theorem
SNoCutP_SNoL_SNoR
SNoCutP_SNoL_SNoR
:
∀ x0 .
SNo
x0
⟶
SNoCutP
(
SNoL
x0
)
(
SNoR
x0
)
(proof)
Theorem
SNoL_E
SNoL_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoL
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x2
)
⟶
x2
(proof)
Theorem
SNoR_E
SNoR_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoR
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x0
x1
⟶
x2
)
⟶
x2
(proof)
Theorem
SNoL_SNoS
SNoL_SNoS
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoL
x0
⟶
x1
∈
SNoS_
(
SNoLev
x0
)
(proof)
Theorem
SNoR_SNoS
SNoR_SNoS
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoR
x0
⟶
x1
∈
SNoS_
(
SNoLev
x0
)
(proof)
Theorem
SNoL_I
SNoL_I
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x1
∈
SNoL
x0
(proof)
Theorem
SNoR_I
SNoR_I
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x0
x1
⟶
x1
∈
SNoR
x0
(proof)
Known
ordinal_trichotomy_or
ordinal_trichotomy_or
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
or
(
x0
∈
x1
)
(
x0
=
x1
)
)
(
x1
∈
x0
)
Theorem
SNo_eta
SNo_eta
:
∀ x0 .
SNo
x0
⟶
x0
=
SNoCut
(
SNoL
x0
)
(
SNoR
x0
)
(proof)
Theorem
SNoCutP_SNo_SNoCut
SNoCutP_SNo_SNoCut
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
SNo
(
SNoCut
x0
x1
)
(proof)
Theorem
SNoCutP_SNoCut_L
SNoCutP_SNoCut_L
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
SNoLt
x2
(
SNoCut
x0
x1
)
(proof)
Theorem
SNoCutP_SNoCut_R
SNoCutP_SNoCut_R
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
x2
∈
x1
⟶
SNoLt
(
SNoCut
x0
x1
)
x2
(proof)
Theorem
SNoCutP_SNoCut_fst
SNoCutP_SNoCut_fst
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
SNo
x2
⟶
(
∀ x3 .
x3
∈
x0
⟶
SNoLt
x3
x2
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
x2
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
x2
)
(proof)
Known
binintersectE2
binintersectE2
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x1
Theorem
SNoCut_Le
SNoCut_Le
:
∀ x0 x1 x2 x3 .
SNoCutP
x0
x1
⟶
SNoCutP
x2
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
SNoLt
x4
(
SNoCut
x2
x3
)
)
⟶
(
∀ x4 .
x4
∈
x3
⟶
SNoLt
(
SNoCut
x0
x1
)
x4
)
⟶
SNoLe
(
SNoCut
x0
x1
)
(
SNoCut
x2
x3
)
(proof)
Theorem
SNoCut_ext
SNoCut_ext
:
∀ x0 x1 x2 x3 .
SNoCutP
x0
x1
⟶
SNoCutP
x2
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
SNoLt
x4
(
SNoCut
x2
x3
)
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
SNoLt
(
SNoCut
x2
x3
)
x4
)
⟶
(
∀ x4 .
x4
∈
x2
⟶
SNoLt
x4
(
SNoCut
x0
x1
)
)
⟶
(
∀ x4 .
x4
∈
x3
⟶
SNoLt
(
SNoCut
x0
x1
)
x4
)
⟶
SNoCut
x0
x1
=
SNoCut
x2
x3
(proof)
Theorem
ordinal_SNo_
ordinal_SNo_
:
∀ x0 .
ordinal
x0
⟶
SNo_
x0
x0
(proof)
Definition
SNo_extend0
SNo_extend0
:=
λ x0 .
PSNo
(
ordsucc
(
SNoLev
x0
)
)
(
λ x1 .
and
(
x1
∈
x0
)
(
x1
=
SNoLev
x0
⟶
∀ x2 : ο .
x2
)
)
Definition
SNo_extend1
SNo_extend1
:=
λ x0 .
PSNo
(
ordsucc
(
SNoLev
x0
)
)
(
λ x1 .
or
(
x1
∈
x0
)
(
x1
=
SNoLev
x0
)
)
Theorem
SNo_extend0_SNo_
SNo_extend0_SNo_
:
∀ x0 .
SNo
x0
⟶
SNo_
(
ordsucc
(
SNoLev
x0
)
)
(
SNo_extend0
x0
)
(proof)
Theorem
SNo_extend1_SNo_
SNo_extend1_SNo_
:
∀ x0 .
SNo
x0
⟶
SNo_
(
ordsucc
(
SNoLev
x0
)
)
(
SNo_extend1
x0
)
(proof)
Theorem
SNo_extend0_SNo
SNo_extend0_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
SNo_extend0
x0
)
(proof)
Theorem
SNo_extend1_SNo
SNo_extend1_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
SNo_extend1
x0
)
(proof)
Theorem
SNo_extend0_SNoLev
SNo_extend0_SNoLev
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
SNo_extend0
x0
)
=
ordsucc
(
SNoLev
x0
)
(proof)
Theorem
SNo_extend1_SNoLev
SNo_extend1_SNoLev
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
SNo_extend1
x0
)
=
ordsucc
(
SNoLev
x0
)
(proof)
Theorem
SNo_extend0_nIn
SNo_extend0_nIn
:
∀ x0 .
SNo
x0
⟶
nIn
(
SNoLev
x0
)
(
SNo_extend0
x0
)
(proof)
Theorem
SNo_extend1_In
SNo_extend1_In
:
∀ x0 .
SNo
x0
⟶
SNoLev
x0
∈
SNo_extend1
x0
(proof)
Theorem
SNo_extend0_SNoEq
SNo_extend0_SNoEq
:
∀ x0 .
SNo
x0
⟶
SNoEq_
(
SNoLev
x0
)
(
SNo_extend0
x0
)
x0
(proof)
Theorem
SNo_extend1_SNoEq
SNo_extend1_SNoEq
:
∀ x0 .
SNo
x0
⟶
SNoEq_
(
SNoLev
x0
)
(
SNo_extend1
x0
)
x0
(proof)
Theorem
ordinal_SNo
ordinal_SNo
:
∀ x0 .
ordinal
x0
⟶
SNo
x0
(proof)
Theorem
ordinal_SNoLev
ordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
x0
=
x0
(proof)
Known
binintersectE1
binintersectE1
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x0
Known
In_no2cycle
In_no2cycle
:
∀ x0 x1 .
x0
∈
x1
⟶
x1
∈
x0
⟶
False
Theorem
ordinal_SNoLev_max
ordinal_SNoLev_max
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
x0
⟶
SNoLt
x1
x0
(proof)
Theorem
ordinal_In_SNoLt
ordinal_In_SNoLt
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
SNoLt
x1
x0
(proof)
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
ordinal_ind
ordinal_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
ordinal
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
ordinal
x1
⟶
x0
x1
Theorem
ordinal_SNoLev_max_2
ordinal_SNoLev_max_2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
ordsucc
x0
⟶
SNoLe
x1
x0
(proof)
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Theorem
ordinal_Subq_SNoLe
ordinal_Subq_SNoLe
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
x0
⊆
x1
⟶
SNoLe
x0
x1
(proof)
Theorem
SNo_etaE
SNo_etaE
:
∀ x0 .
SNo
x0
⟶
∀ x1 : ο .
(
∀ x2 x3 .
SNoCutP
x2
x3
⟶
(
∀ x4 .
x4
∈
x2
⟶
SNoLev
x4
∈
SNoLev
x0
)
⟶
(
∀ x4 .
x4
∈
x3
⟶
SNoLev
x4
∈
SNoLev
x0
)
⟶
x0
=
SNoCut
x2
x3
⟶
x1
)
⟶
x1
(proof)
Theorem
SNo_ind
SNo_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 x2 .
SNoCutP
x1
x2
⟶
(
∀ x3 .
x3
∈
x1
⟶
x0
x3
)
⟶
(
∀ x3 .
x3
∈
x2
⟶
x0
x3
)
⟶
x0
(
SNoCut
x1
x2
)
)
⟶
∀ x1 .
SNo
x1
⟶
x0
x1
(proof)