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
Theorem fe032.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0) (proof)
Theorem 19e27.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x1) (proof)
Theorem f85ed.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x2) (proof)
Theorem 82a17.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x3) (proof)
Theorem 59a5f.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x4) (proof)
Theorem 5ca83.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x5) (proof)
Theorem 40dec.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x6) (proof)
Theorem 41eb8.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x7) (proof)
Theorem 42638.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x8) (proof)
Theorem 34c89.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x9) (proof)
Theorem bf246.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x10) (proof)
Theorem 7e49d.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x11) (proof)
Theorem cc205.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x12) (proof)
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)
Param ordsucc^ordsucc : ι → ι
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Theorem 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0 (proof)
Theorem b4828.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 x1 x0 (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
Theorem b9fc1.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_1_2_3_4_5_6_7_8_9_10_11_12_0 x0) (proof)
Theorem 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) (proof)
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
Theorem 4d61d.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_2_3_4_5_6_7_8_9_10_11_12_0_1 x0) (proof)
Theorem 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) (proof)
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
Theorem ab4f5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_3_4_5_6_7_8_9_10_11_12_0_1_2 x0) (proof)
Theorem 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) (proof)
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
Theorem 074b4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_4_5_6_7_8_9_10_11_12_0_1_2_3 x0) (proof)
Theorem 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) (proof)
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
Theorem 470a8.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_5_6_7_8_9_10_11_12_0_1_2_3_4 x0) (proof)
Theorem 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) (proof)
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
Theorem 0dab4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_6_7_8_9_10_11_12_0_1_2_3_4_5 x0) (proof)
Theorem 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) (proof)