Search for blocks/addresses/...
Proofgold Asset
asset id
f2b6dc1d91c46566c22fe1c52e299865def383afd546fc35627790fa744ac357
asset hash
873b3b1b60f2761add38df8d78c69455acf9419f8a6754a97f93955e8a1503a4
bday / block
19851
tx
7ea05..
preasset
doc published by
Pr4zB..
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Param
u1
:
ι
Param
Sing
Sing
:
ι
→
ι
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Param
equip
equip
:
ι
→
ι
→
ο
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
Known
5169f..
equip_Sing_1
:
∀ x0 .
equip
(
Sing
x0
)
u1
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
Subq_atleastp
Subq_atleastp
:
∀ x0 x1 .
x0
⊆
x1
⟶
atleastp
x0
x1
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Theorem
04353..
:
∀ x0 x1 .
x1
∈
x0
⟶
atleastp
u1
x0
(proof)
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u2
:=
ordsucc
u1
Param
setminus
setminus
:
ι
→
ι
→
ι
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Param
binunion
binunion
:
ι
→
ι
→
ι
Known
eb0c4..
binunion_remove1_eq
:
∀ x0 x1 .
x1
∈
x0
⟶
x0
=
binunion
(
setminus
x0
(
Sing
x1
)
)
(
Sing
x1
)
Known
1dc5a..
:
∀ x0 x1 x2 .
nIn
x2
x1
⟶
atleastp
x0
x1
⟶
atleastp
(
ordsucc
x0
)
(
binunion
x1
(
Sing
x2
)
)
Known
setminus_nIn_I2
setminus_nIn_I2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
nIn
x2
(
setminus
x0
x1
)
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Theorem
ada03..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
atleastp
u2
x0
(proof)
Definition
u3
:=
ordsucc
u2
Theorem
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
(proof)
Definition
u4
:=
ordsucc
u3
Theorem
09d70..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
(
x1
=
x2
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
atleastp
u4
x0
(proof)
Definition
u5
:=
ordsucc
u4
Theorem
368c2..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
(
x1
=
x2
⟶
∀ x6 : ο .
x6
)
⟶
(
x1
=
x3
⟶
∀ x6 : ο .
x6
)
⟶
(
x2
=
x3
⟶
∀ x6 : ο .
x6
)
⟶
(
x1
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x2
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x3
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x1
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x2
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x3
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x4
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
atleastp
u5
x0
(proof)
Definition
u6
:=
ordsucc
u5
Theorem
2e3d8..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
(
x1
=
x2
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x3
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x3
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x4
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x4
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x5
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
atleastp
u6
x0
(proof)
Definition
u7
:=
ordsucc
u6
Theorem
19e0f..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
(
x1
=
x2
⟶
∀ x8 : ο .
x8
)
⟶
(
x1
=
x3
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x3
⟶
∀ x8 : ο .
x8
)
⟶
(
x1
=
x4
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x4
⟶
∀ x8 : ο .
x8
)
⟶
(
x3
=
x4
⟶
∀ x8 : ο .
x8
)
⟶
(
x1
=
x5
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x5
⟶
∀ x8 : ο .
x8
)
⟶
(
x3
=
x5
⟶
∀ x8 : ο .
x8
)
⟶
(
x4
=
x5
⟶
∀ x8 : ο .
x8
)
⟶
(
x1
=
x6
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x6
⟶
∀ x8 : ο .
x8
)
⟶
(
x3
=
x6
⟶
∀ x8 : ο .
x8
)
⟶
(
x4
=
x6
⟶
∀ x8 : ο .
x8
)
⟶
(
x5
=
x6
⟶
∀ x8 : ο .
x8
)
⟶
(
x1
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
(
x3
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
(
x4
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
(
x5
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
atleastp
u7
x0
(proof)
Definition
u8
:=
ordsucc
u7
Theorem
75f77..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
(
x1
=
x2
⟶
∀ x9 : ο .
x9
)
⟶
(
x1
=
x3
⟶
∀ x9 : ο .
x9
)
⟶
(
x2
=
x3
⟶
∀ x9 : ο .
x9
)
⟶
(
x1
=
x4
⟶
∀ x9 : ο .
x9
)
⟶
(
x2
=
x4
⟶
∀ x9 : ο .
x9
)
⟶
(
x3
=
x4
⟶
∀ x9 : ο .
x9
)
⟶
(
x1
=
x5
⟶
∀ x9 : ο .
x9
)
⟶
(
x2
=
x5
⟶
∀ x9 : ο .
x9
)
⟶
(
x3
=
x5
⟶
∀ x9 : ο .
x9
)
⟶
(
x4
=
x5
⟶
∀ x9 : ο .
x9
)
⟶
(
x1
=
x6
⟶
∀ x9 : ο .
x9
)
⟶
(
x2
=
x6
⟶
∀ x9 : ο .
x9
)
⟶
(
x3
=
x6
⟶
∀ x9 : ο .
x9
)
⟶
(
x4
=
x6
⟶
∀ x9 : ο .
x9
)
⟶
(
x5
=
x6
⟶
∀ x9 : ο .
x9
)
⟶
(
x1
=
x7
⟶
∀ x9 : ο .
x9
)
⟶
(
x2
=
x7
⟶
∀ x9 : ο .
x9
)
⟶
(
x3
=
x7
⟶
∀ x9 : ο .
x9
)
⟶
(
x4
=
x7
⟶
∀ x9 : ο .
x9
)
⟶
(
x5
=
x7
⟶
∀ x9 : ο .
x9
)
⟶
(
x6
=
x7
⟶
∀ x9 : ο .
x9
)
⟶
(
x1
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
(
x2
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
(
x3
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
(
x4
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
(
x5
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
(
x6
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
(
x7
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
atleastp
u8
x0
(proof)
Definition
u9
:=
ordsucc
u8
Theorem
04f57..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
(
x1
=
x2
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x3
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x3
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x4
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x4
⟶
∀ x10 : ο .
x10
)
⟶
(
x3
=
x4
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x5
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x5
⟶
∀ x10 : ο .
x10
)
⟶
(
x3
=
x5
⟶
∀ x10 : ο .
x10
)
⟶
(
x4
=
x5
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x3
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x4
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x5
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
x3
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
x4
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
x5
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
x6
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x3
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x4
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x5
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x6
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x7
=
x8
⟶
∀ x10 : ο .
x10
)
⟶
(
x1
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x2
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x3
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x4
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x5
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x6
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x7
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
(
x8
=
x9
⟶
∀ x10 : ο .
x10
)
⟶
atleastp
u9
x0
(proof)
Definition
u10
:=
ordsucc
u9
Theorem
d140d..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
(
x1
=
x2
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x3
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x3
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x4
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x4
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x4
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x7
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x7
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x8
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x7
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x8
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x9
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
atleastp
u10
x0
(proof)
Definition
u11
:=
ordsucc
u10
Theorem
09f2a..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
(
x1
=
x2
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x3
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x3
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x4
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x4
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x4
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x5
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x5
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x5
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x5
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x6
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x6
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x6
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x6
⟶
∀ x12 : ο .
x12
)
⟶
(
x5
=
x6
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x7
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x7
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x7
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x7
⟶
∀ x12 : ο .
x12
)
⟶
(
x5
=
x7
⟶
∀ x12 : ο .
x12
)
⟶
(
x6
=
x7
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x5
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x6
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x7
=
x8
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x5
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x6
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x7
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x8
=
x9
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x5
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x6
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x7
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x8
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x9
=
x10
⟶
∀ x12 : ο .
x12
)
⟶
(
x1
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x2
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x3
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x4
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x5
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x6
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x7
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x8
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x9
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
(
x10
=
x11
⟶
∀ x12 : ο .
x12
)
⟶
atleastp
u11
x0
(proof)
Definition
u12
:=
ordsucc
u11
Theorem
8d9d9..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
(
x1
=
x2
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x3
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x3
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x4
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x4
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x4
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x5
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x5
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x5
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x5
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x6
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x6
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x6
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x6
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x6
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x7
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x7
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x7
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x7
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x7
⟶
∀ x13 : ο .
x13
)
⟶
(
x6
=
x7
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x6
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x7
=
x8
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x6
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x7
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x8
=
x9
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x6
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x7
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x8
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x9
=
x10
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x6
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x7
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x8
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x9
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x10
=
x11
⟶
∀ x13 : ο .
x13
)
⟶
(
x1
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x2
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x3
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x4
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x5
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x6
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x7
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x8
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x9
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x10
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
(
x11
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
atleastp
u12
x0
(proof)
Definition
u13
:=
ordsucc
u12
Theorem
6fc5a..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
(
x1
=
x2
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x3
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x3
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x4
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x4
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x4
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x5
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x5
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x5
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x5
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x6
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x6
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x6
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x6
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x6
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x7
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x7
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x7
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x7
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x7
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x7
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x7
=
x8
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x7
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x8
=
x9
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x7
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x8
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x9
=
x10
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x7
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x8
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x9
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x10
=
x11
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x7
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x8
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x9
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x10
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x11
=
x12
⟶
∀ x14 : ο .
x14
)
⟶
(
x1
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x2
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x3
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x4
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x5
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x6
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x7
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x8
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x9
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x10
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x11
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
(
x12
=
x13
⟶
∀ x14 : ο .
x14
)
⟶
atleastp
u13
x0
(proof)
Definition
u14
:=
ordsucc
u13
Theorem
1565e..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
(
x1
=
x2
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x3
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x3
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x4
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x4
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x4
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x5
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x5
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x5
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x5
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x6
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x6
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x6
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x6
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x6
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x7
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x7
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x7
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x7
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x7
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x7
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x8
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x8
=
x9
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x8
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x9
=
x10
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x8
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x9
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x10
=
x11
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x8
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x9
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x10
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x11
=
x12
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x8
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x9
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x10
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x11
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x12
=
x13
⟶
∀ x15 : ο .
x15
)
⟶
(
x1
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x2
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x3
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x4
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x5
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x6
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x7
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x8
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x9
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x10
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x11
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x12
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
(
x13
=
x14
⟶
∀ x15 : ο .
x15
)
⟶
atleastp
u14
x0
(proof)
Definition
u15
:=
ordsucc
u14
Theorem
1fbf0..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
(
x1
=
x2
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x3
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x3
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x4
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x4
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x4
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x5
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x5
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x5
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x5
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x6
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x6
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x6
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x6
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x6
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x7
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x7
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x7
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x7
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x7
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x7
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x8
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x9
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x9
=
x10
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x9
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x10
=
x11
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x9
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x10
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x11
=
x12
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x9
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x10
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x11
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x12
=
x13
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x9
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x10
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x11
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x12
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x13
=
x14
⟶
∀ x16 : ο .
x16
)
⟶
(
x1
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x2
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x3
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x4
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x5
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x6
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x7
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x8
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x9
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x10
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x11
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x12
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x13
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
(
x14
=
x15
⟶
∀ x16 : ο .
x16
)
⟶
atleastp
u15
x0
(proof)
Definition
u16
:=
ordsucc
u15
Theorem
24b48..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
∀ x16 .
x16
∈
x0
⟶
(
x1
=
x2
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x3
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x3
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x4
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x4
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x4
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x5
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x5
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x5
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x5
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x6
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x6
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x6
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x6
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x6
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x7
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x7
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x7
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x7
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x7
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x7
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x8
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x9
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x10
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x10
=
x11
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x10
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x11
=
x12
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x10
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x11
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x12
=
x13
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x10
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x11
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x12
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x13
=
x14
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x10
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x11
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x12
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x13
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x14
=
x15
⟶
∀ x17 : ο .
x17
)
⟶
(
x1
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x2
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x3
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x4
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x5
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x6
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x7
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x8
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x9
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x10
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x11
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x12
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x13
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x14
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
(
x15
=
x16
⟶
∀ x17 : ο .
x17
)
⟶
atleastp
u16
x0
(proof)
Definition
u17
:=
ordsucc
u16
Theorem
9efa7..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
∀ x16 .
x16
∈
x0
⟶
∀ x17 .
x17
∈
x0
⟶
(
x1
=
x2
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x3
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x3
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x4
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x4
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x4
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x5
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x5
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x5
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x5
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x6
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x6
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x6
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x6
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x6
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x7
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x7
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x7
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x7
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x7
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x7
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x8
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x9
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x10
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x11
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x11
=
x12
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x11
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x12
=
x13
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x11
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x12
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x13
=
x14
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x11
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x12
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x13
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x14
=
x15
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x11
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x12
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x13
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x14
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x15
=
x16
⟶
∀ x18 : ο .
x18
)
⟶
(
x1
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x2
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x3
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x4
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x5
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x6
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x7
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x8
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x9
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x10
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x11
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x12
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x13
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x14
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x15
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
(
x16
=
x17
⟶
∀ x18 : ο .
x18
)
⟶
atleastp
u17
x0
(proof)
Definition
u18
:=
ordsucc
u17
Theorem
74326..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
∀ x16 .
x16
∈
x0
⟶
∀ x17 .
x17
∈
x0
⟶
∀ x18 .
x18
∈
x0
⟶
(
x1
=
x2
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x3
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x3
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x4
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x4
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x4
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x5
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x5
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x5
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x5
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x6
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x6
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x6
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x6
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x6
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x7
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x7
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x7
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x7
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x7
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x7
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x8
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x9
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x10
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x11
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x12
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x12
=
x13
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x12
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x13
=
x14
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x12
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x13
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x14
=
x15
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x12
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x13
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x14
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x15
=
x16
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x12
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x13
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x14
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x15
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x16
=
x17
⟶
∀ x19 : ο .
x19
)
⟶
(
x1
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x2
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x3
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x4
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x5
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x6
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x7
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x8
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x9
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x10
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x11
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x12
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x13
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x14
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x15
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x16
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
(
x17
=
x18
⟶
∀ x19 : ο .
x19
)
⟶
atleastp
u18
x0
(proof)
Definition
u19
:=
ordsucc
u18
Theorem
8ca1e..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
∀ x16 .
x16
∈
x0
⟶
∀ x17 .
x17
∈
x0
⟶
∀ x18 .
x18
∈
x0
⟶
∀ x19 .
x19
∈
x0
⟶
(
x1
=
x2
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x3
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x3
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x4
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x4
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x4
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x5
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x5
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x5
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x5
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x6
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x6
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x6
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x6
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x6
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x7
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x7
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x7
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x7
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x7
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x7
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x8
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x9
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x10
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x11
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x12
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x13
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x13
=
x14
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x13
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x14
=
x15
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x13
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x14
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x15
=
x16
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x13
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x14
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x15
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x16
=
x17
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x13
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x14
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x15
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x16
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x17
=
x18
⟶
∀ x20 : ο .
x20
)
⟶
(
x1
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x2
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x3
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x4
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x5
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x6
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x7
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x8
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x9
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x10
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x11
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x12
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x13
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x14
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x15
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x16
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x17
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
(
x18
=
x19
⟶
∀ x20 : ο .
x20
)
⟶
atleastp
u19
x0
(proof)
Definition
u20
:=
ordsucc
u19
Theorem
f67f7..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
∀ x16 .
x16
∈
x0
⟶
∀ x17 .
x17
∈
x0
⟶
∀ x18 .
x18
∈
x0
⟶
∀ x19 .
x19
∈
x0
⟶
∀ x20 .
x20
∈
x0
⟶
(
x1
=
x2
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x3
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x3
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x4
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x4
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x4
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x5
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x5
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x5
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x5
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x6
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x6
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x6
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x6
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x6
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x7
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x7
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x7
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x7
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x7
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x7
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x8
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x9
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x10
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x11
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x12
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x13
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x14
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x14
=
x15
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x14
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x15
=
x16
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x14
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x15
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x16
=
x17
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x14
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x15
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x16
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x17
=
x18
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x14
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x15
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x16
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x17
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x18
=
x19
⟶
∀ x21 : ο .
x21
)
⟶
(
x1
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x2
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x3
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x4
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x5
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x6
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x7
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x8
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x9
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x10
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x11
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x12
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x13
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x14
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x15
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x16
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x17
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x18
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
(
x19
=
x20
⟶
∀ x21 : ο .
x21
)
⟶
atleastp
u20
x0
(proof)
Definition
u21
:=
ordsucc
u20
Theorem
084ef..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
∀ x15 .
x15
∈
x0
⟶
∀ x16 .
x16
∈
x0
⟶
∀ x17 .
x17
∈
x0
⟶
∀ x18 .
x18
∈
x0
⟶
∀ x19 .
x19
∈
x0
⟶
∀ x20 .
x20
∈
x0
⟶
∀ x21 .
x21
∈
x0
⟶
(
x1
=
x2
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x3
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x3
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x4
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x4
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x4
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x5
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x5
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x5
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x5
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x6
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x6
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x6
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x6
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x6
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x7
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x7
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x7
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x7
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x7
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x7
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x8
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x9
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x10
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x11
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x12
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x13
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x14
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x14
=
x15
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x14
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x15
=
x16
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x14
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x15
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x16
=
x17
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x14
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x15
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x16
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x17
=
x18
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x14
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x15
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x16
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x17
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x18
=
x19
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x12
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x13
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x14
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x15
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x16
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x17
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x18
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x19
=
x20
⟶
∀ x22 : ο .
x22
)
⟶
(
x1
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x2
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x3
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x4
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x5
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x6
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x7
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x8
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x9
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x10
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(
x11
=
x21
⟶
∀ x22 : ο .
x22
)
⟶
(