Proofgold Signed Transaction

Param nat_p^nat_p : ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known 07015.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . nat_p x2 ⟶ equip x0 (ordsucc x2) ⟶ ∀ x3 . equip x3 x2 ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x6 x5 ⟶ x6 = x4 x5) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (∀ x7 . x7 ∈ x3 ⟶ not (x1 x6 x7)) ⟶ x5) ⟶ x5
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param atleastp^atleastp : ι → ι → ο
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param binintersect^binintersect : ι → ι → ι
Param Sep^Sep : ι → (ι → ο) → ι
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3 ⟶ ∀ x4 : ο . x4) (x1 x2 x3)}
Param setminus^setminus : ι → ι → ι
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Known 05419.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . nat_p x2 ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4) ⟶ or (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) x2) (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) (ordsucc x2))) ⟶ ∀ x3 x4 . x3 ∈ x0 ⟶ x4 ∈ DirGraphOutNeighbors x0 x1 x3 ⟶ (∀ x5 . x5 ∈ {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) x2} ⟶ not (x1 x4 x5)) ⟶ binunion (setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (setminus {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) (ordsucc x2)} (setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3))) = {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) (ordsucc x2)}
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Param add_nat^add_nat : ι → ι → ι
Known 8bf56.. : ∀ x0 x1 x2 x3 x4 . binunion x0 x1 = x2 ⟶ (∀ x5 . x5 ∈ x0 ⟶ nIn x5 x1) ⟶ nat_p x3 ⟶ nat_p x4 ⟶ equip x0 x3 ⟶ equip x2 (add_nat x3 x4) ⟶ equip x1 x4
Known f38da.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . nat_p x2 ⟶ ∀ x3 x4 . x3 ∈ x0 ⟶ x4 ∈ DirGraphOutNeighbors x0 x1 x3 ⟶ (∀ x5 . x5 ∈ {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) x2} ⟶ not (x1 x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4)) ⟶ x5 x6 ∈ binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x4)) ⟶ ∀ x6 . x6 ∈ {x7 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x3)) x2} ⟶ ∀ x7 : ο . (∀ x8 . and (x8 ∈ setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (x1 x6 x8) ⟶ x7) ⟶ x7
Known c82b0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x1 x2 x3 ⟶ ∀ x4 . x4 ∈ setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2) ⟶ not (x1 x2 x4)
Known 94e32.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 x3 . x2 ∈ x0 ⟶ ∀ x4 . nat_p x4 ⟶ (∀ x5 . x5 ∈ x0 ⟶ (x5 = x2 ⟶ ∀ x6 : ο . x6) ⟶ not (x1 x5 x2) ⟶ or (equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) x4) (equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) (ordsucc x4))) ⟶ (∀ x5 . x5 ∈ {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x2)) x4} ⟶ not (x1 x3 x5)) ⟶ (∀ x5 . x5 ∈ setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2) ⟶ not (x1 x2 x5)) ⟶ ∀ x5 . x5 ∈ setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2) ⟶ equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) (ordsucc x4)
Definition 15fbd.. := λ x0 : ι → ι → ο . λ x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x1 ⟶ x0 (x2 x3) (x2 (ordsucc x3))) (x0 (x2 x1) (x2 0))
Definition f1360.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ο . (∀ x4 : ι → ι . and (bij (ordsucc x1) x2 x4) (15fbd.. x0 x1 x4) ⟶ x3) ⟶ x3
Definition u4 := ordsucc u3
Known 1f34f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ⊆ x0 ⟶ equip x2 u4 ⟶ ∀ x3 x4 : ι → ι . (∀ x5 . x5 ∈ u4 ⟶ x3 x5 ∈ x2) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x4 x5 ∈ x2) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x3 x5 = x4 x5 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x1 (x3 x5) (x4 x5)) ⟶ (∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x3 x6 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ (∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x4 x6 ⟶ x4 x5 = x3 x6 ⟶ x5 = x6) ⟶ f1360.. x1 u3 x2
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition 4b3fa.. := λ x0 : ι → ι → ο . λ x1 x2 . prim0 (λ x3 . x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1))
Known 998ca.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)) ⟶ 4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)
Known 42af1.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ 4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)
Known 80db2.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ x0 x3 x2 ⟶ x3 = 4b3fa.. x0 x1 x2
Known abdca.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ 4b3fa.. x0 x1 x2 = 4b3fa.. x0 x1 x3 ⟶ x2 = x3
Definition f14ce.. := λ x0 : ι → ι → ο . λ x1 x2 . prim0 (λ x3 . and (x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (x3 = 4b3fa.. x0 x1 x2 ⟶ ∀ x4 : ο . x4))
Known 0ddae.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2} ⟶ and (f14ce.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (f14ce.. x0 x1 x2 = 4b3fa.. x0 x1 x2 ⟶ ∀ x3 : ο . x3)
Param inv^inv : ι → (ι → ι) → ι → ι
Definition 31e20.. := λ x0 : ι → ι → ο . λ x1 . inv {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} (4b3fa.. x0 x1)
Known e1908.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x3 . x3 ∈ setminus (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) (DirGraphOutNeighbors u18 x0 x2) ⟶ 4b3fa.. x0 x1 x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2)
Known 9fceb.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ 31e20.. x0 x1 (4b3fa.. x0 x1 x3) ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}
Known 23d19.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ f14ce.. x0 x1 x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2)
Known eb388.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ 31e20.. x0 x1 (f14ce.. x0 x1 x3) ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}
Known 82836.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) ⟶ and (and (31e20.. x0 x1 x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}) (binintersect (DirGraphOutNeighbors u18 x0 (31e20.. x0 x1 x3)) (DirGraphOutNeighbors u18 x0 x1) = Sing x3)) (4b3fa.. x0 x1 (31e20.. x0 x1 x3) = x3)
Known 68855.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ 31e20.. x0 x1 (4b3fa.. x0 x1 x3) = 31e20.. x0 x1 (f14ce.. x0 x1 x3) ⟶ ∀ x4 : ο . x4
Known 8a908.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ x0 (31e20.. x0 x1 (4b3fa.. x0 x1 x3)) (31e20.. x0 x1 (f14ce.. x0 x1 x3))
Known 51de2.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ and (equip {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} u4) (equip {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u2} u8)
Known nat_4^nat_4 : nat_p 4
Known b4538.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ equip (DirGraphOutNeighbors u18 x0 x1) u5
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known 86f86.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ u18 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (x0 x1 x2) ⟶ or (equip (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u1) (equip (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2)
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known 9c223..^{equip_ordsucc_remove1} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ equip x0 (ordsucc x1) ⟶ equip (setminus x0 (Sing x2)) x1
Known nat_1^nat_1 : nat_p 1
Known b7308.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ ∀ x4 . x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)) ⟶ ∀ x5 . x5 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)) ⟶ x0 x4 x2 ⟶ x0 x5 x2 ⟶ x0 x4 x3 ⟶ x0 x5 x3 ⟶ x4 = x5
Known binintersectE2^{binintersectE2} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x1
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known binintersectE1^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known 36602.. : add_nat 4 4 = 8
Known cfabd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ x2 ∈ DirGraphOutNeighbors x0 x1 x3
Theorem 52c6f.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x4 . x4 ⊆ u18 ⟶ ∀ x5 . x5 ⊆ u18 ⟶ ∀ x6 . x6 ⊆ u18 ⟶ ∀ x7 . x7 ⊆ u18 ⟶ x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3) ⟶ x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1) ⟶ x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6 ⟶ (∀ x8 . x8 ∈ u18 ⟶ ∀ x9 : ο . (x8 = x1 ⟶ x9) ⟶ (x8 = x3 ⟶ x9) ⟶ (x8 ∈ x4 ⟶ x9) ⟶ (x8 ∈ x6 ⟶ x9) ⟶ (x8 ∈ x5 ⟶ x9) ⟶ (x8 ∈ x7 ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x5 ⟶ not (x0 x3 x8)) ⟶ equip x4 u4 ⟶ equip x5 u4 ⟶ equip x6 u4 ⟶ equip x7 u4 ⟶ (∀ x8 . x8 ∈ x6 ⟶ nIn x8 x7) ⟶ (∀ x8 . x8 ∈ x5 ⟶ ∀ x9 : ο . (∀ x10 . and (x10 ∈ x6) (x0 x8 x10) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x6 ⟶ not (x0 x1 x8)) ⟶ (∀ x8 . x8 ∈ x6 ⟶ equip (binintersect (DirGraphOutNeighbors u18 x0 x8) (DirGraphOutNeighbors u18 x0 x1)) u2) ⟶ f1360.. x0 u3 x5 ⟶ x2) ⟶ x2 (proof)
Param SetAdjoin^SetAdjoin : ι → ι → ι
Param UPair^UPair : ι → ι → ι
Known bijE^bijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known In_0_3^In_0_3 : 0 ∈ 3
Known In_2_3^In_2_3 : 2 ∈ 3
Param omega^omega : ι
Definition finite^finite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (equip x0 x2) ⟶ x1) ⟶ x1
Known 1b508.. : ∀ x0 x1 . finite x0 ⟶ atleastp x1 x0 ⟶ x0 ⊆ x1 ⟶ x0 = x1
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known 2c48a..^{atleastp_antisym_equip} : ∀ x0 x1 . atleastp x0 x1 ⟶ atleastp x1 x0 ⟶ equip x0 x1
Known 38089.. : ∀ x0 x1 x2 x3 . atleastp (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) u4
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0 ⟶ x4 x1 ⟶ x4 x2 ⟶ x4 x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 ⟶ x4 x5
Known 09d70.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ atleastp u4 x0
Known 69a9c.. : ∀ x0 x1 x2 x3 . x0 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known e588e.. : ∀ x0 x1 x2 x3 . x1 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known 14338.. : ∀ x0 x1 x2 x3 . x2 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known b253c.. : ∀ x0 x1 x2 x3 . x3 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0 ⟶ x3 x1 ⟶ x3 x2 ⟶ ∀ x4 . x4 ∈ SetAdjoin (UPair x0 x1) x2 ⟶ x3 x4
Known 5d098.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ atleastp u3 x0
Known 6be8c.. : ∀ x0 x1 x2 . x0 ∈ SetAdjoin (UPair x0 x1) x2
Known 535ce.. : ∀ x0 x1 x2 . x1 ∈ SetAdjoin (UPair x0 x1) x2
Known f4e2f.. : ∀ x0 x1 x2 . x2 ∈ SetAdjoin (UPair x0 x1) x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0
Known In_3_4^In_3_4 : 3 ∈ 4
Known In_2_4^In_2_4 : 2 ∈ 4
Known neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0
Known In_1_4^In_1_4 : 1 ∈ 4
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Known In_0_4^In_0_4 : 0 ∈ 4
Known neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Known In_1_3^In_1_3 : 1 ∈ 3
Theorem 8cad5.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x4 . x4 ⊆ u18 ⟶ ∀ x5 . x5 ⊆ u18 ⟶ ∀ x6 . x6 ⊆ u18 ⟶ ∀ x7 . x7 ⊆ u18 ⟶ x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3) ⟶ x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1) ⟶ x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6 ⟶ ∀ x8 . x8 ∈ x5 ⟶ ∀ x9 . x9 ∈ x5 ⟶ ∀ x10 . x10 ∈ x5 ⟶ ∀ x11 . x11 ∈ x5 ⟶ x0 x8 x9 ⟶ x0 x9 x10 ⟶ x0 x10 x11 ⟶ x0 x11 x8 ⟶ (x9 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x10 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x10 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x8 x10) ⟶ not (x0 x9 x11) ⟶ x5 = SetAdjoin (SetAdjoin (UPair x8 x9) x10) x11 ⟶ (∀ x12 . x12 ∈ u18 ⟶ ∀ x13 : ο . (x12 = x1 ⟶ x13) ⟶ (x12 = x3 ⟶ x13) ⟶ (x12 ∈ x4 ⟶ x13) ⟶ (x12 ∈ x6 ⟶ x13) ⟶ (x12 ∈ x5 ⟶ x13) ⟶ (x12 ∈ x7 ⟶ x13) ⟶ x13) ⟶ (∀ x12 . x12 ∈ x5 ⟶ not (x0 x3 x12)) ⟶ equip x4 u4 ⟶ equip x5 u4 ⟶ equip x6 u4 ⟶ equip x7 u4 ⟶ (∀ x12 . x12 ∈ x6 ⟶ nIn x12 x7) ⟶ (∀ x12 . x12 ∈ x5 ⟶ ∀ x13 : ο . (∀ x14 . and (x14 ∈ x6) (x0 x12 x14) ⟶ x13) ⟶ x13) ⟶ (∀ x12 . x12 ∈ x6 ⟶ not (x0 x1 x12)) ⟶ (∀ x12 . x12 ∈ x6 ⟶ equip (binintersect (DirGraphOutNeighbors u18 x0 x12) (DirGraphOutNeighbors u18 x0 x1)) u2) ⟶ x2) ⟶ x2 (proof)
Theorem 8cad5.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x4 . x4 ⊆ u18 ⟶ ∀ x5 . x5 ⊆ u18 ⟶ ∀ x6 . x6 ⊆ u18 ⟶ ∀ x7 . x7 ⊆ u18 ⟶ x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3) ⟶ x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1) ⟶ x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6 ⟶ ∀ x8 . x8 ∈ x5 ⟶ ∀ x9 . x9 ∈ x5 ⟶ ∀ x10 . x10 ∈ x5 ⟶ ∀ x11 . x11 ∈ x5 ⟶ x0 x8 x9 ⟶ x0 x9 x10 ⟶ x0 x10 x11 ⟶ x0 x11 x8 ⟶ (x9 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x10 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x10 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x8 x10) ⟶ not (x0 x9 x11) ⟶ x5 = SetAdjoin (SetAdjoin (UPair x8 x9) x10) x11 ⟶ (∀ x12 . x12 ∈ u18 ⟶ ∀ x13 : ο . (x12 = x1 ⟶ x13) ⟶ (x12 = x3 ⟶ x13) ⟶ (x12 ∈ x4 ⟶ x13) ⟶ (x12 ∈ x6 ⟶ x13) ⟶ (x12 ∈ x5 ⟶ x13) ⟶ (x12 ∈ x7 ⟶ x13) ⟶ x13) ⟶ (∀ x12 . x12 ∈ x5 ⟶ not (x0 x3 x12)) ⟶ equip x4 u4 ⟶ equip x5 u4 ⟶ equip x6 u4 ⟶ equip x7 u4 ⟶ (∀ x12 . x12 ∈ x6 ⟶ nIn x12 x7) ⟶ (∀ x12 . x12 ∈ x5 ⟶ ∀ x13 : ο . (∀ x14 . and (x14 ∈ x6) (x0 x12 x14) ⟶ x13) ⟶ x13) ⟶ (∀ x12 . x12 ∈ x6 ⟶ not (x0 x1 x12)) ⟶ (∀ x12 . x12 ∈ x6 ⟶ equip (binintersect (DirGraphOutNeighbors u18 x0 x12) (DirGraphOutNeighbors u18 x0 x1)) u2) ⟶ x2) ⟶ x2 (proof)
Known 782e4.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ⊆ x0 ⟶ ∀ x3 x4 x5 x6 . x2 = SetAdjoin (SetAdjoin (UPair x3 x4) x5) x6 ⟶ (x4 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x6 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x6 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x6 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x1 x3 x4 ⟶ x1 x4 x5 ⟶ x1 x5 x6 ⟶ x1 x6 x3 ⟶ (∀ x7 . x7 ∈ binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x5) ⟶ or (x7 = x4) (x7 = x6)) ⟶ (∀ x7 . x7 ∈ binintersect (DirGraphOutNeighbors x0 x1 x4) (DirGraphOutNeighbors x0 x1 x6) ⟶ or (x7 = x3) (x7 = x5)) ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ ∀ x9 . x9 ∈ binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x8) ⟶ x9 ∈ x2
Known 02907.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ equip (DirGraphOutNeighbors x0 x1 x2) u5) ⟶ ∀ x2 x3 x4 x5 x6 x7 . x6 ⊆ x0 ⟶ x5 ⊆ x0 ⟶ x6 = {x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))|equip (binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x2)) u1} ⟶ x4 = setminus (DirGraphOutNeighbors x0 x1 x2) (Sing x3) ⟶ (∀ x8 . x8 ∈ x6 ⟶ not (x1 x3 x8)) ⟶ (∀ x8 . x8 ∈ x0 ⟶ ∀ x9 : ο . (x8 = x2 ⟶ x9) ⟶ (x8 = x3 ⟶ x9) ⟶ (x8 ∈ x4 ⟶ x9) ⟶ (x8 ∈ x5 ⟶ x9) ⟶ (x8 ∈ x6 ⟶ x9) ⟶ (x8 ∈ x7 ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x6 ⟶ ∀ x9 : ο . (∀ x10 . x10 ∈ x6 ⟶ ∀ x11 . x11 ∈ x6 ⟶ (x10 = x11 ⟶ ∀ x12 : ο . x12) ⟶ x10 ∈ DirGraphOutNeighbors x0 x1 x8 ⟶ x11 ∈ DirGraphOutNeighbors x0 x1 x8 ⟶ not (x1 x10 x11) ⟶ (∀ x12 . x12 ∈ x6 ⟶ nIn x12 (SetAdjoin (UPair x8 x10) x11) ⟶ not (x1 x8 x12)) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ ∀ x10 . x10 ∈ binintersect (DirGraphOutNeighbors x0 x1 x8) (DirGraphOutNeighbors x0 x1 x9) ⟶ x10 ∈ x6) ⟶ (∀ x8 . x8 ∈ x6 ⟶ nIn x8 x5) ⟶ ∀ x8 x9 : ι → ι . (∀ x10 . x10 ∈ x6 ⟶ ∀ x11 . x11 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ x1 x11 x10 ⟶ x11 = x8 x10) ⟶ (∀ x10 . x10 ∈ x6 ⟶ x9 x10 ∈ x5) ⟶ (∀ x10 . x10 ∈ x6 ⟶ x1 x10 (x9 x10)) ⟶ (∀ x10 . x10 ∈ x5 ⟶ ∀ x11 : ο . (∀ x12 . and (x12 ∈ x6) (x9 x12 = x10) ⟶ x11) ⟶ x11) ⟶ ∀ x10 . x10 ∈ x6 ⟶ ∀ x11 : ο . (∀ x12 . and (x12 ∈ x7) (x1 x10 x12) ⟶ x11) ⟶ x11
Known f0ba0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x1 x2 x3) ⟶ atleastp (binintersect (DirGraphOutNeighbors x0 x1 x2) (DirGraphOutNeighbors x0 x1 x3)) u2) ⟶ ∀ x2 x3 x4 x5 . x2 ⊆ x0 ⟶ x3 ⊆ x0 ⟶ x4 ⊆ x0 ⟶ x5 ⊆ x0 ⟶ (∀ x6 . x6 ∈ x4 ⟶ nIn x6 x2) ⟶ (∀ x6 . x6 ∈ x4 ⟶ nIn x6 x3) ⟶ (∀ x6 . x6 ∈ x4 ⟶ nIn x6 x5) ⟶ (∀ x6 . x6 ∈ x2 ⟶ nIn x6 x3) ⟶ (∀ x6 . x6 ∈ x2 ⟶ nIn x6 x5) ⟶ (∀ x6 . x6 ∈ x3 ⟶ nIn x6 x5) ⟶ ∀ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6 ∈ x4 ⟶ x7 ∈ x4 ⟶ x3 = SetAdjoin (SetAdjoin (UPair x10 x11) x12) x13 ⟶ x14 ∈ x2 ⟶ x15 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x16 : ο . x16) ⟶ x1 x6 x7 ⟶ x1 x6 x10 ⟶ x1 x6 x15 ⟶ x1 x7 x14 ⟶ x1 x7 x11 ⟶ x1 x12 x15 ⟶ not (x1 x14 x6) ⟶ x1 x14 x15 ⟶ x1 x13 x15 ⟶ ∀ x16 . x16 ∈ x3 ⟶ not (x1 x14 x16)
Known edcee.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x9 ⊆ x0 ⟶ x11 ⊆ x0 ⟶ x8 = setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x5) ⟶ x10 = setminus (DirGraphOutNeighbors x0 x1 x5) (Sing x4) ⟶ x9 = {x13 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x13) (DirGraphOutNeighbors x0 x1 x4)) x2} ⟶ x11 = setminus {x13 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x13) (DirGraphOutNeighbors x0 x1 x4)) x3} x10 ⟶ (∀ x12 . x12 ∈ x9 ⟶ nIn x12 x8) ⟶ (∀ x12 . x12 ∈ x9 ⟶ nIn x12 x11) ⟶ (∀ x12 . x12 ∈ x8 ⟶ nIn x12 x11) ⟶ x6 ∈ x9 ⟶ x7 ∈ x11 ⟶ x1 x6 x7 ⟶ ∀ x12 x13 : ι → ι . x1 x6 (x12 x6) ⟶ (∀ x14 . x14 ∈ x8 ⟶ x13 x14 ∈ {x15 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x15) (DirGraphOutNeighbors x0 x1 x4)) x2}) ⟶ (∀ x14 . x14 ∈ x8 ⟶ x12 (x13 x14) = x14) ⟶ atleastp x3 {x14 ∈ setminus x9 (Sing x6)|x1 (x12 x14) x7}
Known 9a487.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 x3 . nat_p x2 ⟶ ∀ x4 x5 . x5 ∈ DirGraphOutNeighbors x0 x1 x4 ⟶ ∀ x6 x7 x8 . x6 ⊆ x0 ⟶ x7 ⊆ x0 ⟶ x8 ⊆ x0 ⟶ x7 = setminus (DirGraphOutNeighbors x0 x1 x5) (Sing x4) ⟶ x8 = setminus {x10 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x4)) x3} x7 ⟶ equip x6 x2 ⟶ (∀ x9 . x9 ∈ x6 ⟶ x9 = x5 ⟶ ∀ x10 : ο . x10) ⟶ (∀ x9 . x9 ∈ x6 ⟶ nIn x9 x7) ⟶ (∀ x9 . x9 ∈ x6 ⟶ nIn x9 x8) ⟶ (∀ x9 . x9 ∈ x6 ⟶ nIn x9 (DirGraphOutNeighbors x0 x1 x4)) ⟶ (∀ x9 . x9 ∈ x6 ⟶ nIn x9 (DirGraphOutNeighbors x0 x1 x5)) ⟶ (∀ x9 . x9 ∈ x6 ⟶ ∀ x10 . x10 ∈ x6 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ ∀ x11 . x11 ∈ binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x10) ⟶ x11 ∈ x6) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ x6 ⟶ x9 x10 ∈ x7) ⟶ (∀ x10 . x10 ∈ x6 ⟶ x1 x10 (x9 x10)) ⟶ (∀ x10 . x10 ∈ x7 ⟶ ∀ x11 : ο . (∀ x12 . and (x12 ∈ x6) (x9 x12 = x10) ⟶ x11) ⟶ x11) ⟶ (∀ x10 . x10 ∈ x8 ⟶ or (equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) u1) (equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) x3)) ⟶ equip {x10 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x5) (Sing x5))|equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) u1} x2 ⟶ x8 ⊆ {x10 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x5) (Sing x5))|equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) x3}
Known 0bee3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 x3 x4 . nat_p x4 ⟶ ∀ x5 x6 x7 . x5 ⊆ x0 ⟶ x6 ⊆ x0 ⟶ x7 ⊆ x0 ⟶ x5 = setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2) ⟶ (∀ x8 . x8 ∈ x6 ⟶ nIn x8 x5) ⟶ (∀ x8 . x8 ∈ x6 ⟶ nIn x8 x7) ⟶ (∀ x8 . x8 ∈ x5 ⟶ nIn x8 x7) ⟶ (∀ x8 . x8 ∈ x7 ⟶ x8 ∈ {x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x3)) x4}) ⟶ ∀ x8 x9 . x8 ∈ x6 ⟶ x9 ∈ x7 ⟶ x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2)) ⟶ x1 x8 x9 ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ x6 ⟶ x10 x11 ∈ x5) ⟶ (∀ x11 . x11 ∈ x6 ⟶ x1 x11 (x10 x11)) ⟶ (∀ x11 . x11 ∈ x5 ⟶ ∀ x12 : ο . (∀ x13 . and (x13 ∈ x6) (x10 x13 = x11) ⟶ x12) ⟶ x12) ⟶ atleastp x4 {x11 ∈ setminus x6 (Sing x8)|x1 (x10 x11) x9}
Known 3eb85.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 . x2 ⊆ x0 ⟶ x3 ⊆ x0 ⟶ x4 ⊆ x0 ⟶ x5 ⊆ x0 ⟶ (∀ x6 . x6 ∈ x2 ⟶ nIn x6 x5) ⟶ (∀ x6 . x6 ∈ x2 ⟶ nIn x6 x3) ⟶ (∀ x6 . x6 ∈ x4 ⟶ nIn x6 x2) ⟶ (∀ x6 . x6 ∈ x4 ⟶ nIn x6 x3) ⟶ (∀ x6 . x6 ∈ x4 ⟶ nIn x6 x5) ⟶ (∀ x6 . x6 ∈ x3 ⟶ nIn x6 x5) ⟶ ∀ x6 x7 x8 x9 x10 . x4 = SetAdjoin (SetAdjoin (UPair x6 x7) x8) x9 ⟶ x10 ∈ x5 ⟶ (∀ x11 . x11 ∈ x4 ⟶ (x11 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x1 x11 x10) ⟶ atleastp (binintersect (DirGraphOutNeighbors x0 x1 x11) (DirGraphOutNeighbors x0 x1 x10)) u2) ⟶ x6 ∈ binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x10) ⟶ x6 ∈ binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x10) ⟶ not (x1 x7 x10) ⟶ not (x1 x9 x10) ⟶ ∀ x11 x12 : ι → ι . (∀ x13 . x13 ∈ x4 ⟶ x11 x13 ∈ x2) ⟶ (∀ x13 . x13 ∈ x4 ⟶ x11 x13 ∈ DirGraphOutNeighbors x0 x1 x13) ⟶ (∀ x13 . x13 ∈ x4 ⟶ x12 x13 ∈ x3) ⟶ (∀ x13 . x13 ∈ x4 ⟶ x12 x13 ∈ DirGraphOutNeighbors x0 x1 x13) ⟶ ∀ x13 . x13 ∈ x4 ⟶ x13 ∈ {x14 ∈ setminus x4 (Sing x6)|x1 (x11 x14) x10} ⟶ x13 ∈ {x14 ∈ setminus x4 (Sing x6)|x1 (x12 x14) x10} ⟶ x13 = x8
Theorem 38ba8.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 . x8 ∈ x4 ⟶ ∀ x9 : ο . (x8 ∈ x0 ⟶ x8 ∈ DirGraphOutNeighbors x0 x1 x3 ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ x1 x3 x8 ⟶ (x8 = x2 ⟶ ∀ x10 : ο . x10) ⟶ x9) ⟶ x9) ⟶ (∀ x8 : ο . (∀ x9 . and (x9 ∈ x4) (x1 x5 x9) ⟶ x8) ⟶ x8) ⟶ (x1 x5 x6 ⟶ x1 x7 x6 ⟶ ∀ x8 . x8 ∈ x4 ⟶ not (x1 x5 x8)) ⟶ x1 x5 x6 ⟶ x1 x7 x6 ⟶ False (proof)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known nat_3^nat_3 : nat_p 3
Known 256ca.. : add_nat 2 2 = 4
Param setsum^setsum : ι → ι → ι
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (add_nat x0 x1) (setsum x2 x3)
Known nat_2^nat_2 : nat_p 2
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known 1fe14.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ (∀ x4 . x4 ∈ x2 ⟶ nIn x4 x3) ⟶ atleastp (setsum x0 x1) (binunion x2 x3)
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Theorem fe2f1.. : ∀ x0 . atleastp x0 u3 ⟶ ∀ x1 . x1 ⊆ x0 ⟶ ∀ x2 . x2 ⊆ x0 ⟶ atleastp u2 x1 ⟶ atleastp u2 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x4 ∈ x2) ⟶ x3) ⟶ x3 (proof)
Known 1aece.. : ∀ x0 x1 x2 x3 x4 . x4 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 ⟶ ∀ x5 : ι → ο . x5 x0 ⟶ x5 x1 ⟶ x5 x2 ⟶ x5 x3 ⟶ x5 x4
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Theorem 71076.. : ∀ x0 x1 x2 x3 . setminus (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) (UPair x0 x2) ⊆ UPair x1 x3 (proof)
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x0 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7)) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x1 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7))) ⟶ x4) ⟶ x4)
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Known 7f437.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ atleastp x0 (ordsucc x1) ⟶ atleastp (setminus x0 (Sing x2)) x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known binintersectE^{binintersectE} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ and (x2 ∈ x0) (x2 ∈ x1)
Known binintersectI^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Known 4f2c3.. : ∀ x0 . atleastp (Sing x0) u1
Known e8716.. : ∀ x0 . atleastp u2 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x1) ⟶ x1
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known 2b310.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ u18 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (x0 x1 x2) ⟶ atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Known 77ee8.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι . nat_p x0 ⟶ equip x1 x0 ⟶ equip x2 x0 ⟶ inj x1 x2 x3 ⟶ bij x1 x2 x3
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known 7fc90.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ ∀ x4 . x4 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Known nat_17^nat_17 : nat_p 17
Theorem d777e.. : TwoRamseyProp_atleastp u3 u6 u18 (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x2
Theorem TwoRamseyProp_3_6_18^{TwoRamseyProp_3_6_18} : TwoRamseyProp u3 u6 u18 (proof)
Theorem TwoRamseyProp_3_6_18^{TwoRamseyProp_3_6_18} : TwoRamseyProp 3 6 18 (proof)