Proofgold Signed Transaction

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
Param u1 : ι
Param u2 : ι
Param u3 : ι
Param u4 : ι
Param u5 : ι
Param u6 : ι
Param u7 : ι
Param u8 : ι
Param u9 : ι
Param u10 : ι
Param u11 : ι
Param u12 : ι
Param u13 : ι
Param u14 : ι
Param u15 : ι
Param u16 : ι
Param TwoRamseyGraph_4_4_Church17 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι
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 ba8e9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 x1 x0
Theorem bea4f.. : ∀ x0 x1 . TwoRamseyGraph_4_4_17 x0 x1 ⟶ TwoRamseyGraph_4_4_17 x1 x0 (proof)
Param u17 : ι
Known 66f20.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ 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 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 x0
Known e70c8.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0)
Known 1b7f9.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x1)
Known 25b64.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x2)
Known 9e7eb.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x3)
Known 51a81.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4)
Known e224e.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x5)
Known 5d397.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6)
Known 3b0d1.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7)
Known e7def.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8)
Known a8b9a.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x9)
Known 4f699.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10)
Known 712d3.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11)
Known d5e0f.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x12)
Known 51598.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13)
Known 15dad.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14)
Known 7e8b2.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15)
Known 02267.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x16)
Theorem 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 (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
Definition Church17_perm_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16
Known 32363.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15 x0)
Known 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)
Known 339e5.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15 x0) (Church17_perm_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15 x1)
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
Definition Church17_perm_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
Known 3d0f9.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14 x0)
Known 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)
Known 0b046.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14 x0) (Church17_perm_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13_14 x1)
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
Definition Church17_perm_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14
Known 8d815.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13 x0)
Known 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)
Known 2b360.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13 x0) (Church17_perm_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12_13 x1)
Definition Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4
Definition Church17_perm_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Known 7599a.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12 x0)
Known edb63.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 x0)
Known 7d016.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12 x0) (Church17_perm_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11_12 x1)
Definition Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5
Definition Church17_perm_12_13_14_15_16_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 x14 x15 x16 x17 . x0 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
Known 88890.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11 x0)
Known 7166e.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 x0)
Known 31bf4.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11 x0) (Church17_perm_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10_11 x1)
Definition Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6
Definition Church17_perm_11_12_13_14_15_16_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 x14 x15 x16 x17 . x0 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11
Known 54f05.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10 x0)
Known 3aad7.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 x0)
Known e43e9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10 x0) (Church17_perm_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9_10 x1)
Definition Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7
Definition Church17_perm_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10
Known b2372.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9 x0)
Known bfee8.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 x0)
Known c7c1b.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9 x0) (Church17_perm_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8_9 x1)
Definition Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8
Definition Church17_perm_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known b07fc.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8 x0)
Known 2bebb.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 x0)
Known cad55.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8 x0) (Church17_perm_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7_8 x1)
Known 1c11b.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 x0) (Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 x1)
Known 9c3ed.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 x0) (Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 x1)
Known 138c9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 x0) (Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 x1)
Known c46f5.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 x0) (Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 x1)
Known fd1d6.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 x0) (Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 x1)
Known 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)
Known 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)
Known 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)
Theorem 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 (proof)