Beginning of Section
Random2
Variable
p :
set
→
prop
Variable
f :
set
→
set
Theorem.
(
conj_Random2_TMWv3SVbM3eZ31azmqFc5rufdMCwpaCexpQ
)
∀X2
⊆
f
(
f
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
,
(
(
∃X3 ∈
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
,
∃X4 :
set
,
atleast5
X4
)
∧
(
(
∀X3
⊆
X2
,
(
(
¬
atleast5
X3
)
∧
(
(
¬
atleast6
(
f
X3
)
)
→
(
¬
p
X3
)
)
)
)
→
(
∀X3
∈
X2
,
∀X4
⊆
∅
,
(
(
(
(
¬
atleast4
X4
)
∧
(
¬
p
(
ordsucc
X2
)
)
)
→
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
→
(
(
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
→
atleast3
∅
)
→
(
¬
equip
X4
X4
)
→
(
(
(
¬
p
∅
)
→
(
p
X4
∧
exactly3
X3
)
)
∧
(
(
(
¬
set_of_pairs
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
(
(
(
p
X3
→
(
(
(
¬
p
∅
)
→
(
(
¬
exactly4
X2
)
∧
(
(
p
(
f
∅
)
∧
(
¬
p
X2
)
)
∧
per_i
(
λX5 :
set
⇒
λX6 :
set
⇒
setsum_p
X3
)
)
)
)
∧
(
¬
p
X3
)
)
→
(
¬
p
X4
)
)
∧
(
(
symmetric_i
(
λX5 :
set
⇒
λX6 :
set
⇒
p
X6
→
(
¬
p
(
𝒫
X6
)
)
)
∧
ordinal
∅
)
→
(
¬
atleast6
X4
)
)
)
∧
atleast5
X3
)
→
(
¬
p
X4
)
→
(
exactly5
X2
→
(
(
¬
SNo
(
⋃
(
f
X3
)
)
)
∧
atleast5
X4
)
)
→
p
X3
)
→
(
(
¬
eqreln_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
SNoLt
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
X5
→
(
(
(
SNo
X5
∧
(
(
(
¬
p
X6
)
→
totalorder_i
(
λX7 :
set
⇒
λX8 :
set
⇒
exactly5
X8
)
→
p
∅
)
→
(
(
(
¬
p
∅
)
→
(
¬
ordinal
X5
)
)
∧
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
→
exactly2
X5
)
)
)
)
→
(
(
(
p
X6
→
(
¬
exactly5
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
→
(
¬
p
X5
)
)
∧
(
(
¬
exactly5
X2
)
→
(
(
(
¬
p
X5
)
∧
(
p
X5
→
(
(
(
¬
p
X6
)
∧
p
X6
)
∧
(
(
¬
setsum_p
(
f
X6
)
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
∧
PNo_downc
(
λX7 :
set
⇒
λX8 :
set
→
prop
⇒
(
(
(
¬
exactly2
X6
)
∧
(
(
¬
set_of_pairs
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
X8
(
f
X6
)
)
)
∧
(
¬
X8
∅
)
)
→
(
(
¬
p
X7
)
∧
(
atleast5
X4
∧
X8
(
f
(
ordsucc
X7
)
)
)
)
)
X4
(
λX7 :
set
⇒
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
(
¬
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
(
exactly5
X5
∧
(
(
(
p
X6
→
(
¬
p
(
f
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
X4
∈
If_i
(
exactly4
X3
∧
(
(
p
X5
∧
(
∅
∈
Sing
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
reflexive_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
exactly3
X7
∧
(
¬
atleast6
X8
)
)
)
)
)
X5
X2
)
)
∧
(
¬
p
X6
)
)
)
∧
(
(
p
X5
→
(
¬
p
X5
)
)
→
exactly5
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
)
)
∧
SNo_
(
f
X3
)
X6
)
)
)
∧
(
(
(
¬
p
X4
)
→
(
¬
p
X2
)
)
∧
(
(
(
(
(
(
(
exactly3
X3
∧
TransSet
(
f
(
f
(
f
X4
)
)
)
)
∧
atleast6
X3
)
→
(
¬
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
→
atleast4
X3
→
(
¬
exactly3
(
ap
X4
∅
)
)
)
∧
(
(
¬
p
(
f
X3
)
)
∧
atleast2
X2
)
)
→
(
(
¬
atleast4
X3
)
∧
exactly4
X3
)
)
→
(
(
(
nat_p
X3
→
(
(
(
¬
p
X3
)
→
(
(
(
¬
atleast4
∅
)
∧
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
→
(
(
¬
exactly4
(
f
X3
)
)
∧
PNoLe
(
proj1
X3
)
(
λX5 :
set
⇒
(
(
(
(
¬
p
X5
)
∧
atleast4
∅
)
∧
(
(
(
¬
p
X4
)
→
(
¬
nat_p
X4
)
)
∧
(
(
¬
p
X4
)
→
(
¬
p
∅
)
)
)
)
→
(
(
¬
p
(
f
X3
)
)
∧
(
¬
atleast2
X4
)
)
)
→
p
(
ordsucc
X3
)
→
(
¬
TransSet
X3
)
)
X4
(
λX5 :
set
⇒
(
(
¬
p
X4
)
∧
(
p
X3
∧
(
(
¬
nat_p
X2
)
∧
atleast2
(
Inj0
∅
)
)
)
)
)
)
)
)
∧
(
(
(
¬
atleast4
X4
)
∧
(
(
¬
p
X3
)
→
(
(
TransSet
X3
∧
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
∧
(
(
(
(
¬
p
X4
)
→
exactly4
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
→
atleast3
X3
)
∧
(
¬
p
X2
)
)
)
)
)
→
exactly2
X3
→
(
(
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
→
(
p
(
UPair
X4
X3
)
∧
(
(
¬
SNoLe
X4
X4
)
→
(
¬
exactly3
X4
)
)
)
)
∧
(
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
∧
set_of_pairs
X3
)
)
)
)
)
∧
(
¬
p
X3
)
)
→
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
p
X3
)
∧
(
atleast6
X4
∧
(
(
(
¬
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
(
¬
nat_p
X5
)
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
(
(
¬
set_of_pairs
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
nat_p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
)
∧
(
p
X4
→
(
¬
p
X3
)
)
)
→
(
¬
p
X4
)
)
)
)
)
)
)
)
→
(
p
(
f
X3
)
∧
(
¬
p
X4
)
)
→
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
¬
nat_p
X4
)
→
nat_p
X4
)
)
)
→
(
p
(
f
X3
)
∧
(
(
¬
exactly4
X3
)
∧
(
¬
p
(
f
(
f
X3
)
)
)
)
)
)
→
(
¬
atleast6
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
→
(
¬
exactly3
(
f
X4
)
)
)
∧
(
¬
p
X2
)
)
→
(
¬
atleast2
∅
)
→
p
X4
)
)
)
In Proofgold the corresponding term root is
56d077...
and proposition id is
3af7c9...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMPfGfGzourdwkEihmiHC8moc9ao7wdjb8m
)
∃X2 :
set
,
(
(
(
(
∃X3 :
set
,
(
(
X3
⊆
Unj
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
∀X4 :
set
,
p
X3
→
(
exactly4
X4
∧
(
(
(
¬
atleast5
(
f
(
f
X4
)
)
)
∧
(
p
X3
→
p
X3
→
(
¬
p
(
f
X3
)
)
)
)
∧
(
p
X4
→
(
(
(
(
(
(
¬
atleast4
(
ap
X3
(
f
X4
)
)
)
→
(
¬
p
X4
)
→
(
(
(
(
(
¬
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
atleast4
(
Inj0
X3
)
)
∧
atleast4
X3
)
∧
TransSet
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
atleast3
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
atleast2
X4
)
→
(
¬
atleast4
X3
)
→
SNo_
X4
X3
)
→
(
¬
atleast5
X3
)
→
(
(
(
¬
p
(
f
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
PNoLt
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
(
λX5 :
set
⇒
(
(
(
¬
SNoLe
X4
X5
)
→
(
¬
p
X2
)
)
∧
p
∅
)
)
X2
(
λX5 :
set
⇒
setsum_p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
exactly3
X4
)
)
∧
nat_p
X2
)
)
→
atleast6
X3
)
→
(
p
X3
∧
(
¬
ordinal
X3
)
)
)
)
)
)
)
)
∧
(
¬
tuple_p
(
f
X2
)
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
(
∀X3 :
set
,
(
(
(
¬
p
X2
)
∧
(
∀X4 :
set
,
(
(
PNo_downc
(
λX5 :
set
⇒
λX6 :
set
→
prop
⇒
(
(
(
(
(
(
equip
∅
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
∧
atleast5
X5
)
∧
(
(
(
(
¬
p
(
f
X3
)
)
∧
(
¬
exactly2
X4
)
)
∧
X6
X5
)
∧
(
(
(
X6
X4
∧
(
¬
p
X4
)
)
→
(
(
X6
X2
∧
(
(
(
exactly2
X3
→
atleast2
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
(
(
(
(
¬
TransSet
∅
)
∧
(
PNoLt
X5
(
λX7 :
set
⇒
TransSet
∅
→
p
X5
)
X5
(
λX7 :
set
⇒
exactly3
X4
)
∧
X6
X4
)
)
∧
(
atleast4
X5
∧
(
(
¬
p
∅
)
→
p
X3
)
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
X6
X5
)
)
∧
(
atleast2
X3
→
(
¬
p
X5
)
)
)
)
∧
atleast5
X4
)
)
→
(
¬
X6
∅
)
)
)
)
→
exactly4
X5
)
∧
(
(
p
X5
∧
(
¬
atleast2
X3
)
)
→
(
¬
ordinal
X4
)
)
)
∧
p
X3
)
∧
X6
X3
)
→
X6
X4
)
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
λX5 :
set
⇒
TransSet
X2
)
→
(
¬
atleast4
X4
)
)
∧
(
(
(
¬
p
(
f
X4
)
)
∧
(
(
¬
p
X3
)
∧
(
¬
SNo
(
f
∅
)
)
)
)
∧
(
¬
p
X4
)
)
)
→
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
(
¬
p
X3
)
∧
(
p
(
f
X4
)
→
(
(
(
(
¬
p
X3
)
→
(
p
X4
∧
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
exactly5
∅
)
)
)
)
→
nat_p
X4
)
→
(
p
X4
∧
(
(
(
(
p
X4
→
atleast4
(
f
(
binunion
X4
X2
)
)
→
p
X4
)
→
(
¬
p
X3
)
)
∧
(
(
p
X4
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
(
(
(
¬
atleast6
X3
)
→
(
(
(
(
(
(
¬
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
→
p
(
f
∅
)
→
(
(
¬
p
X3
)
∧
(
(
(
p
X4
∧
(
ordinal
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
→
(
(
p
X4
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
set_of_pairs
X3
→
(
¬
p
∅
)
)
∧
(
¬
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
→
(
setsum_p
X4
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
(
¬
p
X3
)
)
)
)
∧
(
(
p
X3
∧
(
p
∅
∧
(
¬
p
∅
)
)
)
→
p
(
f
X3
)
)
)
→
(
¬
setsum_p
X2
)
)
→
p
X4
)
→
exactly4
X4
)
→
(
(
(
(
¬
(
X4
⊆
X3
)
)
→
(
p
X3
→
atleast3
(
f
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
→
(
PNoEq_
X4
(
λX5 :
set
⇒
exactly4
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
(
λX5 :
set
⇒
(
p
X5
∧
p
X4
)
→
reflexive_i
(
λX6 :
set
⇒
λX7 :
set
⇒
exactly4
(
Unj
X7
)
)
)
∧
(
(
eqreln_i
(
λX5 :
set
⇒
λX6 :
set
⇒
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
(
exactly4
X4
→
atleast6
(
f
X2
)
)
)
∧
(
¬
atleast3
X2
)
)
)
)
∧
(
(
(
p
X3
∧
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
X4
)
)
→
(
(
¬
set_of_pairs
X4
)
∧
(
TransSet
X2
∧
(
(
¬
nat_p
(
f
(
f
∅
)
)
)
→
setsum_p
X4
)
)
)
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
→
(
¬
p
X3
)
→
(
(
(
(
(
(
(
(
atleast5
X3
→
(
¬
p
X2
)
→
(
¬
nat_p
X3
)
)
∧
(
(
(
(
¬
atleast3
X3
)
∧
(
exactly2
X3
→
(
(
(
exactly5
∅
→
(
(
(
(
¬
atleast3
X3
)
∧
(
¬
p
X3
)
)
∧
(
(
¬
exactly2
X4
)
→
(
¬
atleast2
X4
)
)
)
∧
p
X4
)
)
→
p
X4
)
→
p
X4
)
→
(
p
X4
∧
(
¬
TransSet
X4
)
)
)
)
→
p
X3
)
→
exactly4
X3
)
)
∧
p
X3
)
→
(
¬
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
→
(
p
X4
→
exactly4
X2
)
→
(
¬
SNoLt
X2
X3
)
)
∧
(
p
(
f
(
f
X3
)
)
→
(
¬
p
∅
)
)
)
∧
(
¬
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
atleast2
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
→
(
p
X3
∧
(
¬
p
X3
)
)
)
)
)
∧
exactly2
X3
)
)
)
→
p
X2
→
(
atleast3
X4
∧
exactly2
X2
)
)
)
)
→
(
p
X4
∧
exactly2
X2
)
→
atleast3
X4
)
)
)
)
→
(
∃X4 ∈
X3
,
TransSet
(
f
X4
)
)
)
→
(
p
(
binrep
X2
X3
)
∧
(
¬
exactly4
X2
)
)
)
→
(
∃X3 :
set
,
(
(
X3
⊆
f
X2
)
∧
(
∃X4 :
set
,
(
(
X4
⊆
X3
)
∧
(
(
(
(
(
¬
p
X4
)
→
(
(
¬
p
(
binunion
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
X3
)
)
→
(
(
(
(
(
(
(
¬
atleast4
∅
)
→
exactly3
X4
→
(
(
(
(
(
atleast5
X3
∧
(
(
¬
tuple_p
X2
X4
)
→
p
(
f
X4
)
)
)
∧
(
¬
exactly4
X4
)
)
∧
p
X2
)
∧
(
(
p
X4
∧
(
(
¬
p
X4
)
→
(
¬
p
X3
)
)
)
→
(
(
p
X4
∧
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
∧
(
(
¬
p
X2
)
→
(
(
¬
exactly2
X3
)
∧
nat_p
X3
)
)
)
)
∧
(
¬
atleast4
(
f
X3
)
)
)
)
)
∧
p
X2
)
)
∧
p
X4
)
→
(
(
¬
p
(
setexp
(
f
X2
)
∅
)
)
∧
(
¬
atleast4
(
ReplSep
X2
(
λX5 :
set
⇒
(
(
¬
p
X4
)
∧
atleast5
X4
)
)
(
λX5 :
set
⇒
X5
)
)
)
)
→
(
(
p
X4
∧
(
nat_p
X3
→
(
¬
p
X4
)
)
)
∧
(
(
¬
p
X4
)
→
(
(
(
¬
p
X2
)
→
(
(
¬
set_of_pairs
X3
)
→
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
p
(
⋃
X4
)
)
∧
(
¬
p
X4
)
)
)
)
)
∧
(
¬
TransSet
X3
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
¬
p
X3
)
→
(
(
(
(
f
∅
∈
X4
)
→
(
¬
exactly2
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
→
p
(
f
X2
)
→
(
(
(
(
nat_p
X4
∧
(
(
(
(
¬
setsum_p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
∧
exactly4
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
¬
exactly3
X3
)
)
∧
p
X3
)
)
∧
(
(
¬
SNo
X3
)
∧
(
(
(
p
X2
→
(
¬
atleast3
X3
)
)
→
set_of_pairs
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
¬
p
(
Sing
X3
)
)
)
)
)
→
p
X3
→
(
¬
trichotomous_or_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
atleast6
X6
∧
(
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∧
exactly3
X5
)
)
∧
p
X6
)
)
)
)
∧
(
¬
(
f
X4
∈
X4
)
)
)
)
→
exactly5
∅
)
∧
(
¬
set_of_pairs
X4
)
)
)
∧
(
(
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∧
(
¬
p
(
f
X4
)
)
)
→
(
¬
p
X3
)
)
)
)
)
→
(
TransSet
X4
∧
(
(
¬
p
X4
)
∧
(
¬
p
X4
)
)
)
)
∧
(
(
(
¬
PNo_upc
(
λX5 :
set
⇒
λX6 :
set
→
prop
⇒
(
(
(
(
(
X6
X4
→
(
¬
p
(
f
X5
)
)
)
→
X6
X4
)
∧
exactly4
X3
)
∧
(
(
¬
exactly5
X5
)
→
(
¬
p
X2
)
)
)
∧
(
¬
X6
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
X4
(
λX5 :
set
⇒
(
(
¬
p
X4
)
∧
(
p
∅
∧
p
X3
)
)
)
)
∧
(
(
p
∅
→
atleastp
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
(
f
X3
)
)
→
(
¬
SNo
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
)
→
p
X2
)
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
∧
atleast6
X3
)
)
)
)
)
)
∧
(
∀X3 :
set
,
(
¬
SNo
(
f
(
f
∅
)
)
)
→
(
¬
(
X3
∈
X3
)
)
)
)
In Proofgold the corresponding term root is
4774cd...
and proposition id is
4c34b1...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TML9chQ7pBnmLnJnGW5vSgHh8BXUM622Aqi
)
(
(
(
∃X2 :
set
,
(
TransSet
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∧
(
(
∀X3 :
set
,
(
∃X4 :
set
,
(
(
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
(
(
¬
p
X3
)
→
p
X3
)
∧
p
X4
)
∧
(
(
¬
atleast2
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
→
(
¬
atleast4
X3
)
)
)
∧
(
(
(
(
(
¬
exactly3
(
f
X4
)
)
∧
(
¬
p
X4
)
)
→
p
X3
→
(
(
(
(
¬
p
∅
)
∧
(
¬
p
X3
)
)
→
(
p
X4
→
(
¬
p
X4
)
)
→
atleast3
X3
→
TransSet
(
f
X2
)
)
→
(
(
¬
p
X4
)
∧
(
(
¬
p
(
UPair
(
If_i
(
(
¬
p
(
f
X2
)
)
→
nat_p
∅
)
X2
(
f
(
f
∅
)
)
)
X3
)
)
→
(
¬
exactly5
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
)
→
p
X3
)
∧
(
p
X3
→
(
(
¬
p
X3
)
∧
(
(
(
(
(
(
(
¬
p
(
f
∅
)
)
→
p
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
p
X4
)
∧
atleast4
X2
)
→
p
X2
)
)
)
)
→
(
(
(
¬
atleast3
X4
)
∧
(
(
exactly2
X3
∧
(
(
(
(
¬
exactly5
∅
)
→
p
X3
)
∧
(
¬
atleast4
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
¬
atleast4
X4
)
)
)
→
(
¬
p
X3
)
)
)
∧
exactly4
X3
)
)
)
)
→
(
(
¬
p
X4
)
∧
setsum_p
X3
)
)
∧
(
¬
p
X4
)
)
)
→
exactly3
(
f
(
f
X3
)
)
)
∧
(
∃X3 :
set
,
(
∀X4 :
set
,
(
(
(
atleast3
X4
∧
p
X4
)
→
setsum_p
X3
→
atleast3
X3
)
∧
atleast4
(
𝒫
X4
)
)
→
(
(
¬
p
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
¬
exactly5
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
¬
p
(
ordsucc
X3
)
)
→
(
(
¬
atleast2
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
p
(
f
(
Pi
X4
(
λX5 :
set
⇒
proj0
(
Inj0
X4
)
)
)
)
∧
(
¬
ordinal
X4
)
)
∧
(
(
(
(
¬
SNo
(
f
(
f
(
f
X3
)
)
)
)
→
(
(
(
(
(
¬
(
X3
=
X2
)
)
→
(
(
(
(
¬
p
X2
)
∧
(
¬
atleast4
(
lam
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
λX5 :
set
⇒
X5
)
)
)
)
→
(
¬
p
(
ReplSep
(
Inj1
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
(
λX5 :
set
⇒
TransSet
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
(
λX5 :
set
⇒
X2
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
∧
p
X4
)
→
(
(
(
p
(
f
X2
)
→
atleast6
X3
)
∧
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∧
p
(
binunion
(
Sing
∅
)
X3
)
)
∧
SNo
(
SNoLev
∅
)
)
)
→
exactly4
(
f
X4
)
→
PNoLt
X3
(
λX5 :
set
⇒
(
exactly4
X5
∧
atleast4
∅
)
)
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
λX5 :
set
⇒
(
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∧
(
(
(
¬
p
(
f
X3
)
)
→
SNo
X3
)
∧
(
¬
atleast2
X5
)
)
)
→
(
¬
p
X3
)
)
)
∧
(
(
(
SNo
X3
→
(
(
(
p
X3
→
TransSet
X3
→
p
X3
→
(
(
¬
p
X2
)
∧
(
¬
exactly5
(
f
X2
)
)
)
)
→
(
¬
exactly5
X3
)
)
∧
(
exactly5
X2
∧
(
(
¬
setsum_p
X3
)
→
(
(
(
¬
setsum_p
X4
)
∧
(
¬
(
∅
=
X2
)
)
)
∧
p
X4
)
)
)
)
)
→
(
¬
ordinal
X4
)
)
∧
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
atleast6
X3
)
)
)
)
→
(
¬
p
X2
)
→
(
(
(
¬
p
(
𝒫
X3
)
)
∧
(
(
p
X3
→
ordinal
X3
)
∧
(
(
p
X4
→
(
equip
X2
X4
→
(
¬
p
(
ordsucc
X3
)
)
)
→
(
(
¬
p
X3
)
∧
(
X3
⊆
X4
)
)
)
→
(
¬
atleast4
(
SetAdjoin
X3
X2
)
)
)
)
)
→
(
(
(
¬
p
X3
)
∧
(
¬
p
X2
)
)
∧
(
(
(
(
¬
atleast6
X4
)
→
(
¬
p
X4
)
→
(
(
¬
nat_p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
p
X2
)
)
→
(
¬
exactly3
(
f
(
f
X4
)
)
)
)
→
(
X3
∈
X4
)
)
)
)
→
TransSet
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
atleast2
X3
)
)
)
→
(
(
p
X3
∧
(
(
¬
atleast2
(
Inj1
X3
)
)
∧
(
(
(
(
(
(
¬
atleast3
X4
)
∧
(
p
∅
∧
(
¬
p
X3
)
)
)
→
PNo_downc
(
λX5 :
set
⇒
λX6 :
set
→
prop
⇒
(
atleast6
X4
∧
(
¬
exactly5
X3
)
)
)
X3
(
λX5 :
set
⇒
(
(
¬
p
X3
)
∧
(
¬
p
X3
)
)
)
)
∧
(
(
(
exactly4
X4
→
(
(
setsum_p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
∧
p
(
f
X4
)
)
→
(
atleast4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
∧
(
atleast5
X4
∧
(
¬
p
∅
)
)
)
)
→
(
(
p
X3
→
(
¬
irreflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
(
(
¬
p
X3
)
→
(
(
(
(
¬
p
X5
)
∧
atleast6
X5
)
→
(
(
(
¬
p
X5
)
∧
(
X4
∈
X5
)
)
∧
(
PNoLt
X4
(
λX7 :
set
⇒
(
¬
p
(
f
(
f
X7
)
)
)
)
X5
(
λX7 :
set
⇒
(
¬
p
∅
)
)
∧
(
¬
p
X6
)
)
)
→
(
(
(
¬
exactly4
X5
)
→
(
¬
p
X3
)
)
∧
(
(
(
(
¬
p
X5
)
→
(
p
X5
∧
(
¬
atleast5
X5
)
)
→
SNo_
X5
X2
→
p
X5
)
∧
(
¬
set_of_pairs
X5
)
)
→
equip
X5
X6
)
)
)
→
(
¬
p
X3
)
)
→
(
¬
p
X5
)
→
p
X5
)
→
(
¬
SNo
X6
)
→
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
=
X6
)
)
→
exactly2
X4
)
→
p
X5
)
)
)
∧
(
p
X2
→
(
¬
atleast5
X2
)
)
)
)
→
p
∅
)
∧
p
X4
)
)
→
(
¬
p
X4
)
)
∧
(
¬
exactly4
(
binunion
X4
X3
)
)
)
)
)
∧
p
X3
)
)
)
)
)
)
)
→
p
X3
)
)
)
)
→
(
(
(
(
∃X2 :
set
,
(
(
∀X3 :
set
,
(
∃X4 :
set
,
(
(
X4
⊆
X3
)
∧
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
→
(
¬
p
X2
)
)
)
)
→
(
∀X4 :
set
,
(
(
(
(
(
¬
atleast5
X3
)
→
setsum_p
X4
)
∧
(
¬
exactly4
X3
)
)
→
(
(
¬
atleast3
X2
)
∧
(
exactly5
X3
→
(
(
atleast2
X2
∧
(
¬
p
(
⋃
∅
)
)
)
∧
atleast4
X2
)
)
)
→
p
X3
→
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
ordinal
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
¬
p
(
f
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
∧
p
(
f
(
f
(
f
(
f
∅
)
)
)
)
)
→
(
(
∃X2 ∈
f
(
f
∅
)
,
∀X3 :
set
,
∃X4 :
set
,
(
(
X4
⊆
∅
)
∧
(
¬
tuple_p
X3
X3
)
)
)
∧
(
∀X2 :
set
,
∃X3 ∈
X2
,
∃X4 ∈
f
X3
,
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
∧
exactly4
(
f
X2
)
)
)
)
)
∧
(
(
∀X2 :
set
,
∃X3 :
set
,
(
(
∀X4 :
set
,
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
→
p
∅
→
(
¬
nat_p
X2
)
)
∧
(
¬
reflexive_i
(
λX4 :
set
⇒
λX5 :
set
⇒
(
¬
nat_p
X5
)
→
(
p
(
f
(
f
X4
)
)
∧
TransSet
X5
)
)
)
)
)
∧
(
∀X2
∈
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
,
∃X3 :
set
,
(
(
∀X4 :
set
,
p
X4
→
(
¬
atleast3
X4
)
)
∧
(
∃X4 :
set
,
(
¬
p
X3
)
)
)
)
)
)
)
∧
(
p
(
f
∅
)
→
(
∀X2
⊆
f
(
f
(
SetAdjoin
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
f
∅
)
)
)
,
∃X3 :
set
,
(
(
(
∀X4
⊆
X2
,
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
(
∀X4
∈
X3
,
(
¬
atleast2
X4
)
)
)
∧
(
∃X4 ∈
f
(
f
X3
)
,
(
(
¬
p
X2
)
∧
(
¬
p
(
f
X4
)
)
)
)
)
)
)
)
In Proofgold the corresponding term root is
55cf0b...
and proposition id is
bab480...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMdoopWoA9jfqVyB2wh3mJFCWBhMvSh8fgP
)
(
(
∀X2 :
set
,
(
∃X3 :
set
,
(
(
∃X4 :
set
,
(
(
¬
exactly3
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
¬
set_of_pairs
X3
)
)
)
∧
(
(
(
∃X4 :
set
,
(
(
X4
⊆
X3
)
∧
(
(
¬
ordinal
X2
)
∧
(
¬
set_of_pairs
X3
)
)
)
)
∧
(
(
p
X2
→
(
∃X4 :
set
,
(
exactly5
X3
∧
(
(
p
X3
→
p
X4
)
→
(
¬
TransSet
X4
)
)
)
)
→
(
∀X4 :
set
,
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
∧
(
¬
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
→
(
p
X3
∧
(
∀X4
⊆
f
(
Sing
∅
)
,
(
(
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
→
p
X3
)
∧
(
(
(
(
(
(
¬
exactly3
X3
)
∧
(
¬
p
X2
)
)
→
(
(
(
exactly3
X4
∧
(
¬
p
X4
)
)
∧
atleast4
X4
)
∧
(
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
tuple_p
X4
X4
)
∧
atleast5
X4
)
)
)
→
(
¬
atleast5
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
(
(
(
(
atleast5
X2
→
(
(
(
p
X4
→
(
(
(
¬
exactly5
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
p
X4
)
∧
p
X4
)
→
p
X3
)
∧
(
(
atleastp
(
𝒫
X4
)
X3
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
atleast3
X3
→
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
p
(
nat_primrec
X5
(
λX7 :
set
⇒
λX8 :
set
⇒
X8
)
X3
)
)
)
→
(
(
¬
p
X3
)
∧
(
SNo_
X3
X4
∧
(
exactly3
∅
∧
(
(
(
(
(
(
p
(
f
(
SNoElts_
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
atleast4
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
→
(
(
p
X4
∧
(
exactly3
(
f
X4
)
→
(
equip
X3
X4
∧
(
p
(
V_
X2
)
∧
(
(
(
p
X4
→
(
¬
p
X4
)
→
set_of_pairs
X4
→
(
(
atleast2
X2
→
exactly2
X3
)
∧
p
X4
)
)
∧
(
(
(
¬
exactly2
∅
)
∧
(
(
¬
p
X3
)
→
(
¬
SNo
X3
)
)
)
→
(
¬
SNo
X3
)
)
)
∧
(
exactly3
X4
→
p
(
f
∅
)
)
)
)
)
)
)
→
(
¬
p
X2
)
)
→
(
(
(
(
¬
exactly1of2
(
p
X4
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
(
¬
atleast3
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
→
p
X4
)
→
(
¬
exactly2
(
f
X3
)
)
)
∧
(
p
(
V_
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
→
(
(
¬
atleast2
X3
)
∧
(
(
(
(
¬
p
X4
)
∧
(
strictpartialorder_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
atleast3
X6
→
(
(
(
¬
p
X2
)
∧
(
(
(
p
X5
→
exactly5
X6
)
∧
(
(
atleast4
X4
→
(
(
(
¬
p
X6
)
∧
(
(
¬
atleast6
(
𝒫
(
f
X6
)
)
)
∧
(
(
(
(
(
(
(
(
¬
p
X5
)
∧
(
(
exactly2
X6
→
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
(
(
(
(
p
X5
→
(
¬
exactly3
X2
)
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
¬
p
X2
)
→
p
X6
)
→
(
(
¬
exactly5
X4
)
∧
(
¬
p
X6
)
)
→
atleast6
X6
)
→
p
X6
→
(
¬
atleast3
X4
)
)
∧
stricttotalorder_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
(
(
(
(
p
X4
∧
(
set_of_pairs
X2
∧
(
(
¬
atleast3
(
Sing
X7
)
)
∧
(
p
X8
→
(
¬
p
X6
)
)
)
)
)
∧
(
p
X8
→
(
p
(
V_
X7
)
∧
(
¬
(
X8
⊆
X7
)
)
)
)
)
∧
(
(
¬
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
nat_p
∅
∧
(
¬
nat_p
X5
)
)
)
)
∧
(
(
¬
p
X8
)
→
(
(
¬
atleast2
X2
)
∧
(
(
¬
atleast2
X7
)
∧
(
(
(
(
(
(
(
(
(
ordinal
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
→
(
p
X8
∧
p
(
⋃
X3
)
)
)
→
(
(
(
¬
nat_p
(
f
(
f
X5
)
)
)
∧
(
(
(
setsum_p
X7
→
atleast6
X7
)
→
p
X5
)
∧
(
¬
p
X7
)
)
)
∧
nat_p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
(
(
SNo
∅
→
nat_p
X8
)
∧
(
(
¬
p
X8
)
→
(
nat_p
(
f
X7
)
∧
p
X5
)
)
)
)
→
(
p
X7
→
(
¬
p
X7
)
)
→
(
(
¬
ordinal
∅
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
¬
p
X8
)
)
∧
atleast6
X4
)
∧
(
¬
p
X4
)
)
→
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
atleast6
(
⋃
X7
)
∧
(
(
(
¬
exactly5
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
→
atleast4
X2
)
∧
(
p
X8
∧
p
X7
)
)
)
∧
(
¬
p
X7
)
)
→
atleast4
X4
)
)
∧
(
(
¬
p
X8
)
∧
(
¬
equip
X8
X8
)
)
)
∧
exactly3
X6
)
)
)
)
)
∧
(
p
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
∧
atleast5
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
∧
(
(
¬
p
(
V_
X6
)
)
→
(
(
setsum_p
X6
∧
(
TransSet
(
ordsucc
X5
)
∧
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
p
X5
)
→
atleast3
X6
)
)
)
→
(
¬
exactly5
X6
)
)
∧
ordinal
X6
)
→
(
¬
nat_p
∅
)
)
→
(
¬
set_of_pairs
X6
)
→
(
p
X6
∧
(
p
X5
→
(
p
X2
∧
(
(
¬
p
X2
)
∧
(
(
(
(
(
¬
atleast6
X5
)
→
p
X5
)
∧
(
¬
atleast5
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
¬
p
X3
)
)
→
(
¬
p
∅
)
)
)
)
→
(
¬
exactly5
X5
)
→
(
¬
p
X5
)
)
)
→
trichotomous_or_i
(
λX7 :
set
⇒
λX8 :
set
⇒
p
X8
)
)
→
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
(
(
exactly5
X6
∧
(
(
¬
p
X6
)
∧
(
TransSet
X6
∧
(
(
(
(
(
(
(
X6
⊆
X5
)
∧
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
→
(
exactly5
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
∧
(
(
¬
atleast5
X6
)
→
atleast6
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
¬
p
(
ordsucc
X3
)
)
→
(
(
¬
atleast3
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
atleast5
X6
∧
(
(
p
X6
∧
(
(
¬
p
X5
)
∧
(
p
X6
∧
(
¬
p
X3
)
)
)
)
→
(
¬
p
X5
)
→
(
¬
p
X2
)
→
exactly4
X6
)
)
∧
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
→
(
exactly2
X4
∧
p
X6
)
)
∧
(
¬
SNo
(
proj0
X6
)
)
)
∧
(
(
¬
p
X4
)
∧
(
(
¬
p
X5
)
→
(
¬
atleast2
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
)
)
→
(
(
(
¬
ordinal
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
p
X6
∧
(
(
atleast6
X5
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
¬
p
X6
)
)
)
)
∧
(
(
(
¬
atleast3
X5
)
∧
p
X4
)
∧
(
f
X4
⊆
X5
)
)
)
)
∧
(
¬
atleast6
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
∧
(
(
¬
atleast3
X5
)
→
(
(
¬
exactly4
X6
)
∧
p
X4
)
→
(
p
X6
∧
(
nat_p
X6
∧
(
¬
p
X5
)
)
)
)
)
→
(
(
¬
p
X5
)
∧
(
¬
p
X6
)
)
)
)
)
→
(
setsum_p
(
f
X2
)
∧
(
(
¬
atleast5
X6
)
→
p
X5
)
)
)
)
→
(
¬
SNoLt
X2
(
PSNo
X6
(
λX7 :
set
⇒
(
(
(
(
¬
p
X6
)
∧
(
(
(
(
¬
exactly3
X2
)
∧
atleast5
X6
)
→
(
¬
p
X7
)
)
→
(
(
(
p
X6
→
exactly5
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
→
(
(
¬
SNoLe
(
ap
X6
(
f
X2
)
)
X6
)
∧
(
X3
∈
X6
)
)
)
→
p
X6
)
∧
(
¬
atleast6
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
→
(
¬
p
X6
)
)
∧
(
(
(
p
X6
→
p
X7
)
→
(
¬
exactly3
(
f
X6
)
)
)
∧
(
¬
p
X7
)
)
)
)
)
)
)
)
∧
(
¬
exactly4
(
f
(
𝒫
X6
)
)
)
)
)
→
(
¬
p
X5
)
)
→
(
¬
p
X3
)
)
)
∧
(
p
∅
∧
(
¬
p
(
f
∅
)
)
)
)
∧
(
p
X2
∧
exactly4
X2
)
)
)
)
)
)
∧
(
p
X3
∧
p
X4
)
)
→
(
¬
p
X3
)
)
→
p
∅
)
∧
ordinal
X4
)
→
(
(
p
X2
→
(
(
(
(
¬
p
X3
)
∧
(
(
¬
p
X3
)
∧
(
p
(
Sing
X4
)
→
(
(
(
¬
p
X3
)
→
(
p
X3
∧
(
p
X3
∧
(
¬
p
X4
)
)
)
)
∧
ordinal
∅
)
)
)
)
→
p
(
f
X4
)
)
∧
(
¬
p
X3
)
)
)
∧
(
¬
exactly2
X4
)
)
)
)
)
)
→
(
¬
p
X3
)
)
)
∧
(
¬
set_of_pairs
X4
)
)
)
→
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
∧
(
(
p
X3
→
atleast2
X2
)
∧
(
p
X3
∧
(
irreflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
p
X2
∧
(
nat_p
∅
→
(
(
p
(
f
X6
)
∧
SNo
X5
)
∧
nat_p
X5
)
)
)
→
(
¬
equip
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
X6
)
)
∧
(
¬
atleast3
(
setminus
(
f
(
ap
X3
X3
)
)
X4
)
)
)
)
)
)
)
→
SNo_
X3
X3
)
→
atleast2
X4
)
)
∧
(
¬
p
∅
)
)
)
)
)
)
)
→
(
∀X4 :
set
,
(
atleast5
X3
→
(
¬
p
X3
)
)
→
(
p
X2
∧
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
→
(
(
¬
SNo_
∅
(
binintersect
X4
X3
)
)
∧
(
¬
atleast3
(
UPair
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
X3
)
)
)
→
(
¬
p
(
f
X3
)
)
)
)
)
)
)
)
→
(
∀X3
⊆
X2
,
∃X4 :
set
,
(
(
X4
⊆
∅
)
∧
(
(
¬
TransSet
X4
)
∧
atleast3
∅
)
)
)
)
∧
(
(
∃X2 ∈
V_
∅
,
p
(
f
(
setprod
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
X2
)
)
)
∧
(
¬
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
In Proofgold the corresponding term root is
410070...
and proposition id is
b51035...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMXqWqqXzQ3NLxWJhTMG2iUtcQLWocMTLhX
)
∃X2 :
set
,
(
(
(
∀X3
⊆
setexp
(
f
X2
)
X2
,
∀X4
⊆
X3
,
(
p
X3
∧
(
¬
p
X4
)
)
)
∧
(
∃X3 :
set
,
(
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
∧
(
∀X4 :
set
,
(
(
(
(
(
(
X4
=
∅
)
→
exactly3
(
f
X4
)
→
(
exactly3
X2
∧
(
(
(
¬
atleast6
∅
)
→
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
atleast3
(
f
(
f
X3
)
)
)
)
)
→
(
¬
exactly5
∅
)
)
→
(
p
(
𝒫
X2
)
∧
p
X3
)
→
(
(
(
(
(
(
¬
nat_p
∅
)
∧
(
(
¬
(
X3
=
X4
)
)
→
(
¬
p
X3
)
)
)
→
atleast4
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
SNo
X3
)
→
exactly4
(
f
X2
)
→
(
(
(
(
exactly5
X3
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
¬
ordinal
X4
)
)
→
(
¬
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
p
X5
)
)
)
)
∧
(
(
(
¬
ordinal
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
∧
(
SNo
X3
∧
p
X2
)
)
→
(
(
atleast4
X3
∧
(
exactly4
(
ordsucc
X3
)
∧
(
p
(
f
X4
)
→
(
(
¬
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
p
X4
)
)
)
)
∧
(
(
¬
p
X3
)
→
(
(
p
X4
→
p
X3
)
∧
(
p
(
proj0
X4
)
→
(
¬
exactly3
X4
)
)
)
)
)
)
)
)
∧
(
(
(
(
(
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∧
(
(
(
(
¬
p
X3
)
→
p
X4
→
(
¬
atleast5
X3
)
)
→
(
¬
setsum_p
(
f
X2
)
)
→
SNo
X2
)
∧
exactly4
X4
)
)
→
p
X2
)
→
(
¬
atleast3
(
f
(
f
X4
)
)
)
→
atleast2
(
UPair
(
f
(
f
(
f
X3
)
)
)
X2
)
→
(
p
(
Repl
X3
(
λX5 :
set
⇒
X4
)
)
∧
(
¬
ordinal
X2
)
)
)
∧
(
(
(
¬
atleast2
X3
)
∧
(
(
¬
p
X3
)
→
(
¬
p
X2
)
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
(
(
(
(
¬
exactly3
X4
)
→
(
(
¬
p
X2
)
∧
p
X3
)
)
→
(
(
p
∅
→
(
(
¬
p
X4
)
∧
(
(
(
(
¬
p
∅
)
→
atleast4
X2
)
→
(
(
(
p
X2
→
p
X3
)
→
(
(
¬
ordinal
X4
)
∧
(
(
¬
p
(
f
(
f
(
f
X3
)
)
)
)
∧
set_of_pairs
X2
)
)
)
∧
(
(
¬
(
X4
∈
X3
)
)
→
exactly3
X4
)
)
)
→
(
(
¬
p
X4
)
→
(
¬
p
∅
)
→
(
¬
p
X3
)
)
→
(
¬
atleast5
X4
)
)
)
)
∧
(
(
TransSet
X3
∧
(
(
(
nat_p
X4
∧
atleastp
X2
X3
)
→
(
(
¬
p
(
setprod
X2
X2
)
)
∧
atleast2
∅
)
)
→
(
(
(
p
(
f
X4
)
∧
(
¬
exactly4
X3
)
)
→
(
(
p
(
UPair
X3
(
Inj1
(
f
X2
)
)
)
→
(
(
¬
p
X4
)
∧
(
¬
p
X3
)
)
→
(
exactly4
X4
→
(
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∧
(
(
¬
exactly3
X3
)
→
(
(
¬
atleast3
X3
)
∧
(
¬
nat_p
X3
)
)
→
(
¬
stricttotalorder_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
⊆
X5
)
)
)
)
)
)
→
p
X2
→
(
SNo
X4
→
(
¬
SNo
X3
)
)
→
(
(
¬
p
(
V_
X3
)
)
∧
(
atleast4
X4
∧
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
atleast6
X2
)
→
(
¬
p
X2
)
)
)
)
)
∧
p
(
f
X3
)
)
)
∧
(
¬
atleast4
X3
)
)
)
)
∧
(
(
¬
atleast4
X2
)
∧
(
(
atleast2
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
∧
(
(
(
¬
set_of_pairs
X3
)
→
(
(
¬
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
exactly3
X5
→
(
¬
atleast6
X6
)
)
)
∧
TransSet
(
f
X4
)
)
)
→
p
X3
)
)
∧
p
X2
)
)
)
)
→
(
atleast6
X3
∧
(
¬
TransSet
X4
)
)
)
→
(
¬
atleast5
(
f
X3
)
)
)
)
∧
(
¬
atleast3
X3
)
)
→
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
→
(
¬
atleast6
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
→
(
¬
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
∧
p
X4
)
)
)
)
)
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
In Proofgold the corresponding term root is
fbf8e9...
and proposition id is
bff3a9...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMaGoYyR7LEEd8ArrJUuTmxecbNsSK2fHm8
)
(
∃X2 :
set
,
(
(
X2
⊆
f
(
Inj1
(
f
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
∃X3 ∈
X2
,
∃X4 :
set
,
(
SNoEq_
(
f
X2
)
(
V_
X4
)
X3
∧
p
X3
)
)
)
)
→
(
∃X2 :
set
,
∀X3 :
set
,
∃X4 ∈
f
X3
,
(
¬
exactly2
X2
)
)
In Proofgold the corresponding term root is
f456ed...
and proposition id is
7c1b70...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMFLEHTibZT6RqZDfZoy9ciqK8Lk8uqXkgz
)
∃X2 :
set
,
(
(
¬
p
(
f
(
f
(
f
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
∧
(
(
∃X3 ∈
f
(
f
(
setminus
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
X2
)
)
,
atleast2
X2
)
→
(
(
¬
exactly3
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
∃X3 :
set
,
∃X4 ∈
X3
,
(
¬
exactly2
(
SNoLev
∅
)
)
)
)
)
)
In Proofgold the corresponding term root is
5a60bd...
and proposition id is
dc3479...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMWNJVuZuRma9t57rxUSbiyo2ox4uUs44Fy
)
(
(
∀X2
⊆
∅
,
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
⊆
f
X2
)
)
∧
(
∀X2 :
set
,
(
(
∀X3
∈
f
(
f
(
f
(
f
X2
)
)
)
,
atleast5
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
p
X2
)
)
→
(
∀X3 :
set
,
(
∃X4 :
set
,
(
(
(
(
¬
p
∅
)
∧
atleast5
X3
)
→
(
¬
exactly3
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
→
(
∀X4
∈
X2
,
p
X3
→
atleast3
X2
)
)
)
)
In Proofgold the corresponding term root is
cb0f9b...
and proposition id is
ed5fd5...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMPECRKSuiQJGFYQBiYhwR3RemMX5fhNwtQ
)
∀X2
⊆
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
,
(
TransSet
∅
∧
(
exactly3
∅
→
(
∃X3 :
set
,
(
(
(
∀X4
⊆
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
,
(
(
¬
atleast6
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
(
¬
atleast3
X4
)
)
)
∧
(
∃X4 :
set
,
(
(
p
X4
→
(
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
∧
atleast2
∅
)
)
∧
(
(
¬
atleast5
X4
)
∧
(
f
X3
=
X4
)
)
)
)
)
∧
(
∀X4
∈
X3
,
(
¬
p
X4
)
)
)
)
)
)
In Proofgold the corresponding term root is
fb69e8...
and proposition id is
cc8ecb...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMXDSQpwAARbtWZzbcFckfwWxvYgsnQnqFq
)
∀X2 :
set
,
∃X3 :
set
,
(
(
∃X4 ∈
X3
,
(
(
¬
exactly5
X4
)
∧
(
¬
set_of_pairs
X2
)
)
→
(
¬
p
(
f
∅
)
)
→
(
atleast2
X4
∧
exactly4
(
f
X4
)
)
)
∧
(
¬
p
X2
)
)
In Proofgold the corresponding term root is
c2efd6...
and proposition id is
bb4236...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMH8STG7VZvR7VRBA85rZy5Z71WRmLD5oEK
)
(
(
∀X2 :
set
,
(
(
(
¬
exactly5
(
mul_nat
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
∅
)
)
∧
(
∃X3 :
set
,
(
(
(
∃X4 :
set
,
(
p
X4
∧
(
(
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
∧
(
(
(
p
(
Unj
X3
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
∧
(
(
¬
atleast4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
p
X2
→
p
X4
)
)
)
∧
(
(
¬
TransSet
X3
)
→
(
¬
setsum_p
X3
)
→
(
¬
p
X3
)
)
)
)
→
(
¬
p
∅
)
)
→
(
(
p
X4
∧
(
¬
setsum_p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
p
X4
∧
(
¬
p
X3
)
)
)
)
)
)
∧
(
p
X3
→
(
∃X4 :
set
,
exactly5
X4
)
)
)
∧
(
(
(
∃X4 :
set
,
(
(
(
(
¬
p
(
f
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
p
X2
)
→
(
(
(
(
(
(
¬
totalorder_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
p
X2
)
)
)
→
ordinal
∅
)
→
(
¬
p
X2
)
)
→
(
(
(
(
(
(
¬
atleast4
X4
)
→
(
¬
p
X3
)
)
∧
(
(
¬
p
X4
)
∧
(
p
X4
→
(
(
ordinal
X4
∧
atleast4
(
f
X2
)
)
∧
(
(
(
¬
TransSet
X4
)
→
TransSet
X4
)
∧
(
¬
p
X3
)
)
)
)
)
)
→
(
¬
p
X4
)
)
∧
atleast6
X2
)
∧
atleast3
X4
)
)
∧
(
¬
SNo
X3
)
)
∧
(
(
¬
atleast6
X3
)
→
(
¬
p
X4
)
)
)
)
∧
(
p
X4
→
(
(
(
(
(
(
(
¬
(
X2
∈
f
X4
)
)
∧
(
¬
exactly5
X2
)
)
∧
(
¬
ordinal
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
∧
(
(
(
(
(
(
atleast3
X3
∧
atleast2
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
(
(
¬
p
X2
)
∧
(
(
(
(
X2
∈
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
→
nat_p
(
f
X4
)
→
(
(
(
PNoLt
X3
(
λX5 :
set
⇒
(
X4
∈
X5
)
)
X4
(
λX5 :
set
⇒
(
atleast4
X5
∧
(
(
(
exactly2
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
→
(
(
¬
p
X4
)
∧
(
p
X4
→
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
(
(
atleast4
X3
→
ordinal
X4
)
∧
(
TransSet
X5
∧
(
(
(
¬
exactly4
X3
)
→
p
X4
)
∧
(
¬
ordinal
X3
)
)
)
)
)
∧
(
¬
exactly3
X4
)
)
)
→
trichotomous_or_i
(
λX6 :
set
⇒
λX7 :
set
⇒
(
¬
atleast4
X6
)
)
)
→
p
X4
)
→
(
¬
p
X3
)
)
→
exactly3
∅
)
→
nat_p
X2
)
∧
(
¬
exactly3
X4
)
)
→
(
¬
p
(
f
X4
)
)
)
)
∧
(
(
¬
atleast2
X3
)
∧
(
set_of_pairs
X3
∧
(
(
(
¬
set_of_pairs
X4
)
∧
(
p
X4
∧
(
(
(
(
¬
p
X4
)
∧
(
(
¬
exactly4
X2
)
→
(
¬
TransSet
X3
)
)
)
∧
(
(
¬
p
X4
)
∧
atleast6
∅
)
)
→
(
¬
nat_p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
∧
(
atleast2
X4
→
atleast6
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
)
→
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
(
(
¬
p
(
f
X2
)
)
→
(
¬
TransSet
X3
)
)
∧
(
(
(
(
atleast4
X4
∧
p
X3
)
∧
p
X3
)
∧
(
(
(
(
(
p
(
mul_nat
(
proj1
∅
)
(
f
X4
)
)
→
(
(
¬
TransSet
(
UPair
(
f
X3
)
X4
)
)
∧
(
¬
p
X3
)
)
)
∧
(
p
(
f
(
f
X2
)
)
→
TransSet
X4
→
(
(
(
¬
exactly3
(
f
(
⋃
X3
)
)
)
→
exactly4
X3
)
∧
(
(
(
(
atleastp
X3
X4
→
(
¬
atleast5
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
→
atleast3
(
f
X4
)
)
→
(
¬
atleast2
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
¬
atleast2
X4
)
→
p
X2
)
→
(
(
¬
p
X3
)
∧
(
¬
p
X2
)
)
)
)
→
p
∅
)
)
)
)
∧
(
p
(
f
X3
)
→
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
)
∧
(
¬
ordinal
(
f
X4
)
)
)
∧
(
p
X3
→
(
¬
TransSet
X3
)
→
exactly5
X4
)
)
)
∧
p
X2
)
)
)
∧
(
p
X4
∧
(
(
¬
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
¬
exactly4
X4
)
∧
(
p
X4
∧
(
¬
p
(
f
X3
)
)
)
)
→
(
(
¬
p
X4
)
∧
ordinal
X2
)
)
)
)
)
∧
(
¬
atleast5
X4
)
)
)
→
p
X4
)
→
(
(
(
(
(
SNo
(
f
(
f
(
f
(
f
(
f
(
Inj1
X4
)
)
)
)
)
)
→
p
X3
→
(
¬
(
X4
∈
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
p
(
Inj0
(
f
X4
)
)
)
∧
(
¬
TransSet
X3
)
)
→
(
(
¬
p
(
V_
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
∧
(
(
(
¬
p
X4
)
→
(
¬
nat_p
X2
)
)
∧
(
(
(
exactly2
X4
→
(
(
(
(
p
X4
∧
(
¬
p
(
f
X4
)
)
)
→
(
(
(
¬
exactly4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
ordinal
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
(
X2
∈
binrep
X4
X3
)
)
→
(
¬
p
X4
)
)
→
(
¬
tuple_p
∅
X3
)
)
∧
(
nat_p
∅
∧
(
(
¬
atleast4
X4
)
→
TransSet
(
⋃
∅
)
)
)
)
)
→
atleast2
X3
→
(
(
¬
ordinal
(
setminus
∅
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
exactly5
X4
)
)
∧
(
p
X3
→
(
¬
p
X4
)
)
)
)
)
→
(
¬
p
X2
)
)
∧
exactly4
(
f
X3
)
)
∧
(
p
X4
∧
(
¬
p
X3
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
∀X4 :
set
,
(
p
X3
∧
exactly5
(
f
X4
)
)
→
(
SNoLe
X2
X4
∧
(
(
(
¬
p
X3
)
∧
(
atleast3
X3
→
(
¬
atleast3
X4
)
)
)
→
p
X4
)
)
)
)
→
(
∀X4
∈
∅
,
(
¬
exactly3
X4
)
)
)
)
)
)
∧
(
∀X3 :
set
,
(
∀X4
⊆
f
X2
,
(
(
(
¬
(
X3
∈
X3
)
)
→
(
¬
p
X3
)
)
∧
exactly5
X3
)
)
→
(
∀X4
⊆
f
(
f
X3
)
,
(
SNo
X3
∧
(
(
¬
atleast2
X3
)
→
p
X3
)
)
)
)
)
→
(
∃X3 :
set
,
(
(
∃X4 :
set
,
(
(
X4
⊆
f
(
f
X2
)
)
∧
(
(
¬
p
X3
)
∧
(
(
¬
p
X4
)
→
p
X3
)
)
)
)
∧
(
∀X4 :
set
,
(
(
(
(
(
(
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
(
(
(
p
X3
∧
(
(
(
¬
atleast4
X4
)
∧
(
(
(
(
p
X3
→
atleast5
X3
)
∧
(
(
exactly3
(
binrep
X3
(
f
(
f
X4
)
)
)
→
(
(
(
(
X2
=
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∧
exactly5
X3
)
→
(
(
¬
TransSet
(
f
X4
)
)
→
(
atleast3
X3
∧
(
¬
exactly2
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
→
(
(
(
(
¬
exactly2
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
∧
atleast2
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
p
X2
)
∧
(
(
atleast6
∅
→
(
¬
TransSet
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
exactly5
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
p
X2
)
)
→
(
¬
p
X4
)
)
)
)
∧
(
(
¬
p
(
f
X3
)
)
→
p
X4
→
p
X3
)
)
)
→
(
¬
p
X4
)
)
)
→
(
¬
exactly5
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
(
¬
ordinal
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
∧
set_of_pairs
X4
)
)
∧
(
(
atleast4
X3
∧
(
¬
p
X4
)
)
∧
p
(
f
X4
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
)
∧
(
(
(
p
X3
∧
SNo
X4
)
→
p
X4
→
(
(
(
TransSet
X4
∧
p
X4
)
→
TransSet
(
f
∅
)
)
∧
(
¬
p
X4
)
)
→
atleast2
X3
)
→
TransSet
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
→
(
¬
p
(
f
∅
)
)
→
p
X3
)
→
(
¬
atleast5
X3
)
)
∧
ordinal
(
f
X4
)
)
∧
(
p
∅
∧
(
(
p
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
¬
p
(
𝒫
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
¬
atleast4
X3
)
)
)
)
→
(
atleast6
X3
→
(
(
(
(
setsum_p
X3
→
ordinal
∅
)
∧
(
¬
p
X4
)
)
∧
(
¬
p
X2
)
)
∧
(
(
(
¬
exactly3
∅
)
→
(
(
¬
p
X3
)
∧
(
exactly4
X3
→
p
(
f
∅
)
)
)
)
∧
exactly3
X4
)
)
→
(
¬
setsum_p
X4
)
)
→
(
¬
SNo
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
(
(
ordinal
∅
∧
(
(
¬
p
(
f
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
)
→
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
→
(
¬
atleast2
X4
)
)
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
∧
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
(
(
¬
exactly4
X2
)
∧
atleast4
X3
)
→
(
p
(
f
(
f
X3
)
)
∧
(
¬
exactly4
X3
)
)
)
→
p
X3
)
∧
(
¬
atleast3
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
)
→
(
¬
atleast3
X3
)
)
)
)
→
(
∃X3 :
set
,
(
(
∀X4
∈
f
(
f
X2
)
,
exactly3
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
exactly2
(
f
X3
)
)
)
)
∧
(
∃X2 :
set
,
(
(
(
∀X3 :
set
,
∀X4 :
set
,
(
p
(
Sing
X4
)
∧
(
exactly2
X4
→
(
(
¬
p
X4
)
∧
atleast2
X2
)
)
)
→
p
X4
)
→
(
(
¬
exactly2
(
f
(
ordsucc
X2
)
)
)
∧
(
∀X3
∈
∅
,
∀X4
∈
X3
,
(
(
¬
setsum_p
X2
)
∧
setsum_p
(
f
X3
)
)
)
)
)
∧
atleast5
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
)
In Proofgold the corresponding term root is
51ea01...
and proposition id is
f5a625...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMQyr8o3y2w5QoAGzcUxkoxTtxPrh1jgxAV
)
(
(
∃X2 :
set
,
(
(
¬
atleast6
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
∃X3 :
set
,
(
(
X3
⊆
f
(
f
(
f
X2
)
)
)
∧
(
∃X4 :
set
,
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
→
(
(
¬
exactly2
X3
)
∧
p
(
f
X3
)
)
)
)
)
)
)
→
(
∃X2 :
set
,
nat_p
(
f
X2
)
)
)
→
(
∃X2 :
set
,
(
(
X2
⊆
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
∧
p
X2
)
)
In Proofgold the corresponding term root is
dd0b68...
and proposition id is
b8b5fc...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMcHib4bK6yeTxFVGKF7Ppr7CdEqAsFa51a
)
(
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
∃X2 :
set
,
(
(
∀X3
∈
X2
,
∃X4 ∈
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
,
(
(
¬
nat_p
X4
)
∧
(
(
¬
nat_p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
¬
(
∅
∈
X3
)
)
∧
(
(
¬
atleast2
X4
)
→
(
(
¬
atleast2
X3
)
∧
(
¬
p
X2
)
)
→
(
¬
setsum_p
X4
)
)
)
)
)
)
∧
(
∃X3 :
set
,
(
∃X4 :
set
,
(
(
X4
⊆
∅
)
∧
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
∀X4 :
set
,
exactly4
X4
)
)
)
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
∃X2 :
set
,
(
¬
atleast3
(
f
X2
)
)
)
→
(
∀X2 :
set
,
∀X3 :
set
,
(
∃X4 :
set
,
p
X4
)
→
(
∃X4 ∈
X2
,
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
∧
ordinal
X2
)
)
)
In Proofgold the corresponding term root is
10d925...
and proposition id is
f48718...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMQ1tQnas4fj59K9UafaJbvBtZPtvAbaNiF
)
(
(
∀X2 :
set
,
(
∀X3 :
set
,
(
(
∃X4 :
set
,
(
(
(
(
¬
p
(
SetAdjoin
X4
X4
)
)
→
atleast3
X4
)
∧
(
¬
p
(
f
X3
)
)
)
∧
(
p
X4
→
(
(
¬
p
X4
)
∧
(
p
X2
→
(
(
(
(
atleast5
X4
→
exactly4
X3
)
→
(
(
(
(
(
¬
exactly2
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
p
X3
→
(
TransSet
(
setexp
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
(
ordsucc
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
∧
(
¬
ordinal
∅
)
)
)
→
(
(
¬
p
X4
)
∧
(
(
(
¬
nat_p
(
f
(
f
X2
)
)
)
∧
atleast4
X3
)
∧
(
(
¬
p
X4
)
→
(
¬
exactly2
X2
)
)
)
)
)
→
(
(
¬
p
X3
)
∧
(
(
(
¬
p
∅
)
→
(
¬
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
→
(
(
(
atleast2
(
f
X3
)
∧
(
SNo
X3
→
exactly4
(
combine_funcs
X2
X3
(
λX5 :
set
⇒
X5
)
(
λX5 :
set
⇒
X5
)
X3
)
→
(
(
(
TransSet
X4
∧
(
¬
p
X2
)
)
→
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
p
(
binintersect
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
X4
)
)
)
∧
(
(
p
(
f
(
f
X2
)
)
→
(
¬
p
X4
)
)
∧
(
¬
SNo_
X3
(
proj0
(
f
X3
)
)
)
)
)
)
)
∧
p
X4
)
∧
(
(
(
(
(
¬
exactly3
X3
)
→
(
(
(
p
X4
→
(
(
(
¬
nat_p
X3
)
∧
(
¬
atleast5
X3
)
)
∧
(
¬
exactly5
X3
)
)
)
→
(
¬
exactly4
X4
)
)
∧
(
¬
atleast5
(
𝒫
X3
)
)
)
)
∧
(
(
atleast6
(
f
(
Sep
∅
(
λX5 :
set
⇒
(
¬
p
X4
)
)
)
)
∧
(
(
(
(
p
X4
→
atleast6
X2
→
ordinal
X2
)
∧
(
(
p
∅
→
(
¬
exactly4
∅
)
)
→
(
(
(
(
(
(
¬
atleast4
(
f
X2
)
)
→
(
¬
(
X3
∈
X2
)
)
)
∧
tuple_p
X3
X3
)
→
(
exactly4
∅
∧
(
atleast2
X4
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
¬
exactly2
X3
)
)
∧
(
p
X4
→
(
¬
atleast2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
→
nat_p
(
f
X4
)
→
(
¬
p
(
f
(
𝒫
∅
)
)
)
)
)
→
(
(
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
→
(
(
¬
PNoLt
X2
(
λX5 :
set
⇒
p
(
⋃
X3
)
)
X2
(
λX5 :
set
⇒
(
(
(
¬
p
X4
)
∧
ordinal
X2
)
∧
(
¬
exactly4
X4
)
)
→
p
X5
)
)
∧
(
(
(
(
(
(
(
¬
p
X2
)
∧
(
(
¬
p
X2
)
∧
(
(
¬
p
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
atleast2
(
f
X4
)
→
p
X3
→
(
(
(
(
¬
atleastp
X3
X4
)
→
(
¬
p
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
→
(
¬
p
(
Inj0
∅
)
)
)
∧
(
(
¬
TransSet
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
→
(
atleast3
X3
∧
(
(
p
X4
→
(
(
(
exactly3
X4
∧
(
(
(
(
¬
exactly4
X2
)
→
SNo
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
→
(
(
¬
p
X2
)
→
(
(
p
X4
→
(
(
(
(
exactly4
X2
→
(
(
(
(
X3
⊆
X3
)
∧
(
(
(
¬
p
X2
)
→
(
¬
p
X3
)
)
∧
(
(
(
(
exactly4
X2
→
(
¬
SNo
(
f
(
f
(
f
X3
)
)
)
)
)
∧
(
(
¬
atleastp
X4
X4
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
∧
(
¬
p
X3
)
)
→
nat_p
(
𝒫
X4
)
→
SNo_
∅
X3
)
)
)
∧
(
¬
p
X3
)
)
∧
setsum_p
∅
)
)
∧
(
atleast4
X2
∧
(
(
(
(
¬
exactly3
X3
)
∧
(
¬
exactly2
X2
)
)
→
(
¬
p
(
f
X4
)
)
)
∧
(
(
(
(
(
¬
p
X3
)
→
p
X4
)
→
(
(
(
¬
atleast2
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
¬
p
X4
)
)
∧
(
set_of_pairs
X2
∧
PNoLt
X4
(
λX5 :
set
⇒
setsum_p
X5
)
X3
(
λX5 :
set
⇒
nat_p
∅
→
(
(
(
¬
atleast4
(
f
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
∧
(
¬
p
X4
)
)
→
(
¬
exactly5
∅
)
)
∧
p
X4
)
)
)
)
)
∧
(
(
(
¬
p
X4
)
→
p
(
f
(
f
X4
)
)
)
∧
atleast4
X4
)
)
→
(
¬
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
p
X4
)
)
)
)
∧
(
(
X4
∈
X4
)
→
p
(
f
X3
)
)
)
∧
(
¬
p
(
SNoElts_
(
⋃
X3
)
)
)
)
)
∧
(
(
¬
p
X3
)
∧
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
nat_p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
→
(
¬
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
p
(
binintersect
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
∧
p
∅
)
∧
exactly5
X3
)
)
→
(
(
p
X2
→
atleast6
X4
)
∧
(
¬
ordinal
(
f
X2
)
)
)
)
)
→
(
(
¬
p
X4
)
∧
(
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
∧
(
¬
atleast6
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
)
)
)
)
)
)
)
∧
exactly3
X2
)
∧
p
X2
)
∧
(
(
¬
atleast4
X2
)
→
(
¬
atleast4
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
(
(
(
(
¬
nat_p
X3
)
∧
(
¬
p
X4
)
)
∧
atleast6
X2
)
∧
(
¬
p
X3
)
)
)
→
(
¬
p
(
f
(
f
X4
)
)
)
)
)
)
∧
(
(
¬
atleast5
(
Sep2
X4
(
λX5 :
set
⇒
nat_primrec
∅
(
λX6 :
set
⇒
λX7 :
set
⇒
∅
)
X4
)
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
p
X6
)
)
)
)
→
p
(
f
X3
)
)
)
)
→
ordinal
X4
)
)
∧
p
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
∧
(
(
(
(
¬
atleast2
(
Inj1
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
→
(
(
(
p
X2
∧
p
(
f
∅
)
)
∧
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
∧
(
¬
nat_p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
p
∅
)
)
∧
(
¬
ordinal
(
f
X2
)
)
)
)
→
(
¬
exactly4
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
(
¬
atleast5
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
p
X4
)
)
→
(
¬
p
X2
)
)
)
→
(
¬
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
)
→
(
¬
p
X4
)
)
∧
exactly5
(
f
(
V_
X3
)
)
)
)
∧
(
set_of_pairs
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∧
(
(
(
¬
exactly2
X4
)
→
(
¬
exactly4
X4
)
)
→
atleast5
X4
)
)
)
∧
(
exactly2
X3
∧
(
¬
p
X3
)
)
)
→
(
(
¬
set_of_pairs
X2
)
∧
(
¬
exactly5
(
binrep
X4
X3
)
)
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
∧
(
∃X4 ∈
f
(
Inj0
X3
)
,
p
X2
)
)
→
(
∀X4
∈
X2
,
atleast4
X4
)
)
→
(
(
(
∀X3
⊆
X2
,
(
∃X4 :
set
,
(
(
X4
⊆
X3
)
∧
(
¬
atleast6
(
f
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
→
(
∃X4 ∈
SetAdjoin
(
f
X2
)
∅
,
(
(
(
¬
atleast2
(
f
(
⋃
X3
)
)
)
→
(
¬
p
X3
)
)
∧
(
(
(
¬
p
X3
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
∧
(
(
TransSet
∅
→
SNoLe
X4
(
f
X3
)
)
∧
(
(
¬
p
X3
)
→
(
¬
atleast4
X2
)
)
)
)
)
)
)
→
(
∃X3 :
set
,
(
(
X3
⊆
X2
)
∧
(
∃X4 :
set
,
atleast6
X3
)
)
)
)
∧
(
∀X3 :
set
,
(
¬
ordinal
∅
)
→
(
∀X4 :
set
,
(
¬
exactly3
(
f
∅
)
)
)
)
)
)
∧
p
(
f
(
Inj0
(
f
(
f
(
f
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
)
)
In Proofgold the corresponding term root is
0cde1c...
and proposition id is
87a05a...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMaZmszyn66iEaEB4toUDe9E3L2sSmqMd2R
)
(
∀X2 :
set
,
(
¬
setsum_p
X2
)
→
(
¬
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
→
(
∃X2 :
set
,
(
(
∃X3 :
set
,
(
(
¬
nat_p
(
f
X2
)
)
∧
(
∃X4 :
set
,
(
¬
p
X4
)
)
)
)
∧
(
∀X3 :
set
,
(
(
(
∃X4 ∈
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
,
(
(
(
(
¬
exactly4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
¬
atleast3
(
Inj1
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
→
(
(
(
¬
p
X3
)
→
(
¬
p
(
⋃
X4
)
)
)
∧
(
(
(
p
X3
∧
(
(
(
(
(
(
¬
p
X4
)
→
(
¬
SNo
(
SetAdjoin
X4
X4
)
)
)
∧
(
¬
atleast4
X4
)
)
∧
(
¬
p
X4
)
)
→
p
X3
)
∧
(
(
p
X2
→
p
X3
)
∧
(
¬
p
(
f
(
f
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
)
)
)
)
)
∧
(
setsum_p
X4
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
(
p
X4
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
(
(
¬
p
X3
)
∧
(
(
setsum_p
X3
∧
(
¬
PNoLt_
X4
(
λX5 :
set
⇒
(
(
p
(
UPair
X5
X4
)
∧
(
¬
p
X4
)
)
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
(
λX5 :
set
⇒
(
¬
p
X4
)
)
)
)
∧
ordinal
X4
)
)
∧
(
p
(
f
X4
)
→
(
(
(
¬
exactly3
∅
)
→
nat_p
X3
)
∧
exactly4
(
f
X3
)
)
)
)
)
→
exactly3
X3
)
→
(
∀X4
⊆
X3
,
TransSet
X3
)
→
(
∀X4
⊆
f
(
f
X2
)
,
p
X2
)
)
∧
(
∀X4
⊆
f
∅
,
(
(
¬
TransSet
X2
)
∧
(
(
(
¬
nat_p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
nat_p
X2
)
∧
TransSet
X4
)
)
)
)
)
)
)
In Proofgold the corresponding term root is
59ecec...
and proposition id is
af78d3...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMR4V4zxWLyk9hr24obt2fZA1ZLXxYDQzPc
)
∀X2 :
set
,
(
¬
exactly5
(
f
X2
)
)
→
(
∃X3 :
set
,
(
(
∃X4 :
set
,
(
(
X4
⊆
X3
)
∧
(
(
(
(
nat_p
X4
∧
(
(
(
nat_p
X4
∧
(
(
(
(
(
(
¬
p
X2
)
→
exactly4
(
lam2
(
f
X3
)
(
λX5 :
set
⇒
X4
)
(
λX5 :
set
⇒
λX6 :
set
⇒
X6
)
)
)
→
(
(
(
(
(
(
(
(
(
¬
atleast5
X2
)
→
(
¬
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
exactly3
X5
→
(
(
¬
p
X6
)
∧
p
X5
)
)
→
(
¬
p
X4
)
→
(
¬
nat_p
X2
)
)
→
reflexive_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
exactly5
X8
∧
(
¬
p
(
f
(
lam
X7
(
λX9 :
set
⇒
∅
)
)
)
)
)
)
)
)
)
→
(
¬
nat_p
X3
)
)
∧
ordinal
X3
)
∧
(
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
∧
(
p
X4
→
p
X3
→
p
X3
)
)
∧
(
(
¬
p
X4
)
→
(
¬
p
∅
)
→
(
¬
(
X3
∈
X3
)
)
→
(
atleast6
X4
∧
p
(
f
X3
)
)
→
p
X4
)
)
)
∧
p
(
f
X4
)
)
∧
p
X2
)
→
(
¬
p
X4
)
)
∧
(
¬
atleast6
X4
)
)
→
atleast2
(
f
(
f
X4
)
)
)
→
p
∅
)
→
SNo
X4
)
∧
(
(
¬
inj
X4
X4
(
λX5 :
set
⇒
X3
)
)
→
(
(
(
(
p
X3
→
(
¬
atleast6
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
nat_p
(
f
X4
)
)
)
→
(
(
(
¬
atleast5
X3
)
→
p
∅
)
∧
(
(
p
(
mul_nat
(
f
X3
)
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
(
¬
exactly2
X2
)
→
(
¬
atleast3
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
exactly2
X3
)
→
(
¬
TransSet
X2
)
)
)
)
→
(
(
¬
atleast5
X4
)
∧
(
linear_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
p
∅
∧
(
p
X5
∧
(
p
∅
∧
(
¬
p
∅
)
)
)
)
)
∧
p
X4
)
)
)
∧
(
¬
setsum_p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
→
(
(
¬
p
X4
)
∧
p
X3
)
)
→
(
atleast6
∅
∧
(
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
∧
p
X4
)
∧
(
¬
p
X4
)
)
∧
(
(
(
(
(
(
p
X2
→
atleast6
X2
)
∧
(
¬
exactly4
(
f
X3
)
)
)
→
(
(
p
X3
→
(
¬
p
X3
)
)
∧
(
p
(
SNoLev
X4
)
∧
(
(
(
(
¬
exactly4
X4
)
→
(
(
atleast2
X4
∧
(
¬
p
X3
)
)
∧
(
¬
p
(
f
X3
)
)
)
)
∧
equip
X2
X4
)
∧
(
exactly3
∅
→
p
(
f
∅
)
)
)
)
)
)
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
(
¬
atleast6
(
In_rec_i
(
λX5 :
set
⇒
λX6 :
set
→
set
⇒
∅
)
(
f
X4
)
)
)
)
∧
(
(
¬
exactly3
X4
)
∧
p
X2
)
)
)
)
)
∧
(
¬
SNo
(
f
X2
)
)
)
)
In Proofgold the corresponding term root is
298f7a...
and proposition id is
144c82...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMVX3aLbsURiES9rip6Kpcy3wMgYJpzL6n5
)
p
(
f
(
f
(
f
(
f
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
→
(
(
∀X2
∈
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
,
(
(
(
¬
exactly3
(
f
X2
)
)
∧
(
∀X3 :
set
,
p
X2
)
)
∧
(
∃X3 :
set
,
(
(
∃X4 :
set
,
(
(
set_of_pairs
X3
→
(
¬
atleast4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
p
X3
)
)
∧
(
∀X4 :
set
,
atleast6
X3
→
(
¬
TransSet
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
)
∧
(
∃X2 :
set
,
(
(
(
∀X3
⊆
f
X2
,
∃X4 :
set
,
(
(
X4
⊆
X3
)
∧
(
¬
p
(
V_
(
setminus
(
f
(
ordsucc
X3
)
)
(
f
(
f
X4
)
)
)
)
)
)
)
→
(
∀X3 :
set
,
(
∀X4 :
set
,
(
(
(
¬
p
X4
)
∧
(
¬
atleast4
X2
)
)
∧
(
¬
ordinal
X3
)
)
→
exactly2
X3
)
→
(
¬
atleast5
∅
)
)
)
∧
(
(
∃X3 :
set
,
(
¬
p
X3
)
)
→
exactly2
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
In Proofgold the corresponding term root is
7b47c6...
and proposition id is
a2591a...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMPrvfQbYpDnCoA5i3J3zHJrznWZh1mCkfL
)
∀X2
∈
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
,
∀X3 :
set
,
nat_p
X3
→
(
¬
reflexive_i
(
λX4 :
set
⇒
λX5 :
set
⇒
(
(
¬
PNo_downc
(
λX6 :
set
⇒
λX7 :
set
→
prop
⇒
nat_p
X3
)
(
f
X3
)
(
λX6 :
set
⇒
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
∧
(
(
exactly3
X6
→
(
(
(
(
(
(
(
(
(
¬
p
X2
)
∧
(
p
X6
→
(
¬
atleast2
X3
)
)
)
∧
(
(
(
(
¬
p
∅
)
→
exactly4
X2
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
(
(
(
p
X5
→
(
(
(
(
(
(
(
p
X4
∧
(
p
X5
∧
(
(
¬
p
X4
)
→
per_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
¬
p
X2
)
)
)
)
)
∧
(
¬
atleast6
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
∧
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
¬
p
(
⋃
(
f
X6
)
)
)
→
atleast6
X6
)
→
p
X3
)
→
(
(
¬
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
∈
X2
)
)
∧
(
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
→
atleast6
X6
)
)
→
(
(
(
¬
p
X5
)
∧
(
p
X3
∧
(
p
X5
→
p
X6
)
)
)
∧
(
(
¬
p
X5
)
→
atleast4
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
→
p
∅
→
(
(
(
¬
exactly5
X6
)
∧
(
atleast5
(
Unj
X5
)
∧
(
p
X5
→
(
¬
trichotomous_or_i
(
λX7 :
set
⇒
λX8 :
set
⇒
atleast2
(
f
X8
)
)
)
→
nat_p
X5
)
)
)
∧
(
(
atleast4
X5
→
(
¬
exactly4
X6
)
→
(
(
(
p
X2
∧
TransSet
X5
)
∧
p
∅
)
∧
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
→
(
(
(
¬
p
X5
)
∧
(
¬
p
∅
)
)
∧
(
¬
TransSet
X5
)
)
)
)
)
)
)
→
(
¬
p
X5
)
)
)
→
(
(
¬
exactly3
X2
)
→
(
¬
exactly3
X6
)
)
→
atleastp
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
X6
)
∧
(
(
(
TransSet
(
f
(
f
X6
)
)
→
(
(
¬
atleast3
X3
)
∧
(
¬
exactly5
∅
)
)
)
→
p
X5
)
→
(
¬
(
X6
⊆
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
→
(
(
(
(
p
X6
∧
(
p
X4
→
p
X2
)
)
∧
(
¬
(
∅
∈
∅
)
)
)
→
(
exactly2
(
f
X6
)
∧
(
(
(
¬
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
p
∅
)
)
→
exactly5
X5
→
(
¬
TransSet
X5
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
→
p
X5
)
∧
(
(
p
X6
∧
(
(
¬
p
X5
)
∧
(
¬
p
∅
)
)
)
∧
(
p
∅
∧
p
X5
)
)
)
)
∧
(
(
p
∅
→
(
¬
p
X3
)
)
∧
reflexive_i
(
λX7 :
set
⇒
λX8 :
set
⇒
p
(
binunion
(
f
X8
)
X8
)
→
(
atleast6
X7
→
(
(
¬
exactly4
X8
)
∧
p
X6
)
)
→
(
(
¬
p
X7
)
∧
set_of_pairs
∅
)
)
)
)
∧
(
exactly4
X5
→
p
X3
→
(
strictpartialorder_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
¬
atleast4
X7
)
)
∧
(
¬
(
X3
∈
X4
)
)
)
)
)
)
)
→
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
∧
(
(
¬
exactly4
X5
)
→
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
)
→
(
¬
atleast5
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
(
¬
p
(
f
X5
)
)
)
∧
p
X6
)
∧
(
(
(
(
(
(
(
(
(
(
¬
atleast3
X4
)
→
(
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
¬
SNo_
(
Inj0
X6
)
X6
)
)
→
(
¬
SNo
X5
)
)
∧
(
(
ordinal
X5
∧
p
X6
)
∧
(
p
(
f
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
(
¬
nat_p
X6
)
→
p
X5
)
∧
(
(
(
p
X5
→
(
¬
SNoLe
X6
X5
)
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
∧
(
exactly3
X5
→
p
X2
)
)
)
)
)
)
→
(
(
SNoLe
X4
X6
→
p
X3
)
∧
(
¬
p
X6
)
)
)
→
SNo
X5
)
∧
exactly5
X5
)
→
(
¬
p
X6
)
→
(
f
X6
∈
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
¬
p
X6
)
)
∧
(
¬
p
(
f
X4
)
)
)
∧
(
(
(
(
¬
p
X6
)
→
(
(
¬
p
X5
)
∧
(
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
=
X6
)
→
(
¬
atleast3
X6
)
→
tuple_p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
X6
)
)
→
atleast4
X6
→
ordinal
X6
)
∧
(
(
atleast5
X5
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
(
p
∅
∧
exactly4
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
¬
p
X3
)
→
(
(
p
X3
∧
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
p
(
proj1
X3
)
)
)
)
)
)
→
(
(
¬
p
X6
)
∧
(
(
exactly4
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
∧
p
X6
)
∧
PNoLe
X6
(
λX7 :
set
⇒
(
(
p
(
f
X7
)
∧
p
X7
)
∧
(
(
atleast4
X7
∧
(
(
¬
p
X7
)
→
(
(
p
(
proj1
(
f
(
Inj0
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
→
TransSet
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
(
¬
atleast5
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
p
X6
)
)
)
∧
(
(
(
(
¬
p
X7
)
→
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
→
(
(
¬
atleast4
X7
)
→
(
p
X4
∧
(
¬
atleast4
(
Sep2
(
UPair
(
f
X6
)
X7
)
(
λX8 :
set
⇒
X3
)
(
λX8 :
set
⇒
λX9 :
set
⇒
(
X7
∈
X9
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
→
p
∅
)
→
partialorder_i
(
λX8 :
set
⇒
λX9 :
set
⇒
atleast4
X8
)
)
∧
(
(
¬
atleast6
X7
)
∧
(
(
(
(
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
PNoLe
X7
(
λX8 :
set
⇒
(
¬
exactly3
X8
)
)
X6
(
λX8 :
set
⇒
atleast5
∅
)
)
∧
(
¬
exactly3
(
f
X7
)
)
)
→
(
¬
p
X6
)
)
→
(
¬
p
(
f
∅
)
)
→
(
¬
ordinal
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
)
)
→
(
¬
p
X2
)
)
)
)
∅
(
λX7 :
set
⇒
(
(
p
X6
→
(
(
(
(
(
(
¬
exactly3
∅
)
→
(
¬
p
X6
)
)
∧
(
(
(
(
(
(
¬
SNo
X6
)
→
(
(
¬
p
(
f
X2
)
)
→
p
X6
)
→
(
(
¬
atleast6
(
f
X7
)
)
→
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
→
atleast3
(
SNoLev
∅
)
→
setsum_p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
(
atleast3
(
proj1
∅
)
→
p
X4
)
∧
(
¬
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
→
(
¬
p
∅
)
)
→
(
inj
X7
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
(
λX8 :
set
⇒
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
∧
(
p
X7
→
(
¬
exactly3
∅
)
→
(
(
(
¬
nat_p
X6
)
∧
(
¬
p
X7
)
)
∧
p
X6
)
→
(
(
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
∧
atleast3
∅
)
→
(
(
(
¬
atleast2
(
ordsucc
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
→
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
¬
PNoLe
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
(
λX8 :
set
⇒
(
¬
atleast3
X7
)
)
(
f
X6
)
(
λX8 :
set
⇒
(
¬
p
X7
)
)
)
)
)
→
(
¬
exactly3
X6
)
)
)
)
∧
(
¬
atleast5
X5
)
)
→
(
¬
atleast5
X6
)
)
→
ordinal
X7
)
)
→
(
¬
p
X3
)
)
∧
(
(
¬
atleast6
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
∧
(
(
¬
(
f
X7
∈
X6
)
)
∧
atleast4
X7
)
)
)
∧
(
¬
p
X7
)
)
)
→
(
nat_p
(
f
∅
)
→
ordinal
X7
)
→
(
¬
atleast4
X6
)
)
→
(
(
(
¬
atleast6
X7
)
∧
(
(
(
(
¬
SNo
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
p
(
ordsucc
X6
)
→
(
¬
TransSet
X5
)
→
(
¬
atleast2
X6
)
)
)
→
(
(
¬
TransSet
(
f
X7
)
)
∧
(
¬
exactly5
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
∧
p
X7
)
)
∧
(
¬
exactly4
∅
)
)
)
)
)
)
)
∧
exactly5
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
p
(
famunion
X6
(
λX7 :
set
⇒
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
∧
SNoLe
X3
X6
)
)
→
(
¬
p
X2
)
)
→
(
(
(
p
X5
→
(
¬
p
∅
)
)
→
TransSet
X3
)
∧
(
(
SNo
X6
→
(
(
(
(
(
(
(
(
(
¬
p
X5
)
∧
(
¬
p
X5
)
)
→
(
¬
p
X5
)
)
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
¬
nat_p
(
Sep2
X6
(
λX7 :
set
⇒
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
(
λX7 :
set
⇒
λX8 :
set
⇒
atleast3
X5
)
)
)
)
∧
equip
X4
X5
)
∧
(
(
(
(
¬
SNoLt
X5
X6
)
∧
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
¬
p
X6
)
)
)
∧
ordinal
X5
)
∧
(
¬
p
X4
)
)
)
→
(
¬
SNoLt
X5
X5
)
)
∧
p
X5
)
)
∧
(
(
¬
p
X5
)
∧
TransSet
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
→
p
X3
)
)
∧
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
→
(
¬
equip
X5
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
¬
reflexive_i
(
λX7 :
set
⇒
λX8 :
set
⇒
atleast2
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
→
(
(
(
¬
p
X2
)
∧
(
(
(
(
(
(
¬
strictpartialorder_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
p
(
Inj0
X4
)
∧
(
(
¬
atleast6
X4
)
→
(
(
¬
p
X8
)
∧
(
¬
atleast5
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
)
→
(
(
(
¬
p
(
f
(
f
X6
)
)
)
→
(
¬
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
atleast2
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
p
X5
∧
(
¬
p
X6
)
)
→
(
¬
p
∅
)
)
→
p
∅
→
(
(
¬
p
X5
)
→
(
¬
ordinal
X5
)
→
(
¬
p
X2
)
)
→
(
¬
p
(
add_nat
X5
X5
)
)
)
)
→
(
¬
p
X5
)
)
)
∧
exactly2
X3
)
)
)
)
)
∧
atleast4
(
Unj
X4
)
)
)
)
In Proofgold the corresponding term root is
46ef63...
and proposition id is
6a5e70...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMLaAketNmGRoYKwURuF5Zgute9715hWJCX
)
∀X2 :
set
,
(
(
(
∃X3 :
set
,
(
(
∃X4 ∈
f
(
f
(
f
(
f
X3
)
)
)
,
(
exactly5
(
f
X3
)
∧
p
(
f
X3
)
)
→
p
X4
)
∧
(
(
¬
p
(
f
X2
)
)
→
(
∃X4 :
set
,
(
(
X4
⊆
X2
)
∧
(
(
antisymmetric_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
nat_p
X5
)
)
→
exactly4
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
∧
TransSet
X3
)
)
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
∀X3
∈
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
,
∀X4
⊆
X3
,
(
(
(
¬
p
(
Inj1
(
f
X2
)
)
)
∧
exactly3
(
setexp
(
Inj1
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
X2
)
)
∧
p
X3
)
)
)
In Proofgold the corresponding term root is
40ea7f...
and proposition id is
bfc876...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMWLLDvpuWN2oCWVjoR9DN4ayrdXLykgyWr
)
∀X2 :
set
,
(
(
(
∀X3
⊆
X2
,
p
X2
)
∧
(
¬
atleastp
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
X2
)
)
→
(
¬
p
X2
)
)
→
PNoLt
X2
(
λX3 :
set
⇒
∀X4
⊆
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
,
(
p
X3
∧
(
(
(
p
X4
→
(
¬
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
∧
(
(
(
¬
exactly5
X2
)
∧
atleast3
(
lam2
(
f
X3
)
(
λX5 :
set
⇒
X4
)
(
λX5 :
set
⇒
λX6 :
set
⇒
X4
)
)
)
→
p
X3
)
)
∧
(
¬
exactly5
X4
)
)
)
)
X2
(
λX3 :
set
⇒
∀X4
⊆
X3
,
(
(
(
¬
p
X3
)
∧
(
(
¬
equip
X2
(
f
X2
)
)
∧
(
(
¬
ordinal
X4
)
→
exactly5
X2
)
)
)
∧
p
(
f
X3
)
)
)
In Proofgold the corresponding term root is
d536a8...
and proposition id is
732812...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMWTB6hz7fpvZeU9nnH6ccjUEmLokkpHp8N
)
∃X2 ∈
famunion
(
SetAdjoin
(
binintersect
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
(
Inj1
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∅
)
(
λX3 :
set
⇒
X3
)
,
∃X3 :
set
,
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
In Proofgold the corresponding term root is
7672f7...
and proposition id is
22fc32...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMJY61Xne5gMsT2R6SoGE1dZ1G381nR7ybe
)
(
(
∀X2 :
set
,
(
∀X3
∈
X2
,
ordinal
(
Inj1
X2
)
)
→
(
∃X3 :
set
,
(
(
¬
atleast5
(
Inj1
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
∧
(
∃X4 :
set
,
(
(
¬
exactly5
X3
)
∧
totalorder_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
¬
nat_p
X4
)
→
(
¬
p
X5
)
)
→
exactly3
X5
)
)
)
)
)
)
→
(
(
∀X2 :
set
,
∃X3 :
set
,
(
(
(
p
(
f
X3
)
→
(
∀X4
⊆
X3
,
(
¬
ordinal
X2
)
→
(
¬
atleast2
X3
)
)
)
→
(
(
¬
exactly5
(
f
(
f
X3
)
)
)
→
(
∃X4 :
set
,
p
X3
)
)
→
p
X2
)
∧
(
(
∀X4 :
set
,
(
¬
TransSet
(
Inj1
X3
)
)
→
p
X3
)
→
(
∃X4 :
set
,
(
(
(
¬
exactly3
X4
)
→
(
p
(
f
∅
)
∧
(
¬
p
∅
)
)
)
∧
(
p
(
f
X2
)
∧
(
(
(
¬
p
(
binrep
(
UPair
(
f
∅
)
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
(
⋃
X4
)
)
)
∧
(
¬
atleast6
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
∧
exactly2
X2
)
)
)
)
)
)
)
∧
(
∃X2 :
set
,
∀X3 :
set
,
(
¬
atleast5
X3
)
→
(
(
(
∃X4 :
set
,
(
(
¬
atleast3
X3
)
∧
(
¬
p
X4
)
)
)
∧
(
∃X4 ∈
Inj0
(
f
(
f
X3
)
)
,
p
X2
)
)
∧
(
¬
atleast2
X2
)
)
)
)
)
→
exactly2
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
In Proofgold the corresponding term root is
173804...
and proposition id is
39c396...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMFrw98Z9CKJ33Bmkpg3GVQiCs3CuAQnyyx
)
(
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
∧
(
∀X2 :
set
,
∀X3
⊆
X2
,
∀X4
∈
X3
,
(
(
(
(
¬
set_of_pairs
X2
)
∧
(
(
¬
exactly2
X4
)
→
(
¬
p
X3
)
)
)
∧
(
¬
p
X3
)
)
∧
(
(
(
¬
p
X4
)
∧
p
X4
)
∧
(
¬
(
∅
∈
∅
)
)
)
)
→
exactly5
X3
)
)
In Proofgold the corresponding term root is
2f6f38...
and proposition id is
84f537...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMVD8ZHapwQ4grnEca8ak4dzaBe3FaQvdsq
)
(
(
∃X2 ∈
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
,
∃X3 :
set
,
(
(
¬
p
(
f
(
f
(
𝒫
(
f
X3
)
)
)
)
)
∧
(
∃X4 :
set
,
(
p
X4
→
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
(
TransSet
X3
∧
(
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
exactly5
X3
)
)
∧
exactly4
X4
)
)
)
)
)
→
atleast6
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
→
(
∀X2 :
set
,
(
∃X3 :
set
,
∀X4 :
set
,
(
¬
atleast3
X3
)
→
(
¬
p
X3
)
)
→
exactly4
X2
)
In Proofgold the corresponding term root is
86e855...
and proposition id is
64be5b...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMTUFamLkk9shVFirwRp3rmxtApAA81krcp
)
(
∃X2 :
set
,
(
(
X2
⊆
Sing
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
∀X3 :
set
,
exactly3
X2
→
(
(
∃X4 ∈
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
,
(
(
(
(
(
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
→
p
(
f
X4
)
)
→
(
(
(
(
(
(
(
¬
p
X4
)
→
(
(
(
(
¬
SNo
(
f
X2
)
)
→
(
(
set_of_pairs
X4
∧
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
∧
(
¬
p
(
f
X4
)
)
)
∧
(
p
X4
∧
(
(
(
p
(
f
∅
)
∧
(
(
(
(
∅
=
X3
)
→
(
(
exactly4
X3
→
(
¬
exactly2
X3
)
)
∧
(
atleast5
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
∧
(
¬
p
X4
)
)
)
)
∧
(
(
(
(
p
X3
∧
atleast6
X4
)
∧
(
(
(
exactly5
∅
∧
(
(
¬
p
X3
)
→
(
¬
exactly3
X3
)
→
(
¬
ordinal
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
(
(
(
atleast5
X4
∧
(
(
(
(
(
¬
ordinal
∅
)
∧
p
X2
)
∧
(
p
(
⋃
X3
)
→
(
(
¬
exactly5
(
f
(
f
X3
)
)
)
∧
(
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
∈
X2
)
∧
(
¬
p
X3
)
)
)
→
(
p
∅
∧
p
X3
)
)
)
→
(
(
(
exactly4
X2
∧
p
X3
)
∧
p
(
f
X3
)
)
∧
p
X3
)
)
→
p
X3
)
)
→
(
(
(
(
X3
∈
X3
)
∧
(
atleast2
X3
∧
p
X4
)
)
∧
(
¬
p
X4
)
)
∧
(
(
p
X4
→
(
p
(
f
X3
)
∧
(
¬
p
X3
)
)
→
(
(
(
¬
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
∧
(
(
¬
p
(
f
X4
)
)
∧
(
¬
p
X2
)
)
)
∧
(
¬
p
∅
)
)
)
∧
(
(
¬
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
¬
p
∅
)
)
)
)
)
∧
(
¬
p
X2
)
)
→
p
X2
)
)
→
(
¬
exactly3
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
)
→
(
set_of_pairs
∅
→
(
(
(
(
¬
atleast5
X4
)
∧
(
(
X4
=
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
∧
(
¬
p
X2
)
)
)
∧
(
(
X3
∈
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
→
(
(
¬
p
(
f
X4
)
)
∧
p
(
Sing
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
)
)
∧
(
(
p
X4
→
(
p
X4
∧
(
¬
p
∅
)
)
)
→
(
¬
p
(
setminus
X4
X3
)
)
)
)
)
→
(
¬
atleast5
X4
)
)
→
atleast6
∅
→
(
¬
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
→
(
¬
p
X3
)
)
)
∧
(
exactly5
X3
→
(
¬
exactly2
(
f
X3
)
)
→
(
(
¬
atleast5
X3
)
∧
(
¬
ordinal
X3
)
)
)
)
∧
(
(
(
p
X3
∧
(
(
(
p
X4
∧
(
¬
atleast3
X3
)
)
∧
(
(
¬
tuple_p
X4
X4
)
∧
(
nat_p
X4
→
(
p
X4
∧
(
¬
exactly4
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
→
(
¬
atleast4
X3
)
)
)
∧
(
ordinal
X2
→
(
¬
p
X3
)
)
)
→
(
(
¬
exactly5
∅
)
→
atleast4
X4
)
→
p
(
combine_funcs
(
f
(
f
X4
)
)
X4
(
λX5 :
set
⇒
X3
)
(
λX5 :
set
⇒
SetAdjoin
X3
X5
)
(
add_nat
(
binrep
(
Unj
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
X4
)
)
→
(
(
(
(
¬
p
X4
)
∧
(
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
atleast2
X2
)
)
∧
(
¬
exactly3
(
f
X4
)
)
)
)
→
p
X4
)
∧
(
(
(
(
p
X3
→
(
¬
p
X3
)
)
→
(
(
(
(
(
exactly3
X3
∧
(
(
p
X4
→
SNo
X3
)
→
(
X2
∈
f
X2
)
)
)
→
(
(
set_of_pairs
X3
∧
(
¬
atleast3
X4
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
exactly4
X4
)
∧
(
(
(
¬
nat_p
∅
)
∧
p
X4
)
∧
(
(
(
exactly2
X2
→
p
X3
)
∧
(
(
¬
atleast6
X4
)
→
(
(
(
(
(
(
(
¬
atleast5
X3
)
∧
(
exactly3
∅
∧
ordinal
(
proj1
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
¬
exactly3
X3
)
)
∧
p
(
f
X4
)
)
∧
(
(
p
X3
∧
(
(
p
(
f
X4
)
∧
(
p
X3
∧
(
(
¬
p
∅
)
→
p
X3
)
)
)
→
exactly3
X2
)
)
∧
(
¬
atleast6
X4
)
)
)
→
(
¬
ordinal
X3
)
→
nat_p
X3
→
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
p
X4
)
)
)
)
∧
(
(
¬
p
X3
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
→
(
atleast2
(
f
X3
)
∧
(
(
(
atleast3
X4
→
(
¬
TransSet
X3
)
)
→
(
(
exactly5
(
f
X4
)
→
(
¬
p
X3
)
)
→
(
¬
p
X3
)
)
→
(
¬
p
X3
)
)
→
atleast2
∅
)
)
)
)
)
)
∧
exactly5
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
∧
exactly2
∅
)
∧
p
X2
)
)
)
)
)
)
)
∧
p
(
f
∅
)
)
)
→
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
(
(
(
(
¬
p
(
f
X4
)
)
→
atleast2
X3
→
p
X4
→
setsum_p
X3
)
∧
(
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
∧
(
(
p
X4
→
(
¬
p
X4
)
)
∧
(
¬
p
X3
)
)
)
→
p
X4
→
(
set_of_pairs
X4
∧
p
X3
)
)
→
(
(
¬
p
(
f
(
Unj
(
f
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
∧
(
(
¬
p
X3
)
∧
(
(
(
exactly2
X4
∧
(
¬
p
(
f
X2
)
)
)
∧
(
(
¬
p
(
f
X4
)
)
→
(
(
(
(
¬
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
TransSet
X6
)
)
)
→
(
¬
nat_p
X3
)
)
∧
(
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
→
(
¬
set_of_pairs
(
Inj1
X2
)
)
)
∧
ordinal
X3
)
∧
binop_on
X2
(
λX5 :
set
⇒
λX6 :
set
⇒
X5
)
)
)
∧
(
(
(
¬
setsum_p
X3
)
∧
(
¬
atleast4
X3
)
)
→
(
¬
p
X3
)
)
)
)
)
∧
(
(
p
X3
∧
(
¬
p
(
f
X4
)
)
)
→
(
(
p
X2
∧
(
¬
tuple_p
X4
X4
)
)
∧
(
(
¬
p
(
f
X2
)
)
→
(
¬
p
X3
)
→
(
¬
p
X4
)
)
)
)
)
)
)
→
(
¬
p
X2
)
)
)
→
eqreln_i
(
λX5 :
set
⇒
λX6 :
set
⇒
p
X6
→
atleast2
X6
→
(
¬
p
X6
)
)
)
→
(
p
X3
∧
(
(
¬
exactly2
(
V_
X3
)
)
∧
(
¬
atleast5
(
⋃
(
f
∅
)
)
)
)
)
)
∧
TransSet
X3
)
→
transitive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
atleastp
X2
∅
→
(
(
¬
atleast2
X6
)
∧
p
X5
)
)
→
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
(
¬
p
X3
)
)
)
)
∧
(
¬
p
X4
)
)
∧
(
(
(
(
(
¬
TransSet
(
f
X4
)
)
∧
(
(
¬
atleast4
X2
)
→
(
(
(
atleast2
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
→
p
X3
)
→
(
(
(
exactly4
(
f
X3
)
→
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
p
X4
)
∧
p
X3
)
)
∧
setsum_p
X4
)
→
(
¬
nat_p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
→
(
p
(
f
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
¬
p
X4
)
∧
(
¬
p
X4
)
)
)
)
→
p
X4
→
(
(
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
∧
(
¬
p
X3
)
)
∧
(
¬
p
X3
)
)
)
∧
p
X4
)
)
∧
setsum_p
X4
)
∧
(
¬
p
X3
)
)
→
(
(
(
(
p
X3
→
(
atleast5
X2
∧
(
(
¬
TransSet
X3
)
→
exactly5
X4
)
)
)
∧
(
¬
SNo
X2
)
)
∧
(
¬
exactly5
(
⋃
X3
)
)
)
∧
p
X4
)
)
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
→
p
X2
→
(
(
¬
p
X3
)
∧
(
(
(
(
atleast5
X3
→
(
(
(
¬
p
X3
)
→
(
¬
exactly2
X3
)
)
∧
(
p
(
proj1
X4
)
→
(
¬
exactly3
X4
)
)
)
)
∧
p
X2
)
∧
(
¬
atleast5
∅
)
)
∧
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
¬
ordinal
(
f
∅
)
)
→
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
)
)
)
)
→
(
p
∅
∧
(
p
X3
∧
TransSet
∅
)
)
)
∧
(
(
¬
nat_p
X4
)
→
(
¬
p
∅
)
)
)
)
→
(
∃X4 :
set
,
(
(
X4
⊆
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
∧
(
¬
atleast2
(
f
X2
)
)
)
)
)
→
(
∀X4
⊆
∅
,
(
¬
p
X3
)
)
)
)
)
→
ordinal
(
Inj0
∅
)
In Proofgold the corresponding term root is
44d6e2...
and proposition id is
6db6a4...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMUi6PEigN1f7kSQiHvZw7SoL8Qnt9Szn6o
)
∀X2
⊆
Sing
(
SNoLev
(
f
(
⋃
(
f
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
)
,
(
∀X3
∈
X2
,
∀X4 :
set
,
(
(
¬
atleast3
(
f
(
f
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
→
(
nat_p
X3
∧
(
¬
(
X3
=
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
)
→
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
→
(
(
(
(
(
(
(
(
¬
p
X4
)
→
p
X3
)
∧
atleast3
(
f
X2
)
)
→
atleast2
X3
)
→
(
(
¬
setsum_p
X3
)
∧
(
(
¬
p
X3
)
→
p
(
proj1
X3
)
)
)
)
→
(
¬
atleast4
X3
)
→
atleast2
X3
)
→
(
(
(
(
¬
exactly4
X2
)
∧
(
¬
antisymmetric_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
(
(
(
(
SNo
X5
→
atleast2
X6
)
∧
(
¬
p
(
f
X5
)
)
)
→
(
(
¬
p
X5
)
∧
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
∧
(
(
(
(
(
(
(
¬
exactly4
(
Inj1
X6
)
)
→
(
¬
p
X4
)
)
∧
(
(
¬
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
p
X4
)
)
→
(
¬
p
(
nat_primrec
X6
(
λX7 :
set
⇒
λX8 :
set
⇒
X8
)
X6
)
)
→
(
¬
p
X6
)
)
∧
(
(
(
¬
ordinal
X4
)
→
(
exactly3
X6
→
(
¬
p
X5
)
)
→
(
p
X6
∧
(
(
(
(
¬
exactly2
X4
)
∧
(
(
¬
p
X5
)
→
p
X6
)
)
∧
p
(
setsum
∅
X6
)
)
∧
(
¬
nat_p
X2
)
)
)
)
→
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
→
(
(
(
(
¬
p
X3
)
∧
(
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
p
X4
∧
(
¬
atleast4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
∧
(
p
X6
→
atleast4
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
(
(
(
¬
atleast2
X5
)
→
(
(
(
(
¬
p
X6
)
→
exactly4
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
(
(
(
¬
exactly4
X6
)
→
p
X6
)
∧
(
¬
p
X3
)
)
→
SNo
X4
)
→
atleast4
X6
)
→
(
¬
nat_p
X6
)
)
)
∧
(
(
¬
exactly2
X2
)
→
set_of_pairs
∅
→
(
(
p
∅
∧
(
¬
atleast6
X5
)
)
∧
(
(
¬
p
X6
)
∧
(
¬
set_of_pairs
X6
)
)
)
)
)
)
→
atleast3
X6
)
∧
(
atleast3
X5
∧
(
(
¬
setsum_p
X6
)
→
(
¬
TransSet
X6
)
)
)
)
)
→
atleast2
X3
)
→
p
X6
)
)
∧
(
(
p
X3
∧
(
(
(
¬
exactly3
X5
)
→
(
(
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
→
(
(
¬
p
X5
)
∧
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
∧
(
¬
p
X6
)
)
)
∧
(
(
(
(
¬
atleast4
X5
)
∧
(
(
atleast5
X5
∧
(
(
(
¬
p
X6
)
→
(
¬
nat_p
X6
)
→
p
(
If_i
(
(
p
X5
∧
(
(
¬
p
X2
)
→
(
(
(
p
X6
∧
(
¬
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
→
p
X6
)
→
(
¬
SNo
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
→
(
¬
atleast2
(
f
∅
)
)
)
→
(
atleastp
(
f
X6
)
X5
∧
(
¬
p
X6
)
)
)
)
→
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∅
X5
)
)
→
(
¬
p
X6
)
→
p
X2
)
)
→
(
atleast6
X5
∧
p
(
f
(
Pi
X5
(
λX7 :
set
⇒
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
∧
(
¬
(
SNoLev
X2
=
X6
)
)
)
→
p
(
Inj0
X5
)
)
)
)
∧
(
(
¬
p
X5
)
→
(
¬
p
X5
)
)
)
)
→
(
¬
(
X5
∈
UPair
∅
(
Inj1
X5
)
)
)
)
)
∧
(
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
∧
p
∅
)
)
)
)
)
∧
p
X2
)
∧
(
p
(
f
X3
)
→
(
¬
p
X3
)
)
)
)
∧
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
)
→
(
(
∃X3 :
set
,
(
(
∃X4 ∈
f
(
f
X2
)
,
(
¬
ordinal
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
(
∀X4 :
set
,
(
p
X3
∧
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
exactly5
X4
)
→
(
p
(
f
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
∧
(
p
X4
→
atleast4
∅
)
)
)
→
(
∃X4 :
set
,
(
atleast2
∅
∧
SNoLt
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
X4
)
)
→
(
¬
p
X2
)
)
→
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
→
(
∀X4
⊆
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
,
(
¬
reflexive_i
(
λX5 :
set
⇒
λX6 :
set
⇒
(
¬
p
X2
)
→
(
¬
atleast6
X5
)
)
)
)
)
∧
(
∃X4 :
set
,
(
(
¬
equip
∅
X3
)
∧
(
¬
exactly2
(
f
X4
)
)
)
)
)
)
)
→
(
∃X3 :
set
,
(
(
∃X4 ∈
X3
,
(
nat_p
∅
∧
(
(
¬
exactly2
X4
)
∧
(
(
(
(
(
p
X4
→
p
X4
)
→
(
(
(
p
X4
→
(
¬
ordinal
X4
)
→
p
X3
)
∧
(
(
(
¬
atleast5
X3
)
∧
(
(
(
(
p
X3
→
(
(
(
(
(
¬
exactly5
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
¬
p
(
SNoLev
X2
)
)
)
→
(
(
¬
p
X4
)
∧
(
p
X4
→
(
(
(
¬
p
X2
)
∧
(
¬
p
∅
)
)
∧
(
¬
atleast4
(
Sing
X4
)
)
)
)
)
)
∧
p
X3
)
∧
(
(
p
∅
→
(
¬
ordinal
X4
)
)
→
(
¬
tuple_p
X2
X3
)
)
)
)
∧
(
(
¬
p
X3
)
∧
p
X3
)
)
→
p
(
f
X3
)
)
∧
(
¬
TransSet
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
→
p
X4
)
)
∧
(
¬
nat_p
X2
)
)
→
(
¬
(
X2
⊆
X3
)
)
)
∧
(
(
(
(
¬
SNo_
∅
(
f
(
f
X3
)
)
)
∧
(
X3
⊆
X3
)
)
∧
(
(
(
¬
TransSet
∅
)
→
p
∅
)
→
p
∅
)
)
→
TransSet
X2
)
)
∧
(
¬
ordinal
X3
)
)
∧
(
¬
setsum_p
X4
)
)
)
)
)
∧
(
∃X4 :
set
,
(
(
X4
⊆
X2
)
∧
(
ordinal
X2
∧
p
X4
)
)
)
)
)
)
→
(
∀X3 :
set
,
∀X4
⊆
X3
,
(
(
p
X4
→
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
In Proofgold the corresponding term root is
b1cdd6...
and proposition id is
fe1590...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMPCiuyy6Tv8QvQxbcPbj2DcuYQjjRRhatc
)
∃X2 :
set
,
(
(
X2
⊆
f
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
∃X3 :
set
,
(
(
(
∃X4 ∈
f
(
f
(
f
∅
)
)
,
p
X3
)
→
(
¬
p
X3
)
)
∧
(
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
∧
(
¬
p
(
f
X2
)
)
)
)
)
→
(
¬
exactly2
(
ordsucc
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
)
)
)
∧
(
∀X3 :
set
,
(
∃X4 ∈
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
,
(
(
p
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
∧
(
¬
p
X4
)
)
∧
(
atleast6
X4
→
nat_p
(
f
∅
)
)
)
→
(
¬
p
X4
)
)
→
p
X2
)
)
)
In Proofgold the corresponding term root is
edf9a9...
and proposition id is
91810d...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMP7zpTxFP9DDvFw3a4Nh61KhRi99NyBCdH
)
∃X2 :
set
,
∀X3
∈
f
(
f
X2
)
,
(
(
∃X4 ∈
In_rec_i
(
λX5 :
set
⇒
λX6 :
set
→
set
⇒
X3
)
(
f
X3
)
,
p
X4
)
→
(
∀X4
∈
X3
,
(
¬
p
X4
)
)
)
→
(
∃X4 ∈
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
X2
,
(
(
(
(
(
(
(
exactly2
X3
∧
(
¬
atleast4
(
f
X4
)
)
)
→
exactly3
X4
)
→
(
(
¬
p
X2
)
∧
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
→
(
exactly5
X2
∧
(
(
¬
(
X2
⊆
X4
)
)
→
p
X3
)
)
)
∧
(
(
(
(
(
¬
p
X4
)
∧
(
ordinal
(
f
X2
)
→
(
(
p
X3
→
exactly3
∅
)
∧
p
X3
)
)
)
→
(
(
(
(
(
¬
atleast2
X2
)
∧
exactly5
X3
)
→
(
¬
atleast4
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
¬
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
∈
ordsucc
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
)
∧
p
(
f
∅
)
)
)
∧
(
(
¬
atleast3
(
f
X4
)
)
→
setsum_p
X4
→
(
¬
exactly2
X4
)
)
)
→
nat_p
X2
)
)
∧
(
(
p
X3
∧
(
¬
exactly4
X2
)
)
→
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
)
∧
(
(
¬
p
X2
)
∧
exactly4
X3
)
)
)
In Proofgold the corresponding term root is
58516b...
and proposition id is
6bde7f...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMaTZuCoTx1hfdPahzXbWdvfDKa4LcwuhHF
)
∃X2 ∈
f
(
f
(
f
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
)
,
(
(
¬
p
X2
)
∧
(
∀X3
∈
X2
,
∀X4
⊆
X2
,
(
p
X3
→
(
(
¬
p
X3
)
∧
p
X2
)
→
(
exactly5
X4
→
(
¬
ordinal
(
f
X4
)
)
→
exactly3
(
f
X4
)
)
→
(
¬
exactly5
X3
)
→
(
¬
set_of_pairs
∅
)
)
→
exactly2
X2
)
)
In Proofgold the corresponding term root is
fe1117...
and proposition id is
553cb9...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMZXRW7zibDFmC6NZuJKGwJxkcAGMAKd3ER
)
(
exactly3
(
f
∅
)
∧
(
∃X2 :
set
,
∀X3 :
set
,
(
∃X4 :
set
,
(
(
(
p
X3
→
atleast3
X4
→
(
¬
p
X4
)
)
→
exactly5
X3
→
(
(
(
(
p
(
f
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
p
X3
)
→
p
∅
)
→
p
X4
)
∧
(
(
p
X2
∧
nat_p
∅
)
∧
(
exactly2
(
SNoElts_
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
¬
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
→
p
X3
)
)
)
)
∧
(
ordinal
∅
→
atleast4
X3
)
)
)
→
(
(
TransSet
(
f
(
Inj0
∅
)
)
∧
exactly5
X2
)
∧
(
(
∀X4 :
set
,
(
(
¬
ordinal
∅
)
∧
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
→
(
(
¬
atleast5
X3
)
∧
(
(
p
X3
∧
p
X3
)
∧
(
¬
(
X3
=
X2
)
)
)
)
)
→
(
¬
(
X3
=
X4
)
)
)
)
)
→
(
∀X4
∈
f
X2
,
p
X4
)
→
atleast3
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
→
(
∀X4
∈
f
X3
,
(
(
PNo_upc
(
λX5 :
set
⇒
λX6 :
set
→
prop
⇒
(
(
(
X6
X3
∧
p
(
f
∅
)
)
∧
atleast2
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
(
p
X5
∧
X6
X5
)
→
nat_p
X4
)
)
)
X3
(
λX5 :
set
⇒
p
X3
)
→
(
¬
p
X3
)
→
p
X3
→
p
(
f
X2
)
→
(
¬
p
∅
)
)
∧
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
)
)
)
)
In Proofgold the corresponding term root is
b36b33...
and proposition id is
870347...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMFsvdcRLDCSVfJPfGxxAKDnme8ppV7NWB4
)
∃X2 ∈
f
(
Inj0
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
,
∀X3
∈
f
X2
,
(
(
¬
p
X3
)
∧
(
∀X4 :
set
,
p
(
UPair
∅
X4
)
→
(
X4
∈
∅
)
→
(
¬
exactly3
X2
)
)
)
In Proofgold the corresponding term root is
1bbd21...
and proposition id is
5946f7...
Proof:
The rest of this subproof is missing.
∎
Theorem.
(
conj_Random2_TMW6eLRc5zbuwV3GcNosifHXyMRAtZqP9RT
)
∃X2 :
set
,
(
(
∃X3 ∈
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
,
∃X4 :
set
,
(
(
(
p
∅
∧
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
∧
(
(
¬
(
X3
∈
X4
)
)
∧
(
(
(
(
(
setsum_p
X3
∧
ordinal
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
→
atleast6
(
f
(
f
X3
)
)
)
→
(
equip
X3
(
f
X2
)
∧
(
¬
PNoEq_
X2
(
λX5 :
set
⇒
(
(
p
(
f
X5
)
∧
(
(
(
(
¬
atleast2
X3
)
∧
(
(
(
(
atleast5
X3
∧
p
X4
)
→
(
¬
p
X5
)
)
∧
exactly2
X3
)
→
(
¬
exactly3
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
∧
(
(
(
¬
exactly4
X5
)
→
atleast2
X5
)
∧
(
(
¬
ordinal
(
Inj0
X5
)
)
∧
atleast3
∅
)
)
)
∧
(
p
X3
→
(
(
(
(
¬
tuple_p
X5
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
(
(
(
¬
atleast4
(
V_
(
f
X5
)
)
)
→
(
¬
nat_p
∅
)
)
→
(
¬
exactly4
X4
)
)
→
(
¬
p
X3
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
(
(
(
(
p
X4
∧
p
X3
)
∧
p
(
Sep
X4
(
λX6 :
set
⇒
(
(
¬
TransSet
X5
)
∧
p
X6
)
)
)
)
→
(
(
(
(
(
(
(
¬
p
(
UPair
X4
X4
)
)
→
(
¬
p
∅
)
)
∧
p
X4
)
→
(
¬
SNo_
X4
∅
)
→
(
¬
p
X5
)
→
(
¬
p
X3
)
→
(
p
X4
∧
(
(
(
(
(
(
¬
exactly4
X5
)
→
p
X4
→
(
¬
p
X5
)
)
→
(
¬
p
X4
)
)
∧
(
(
¬
p
∅
)
∧
(
(
(
(
(
(
(
(
atleast5
X4
∧
p
X5
)
∧
(
(
(
¬
exactly2
X5
)
∧
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
→
(
(
(
¬
p
X5
)
∧
(
¬
p
X5
)
)
∧
exactly5
X4
)
)
∧
(
exactly2
∅
∧
exactly5
X5
)
)
)
∧
(
(
(
(
(
(
(
¬
ordinal
∅
)
→
(
(
(
(
(
p
X4
→
(
(
exactly2
X4
∧
(
p
X5
∧
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
¬
p
(
setsum
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
X5
)
)
)
)
)
→
(
¬
p
X4
)
)
→
atleast4
(
⋃
X4
)
)
→
atleast5
X5
)
→
(
¬
p
(
f
∅
)
)
)
→
set_of_pairs
X5
→
atleast3
(
f
∅
)
)
∧
atleast6
X5
)
)
∧
(
(
¬
p
X4
)
∧
(
SNo
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
¬
p
X3
)
→
(
(
exactly4
(
f
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
∅
)
)
→
(
(
p
X4
∧
(
(
¬
ordinal
∅
)
→
(
(
¬
p
X4
)
∧
(
¬
p
X5
)
)
→
atleast4
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
)
)
∧
(
¬
TransSet
X3
)
)
)
∧
p
X3
)
)
∧
(
(
¬
p
X5
)
∧
(
(
¬
p
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
)
∧
(
p
X5
∧
p
X5
)
)
)
)
)
)
)
→
(
¬
atleast6
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
p
X4
)
→
(
(
p
X3
∧
TransSet
X5
)
∧
(
(
¬
nat_p
X5
)
∧
(
atleast4
X5
∧
(
¬
p
X5
)
)
)
)
)
∧
p
X2
)
∧
(
(
(
(
p
X5
→
(
¬
eqreln_i
(
λX6 :
set
⇒
λX7 :
set
⇒
p
X6
→
p
(
setsum
X7
X7
)
)
)
→
(
¬
nat_p
X4
)
)
∧
p
X4
)
→
(
p
X4
→
(
(
¬
reflexive_i
(
λX6 :
set
⇒
λX7 :
set
⇒
(
¬
atleast2
X5
)
)
)
∧
(
(
exactly4
X5
→
(
¬
p
X3
)
→
atleast6
X3
)
∧
p
X4
)
)
)
→
(
¬
PNoLt_
(
f
(
f
X5
)
)
(
λX6 :
set
⇒
(
(
TransSet
X5
→
(
¬
p
∅
)
)
∧
(
SNo
X6
∧
(
¬
ordinal
X5
)
)
)
)
(
λX6 :
set
⇒
(
¬
exactly3
X4
)
)
)
→
atleast6
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
→
p
X5
)
)
)
)
→
(
(
p
X4
→
p
X4
)
∧
(
(
(
(
(
¬
p
(
f
X5
)
)
∧
(
¬
atleast2
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
nat_p
(
f
X5
)
)
→
(
¬
p
X3
)
)
∧
(
(
(
(
p
X3
∧
(
¬
atleast5
X5
)
)
→
(
(
(
¬
p
X5
)
∧
(
¬
exactly1of3
(
p
X4
)
(
¬
ordinal
X4
)
(
p
(
Sing
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
∧
(
¬
ordinal
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
∧
(
(
(
¬
strictpartialorder_i
(
λX6 :
set
⇒
λX7 :
set
⇒
p
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
p
X3
)
∧
(
(
(
(
(
¬
nat_p
X5
)
∧
(
(
p
X4
∧
(
strictpartialorder_i
(
λX6 :
set
⇒
λX7 :
set
⇒
p
X7
)
→
(
(
(
(
¬
(
X2
∈
f
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
∧
(
(
(
¬
exactly2
X5
)
∧
(
(
(
¬
p
X3
)
∧
(
(
(
(
(
¬
(
X4
∈
X4
)
)
∧
(
ordinal
X5
→
(
(
(
¬
exactly5
∅
)
→
exactly3
X5
)
∧
atleast6
X5
)
)
)
→
p
X3
→
atleast4
X5
)
→
(
(
(
(
¬
p
X3
)
→
(
¬
p
∅
)
→
(
X3
⊆
f
(
𝒫
X3
)
)
)
∧
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
(
¬
ordinal
X5
)
∧
(
nat_p
X5
→
setsum_p
X4
)
)
)
)
∧
(
(
(
(
(
(
(
¬
p
X3
)
→
exactly2
X5
)
∧
nat_p
∅
)
∧
(
(
(
¬
ordinal
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
∧
(
(
(
¬
p
X5
)
∧
(
¬
TransSet
X3
)
)
∧
(
(
¬
p
∅
)
→
(
(
(
(
¬
exactly2
X4
)
→
nat_p
X4
→
(
¬
TransSet
X4
)
)
→
(
¬
exactly5
X3
)
)
∧
(
(
¬
p
X5
)
→
(
¬
exactly2
(
f
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
)
)
)
)
)
)
∧
p
X4
)
)
∧
(
(
p
X5
∧
(
¬
p
X2
)
)
∧
(
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
∧
(
p
(
f
(
f
X4
)
)
→
(
(
¬
p
X5
)
→
(
¬
atleast4
X5
)
)
→
(
(
¬
TransSet
X5
)
∧
(
atleast5
∅
→
(
(
(
¬
p
X4
)
→
(
¬
p
X4
)
)
∧
(
(
(
(
¬
exactly4
X2
)
→
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
∧
(
(
¬
SNo
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
∧
(
(
(
(
SNo
X5
→
(
p
X4
∧
(
¬
p
X4
)
)
)
→
(
¬
reflexive_i
(
λX6 :
set
⇒
λX7 :
set
⇒
p
X6
)
)
)
→
(
¬
exactly3
X4
)
)
→
(
(
(
(
¬
nat_p
(
Sep
X4
(
λX6 :
set
⇒
(
(
¬
p
X6
)
∧
(
exactly1of2
(
exactly2
X2
)
(
exactly3
X5
→
(
(
(
(
¬
atleast2
X5
)
∧
(
(
p
X6
∧
p
X5
)
→
p
X5
)
)
∧
(
(
(
p
X6
→
(
(
(
¬
exactly3
X6
)
→
(
¬
atleast2
X3
)
→
(
(
¬
stricttotalorder_i
(
λX7 :
set
⇒
λX8 :
set
⇒
(
(
p
X5
→
atleast2
X8
)
∧
(
(
(
(
(
¬
atleast5
(
ap
X8
X7
)
)
→
atleast6
X7
)
∧
(
(
p
X8
∧
(
(
¬
p
∅
)
→
(
¬
SNo
X7
)
)
)
∧
atleast2
(
Sing
X7
)
)
)
∧
(
¬
p
X7
)
)
→
p
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
∧
(
(
¬
atleast6
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
)
∧
p
X5
)
)
)
→
(
¬
atleast5
X6
)
)
→
ordinal
X5
)
→
p
(
f
X2
)
)
∧
(
(
(
(
(
(
p
X5
∧
(
¬
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
→
atleast4
X4
)
∧
(
(
p
(
Inj0
(
f
(
f
X6
)
)
)
∧
(
(
(
¬
p
X5
)
∧
(
(
(
(
¬
nat_p
∅
)
∧
(
¬
p
X2
)
)
→
(
¬
p
X5
)
)
∧
(
¬
TransSet
X5
)
)
)
∧
exactly2
X6
)
)
→
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
→
p
X5
)
∧
(
(
(
(
(
¬
ordinal
X3
)
→
(
¬
p
X6
)
)
→
p
X5
)
∧
(
(
¬
p
(
binrep
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
(
atleast5
X4
→
(
(
p
X6
→
(
¬
p
X5
)
)
∧
(
¬
set_of_pairs
X5
)
)
→
(
¬
exactly2
(
Inj0
X6
)
)
)
∧
(
¬
p
X5
)
)
)
)
∧
(
¬
SNo
X5
)
)
)
∧
(
¬
exactly2
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
¬
atleast6
X5
)
)
)
∧
(
¬
p
X5
)
)
)
)
)
)
∧
(
(
p
X4
→
PNoLt_
X5
(
λX6 :
set
⇒
(
atleast2
X5
∧
(
atleast6
X3
→
(
¬
p
∅
)
)
)
)
(
λX6 :
set
⇒
(
X5
∈
X6
)
)
)
→
p
X5
)
)
∧
(
SNo
X5
∧
(
¬
set_of_pairs
X4
)
)
)
∧
(
(
¬
exactly2
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
→
exactly2
(
Sing
X2
)
→
(
(
(
¬
p
X2
)
→
exactly4
X4
)
→
(
(
¬
setsum_p
(
setminus
(
f
∅
)
X4
)
)
∧
(
(
¬
p
X4
)
→
(
¬
p
∅
)
)
)
)
→
(
¬
atleast4
(
Sing
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
)
)
)
)
)
)
∧
(
(
¬
TransSet
X2
)
→
(
atleast4
X4
∧
(
¬
setsum_p
X4
)
)
)
)
)
)
)
→
(
(
(
¬
atleast5
X4
)
∧
(
¬
p
X4
)
)
∧
(
(
¬
equip
(
proj0
(
binrep
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∅
)
)
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
∧
(
¬
atleast3
X4
)
)
)
)
)
)
)
∧
p
X3
)
∧
(
¬
atleast4
∅
)
)
)
→
(
(
p
X4
∧
exactly2
X5
)
∧
(
p
X5
→
atleast4
X3
)
)
→
(
¬
atleast6
(
f
X4
)
)
)
→
atleast5
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
→
p
X2
)
)
∧
(
(
(
(
(
p
X5
→
atleast3
X3
)
→
(
¬
trichotomous_or_i
(
λX6 :
set
⇒
λX7 :
set
⇒
(
(
(
¬
exactly2
X6
)
∧
(
¬
p
X7
)
)
∧
(
(
(
(
atleast4
X4
∧
(
¬
atleast6
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
→
(
¬
p
∅
)
→
(
¬
p
(
f
(
f
X7
)
)
)
)
→
(
(
(
¬
exactly5
X6
)
∧
(
¬
TransSet
X6
)
)
∧
(
¬
p
X7
)
)
)
→
(
¬
p
X7
)
)
)
)
)
→
(
p
X3
→
p
(
setminus
X2
X4
)
)
→
(
(
¬
exactly5
X3
)
∧
p
X4
)
)
∧
(
¬
p
X3
)
)
→
(
(
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
→
(
¬
p
X4
)
)
∧
atleast4
X5
)
→
(
(
¬
exactly5
X4
)
∧
exactly4
X5
)
)
∧
(
nat_p
X5
→
(
(
TransSet
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∧
(
(
SNo
∅
∧
p
X3
)
∧
(
(
(
(
¬
TransSet
(
lam2
(
f
∅
)
(
λX6 :
set
⇒
X6
)
(
λX6 :
set
⇒
λX7 :
set
⇒
X6
)
)
)
∧
(
(
(
(
(
¬
p
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
¬
p
X4
)
)
→
(
¬
p
X4
)
)
→
(
(
(
(
(
(
(
(
¬
atleast4
X4
)
∧
(
(
¬
p
∅
)
∧
exactly2
X5
)
)
→
exactly5
X5
)
∧
(
(
(
¬
p
X5
)
→
(
(
p
X4
∧
(
atleast3
(
binrep
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∧
(
(
¬
p
X5
)
∧
(
(
(
(
¬
ordinal
X2
)
∧
(
(
(
p
X4
→
p
X5
→
(
(
p
(
setsum
X4
X3
)
∧
(
(
(
(
(
(
p
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
∧
(
¬
atleast5
X5
)
)
∧
(
(
(
p
(
f
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
)
→
(
(
(
(
exactly5
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
∧
(
(
¬
p
X4
)
∧
p
X2
)
)
→
(
¬
atleast2
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
)
)
→
exactly3
X4
→
p
X4
)
→
(
(
(
p
(
Sing
X5
)
→
(
(
(
(
¬
p
X4
)
→
(
¬
p
X5
)
)
→
(
¬
p
(
f
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
(
(
(
¬
TransSet
X5
)
∧
atleast2
X5
)
∧
(
p
X4
∧
p
X4
)
)
)
)
→
(
(
(
(
(
p
X4
∧
(
¬
p
∅
)
)
→
(
(
ordinal
X5
∧
(
(
(
p
X5
∧
(
(
(
¬
TransSet
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
¬
p
(
f
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
)
∧
transitive_i
(
λX6 :
set
⇒
λX7 :
set
⇒
SNo
(
f
(
V_
X7
)
)
)
)
)
→
(
TransSet
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
(
𝒫
∅
)
)
∧
(
¬
p
∅
)
)
)
∧
p
(
f
X5
)
)
)
∧
p
∅
)
)
→
(
¬
p
X5
)
)
∧
p
X5
)
∧
(
(
¬
p
X4
)
∧
(
ordinal
X5
∧
(
(
¬
exactly2
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
→
p
(
binrep
X3
(
binrep
X5
X2
)
)
→
(
¬
ordinal
X4
)
→
(
¬
p
X5
)
)
)
)
)
)
∧
(
(
¬
p
X4
)
→
(
¬
exactly4
(
f
∅
)
)
)
)
)
→
trichotomous_or_i
(
λX6 :
set
⇒
λX7 :
set
⇒
atleast2
X6
)
)
∧
atleast3
X3
)
→
(
¬
exactly3
X4
)
)
)
∧
(
(
¬
exactly3
X5
)
∧
(
(
(
¬
atleast3
X4
)
∧
(
(
(
¬
p
(
f
X3
)
)
∧
p
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
∅
)
)
∅
)
)
→
(
(
exactly4
X4
→
(
¬
reflexive_i
(
λX6 :
set
⇒
λX7 :
set
⇒
(
¬
p
X6
)
)
)
)
∧
(
(
p
X4
∧
(
¬
p
X5
)
)
∧
p
(
f
X3
)
)
)
→
(
¬
exactly5
X3
)
)
)
∧
(
(
¬
ordinal
X2
)
∧
(
(
exactly3
(
binrep
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
(
𝒫
∅
)
)
∧
(
(
¬
totalorder_i
(
λX6 :
set
⇒
λX7 :
set
⇒
atleast4
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
∅
)
)
)
∧
(
(
p
X4
→
(
(
(
¬
p
X4
)
→
atleast3
X4
)
→
(
PNoLt
(
binrep
(
binrep
(
𝒫
(
binrep
(
𝒫
(
𝒫
∅
)
)
∅
)
)
(
𝒫
(
𝒫
∅
)
)
)
∅
)
(
λX6 :
set
⇒
(
(
¬
exactly2
X3
)
∧
(
¬
exactly3
(
𝒫
(
𝒫
(
𝒫
(
𝒫
∅
)
)
)
)
)
)
→
(
(
(
(
(
(
(
(
(
(
(
(
(
¬
atleast5
X2
)
→
(
¬
p
X3
)
→
(
¬
p
X5
)
)
→
(
¬
p
X5
)
)
∧
p
X4
)
∧
(
(
(
(
(
equip
X6
(