Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known dd142.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2 ⟶ x8 x3 ⟶ x8 x4 ⟶ x8 x5 ⟶ x8 x6 ⟶ x8 x7 ⟶ ∀ x9 . x0 x9 ⟶ x8 x9) ⟶ (∀ x8 : ι → ο . x8 x2 ⟶ x8 x3 ⟶ x8 x4 ⟶ x8 x5 ⟶ ∀ x9 . x1 x9 ⟶ x8 x9) ⟶ (∀ x8 . x0 x8 ⟶ not (x1 x8) ⟶ ∀ x9 : ι → ο . x9 x6 ⟶ x9 x7 ⟶ x9 x8) ⟶ x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ not (x1 x6) ⟶ not (x1 x7) ⟶ (x2 = x3 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x4 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x5 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x4 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x5 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x5 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ ∀ x8 x9 x10 : ι → ι → ι . (∀ x11 . x0 x11 ⟶ ∀ x12 . x0 x12 ⟶ x0 (x8 x11 x12)) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x12 ⟶ x1 (x8 x11 x12)) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x0 x12 ⟶ x8 x11 (x8 x11 x12) = x12) ⟶ (∀ x11 . x0 x11 ⟶ x8 x11 x2 = x3) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x0 x12 ⟶ x0 (x9 x11 x12)) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x12 ⟶ x1 (x9 x11 x12)) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x0 x12 ⟶ x9 x11 (x9 x11 x12) = x12) ⟶ (∀ x11 . x0 x11 ⟶ x9 x11 x2 = x4) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x0 x12 ⟶ x0 (x10 x11 x12)) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x12 ⟶ x1 (x10 x11 x12)) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x0 x12 ⟶ x10 x11 (x10 x11 x12) = x12) ⟶ (∀ x11 . x0 x11 ⟶ x10 x11 x2 = x5) ⟶ ∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . not (x11 x12 x13 x12 x13)) ⟶ (∀ x12 x13 x14 x15 x16 x17 . x0 x16 ⟶ x0 x17 ⟶ x11 x12 x13 x14 x15 ⟶ x11 x14 x15 x16 x17 ⟶ x11 x12 x13 x16 x17) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x1 x13 ⟶ ∀ x14 . x0 x14 ⟶ ∀ x15 . x0 x15 ⟶ not (x1 x15) ⟶ x11 x12 x13 x14 x15) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x3 x13 x2)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x4 x13 x2)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x5 x13 x2)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x6 x13 x2)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x7 x13 x2)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x4 x13 x3)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x5 x13 x3)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x6 x13 x3)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x7 x13 x3)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x5 x13 x4)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x6 x13 x4)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x7 x13 x4)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x6 x13 x5)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x7 x13 x5)) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ not (x11 x12 x7 x13 x6)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x2 x12 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x3 x12 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x12 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x12 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x12 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x12 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x3 x12 x3 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x12 x3 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x12 x3 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x12 x3 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x12 x3 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x12 x4 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x12 x4 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x12 x4 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x12 x4 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x12 x5 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x12 x5 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x12 x5 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x12 x6 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x12 x6 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x12 x7 x12)) ⟶ ∀ x12 : ι → ι → ι → ι → ο . (∀ x13 x14 x15 x16 . x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ ∀ x17 : ο . (x11 x13 x14 x15 x16 ⟶ x17) ⟶ (x12 x13 x14 x15 x16 ⟶ x17) ⟶ (x11 x15 x16 x13 x14 ⟶ x17) ⟶ x17) ⟶ (∀ x13 x14 x15 x16 . x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ not (x12 x13 x14 x15 x16) ⟶ not (x12 x13 (x8 x13 x14) x15 (x8 x15 x16))) ⟶ (∀ x13 x14 x15 x16 . x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ not (x12 x13 x14 x15 x16) ⟶ not (x12 x13 (x9 x13 x14) x15 (x9 x15 x16))) ⟶ (∀ x13 x14 x15 x16 . x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ not (x12 x13 x14 x15 x16) ⟶ not (x12 x13 (x10 x13 x14) x15 (x10 x15 x16))) ⟶ (∀ x13 x14 . x0 x13 ⟶ x0 x14 ⟶ x12 x13 x14 x13 x14) ⟶ (∀ x13 x14 x15 x16 . x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x12 x13 x14 x15 x16 ⟶ x12 x15 x16 x13 x14) ⟶ (∀ x13 x14 . x0 x13 ⟶ x0 x14 ⟶ x12 x13 x14 x7 x7) ⟶ (∀ x13 . x0 x13 ⟶ x12 x6 x6 x7 x13) ⟶ (∀ x13 . x0 x13 ⟶ x12 x6 x7 x7 x13) ⟶ x12 x2 x2 x2 x4 ⟶ x12 x2 x2 x2 x6 ⟶ x12 x2 x2 x3 x2 ⟶ x12 x2 x2 x3 x3 ⟶ x12 x2 x2 x3 x6 ⟶ x12 x2 x2 x4 x4 ⟶ x12 x2 x2 x4 x5 ⟶ x12 x2 x2 x4 x6 ⟶ x12 x2 x2 x5 x3 ⟶ x12 x2 x2 x5 x4 ⟶ x12 x2 x2 x5 x6 ⟶ x12 x2 x2 x6 x4 ⟶ x12 x2 x2 x6 x5 ⟶ x12 x2 x2 x7 x2 ⟶ x12 x2 x2 x7 x4 ⟶ x12 x2 x2 x7 x5 ⟶ x12 x2 x3 x2 x5 ⟶ x12 x2 x3 x2 x7 ⟶ x12 x2 x3 x3 x2 ⟶ x12 x2 x3 x3 x3 ⟶ x12 x2 x3 x3 x7 ⟶ x12 x2 x3 x4 x4 ⟶ x12 x2 x3 x4 x5 ⟶ x12 x2 x3 x4 x7 ⟶ x12 x2 x3 x5 x2 ⟶ x12 x2 x3 x5 x5 ⟶ x12 x2 x3 x5 x7 ⟶ x12 x2 x3 x6 x4 ⟶ x12 x2 x3 x6 x5 ⟶ x12 x2 x3 x7 x3 ⟶ x12 x2 x3 x7 x4 ⟶ x12 x2 x3 x7 x5 ⟶ x12 x2 x4 x2 x7 ⟶ x12 x2 x4 x3 x4 ⟶ x12 x2 x4 x3 x5 ⟶ x12 x2 x4 x3 x6 ⟶ x12 x2 x4 x4 x2 ⟶ x12 x2 x4 x4 x3 ⟶ x12 x2 x4 x4 x6 ⟶ x12 x2 x4 x5 x2 ⟶ x12 x2 x4 x5 x5 ⟶ x12 x2 x4 x5 x7 ⟶ x12 x2 x4 x6 x2 ⟶ x12 x2 x4 x6 x3 ⟶ x12 x2 x4 x7 x2 ⟶ x12 x2 x4 x7 x3 ⟶ x12 x2 x4 x7 x4 ⟶ x12 x2 x5 x2 x6 ⟶ x12 x2 x5 x3 x4 ⟶ x12 x2 x5 x3 x5 ⟶ x12 x2 x5 x3 x7 ⟶ x12 x2 x5 x4 x2 ⟶ x12 x2 x5 x4 x3 ⟶ x12 x2 x5 x4 x7 ⟶ x12 x2 x5 x5 x3 ⟶ x12 x2 x5 x5 x4 ⟶ x12 x2 x5 x5 x6 ⟶ x12 x2 x5 x6 x2 ⟶ x12 x2 x5 x6 x3 ⟶ x12 x2 x5 x7 x2 ⟶ x12 x2 x5 x7 x3 ⟶ x12 x2 x5 x7 x5 ⟶ x12 x2 x6 x3 x3 ⟶ x12 x2 x6 x3 x4 ⟶ x12 x2 x6 x4 x2 ⟶ x12 x2 x6 x4 x5 ⟶ x12 x2 x6 x4 x6 ⟶ x12 x2 x6 x4 x7 ⟶ x12 x2 x6 x5 x2 ⟶ x12 x2 x6 x5 x5 ⟶ x12 x2 x6 x5 x6 ⟶ x12 x2 x6 x5 x7 ⟶ x12 x2 x6 x6 x3 ⟶ x12 x2 x6 x6 x4 ⟶ x12 x2 x6 x7 x6 ⟶ x12 x2 x7 x3 x2 ⟶ x12 x2 x7 x3 x5 ⟶ x12 x2 x7 x4 x3 ⟶ x12 x2 x7 x4 x4 ⟶ x12 x2 x7 x4 x6 ⟶ x12 x2 x7 x4 x7 ⟶ x12 x2 x7 x5 x3 ⟶ x12 x2 x7 x5 x4 ⟶ x12 x2 x7 x5 x6 ⟶ x12 x2 x7 x5 x7 ⟶ x12 x2 x7 x6 x2 ⟶ x12 x2 x7 x6 x5 ⟶ x12 x2 x7 x7 x6 ⟶ x12 x3 x2 x3 x4 ⟶ x12 x3 x2 x3 x7 ⟶ x12 x3 x2 x4 x2 ⟶ x12 x3 x2 x4 x6 ⟶ x12 x3 x2 x5 x3 ⟶ x12 x3 x2 x5 x4 ⟶ x12 x3 x2 x5 x5 ⟶ x12 x3 x2 x5 x6 ⟶ x12 x3 x2 x6 x3 ⟶ x12 x3 x2 x6 x4 ⟶ x12 x3 x2 x6 x7 ⟶ x12 x3 x2 x7 x3 ⟶ x12 x3 x3 x3 x5 ⟶ x12 x3 x3 x3 x6 ⟶ x12 x3 x3 x4 x3 ⟶ x12 x3 x3 x4 x7 ⟶ x12 x3 x3 x5 x2 ⟶ x12 x3 x3 x5 x4 ⟶ x12 x3 x3 x5 x5 ⟶ x12 x3 x3 x5 x7 ⟶ x12 x3 x3 x6 x2 ⟶ x12 x3 x3 x6 x5 ⟶ x12 x3 x3 x6 x6 ⟶ x12 x3 x3 x7 x2 ⟶ x12 x3 x4 x3 x7 ⟶ x12 x3 x4 x4 x4 ⟶ x12 x3 x4 x4 x6 ⟶ x12 x3 x4 x5 x2 ⟶ x12 x3 x4 x5 x3 ⟶ x12 x3 x4 x5 x5 ⟶ x12 x3 x4 x5 x7 ⟶ x12 x3 x4 x6 x2 ⟶ x12 x3 x4 x6 x5 ⟶ x12 x3 x4 x6 x7 ⟶ x12 x3 x4 x7 x5 ⟶ x12 x3 x5 x3 x6 ⟶ x12 x3 x5 x4 x5 ⟶ x12 x3 x5 x4 x7 ⟶ x12 x3 x5 x5 x2 ⟶ x12 x3 x5 x5 x3 ⟶ x12 x3 x5 x5 x4 ⟶ x12 x3 x5 x5 x6 ⟶ x12 x3 x5 x6 x3 ⟶ x12 x3 x5 x6 x4 ⟶ x12 x3 x5 x6 x6 ⟶ x12 x3 x5 x7 x4 ⟶ x12 x3 x6 x3 x7 ⟶ x12 x3 x6 x4 x3 ⟶ x12 x3 x6 x4 x5 ⟶ x12 x3 x6 x5 x6 ⟶ x12 x3 x6 x5 x7 ⟶ x12 x3 x6 x6 x7 ⟶ x12 x3 x6 x7 x3 ⟶ x12 x3 x6 x7 x5 ⟶ x12 x3 x6 x7 x6 ⟶ x12 x3 x7 x4 x2 ⟶ x12 x3 x7 x4 x4 ⟶ x12 x3 x7 x5 x6 ⟶ x12 x3 x7 x5 x7 ⟶ x12 x3 x7 x6 x6 ⟶ x12 x3 x7 x7 x2 ⟶ x12 x3 x7 x7 x4 ⟶ x12 x3 x7 x7 x6 ⟶ x12 x4 x2 x4 x3 ⟶ x12 x4 x2 x4 x6 ⟶ x12 x4 x2 x5 x3 ⟶ x12 x4 x2 x5 x4 ⟶ x12 x4 x2 x5 x7 ⟶ x12 x4 x2 x6 x4 ⟶ x12 x4 x2 x6 x5 ⟶ x12 x4 x2 x7 x4 ⟶ x12 x4 x2 x7 x6 ⟶ x12 x4 x3 x4 x7 ⟶ x12 x4 x3 x5 x2 ⟶ x12 x4 x3 x5 x5 ⟶ x12 x4 x3 x5 x6 ⟶ x12 x4 x3 x6 x4 ⟶ x12 x4 x3 x6 x5 ⟶ x12 x4 x3 x7 x5 ⟶ x12 x4 x3 x7 x6 ⟶ x12 x4 x4 x4 x5 ⟶ x12 x4 x4 x4 x6 ⟶ x12 x4 x4 x5 x2 ⟶ x12 x4 x4 x5 x5 ⟶ x12 x4 x4 x5 x6 ⟶ x12 x4 x4 x6 x2 ⟶ x12 x4 x4 x6 x3 ⟶ x12 x4 x4 x7 x2 ⟶ x12 x4 x4 x7 x6 ⟶ x12 x4 x5 x4 x7 ⟶ x12 x4 x5 x5 x3 ⟶ x12 x4 x5 x5 x4 ⟶ x12 x4 x5 x5 x7 ⟶ x12 x4 x5 x6 x2 ⟶ x12 x4 x5 x6 x3 ⟶ x12 x4 x5 x7 x3 ⟶ x12 x4 x5 x7 x6 ⟶ x12 x4 x6 x2 x7 ⟶ x12 x4 x6 x4 x7 ⟶ x12 x4 x6 x6 x3 ⟶ x12 x4 x6 x6 x5 ⟶ x12 x4 x7 x6 x2 ⟶ x12 x4 x7 x6 x4 ⟶ x12 x5 x2 x5 x3 ⟶ x12 x5 x2 x5 x6 ⟶ x12 x5 x2 x6 x4 ⟶ x12 x5 x2 x6 x7 ⟶ x12 x5 x2 x7 x2 ⟶ x12 x5 x2 x7 x3 ⟶ x12 x5 x2 x7 x6 ⟶ x12 x5 x3 x5 x7 ⟶ x12 x5 x3 x6 x5 ⟶ x12 x5 x3 x6 x6 ⟶ x12 x5 x3 x7 x2 ⟶ x12 x5 x3 x7 x3 ⟶ x12 x5 x3 x7 x6 ⟶ x12 x5 x4 x5 x5 ⟶ x12 x5 x4 x5 x7 ⟶ x12 x5 x4 x6 x2 ⟶ x12 x5 x4 x6 x7 ⟶ x12 x5 x4 x7 x4 ⟶ x12 x5 x4 x7 x5 ⟶ x12 x5 x4 x7 x6 ⟶ x12 x5 x5 x5 x6 ⟶ x12 x5 x5 x6 x3 ⟶ x12 x5 x5 x6 x6 ⟶ x12 x5 x5 x7 x4 ⟶ x12 x5 x5 x7 x5 ⟶ x12 x5 x5 x7 x6 ⟶ x12 x5 x6 x2 x7 ⟶ x12 x5 x6 x3 x7 ⟶ x12 x5 x6 x7 x3 ⟶ x12 x5 x6 x7 x4 ⟶ x12 x5 x7 x7 x2 ⟶ x12 x5 x7 x7 x5 ⟶ x12 x6 x2 x6 x4 ⟶ x12 x6 x2 x6 x5 ⟶ x12 x6 x2 x6 x7 ⟶ x12 x6 x2 x7 x2 ⟶ x12 x6 x2 x7 x3 ⟶ x12 x6 x3 x6 x4 ⟶ x12 x6 x3 x6 x5 ⟶ x12 x6 x3 x6 x6 ⟶ x12 x6 x3 x7 x2 ⟶ x12 x6 x3 x7 x3 ⟶ x12 x6 x4 x6 x7 ⟶ x12 x6 x4 x7 x4 ⟶ x12 x6 x4 x7 x5 ⟶ x12 x6 x5 x6 x6 ⟶ x12 x6 x5 x7 x4 ⟶ x12 x6 x5 x7 x5 ⟶ x12 x6 x6 x3 x7 ⟶ x12 x7 x2 x7 x5 ⟶ x12 x7 x3 x7 x4 ⟶ x12 x7 x6 x2 x7 ⟶ x12 x7 x6 x3 x7 ⟶ x12 x7 x6 x6 x7 ⟶ ∀ x13 . x0 x13 ⟶ ∀ x14 . x0 x14 ⟶ ∀ x15 . x0 x15 ⟶ ∀ x16 . x0 x16 ⟶ ∀ x17 . x0 x17 ⟶ ∀ x18 . x0 x18 ⟶ ∀ x19 . x0 x19 ⟶ ∀ x20 . x0 x20 ⟶ ∀ x21 . x0 x21 ⟶ ∀ x22 . x0 x22 ⟶ ∀ x23 . x0 x23 ⟶ ∀ x24 . x0 x24 ⟶ not (x12 x13 x14 x15 x16) ⟶ not (x12 x13 x14 x17 x18) ⟶ not (x12 x13 x14 x19 x20) ⟶ not (x12 x13 x14 x21 x22) ⟶ not (x12 x13 x14 x23 x24) ⟶ not (x12 x15 x16 x17 x18) ⟶ not (x12 x15 x16 x19 x20) ⟶ not (x12 x15 x16 x21 x22) ⟶ not (x12 x15 x16 x23 x24) ⟶ not (x12 x17 x18 x19 x20) ⟶ not (x12 x17 x18 x21 x22) ⟶ not (x12 x17 x18 x23 x24) ⟶ not (x12 x19 x20 x21 x22) ⟶ not (x12 x19 x20 x23 x24) ⟶ not (x12 x21 x22 x23 x24) ⟶ False
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Param TwoRamseyGraph_4_6_35_b : ι → ι → ι → ι → ο
Known 1f9f5.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x4 x5 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x6 x7 ⟶ TwoRamseyGraph_4_6_35_b x2 x3 x4 x5 ⟶ TwoRamseyGraph_4_6_35_b x2 x3 x6 x7 ⟶ TwoRamseyGraph_4_6_35_b x4 x5 x6 x7 ⟶ False
Definition Church6_p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x7) ⟶ x1 x0
Definition Church6_lt4p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x5) ⟶ x1 x0
Definition permargs_i_1_0_3_2_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x2 x1 x4 x3
Definition Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x6 x7)
Known 3f4a9.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (permargs_i_1_0_3_2_4_5 x0)
Known bc219.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x1)
Known 39a8c.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x0)
Known 22a13.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x3)
Known a050d.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x2)
Theorem 3a34f.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1 ⟶ Church6_lt4p (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x1) (proof)
Definition permargs_i_2_3_0_1_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x3 x4 x1 x2
Definition Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7)
Known bc9c2.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (permargs_i_2_3_0_1_4_5 x0)
Theorem ca554.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1 ⟶ Church6_lt4p (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x1) (proof)
Definition permargs_i_3_2_1_0_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x4 x3 x2 x1
Definition Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7)
Known bcfec.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (permargs_i_3_2_1_0_4_5 x0)
Theorem 5bea3.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1 ⟶ Church6_lt4p (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x1) (proof)
Definition TwoRamseyGraph_4_6_Church6_squared_a := λ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . λ x4 x5 . x0 (x1 (x2 (x3 x4 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x4 x5 x4 x4 x5 x4)) (x2 (x3 x5 x4 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x4 x4 x4 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x5 x4)) (x2 (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4))) (x1 (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x4 x4 x4)) (x2 (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x5) (x3 x4 x5 x4 x5 x4 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x5 x4 x4 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x4))) (x1 (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x5 x4 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x4 x4 x4 x4 x4 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x4 x4 x4 x4 x4))) (x1 (x2 (x3 x4 x5 x4 x4 x5 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x4 x4 x4 x5 x5) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x4 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x5 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x4 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4) (x3 x4 x4 x4 x4 x5 x5) (x3 x4 x4 x4 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4)))
Param nth_6_tuple : ι → ι → ι → ι → ι → ι → ι → ι
Definition TwoRamseyGraph_4_6_35_a := λ x0 x1 x2 x3 . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x5 x6 . x5
Param In2_lexicographic : ι → ι → ι → ι → ο
Definition Church6_to_u6 := λ x0 : ι → ι → ι → ι → ι → ι → ι . x0 0 u1 u2 u3 u4 u5
Definition u6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 := λ x0 x1 . Church6_to_u6 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 (nth_6_tuple x0) (nth_6_tuple x1))
Definition u6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 := λ x0 x1 . Church6_to_u6 (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 (nth_6_tuple x0) (nth_6_tuple x1))
Definition u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 := λ x0 x1 . Church6_to_u6 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (nth_6_tuple x0) (nth_6_tuple x1))
Known In_0_6^In_0_6 : 0 ∈ u6
Known In_1_6^In_1_6 : u1 ∈ u6
Known In_2_6^In_2_6 : u2 ∈ u6
Known In_3_6^In_3_6 : u3 ∈ u6
Known In_4_6^In_4_6 : u4 ∈ u6
Known In_5_6^In_5_6 : u5 ∈ u6
Known In_0_4^In_0_4 : 0 ∈ 4
Known In_1_4^In_1_4 : 1 ∈ 4
Known In_2_4^In_2_4 : 2 ∈ 4
Known In_3_4^In_3_4 : 3 ∈ 4
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known In_4_5^In_4_5 : 4 ∈ 5
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_4_0^neq_4_0 : u4 = 0 ⟶ ∀ x0 : ο . x0
Known neq_5_0^neq_5_0 : u5 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0
Known neq_4_1^neq_4_1 : u4 = u1 ⟶ ∀ x0 : ο . x0
Known neq_5_1^neq_5_1 : u5 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_2^neq_4_2 : u4 = u2 ⟶ ∀ x0 : ο . x0
Known neq_5_2^neq_5_2 : u5 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_3^neq_4_3 : u4 = u3 ⟶ ∀ x0 : ο . x0
Known neq_5_3^neq_5_3 : u5 = u3 ⟶ ∀ x0 : ο . x0
Known neq_5_4^neq_5_4 : u5 = u4 ⟶ ∀ x0 : ο . x0
Known e1c62.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ u6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 (u6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x1) = x1
Known d47b4.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ u6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 (u6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x1) = x1
Known 23ec1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 (u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x1) = x1
Known 94e96.. : ∀ x0 x1 . not (In2_lexicographic x0 x1 x0 x1)
Known 6f0f0.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u1 x1 0)
Known 1b2aa.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u2 x1 0)
Known 829cc.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u3 x1 0)
Known 1c740.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 0)
Known 196b9.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 0)
Known 97a37.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u2 x1 u1)
Known b27e1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u3 x1 u1)
Known 52c59.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 u1)
Known 2efb1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u1)
Known 696a1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u3 x1 u2)
Known dd794.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 u2)
Known dd382.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u2)
Known ffa46.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 u3)
Known e28f6.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u3)
Known 1f4d3.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u4)
Known b5ca8.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic 0 x0 0 x0)
Known 15042.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u1 x0 0 x0)
Known 4ed6e.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u2 x0 0 x0)
Known aa680.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 0 x0)
Known be2c5.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 0 x0)
Known fb400.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 0 x0)
Known 69e13.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u1 x0 u1 x0)
Known b695a.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u2 x0 u1 x0)
Known e7d59.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 u1 x0)
Known a3e6e.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u1 x0)
Known dadcc.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u1 x0)
Known 05e9c.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u2 x0 u2 x0)
Known a73b8.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 u2 x0)
Known b6f90.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u2 x0)
Known 6bc25.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u2 x0)
Known 52f87.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 u3 x0)
Known dc51f.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u3 x0)
Known 447d5.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u3 x0)
Known a58bd.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u4 x0)
Known 2313b.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u4 x0)
Known 56b5c.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u5 x0)
Known 2e599.. : ∀ x0 . x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a u4 u4 u5 x0
Known ff9a1.. : ∀ x0 . x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a u4 u5 u5 x0
Known 33924.. : nth_6_tuple u4 = λ x1 x2 x3 x4 x5 x6 . x5
Known fed6d.. : nth_6_tuple u5 = λ x1 x2 x3 x4 x5 x6 . x6
Known a7cad.. : nth_6_tuple u1 = λ x1 x2 x3 x4 x5 x6 . x2
Known a1243.. : nth_6_tuple 0 = λ x1 x2 x3 x4 x5 x6 . x1
Known a0d60.. : nth_6_tuple u2 = λ x1 x2 x3 x4 x5 x6 . x3
Known 89684.. : nth_6_tuple u3 = λ x1 x2 x3 x4 x5 x6 . x4
Known e2503.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_a x0 (u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x1) x2 (u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 x3)
Known e77b8.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_a x0 (u6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x1) x2 (u6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x2 x3)
Known 08bf6.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_a x0 (u6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x1) x2 (u6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x2 x3)
Known aaf54.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 u5 u5
Known dd147.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_a x2 x3 x0 x1
Known dd650.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x0 x1
Param TransSet^TransSet : ι → ο
Known 65c2b.. : ∀ x0 x1 x2 x3 x4 x5 . TransSet x4 ⟶ TransSet x5 ⟶ In2_lexicographic x0 x1 x2 x3 ⟶ In2_lexicographic x2 x3 x4 x5 ⟶ In2_lexicographic x0 x1 x4 x5
Param ordinal^ordinal : ι → ο
Known ordinal_In_TransSet^{ordinal_In_TransSet} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ TransSet x1
Param nat_p^nat_p : ι → ο
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known nat_6^nat_6 : nat_p 6
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known 67627.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3) ⟶ or (In2_lexicographic x0 x1 x2 x3) (In2_lexicographic x2 x3 x0 x1)
Known 6629a.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_to_u6 x0 ∈ u4
Known 3b8c0.. : ∀ x0 . x0 ∈ u6 ⟶ Church6_p (nth_6_tuple x0)
Known c3ac2.. : ∀ x0 . x0 ∈ u4 ⟶ Church6_lt4p (nth_6_tuple x0)
Known 38ba0.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ Church6_to_u6 x0 ∈ u6
Known 58601.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x1 ⟶ Church6_p (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x1)
Known cc59f.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x1 ⟶ Church6_p (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x1)
Known 0dc4b.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x1 ⟶ Church6_p (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x1)
Known 3f697.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u4
Known 03171.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u5
Known be5f9.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u1 x1 u4
Known 9750a.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u1 x1 u5
Known 952f7.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u2 x1 u4
Known f1e9b.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u2 x1 u5
Known e60e7.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u3 x1 u4
Known b30df.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u3 x1 u5
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Known cases_6^cases_6 : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem 2112e.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ ∀ x10 . x10 ∈ u6 ⟶ ∀ x11 . x11 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3) ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x4 x5) ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x6 x7) ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x8 x9) ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x10 x11) ⟶ not (TwoRamseyGraph_4_6_35_a x2 x3 x4 x5) ⟶ not (TwoRamseyGraph_4_6_35_a x2 x3 x6 x7) ⟶ not (TwoRamseyGraph_4_6_35_a x2 x3 x8 x9) ⟶ not (TwoRamseyGraph_4_6_35_a x2 x3 x10 x11) ⟶ not (TwoRamseyGraph_4_6_35_a x4 x5 x6 x7) ⟶ not (TwoRamseyGraph_4_6_35_a x4 x5 x8 x9) ⟶ not (TwoRamseyGraph_4_6_35_a x4 x5 x10 x11) ⟶ not (TwoRamseyGraph_4_6_35_a x6 x7 x8 x9) ⟶ not (TwoRamseyGraph_4_6_35_a x6 x7 x10 x11) ⟶ not (TwoRamseyGraph_4_6_35_a x8 x9 x10 x11) ⟶ False (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known df3e1.. : ∀ x0 x1 : ι → ι → ι → ι → ο . (∀ x2 x3 x4 x5 . x0 x2 x3 x4 x5 ⟶ x0 x4 x5 x2 x3) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ not (x0 x2 x3 x2 x3)) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ x1 x2 x3 x2 x3) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x4 = u5 ⟶ x5 = u5 ⟶ False) ⟶ x0 x2 x3 x4 x5 ⟶ x1 x2 x3 x4 x5) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x4 = u5 ⟶ x5 = u5 ⟶ False) ⟶ (x2 = x4 ⟶ x3 = x5 ⟶ False) ⟶ x1 x2 x3 x4 x5 ⟶ x0 x2 x3 x4 x5) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ x0 x2 x3 x4 x5 ⟶ x0 x2 x3 x6 x7 ⟶ x0 x2 x3 x8 x9 ⟶ x0 x4 x5 x6 x7 ⟶ x0 x4 x5 x8 x9 ⟶ x0 x6 x7 x8 x9 ⟶ False) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ ∀ x10 . x10 ∈ u6 ⟶ ∀ x11 . x11 ∈ u6 ⟶ ∀ x12 . x12 ∈ u6 ⟶ ∀ x13 . x13 ∈ u6 ⟶ not (x1 x2 x3 x4 x5) ⟶ not (x1 x2 x3 x6 x7) ⟶ not (x1 x2 x3 x8 x9) ⟶ not (x1 x2 x3 x10 x11) ⟶ not (x1 x2 x3 x12 x13) ⟶ not (x1 x4 x5 x6 x7) ⟶ not (x1 x4 x5 x8 x9) ⟶ not (x1 x4 x5 x10 x11) ⟶ not (x1 x4 x5 x12 x13) ⟶ not (x1 x6 x7 x8 x9) ⟶ not (x1 x6 x7 x10 x11) ⟶ not (x1 x6 x7 x12 x13) ⟶ not (x1 x8 x9 x10 x11) ⟶ not (x1 x8 x9 x12 x13) ⟶ not (x1 x10 x11 x12 x13) ⟶ False) ⟶ not (TwoRamseyProp 4 6 35)
Known a3e36.. : ∀ x0 x1 x2 x3 . TwoRamseyGraph_4_6_35_b x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_b x2 x3 x0 x1
Known c0174.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b x0 x1 x0 x1)
Known 76062.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ (x0 = u5 ⟶ x1 = u5 ⟶ False) ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3
Known 1fefd.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ (x0 = u5 ⟶ x1 = u5 ⟶ False) ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x0 = x2 ⟶ x1 = x3 ⟶ False) ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x2 x3
Theorem not_TwoRamseyProp_4_6_35^{not_TwoRamseyProp_4_6_35} : not (TwoRamseyProp 4 6 35) (proof)
Param equip^equip : ι → ι → ο
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 u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Definition u25 := ordsucc u24
Definition u26 := ordsucc u25
Definition u27 := ordsucc u26
Definition u28 := ordsucc u27
Definition u29 := ordsucc u28
Definition u30 := ordsucc u29
Definition u31 := ordsucc u30
Definition u32 := ordsucc u31
Param exp_nat^exp_nat : ι → ι → ι
Known e089c.. : exp_nat 2 5 = 32
Known 293d3.. : ∀ x0 . nat_p x0 ⟶ equip (prim4 x0) (exp_nat 2 x0)
Known nat_5^nat_5 : nat_p 5
Theorem 2b2ae.. : equip (prim4 u5) u32 (proof)
Param atleastp^atleastp : ι → ι → ο
Definition u33 := ordsucc u32
Definition u34 := ordsucc u33
Definition u35 := ordsucc u34
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 nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known 966a2.. : nat_p u35
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem dbdae.. : atleastp (prim4 u5) u35 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Theorem not_TwoRamseyProp_4_6_Power_5^{not_TwoRamseyProp_4_6_Power_5} : not (TwoRamseyProp 4 6 (prim4 5)) (proof)
Param TwoRamseyProp_atleastp : ι → ι → ι → ο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x2
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4 ⟶ atleastp x1 x0 ⟶ atleastp x3 x2 ⟶ TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known nat_7^nat_7 : nat_p 7
Known In_6_7^In_6_7 : 6 ∈ 7
Theorem not_TwoRamseyProp_4_7_Power_5^{not_TwoRamseyProp_4_7_Power_5} : not (TwoRamseyProp 4 7 (prim4 5)) (proof)
Known nat_8^nat_8 : nat_p 8
Known In_7_8^In_7_8 : 7 ∈ 8
Theorem not_TwoRamseyProp_4_8_Power_5^{not_TwoRamseyProp_4_8_Power_5} : not (TwoRamseyProp 4 8 (prim4 5)) (proof)
Known nat_9^nat_9 : nat_p 9
Known In_8_9^In_8_9 : 8 ∈ 9
Theorem not_TwoRamseyProp_4_9_Power_5^{not_TwoRamseyProp_4_9_Power_5} : not (TwoRamseyProp 4 9 (prim4 5)) (proof)
Theorem not_TwoRamseyProp_5_6_Power_5^{not_TwoRamseyProp_5_6_Power_5} : not (TwoRamseyProp 5 6 (prim4 5)) (proof)
Theorem not_TwoRamseyProp_5_7_Power_5^{not_TwoRamseyProp_5_7_Power_5} : not (TwoRamseyProp 5 7 (prim4 5)) (proof)
Theorem not_TwoRamseyProp_5_8_Power_5^{not_TwoRamseyProp_5_8_Power_5} : not (TwoRamseyProp 5 8 (prim4 5)) (proof)
Theorem not_TwoRamseyProp_6_6_Power_5^{not_TwoRamseyProp_6_6_Power_5} : not (TwoRamseyProp 6 6 (prim4 5)) (proof)
Theorem not_TwoRamseyProp_6_7_Power_5^{not_TwoRamseyProp_6_7_Power_5} : not (TwoRamseyProp 6 7 (prim4 5)) (proof)