Proofgold Address

Definition Church13_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x14) ⟶ x1 x0
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Param u4 : ι
Param u5 : ι
Param u6 : ι
Param u7 : ι
Param u8 : ι
Param u9 : ι
Param u10 : ι
Param u11 : ι
Param u12 : ι
Definition TwoRamseyGraph_3_5_Church13 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3)
Definition TwoRamseyGraph_3_5_13 := λ x0 x1 . ∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ Church13_p x3 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ TwoRamseyGraph_3_5_Church13 x2 x3 = λ x5 x6 . x5
Known b4828.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 x1 x0
Theorem 09b0c.. : ∀ x0 x1 . TwoRamseyGraph_3_5_13 x0 x1 ⟶ TwoRamseyGraph_3_5_13 x1 x0 (proof)
Param u13 : ι
Known 6de8d.. : ∀ x0 . x0 ∈ u13 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 x0
Known fe032.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0)
Known 19e27.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x1)
Known f85ed.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x2)
Known 82a17.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x3)
Known 59a5f.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x4)
Known 5ca83.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x5)
Known 40dec.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x6)
Known 41eb8.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x7)
Known 42638.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x8)
Known 34c89.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x9)
Known bf246.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x10)
Known 7e49d.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x11)
Known cc205.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x12)
Theorem 783ed.. : ∀ x0 . x0 ∈ u13 ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1) ⟶ x1 (proof)
Definition Church13_perm_1_2_3_4_5_6_7_8_9_10_11_12_0 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1
Definition Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
Known 1e494.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x0)
Known b9fc1.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_1_2_3_4_5_6_7_8_9_10_11_12_0 x0)
Known 85fe9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x0) (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x1)
Definition Church13_perm_2_3_4_5_6_7_8_9_10_11_12_0_1 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2
Definition Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11
Known 92c84.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x0)
Known 4d61d.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_2_3_4_5_6_7_8_9_10_11_12_0_1 x0)
Known db65d.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x0) (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x1)
Definition Church13_perm_3_4_5_6_7_8_9_10_11_12_0_1_2 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3
Definition Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10
Known 091d5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x0)
Known ab4f5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_3_4_5_6_7_8_9_10_11_12_0_1_2 x0)
Known 6d980.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x0) (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x1)
Definition Church13_perm_4_5_6_7_8_9_10_11_12_0_1_2_3 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4
Definition Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known 30073.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x0)
Known 074b4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_4_5_6_7_8_9_10_11_12_0_1_2_3 x0)
Known 9e4f1.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x0) (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x1)
Definition Church13_perm_5_6_7_8_9_10_11_12_0_1_2_3_4 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5
Definition Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8
Known ab802.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x0)
Known 470a8.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_5_6_7_8_9_10_11_12_0_1_2_3_4 x0)
Known d457e.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x0) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x1)
Definition Church13_perm_6_7_8_9_10_11_12_0_1_2_3_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6
Definition Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7
Known 099c4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x0)
Known 0dab4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_6_7_8_9_10_11_12_0_1_2_3_4_5 x0)
Known a3398.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x0) (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x1)
Known 696fa.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_6_7_8_9_10_11_12_0_1_2_3_4_5 x0) (Church13_perm_6_7_8_9_10_11_12_0_1_2_3_4_5 x1)
Known 87eb0.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_5_6_7_8_9_10_11_12_0_1_2_3_4 x0) (Church13_perm_5_6_7_8_9_10_11_12_0_1_2_3_4 x1)
Known c0039.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_4_5_6_7_8_9_10_11_12_0_1_2_3 x0) (Church13_perm_4_5_6_7_8_9_10_11_12_0_1_2_3 x1)
Known 23927.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_3_4_5_6_7_8_9_10_11_12_0_1_2 x0) (Church13_perm_3_4_5_6_7_8_9_10_11_12_0_1_2 x1)
Known 9e139.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_2_3_4_5_6_7_8_9_10_11_12_0_1 x0) (Church13_perm_2_3_4_5_6_7_8_9_10_11_12_0_1 x1)
Known 00a87.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_1_2_3_4_5_6_7_8_9_10_11_12_0 x0) (Church13_perm_1_2_3_4_5_6_7_8_9_10_11_12_0 x1)
Theorem b9bfd.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ ∀ x1 : ο . (∀ x2 x3 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x4 ⟶ Church13_p (x2 x4)) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x4 ⟶ Church13_p (x3 x4)) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x2 (x3 x4) = x4) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x3 (x2 x4) = x4) ⟶ (∀ x4 x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x4 ⟶ Church13_p x5 ⟶ TwoRamseyGraph_3_5_Church13 x4 x5 = TwoRamseyGraph_3_5_Church13 (x2 x4) (x2 x5)) ⟶ (x2 x0 = λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) ⟶ x1) ⟶ x1 (proof)
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem 37cbe.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) = x0 ⟶ ∀ x2 : ο . x2) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) = x1 ⟶ ∀ x2 : ο . x2) ⟶ (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) x0 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) x1 = λ x3 x4 . x3) ⟶ False (proof)
Theorem b83f8.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x4) ⟶ False (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param atleastp^atleastp : ι → ι → ο
Definition not^not := λ x0 : ο . x0 ⟶ False
Known f03aa.. : ∀ x0 . atleastp 3 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1) ⟶ x1
Theorem 0ff84.. : ∀ x0 . x0 ⊆ u13 ⟶ atleastp u3 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_5_13 x1 x2) (proof)