Beginning of Section
Random2
(*** $T hf ***)
(*** $I sig/PfgPreambleSep2020.mgs ***)
L4
Variable
p :
set
β
prop
L6
Variable
f :
set
β
set
L7
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:
Load proof
Proof not loaded.
L11
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:
Load proof
Proof not loaded.
L15
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:
Load proof
Proof not loaded.
L19
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:
Load proof
Proof not loaded.
L23
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:
Load proof
Proof not loaded.
L27
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:
Load proof
Proof not loaded.
L31
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:
Load proof
Proof not loaded.
L35
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:
Load proof
Proof not loaded.
L39
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:
Load proof
Proof not loaded.
L43
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:
Load proof
Proof not loaded.
L47
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:
Load proof
Proof not loaded.
L51
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:
Load proof
Proof not loaded.
L55
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:
Load proof
Proof not loaded.
L59
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:
Load proof
Proof not loaded.
L63
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:
Load proof
Proof not loaded.
L67
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:
Load proof
Proof not loaded.
L71
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:
Load proof
Proof not loaded.
L75
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:
Load proof
Proof not loaded.
L79
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:
Load proof
Proof not loaded.
L83
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:
Load proof
Proof not loaded.
L87
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:
Load proof
Proof not loaded.
L91
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:
Load proof
Proof not loaded.
L95
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:
Load proof
Proof not loaded.
L99
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:
Load proof
Proof not loaded.
L103
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:
Load proof
Proof not loaded.
L107
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:
Load proof
Proof not loaded.
L111
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:
Load proof
Proof not loaded.
L115
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:
Load proof
Proof not loaded.
L119
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:
Load proof
Proof not loaded.
L123
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:
Load proof
Proof not loaded.
L127
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:
Load proof
Proof not loaded.
L131
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
(