Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrCit..
/
ac2a7..
PUQ2e..
/
fad5d..
vout
PrCit..
/
23779..
3.96 bars
TMZTe..
/
e9aa2..
ownership of
51de2..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMYTn..
/
2ad50..
ownership of
4fbe2..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcQJ..
/
ae8e8..
ownership of
05730..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMLT6..
/
f31fc..
ownership of
ad62e..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZ5r..
/
919c7..
ownership of
4948f..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMd1g..
/
2ddb9..
ownership of
5a096..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMb4Q..
/
8a19b..
ownership of
36d6a..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQZs..
/
db2aa..
ownership of
9266f..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQqE..
/
f611b..
ownership of
141e8..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGPk..
/
b56c6..
ownership of
52137..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUpZ..
/
4fdd6..
ownership of
eeb21..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMNXo..
/
2da49..
ownership of
4f44c..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGy1..
/
fab9e..
ownership of
f7ea8..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMa7H..
/
c7a50..
ownership of
40c2c..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMM7S..
/
25f43..
ownership of
7c521..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJKE..
/
ee448..
ownership of
caaed..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMW1p..
/
95184..
ownership of
d70cc..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMU9M..
/
67a06..
ownership of
1692d..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMXzm..
/
879d6..
ownership of
ff095..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMd2N..
/
6a334..
ownership of
6502b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMFt5..
/
d267e..
ownership of
4b1ff..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZwp..
/
94b2c..
ownership of
01a11..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMLB7..
/
3479c..
ownership of
d67ed..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSZL..
/
4d6e5..
ownership of
e5d03..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMFq3..
/
3e294..
ownership of
a1aba..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGQx..
/
cacbb..
ownership of
61965..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZPY..
/
508bb..
ownership of
65ef6..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbAm..
/
89316..
ownership of
f10dc..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMaS9..
/
1af27..
ownership of
e6d41..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSZG..
/
b06de..
ownership of
8e052..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMEiL..
/
af22c..
ownership of
386bf..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHJh..
/
b3d9a..
ownership of
3e024..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMYTQ..
/
4a55b..
ownership of
5983e..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMEre..
/
201f0..
ownership of
c46d2..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMXcF..
/
55633..
ownership of
34b98..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMYqK..
/
22d56..
ownership of
114be..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMdD5..
/
c8799..
ownership of
4f936..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMamd..
/
0a556..
ownership of
541d2..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMRip..
/
af0d2..
ownership of
411b1..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMFEw..
/
f19a0..
ownership of
049aa..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJkR..
/
3ab0f..
ownership of
8f044..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMG5R..
/
8170c..
ownership of
ca359..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbiu..
/
30b3f..
ownership of
663d6..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMWpc..
/
26722..
ownership of
6e7cb..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMV9J..
/
8216f..
ownership of
8f72e..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMLFv..
/
b69db..
ownership of
b33aa..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMPAN..
/
65548..
ownership of
c7bb7..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMWNM..
/
6098d..
ownership of
e7a22..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMceb..
/
4fc28..
ownership of
db10e..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUbz..
/
a3237..
ownership of
b152a..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQeT..
/
5d50c..
ownership of
b70a6..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMVVL..
/
00fae..
ownership of
8b064..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZU5..
/
49a16..
ownership of
3d32d..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMFZP..
/
fced3..
ownership of
ad830..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMXdZ..
/
64087..
ownership of
6cd03..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHqT..
/
37dc7..
ownership of
15832..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMXqS..
/
89b4d..
ownership of
9b83b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMH3R..
/
2aeab..
ownership of
a27db..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcpf..
/
694bc..
ownership of
feddd..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHx3..
/
6ad84..
ownership of
4d754..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMKqA..
/
eb9a9..
ownership of
f5939..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZcG..
/
66704..
ownership of
9c057..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUuD..
/
59617..
ownership of
c6b87..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMdZM..
/
2fa23..
ownership of
99998..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUid..
/
20bf3..
ownership of
2f205..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbK7..
/
aac3a..
ownership of
e5120..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGqr..
/
bff18..
ownership of
b3144..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHnH..
/
1f73f..
ownership of
f861a..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMYPC..
/
524f8..
ownership of
0564f..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMd8Q..
/
50787..
ownership of
06ae9..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMMZb..
/
f2856..
ownership of
18365..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMRzw..
/
03508..
ownership of
00d51..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUUR..
/
48939..
ownership of
df221..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGt2..
/
6846f..
ownership of
6c01c..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSSf..
/
421dc..
ownership of
4cfca..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMTcY..
/
c7660..
ownership of
67d94..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMKrS..
/
abdc9..
ownership of
0f811..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZ3Q..
/
51c26..
ownership of
a1a90..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMa32..
/
0bc66..
ownership of
ec3c1..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbNd..
/
212b3..
ownership of
50aa1..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZv1..
/
42f25..
ownership of
b1ec3..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMd49..
/
98d2a..
ownership of
0ca6b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMTtJ..
/
8c9e3..
ownership of
ecf06..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJqv..
/
10e40..
ownership of
26eda..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJ2Z..
/
1534e..
ownership of
fe08b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSiX..
/
a0fbd..
ownership of
0b9ff..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGQZ..
/
9b4f6..
ownership of
9e8b0..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMFdV..
/
9dd9e..
ownership of
b16b8..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHqb..
/
bda37..
ownership of
0aa1b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSGY..
/
f71ff..
ownership of
b34a1..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
PUf8d..
/
4dad6..
doc published by
Pr4zB..
Param
add_nat
add_nat
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
u4
:=
ordsucc
u3
Definition
u5
:=
ordsucc
u4
Definition
u6
:=
ordsucc
u5
Definition
u7
:=
ordsucc
u6
Definition
u8
:=
ordsucc
u7
Definition
u9
:=
ordsucc
u8
Param
nat_p
nat_p
:
ι
→
ο
Known
add_nat_SR
add_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
add_nat
x0
(
ordsucc
x1
)
=
ordsucc
(
add_nat
x0
x1
)
Known
nat_3
nat_3
:
nat_p
3
Known
e705e..
:
add_nat
u5
u3
=
u8
Theorem
0aa1b..
:
add_nat
u5
u4
=
u9
(proof)
Definition
u10
:=
ordsucc
u9
Known
nat_4
nat_4
:
nat_p
4
Theorem
9e8b0..
:
add_nat
u5
u5
=
u10
(proof)
Definition
u11
:=
ordsucc
u10
Known
nat_5
nat_5
:
nat_p
5
Theorem
fe08b..
:
add_nat
u5
u6
=
u11
(proof)
Definition
u12
:=
ordsucc
u11
Known
nat_6
nat_6
:
nat_p
6
Theorem
ecf06..
:
add_nat
u5
u7
=
u12
(proof)
Definition
u13
:=
ordsucc
u12
Known
nat_7
nat_7
:
nat_p
7
Theorem
b1ec3..
:
add_nat
u5
u8
=
u13
(proof)
Definition
u14
:=
ordsucc
u13
Known
nat_8
nat_8
:
nat_p
8
Theorem
ec3c1..
:
add_nat
u5
u9
=
u14
(proof)
Definition
u15
:=
ordsucc
u14
Known
nat_9
nat_9
:
nat_p
9
Theorem
0f811..
:
add_nat
u5
u10
=
u15
(proof)
Definition
u16
:=
ordsucc
u15
Known
nat_10
nat_10
:
nat_p
10
Theorem
4cfca..
:
add_nat
u5
u11
=
u16
(proof)
Definition
u17
:=
ordsucc
u16
Known
nat_11
nat_11
:
nat_p
11
Theorem
df221..
:
add_nat
u5
u12
=
u17
(proof)
Definition
u18
:=
ordsucc
u17
Known
nat_12
nat_12
:
nat_p
12
Theorem
18365..
:
add_nat
u5
u13
=
u18
(proof)
Definition
u19
:=
ordsucc
u18
Known
nat_13
nat_13
:
nat_p
13
Theorem
0564f..
:
add_nat
u5
u14
=
u19
(proof)
Definition
u20
:=
ordsucc
u19
Known
nat_14
nat_14
:
nat_p
14
Theorem
b3144..
:
add_nat
u5
u15
=
u20
(proof)
Known
nat_2
nat_2
:
nat_p
2
Known
nat_1
nat_1
:
nat_p
1
Known
nat_0
nat_0
:
nat_p
0
Known
add_nat_0R
add_nat_0R
:
∀ x0 .
add_nat
x0
0
=
x0
Theorem
2f205..
:
add_nat
u13
u6
=
u19
(proof)
Param
mul_nat
mul_nat
:
ι
→
ι
→
ι
Known
mul_nat_SR
mul_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
mul_nat
x0
(
ordsucc
x1
)
=
add_nat
x0
(
mul_nat
x0
x1
)
Known
mul_nat_com
mul_nat_com
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
mul_nat
x0
x1
=
mul_nat
x1
x0
Known
6cce6..
:
∀ x0 .
nat_p
x0
⟶
mul_nat
u2
x0
=
add_nat
x0
x0
Theorem
c6b87..
:
mul_nat
u5
u4
=
u20
(proof)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
Sing
Sing
:
ι
→
ι
Known
bijE
bijE
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
∀ x3 : ο .
(
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
∈
x1
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
=
x2
x5
⟶
x4
=
x5
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x0
)
(
x2
x6
=
x4
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
In_0_1
In_0_1
:
0
∈
1
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
cases_1
cases_1
:
∀ x0 .
x0
∈
1
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
x0
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Theorem
f5939..
:
∀ x0 .
equip
u1
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
x0
)
(
x0
=
Sing
x2
)
⟶
x1
)
⟶
x1
(proof)
Param
UPair
UPair
:
ι
→
ι
→
ι
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Known
e8716..
:
∀ x0 .
atleastp
u2
x0
⟶
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x1
)
⟶
x1
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
4fb58..
Pigeonhole_not_atleastp_ordsucc
:
∀ x0 .
nat_p
x0
⟶
not
(
atleastp
(
ordsucc
x0
)
x0
)
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Known
5d098..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
(
x1
=
x2
⟶
∀ x4 : ο .
x4
)
⟶
(
x1
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
atleastp
u3
x0
Known
UPairI1
UPairI1
:
∀ x0 x1 .
x0
∈
UPair
x0
x1
Known
UPairI2
UPairI2
:
∀ x0 x1 .
x1
∈
UPair
x0
x1
Known
equip_atleastp
equip_atleastp
:
∀ x0 x1 .
equip
x0
x1
⟶
atleastp
x0
x1
Known
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
UPairE
UPairE
:
∀ x0 x1 x2 .
x0
∈
UPair
x1
x2
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
Theorem
feddd..
:
∀ x0 .
equip
u2
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
x0
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
and
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
(
x0
=
UPair
x2
x4
)
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
(proof)
Param
omega
omega
:
ι
Definition
finite
finite
:=
λ x0 .
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
equip
x0
x2
)
⟶
x1
)
⟶
x1
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
equip_ref
equip_ref
:
∀ x0 .
equip
x0
x0
Theorem
9b83b..
nat_finite
:
∀ x0 .
nat_p
x0
⟶
finite
x0
(proof)
Theorem
6cd03..
:
∀ x0 x1 .
x1
∈
x0
⟶
Sing
x1
⊆
x0
(proof)
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
setminus
setminus
:
ι
→
ι
→
ι
Known
e6195..
:
∀ x0 x1 .
x1
⊆
x0
⟶
x0
=
binunion
(
setminus
x0
x1
)
x1
Theorem
eb0c4..
binunion_remove1_eq
:
∀ x0 x1 .
x1
∈
x0
⟶
x0
=
binunion
(
setminus
x0
(
Sing
x1
)
)
(
Sing
x1
)
(proof)
Param
ordinal
ordinal
:
ι
→
ο
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
nat_trans
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Theorem
3d32d..
:
∀ x0 x1 .
nat_p
x0
⟶
nat_p
x1
⟶
x0
⊆
x1
⟶
ordsucc
x0
⊆
ordsucc
x1
(proof)
Known
nat_ind
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
Empty_Subq_eq
Empty_Subq_eq
:
∀ x0 .
x0
⊆
0
⟶
x0
=
0
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
e8bc0..
equip_adjoin_ordsucc
:
∀ x0 x1 x2 .
nIn
x2
x1
⟶
equip
x0
x1
⟶
equip
(
ordsucc
x0
)
(
binunion
x1
(
Sing
x2
)
)
Known
setminus_nIn_I2
setminus_nIn_I2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
nIn
x2
(
setminus
x0
x1
)
Known
setminusE
setminusE
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
and
(
x2
∈
x0
)
(
nIn
x2
x1
)
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
Subq_tra
Subq_tra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
x1
⊆
x2
⟶
x0
⊆
x2
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Theorem
b70a6..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
⊆
x0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
and
(
nat_p
x3
)
(
x3
⊆
x0
)
)
(
equip
x1
x3
)
⟶
x2
)
⟶
x2
(proof)
Known
2d48b..
:
∀ x0 x1 .
atleastp
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
x3
⊆
x1
⟶
equip
x0
x3
⟶
x2
)
⟶
x2
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
equip_tra
equip_tra
:
∀ x0 x1 x2 .
equip
x0
x1
⟶
equip
x1
x2
⟶
equip
x0
x2
Known
Subq_atleastp
Subq_atleastp
:
∀ x0 x1 .
x0
⊆
x1
⟶
atleastp
x0
x1
Theorem
db10e..
:
∀ x0 x1 .
x1
⊆
x0
⟶
finite
x0
⟶
finite
x1
(proof)
Definition
u21
:=
ordsucc
u20
Definition
u22
:=
ordsucc
u21
Definition
u23
:=
ordsucc
u22
Definition
u24
:=
ordsucc
u23
Theorem
c7bb7..
:
add_nat
u20
u4
=
u24
(proof)
Theorem
8f72e..
:
add_nat
u12
u8
=
u20
(proof)
Theorem
663d6..
:
add_nat
u12
u12
=
u24
(proof)
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Definition
setprod
setprod
:=
λ x0 x1 .
lam
x0
(
λ x2 .
x1
)
Param
Pi
Pi
:
ι
→
(
ι
→
ι
) →
ι
Definition
setexp
setexp
:=
λ x0 x1 .
Pi
x1
(
λ x2 .
x0
)
Param
ap
ap
:
ι
→
ι
→
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
bijI
bijI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
⟶
bij
x0
x1
x2
Known
tuple_2_setprod
tuple_2_setprod
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
x2
x3
)
∈
setprod
x0
x1
Known
ap_Pi
ap_Pi
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
Pi
x0
x1
⟶
x3
∈
x0
⟶
ap
x2
x3
∈
x1
x3
Known
ap1_Sigma
ap1_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
1
∈
x1
(
ap
x2
0
)
Known
ap0_Sigma
ap0_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
0
∈
x0
Known
tuple_Sigma_eta
tuple_Sigma_eta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
ap
x2
0
)
(
ap
x2
1
)
)
=
x2
Known
tuple_2_1_eq
tuple_2_1_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
1
=
x1
Known
tuple_2_0_eq
tuple_2_0_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
0
=
x0
Known
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
Known
Eps_i_ex
Eps_i_ex
:
∀ x0 :
ι → ο
.
(
∀ x1 : ο .
(
∀ x2 .
x0
x2
⟶
x1
)
⟶
x1
)
⟶
x0
(
prim0
x0
)
Known
lam_Pi
lam_Pi
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
x3
)
⟶
lam
x0
x2
∈
Pi
x0
x1
Known
beta
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
Theorem
8f044..
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
equip
(
x2
x3
)
x1
)
⟶
equip
(
lam
x0
x2
)
(
setprod
x0
x1
)
(proof)
Param
famunion
famunion
:
ι
→
(
ι
→
ι
) →
ι
Known
famunionI
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
x0
⟶
x3
∈
x1
x2
⟶
x3
∈
famunion
x0
x1
Known
famunionE_impred
famunionE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
∈
x1
x4
⟶
x3
)
⟶
x3
Theorem
411b1..
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x1
x2
⟶
x4
∈
x1
x3
⟶
x2
=
x3
)
⟶
equip
(
lam
x0
x1
)
(
famunion
x0
x1
)
(proof)
Theorem
4f936..
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
equip
(
x2
x3
)
x1
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x2
x3
⟶
x5
∈
x2
x4
⟶
x3
=
x4
)
⟶
equip
(
famunion
x0
x2
)
(
setprod
x0
x1
)
(proof)
Theorem
34b98..
:
∀ x0 x1 x2 x3 .
equip
x0
x1
⟶
equip
x2
x3
⟶
equip
(
setprod
x0
x2
)
(
setprod
x1
x3
)
(proof)
Theorem
5983e..
:
∀ x0 x1 x2 .
∀ x3 :
ι → ι
.
equip
x0
x1
⟶
(
∀ x4 .
x4
∈
x0
⟶
equip
(
x3
x4
)
x2
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x3
x4
⟶
x6
∈
x3
x5
⟶
x4
=
x5
)
⟶
equip
(
famunion
x0
x3
)
(
setprod
x1
x2
)
(proof)
Known
Subq_Empty
Subq_Empty
:
∀ x0 .
0
⊆
x0
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Theorem
386bf..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
atleastp
x1
x0
⟶
x1
⊆
x0
(proof)
Theorem
e6d41..
:
∀ x0 x1 .
nat_p
x0
⟶
nat_p
x1
⟶
equip
x0
x1
⟶
x0
=
x1
(proof)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Known
add_nat_p
add_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
add_nat
x0
x1
)
Param
setsum
setsum
:
ι
→
ι
→
ι
Known
c88e0..
:
∀ x0 x1 x2 x3 .
nat_p
x0
⟶
nat_p
x1
⟶
equip
x0
x2
⟶
equip
x1
x3
⟶
equip
(
add_nat
x0
x1
)
(
setsum
x2
x3
)
Known
d778e..
:
∀ x0 x1 x2 x3 .
equip
x0
x2
⟶
equip
x1
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
nIn
x4
x1
)
⟶
equip
(
binunion
x0
x1
)
(
setsum
x2
x3
)
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
SepE1
SepE1
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x2
∈
x0
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Theorem
65ef6..
:
∀ x0 x1 .
nat_p
x1
⟶
∀ x2 :
ι → ι
.
∀ x3 x4 x5 x6 .
nat_p
x3
⟶
nat_p
x4
⟶
(
x3
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
nat_p
x5
⟶
nat_p
x6
⟶
(
∀ x7 .
x7
∈
x1
⟶
or
(
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x3
)
(
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x4
)
)
⟶
equip
{x7 ∈
x1
|
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x3
}
x5
⟶
equip
{x7 ∈
x1
|
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x4
}
x6
⟶
add_nat
x5
x6
=
x1
(proof)
Known
mul_nat_p
mul_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
mul_nat
x0
x1
)
Known
63881..
:
∀ x0 x1 x2 x3 .
nat_p
x0
⟶
nat_p
x1
⟶
equip
x0
x2
⟶
equip
x1
x3
⟶
equip
(
mul_nat
x0
x1
)
(
setprod
x2
x3
)
Theorem
a1aba..
:
∀ x0 x1 .
nat_p
x0
⟶
∀ x2 :
ι → ι
.
∀ x3 x4 x5 x6 .
nat_p
x3
⟶
nat_p
x4
⟶
(
x3
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
nat_p
x5
⟶
nat_p
x6
⟶
(
∀ x7 .
x7
∈
x0
⟶
x2
x7
∈
x1
)
⟶
(
∀ x7 .
x7
∈
x1
⟶
or
(
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x3
)
(
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x4
)
)
⟶
equip
{x7 ∈
x1
|
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x3
}
x5
⟶
equip
{x7 ∈
x1
|
equip
{x8 ∈
x0
|
x2
x8
=
x7
}
x4
}
x6
⟶
add_nat
(
mul_nat
x5
x3
)
(
mul_nat
x6
x4
)
=
x0
(proof)
Param
SNo
SNo
:
ι
→
ο
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Known
add_SNo_1_1_2
add_SNo_1_1_2
:
add_SNo
1
1
=
2
Known
mul_SNo_distrR
mul_SNo_distrR
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
(
add_SNo
x0
x1
)
x2
=
add_SNo
(
mul_SNo
x0
x2
)
(
mul_SNo
x1
x2
)
Known
SNo_1
SNo_1
:
SNo
1
Known
mul_SNo_oneL
mul_SNo_oneL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
1
x0
=
x0
Theorem
d67ed..
:
∀ x0 .
SNo
x0
⟶
mul_SNo
2
x0
=
add_SNo
x0
x0
(proof)
Param
minus_SNo
minus_SNo
:
ι
→
ι
Known
mul_SNo_distrL
mul_SNo_distrL
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
(
mul_SNo
x0
x1
)
(
mul_SNo
x0
x2
)
Known
SNo_2
SNo_2
:
SNo
2
Known
minus_add_SNo_distr
minus_add_SNo_distr
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
minus_SNo
(
add_SNo
x0
x1
)
=
add_SNo
(
minus_SNo
x0
)
(
minus_SNo
x1
)
Known
add_SNo_com_4_inner_mid
add_SNo_com_4_inner_mid
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
add_SNo
(
add_SNo
x0
x1
)
(
add_SNo
x2
x3
)
=
add_SNo
(
add_SNo
x0
x2
)
(
add_SNo
x1
x3
)
Known
add_SNo_minus_SNo_rinv
add_SNo_minus_SNo_rinv
:
∀ x0 .
SNo
x0
⟶
add_SNo
x0
(
minus_SNo
x0
)
=
0
Known
add_SNo_0R
add_SNo_0R
:
∀ x0 .
SNo
x0
⟶
add_SNo
x0
0
=
x0
Known
SNo_add_SNo
SNo_add_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
add_SNo
x0
x1
)
Known
add_SNo_cancel_R
add_SNo_cancel_R
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
x1
=
add_SNo
x2
x1
⟶
x0
=
x2
Known
add_SNo_minus_R2'
add_SNo_minus_R2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
(
add_SNo
x0
(
minus_SNo
x1
)
)
x1
=
x0
Known
add_SNo_0L
add_SNo_0L
:
∀ x0 .
SNo
x0
⟶
add_SNo
0
x0
=
x0
Known
add_SNo_assoc
add_SNo_assoc
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
(
add_SNo
x0
x1
)
x2
Known
add_SNo_minus_SNo_linv
add_SNo_minus_SNo_linv
:
∀ x0 .
SNo
x0
⟶
add_SNo
(
minus_SNo
x0
)
x0
=
0
Known
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
Known
SNo_mul_SNo
SNo_mul_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
mul_SNo
x0
x1
)
Theorem
4b1ff..
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
add_SNo
x0
x1
=
x2
⟶
add_SNo
x0
(
mul_SNo
2
x1
)
=
x3
⟶
and
(
x1
=
add_SNo
x3
(
minus_SNo
x2
)
)
(
x0
=
add_SNo
(
mul_SNo
2
x2
)
(
minus_SNo
x3
)
)
(proof)
Known
nat_p_SNo
nat_p_SNo
:
∀ x0 .
nat_p
x0
⟶
SNo
x0
Known
2669c..
:
nat_p
u20
Known
add_SNo_com
add_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
x0
x1
=
add_SNo
x1
x0
Known
add_nat_add_SNo
add_nat_add_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
add_nat
x0
x1
=
add_SNo
x0
x1
Theorem
ff095..
:
add_SNo
u20
(
minus_SNo
u12
)
=
u8
(proof)
Theorem
d70cc..
:
mul_SNo
u2
u12
=
u24
(proof)
Known
73189..
:
nat_p
u24
Theorem
7c521..
:
add_SNo
u24
(
minus_SNo
u20
)
=
u4
(proof)
Theorem
f7ea8..
:
∀ x0 x1 .
nat_p
x0
⟶
nat_p
x1
⟶
add_SNo
x0
x1
=
u12
⟶
add_SNo
x0
(
mul_SNo
2
x1
)
=
u20
⟶
and
(
x0
=
u4
)
(
x1
=
u8
)
(proof)
Known
mul_SNo_oneR
mul_SNo_oneR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
1
=
x0
Known
mul_SNo_com
mul_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
x0
x1
=
mul_SNo
x1
x0
Known
mul_nat_mul_SNo
mul_nat_mul_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_nat
x0
x1
=
mul_SNo
x0
x1
Known
neq_1_2
neq_1_2
:
1
=
2
⟶
∀ x0 : ο .
x0
Theorem
eeb21..
:
∀ x0 :
ι → ι
.
∀ x1 x2 .
nat_p
x1
⟶
nat_p
x2
⟶
(
∀ x3 .
x3
∈
u20
⟶
x0
x3
∈
u12
)
⟶
(
∀ x3 .
x3
∈
u12
⟶
or
(
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u1
)
(
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u2
)
)
⟶
equip
{x3 ∈
u12
|
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u1
}
x1
⟶
equip
{x3 ∈
u12
|
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u2
}
x2
⟶
and
(
x1
=
u4
)
(
x2
=
u8
)
(proof)
Definition
DirGraphOutNeighbors
:=
λ x0 .
λ x1 :
ι →
ι → ο
.
λ x2 .
{x3 ∈
x0
|
and
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
(
x1
x2
x3
)
}
Known
9c223..
equip_ordsucc_remove1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
equip
x0
(
ordsucc
x1
)
⟶
equip
(
setminus
x0
(
Sing
x2
)
)
x1
Known
cfabd..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x2
x3
⟶
x1
x3
x2
)
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
DirGraphOutNeighbors
x0
x1
x2
⟶
x2
∈
DirGraphOutNeighbors
x0
x1
x3
Known
b4538..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
equip
(
DirGraphOutNeighbors
u18
x0
x1
)
u5
Theorem
141e8..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
∀ x2 .
x2
∈
DirGraphOutNeighbors
u18
x0
x1
⟶
equip
(
setminus
(
DirGraphOutNeighbors
u18
x0
x2
)
(
Sing
x1
)
)
u4
(proof)
Theorem
36d6a..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
equip
(
lam
(
DirGraphOutNeighbors
u18
x0
x1
)
(
λ x2 .
setminus
(
DirGraphOutNeighbors
u18
x0
x2
)
(
Sing
x1
)
)
)
u20
(proof)
Theorem
4948f..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
equip
(
binunion
(
DirGraphOutNeighbors
u18
x0
x1
)
(
Sing
x1
)
)
u6
(proof)
Known
2c48a..
atleastp_antisym_equip
:
∀ x0 x1 .
atleastp
x0
x1
⟶
atleastp
x1
x0
⟶
equip
x0
x1
Known
48e0f..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
or
(
atleastp
x1
x0
)
(
atleastp
(
ordsucc
x0
)
x1
)
Known
86c65..
:
nat_p
u18
Known
1fe14..
:
∀ x0 x1 x2 x3 .
atleastp
x0
x2
⟶
atleastp
x1
x3
⟶
(
∀ x4 .
x4
∈
x2
⟶
nIn
x4
x3
)
⟶
atleastp
(
setsum
x0
x1
)
(
binunion
x2
x3
)
Known
setminusE2
setminusE2
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
nIn
x2
x1
Known
nat_17
nat_17
:
nat_p
17
Known
c558f..
:
∀ x0 x1 x2 x3 .
atleastp
x0
x2
⟶
atleastp
x1
x3
⟶
atleastp
(
binunion
x0
x1
)
(
setsum
x2
x3
)
Known
91a85..
:
add_nat
11
6
=
17
Known
binunion_Subq_min
binunion_Subq_min
:
∀ x0 x1 x2 .
x0
⊆
x2
⟶
x1
⊆
x2
⟶
binunion
x0
x1
⊆
x2
Known
Sep_Subq
Sep_Subq
:
∀ x0 .
∀ x1 :
ι → ο
.
Sep
x0
x1
⊆
x0
Theorem
05730..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
equip
(
setminus
u18
(
binunion
(
DirGraphOutNeighbors
u18
x0
x1
)
(
Sing
x1
)
)
)
u12
(proof)
Param
binintersect
binintersect
:
ι
→
ι
→
ι
Known
86f86..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
∀ x2 .
x2
∈
u18
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
not
(
x0
x1
x2
)
⟶
or
(
equip
(
binintersect
(
DirGraphOutNeighbors
u18
x0
x1
)
(
DirGraphOutNeighbors
u18
x0
x2
)
)
u1
)
(
equip
(
binintersect
(
DirGraphOutNeighbors
u18
x0
x1
)
(
DirGraphOutNeighbors
u18
x0
x2
)
)
u2
)
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
binintersectE
binintersectE
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
and
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
5169f..
equip_Sing_1
:
∀ x0 .
equip
(
Sing
x0
)
u1
Known
binintersectI
binintersectI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
x1
⟶
x2
∈
binintersect
x0
x1
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
ced33..
:
∀ x0 x1 .
(
x0
=
x1
⟶
∀ x2 : ο .
x2
)
⟶
equip
(
UPair
x0
x1
)
u2
Known
binintersectE2
binintersectE2
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x1
Known
binintersectE1
binintersectE1
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x0
Param
SetAdjoin
SetAdjoin
:
ι
→
ι
→
ι
Known
aa241..
:
∀ x0 x1 x2 .
∀ x3 :
ι → ο
.
x3
x0
⟶
x3
x1
⟶
x3
x2
⟶
∀ x4 .
x4
∈
SetAdjoin
(
UPair
x0
x1
)
x2
⟶
x3
x4
Known
a515c..
:
∀ x0 x1 x2 .
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
equip
(
SetAdjoin
(
UPair
x0
x1
)
x2
)
u3
Known
setminus_Subq
setminus_Subq
:
∀ x0 x1 .
setminus
x0
x1
⊆
x0
Theorem
51de2..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u3
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
x0
x2
x3
)
)
⟶
(
∀ x1 .
x1
⊆
u18
⟶
atleastp
u6
x1
⟶
not
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
x0
x2
x3
)
)
)
⟶
∀ x1 .
x1
∈
u18
⟶
and
(
equip
{x2 ∈
setminus
u18
(
binunion
(
DirGraphOutNeighbors
u18
x0
x1
)
(
Sing
x1
)
)
|
equip
(
binintersect
(
DirGraphOutNeighbors
u18
x0
x2
)
(
DirGraphOutNeighbors
u18
x0
x1
)
)
u1
}
u4
)
(
equip
{x2 ∈
setminus
u18
(
binunion
(
DirGraphOutNeighbors
u18
x0
x1
)
(
Sing
x1
)
)
|
equip
(
binintersect
(
DirGraphOutNeighbors
u18
x0
x2
)
(
DirGraphOutNeighbors
u18
x0
x1
)
)
u2
}
u8
)
(proof)