Proofgold Address

Definition Church17_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x14) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x15) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x17) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x18) ⟶ x1 x0
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 3dec4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ or ((λ x2 x3 . x0 x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) = λ x2 x3 . x2) ((λ x2 x3 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x2 x2) = λ x2 x3 . x2) (proof)
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
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
Known d6f89.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ ((λ x3 x4 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x4 x4 x4 x4 x4 x4 x4 x4) = λ x3 x4 . x3) ⟶ x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x0 = x1
Known d74be.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ ((λ x3 x4 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x3 x3 x3 x3 x3 x3 x3 x3) = λ x3 x4 . x3) ⟶ x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x0 = x1
Theorem 75e61.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x0 = x1 (proof)
Definition TwoRamseyGraph_4_4_Church17 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3) (x1 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2) (x1 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3)
Definition False^False := ∀ x0 : ο . x0
Known cc816.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x5 x5 x5 x5 x5 x5 x5 x5) = λ x4 x5 . x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4) ⟶ False
Known fb66e.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 . x0 x5 x5 x5 x5 x5 x5 x5 x5 x5 x4 x4 x4 x4 x4 x4 x4 x4) = λ x4 x5 . x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4) ⟶ False
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem b8710.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4) ⟶ False (proof)
Known 745f5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ ∀ x1 : ο . (∀ x2 x3 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x4 ⟶ Church17_p (x2 x4)) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x4 ⟶ Church17_p (x3 x4)) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x2 (x3 x4) = x4) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x3 (x2 x4) = x4) ⟶ (∀ x4 x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x4 ⟶ Church17_p x5 ⟶ TwoRamseyGraph_4_4_Church17 x4 x5 = TwoRamseyGraph_4_4_Church17 (x2 x4) (x2 x5)) ⟶ (x2 x0 = λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . x5) ⟶ x1) ⟶ x1
Theorem 946e7.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ Church17_p x3 ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x2 x3 = λ x5 x6 . x5) ⟶ False (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition u17 := ordsucc u16
Param atleastp^atleastp : ι → ι → ο
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition TwoRamseyGraph_4_4_17 := λ x0 x1 . ∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ Church17_p x3 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ TwoRamseyGraph_4_4_Church17 x2 x3 = λ x5 x6 . x5
Known d03c6.. : ∀ x0 . atleastp u4 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x1) ⟶ x1
Known ec2ba.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1) ⟶ x1
Theorem 788d0.. : ∀ x0 . x0 ⊆ u17 ⟶ atleastp u4 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_4_17 x1 x2) (proof)
Theorem eb902.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ or (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x3 x4 . x3) (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x3 x4 . x4) (proof)
Known 7861e.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 . x4) = λ x4 x5 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x5 x5 x5 x5 x5 x5 x5 x5) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 2f37a.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 . x4) = λ x4 x5 . x0 x5 x5 x5 x5 x5 x5 x5 x5 x5 x4 x4 x4 x4 x4 x4 x4 x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x5) ⟶ False
Theorem ea2d2.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x5) ⟶ False (proof)
Theorem 5e23e.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ Church17_p x3 ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x3 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x3 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_4_4_Church17 x2 x3 = λ x5 x6 . x6) ⟶ False (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem dd7b9.. : ∀ x0 . x0 ⊆ u17 ⟶ atleastp u4 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_4_17 x1 x2)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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 bea4f.. : ∀ x0 x1 . TwoRamseyGraph_4_4_17 x0 x1 ⟶ TwoRamseyGraph_4_4_17 x1 x0
Theorem not_TwoRamseyProp_atleast_4_4_17 : not (TwoRamseyProp_atleastp 4 4 17) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
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
Theorem not_TwoRamseyProp_4_4_17^{not_TwoRamseyProp_4_4_17} : not (TwoRamseyProp 4 4 17) (proof)