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)
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
Theorem 099c4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x0) (proof)
Theorem 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) (proof)
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
Theorem ab802.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x0) (proof)
Theorem 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) (proof)
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
Theorem 30073.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x0) (proof)
Theorem 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) (proof)
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
Theorem 091d5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x0) (proof)
Theorem 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) (proof)
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
Theorem 92c84.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x0) (proof)
Theorem 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) (proof)
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
Theorem 1e494.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x0) (proof)
Theorem 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) (proof)