Beginning of Section Random2
Variable p : set β prop
Variable f : set β set
Proof: Proof not loaded.
Proof: Proof not loaded.
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))))))))
Proof: Proof not loaded.
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 (π« (π« β
)) β
)) (π« β
)) β
)))))
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
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 (π« (π« β
)) β
)))))
Proof: Proof not loaded.
Proof: Proof not loaded.
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)))
Proof: Proof not loaded.
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 (π« (π« β
)) β
)) (π« (π« β
))))))))))
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
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 (π« (π« (π« (π« β
)))) (π« β
)) β
)))))
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
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 (π« (π« (π« (π« β
)))) (π« β
)) β
)
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
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 (π« (π« β
)) β
)) β
)))
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.
Proof: Proof not loaded.