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
Theorem e70c8.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0) (proof)
Theorem 1b7f9.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x1) (proof)
Theorem 25b64.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x2) (proof)
Theorem 9e7eb.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x3) (proof)
Theorem 51a81.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (proof)
Theorem e224e.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x5) (proof)
Theorem 5d397.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) (proof)
Theorem 3b0d1.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) (proof)
Theorem e7def.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) (proof)
Theorem a8b9a.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x9) (proof)
Theorem 4f699.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) (proof)
Theorem 712d3.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) (proof)
Theorem d5e0f.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x12) (proof)
Theorem 51598.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) (proof)
Theorem 15dad.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) (proof)
Theorem 7e8b2.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) (proof)
Theorem 02267.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x16) (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)
Theorem ba8e9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 x1 x0 (proof)
Definition Church17_perm_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1
Theorem f6e2e.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0 x0) (proof)
Theorem c5dbb.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0 x0) (Church17_perm_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0 x1) (proof)
Definition Church17_perm_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2
Theorem e9109.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1 x0) (proof)
Theorem f730a.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1 x0) (Church17_perm_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1 x1) (proof)
Definition Church17_perm_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3
Theorem efbb9.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2 x0) (proof)
Theorem b6d33.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2 x0) (Church17_perm_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2 x1) (proof)