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
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 : ι
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_4_0^neq_4_0 : u4 = 0 ⟶ ∀ x0 : ο . x0
Known neq_5_0^neq_5_0 : u5 = 0 ⟶ ∀ x0 : ο . x0
Known neq_6_0^neq_6_0 : u6 = 0 ⟶ ∀ x0 : ο . x0
Known neq_7_0^neq_7_0 : u7 = 0 ⟶ ∀ x0 : ο . x0
Known neq_8_0^neq_8_0 : u8 = 0 ⟶ ∀ x0 : ο . x0
Known neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0
Known 0e10e.. : u10 = 0 ⟶ ∀ x0 : ο . x0
Known 19f75.. : u11 = 0 ⟶ ∀ x0 : ο . x0
Known efdfc.. : u12 = 0 ⟶ ∀ x0 : ο . x0
Known 733b2.. : u13 = 0 ⟶ ∀ x0 : ο . x0
Known fc551.. : u14 = 0 ⟶ ∀ x0 : ο . x0
Known 160ad.. : u15 = 0 ⟶ ∀ x0 : ο . x0
Known 86ae3.. : u16 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0
Known neq_4_1^neq_4_1 : u4 = u1 ⟶ ∀ x0 : ο . x0
Known neq_5_1^neq_5_1 : u5 = u1 ⟶ ∀ x0 : ο . x0
Known neq_6_1^neq_6_1 : u6 = u1 ⟶ ∀ x0 : ο . x0
Known neq_7_1^neq_7_1 : u7 = u1 ⟶ ∀ x0 : ο . x0
Known neq_8_1^neq_8_1 : u8 = u1 ⟶ ∀ x0 : ο . x0
Known neq_9_1^neq_9_1 : u9 = u1 ⟶ ∀ x0 : ο . x0
Known d183f.. : u10 = u1 ⟶ ∀ x0 : ο . x0
Known 618f7.. : u11 = u1 ⟶ ∀ x0 : ο . x0
Known ce0cd.. : u12 = u1 ⟶ ∀ x0 : ο . x0
Known 16246.. : u13 = u1 ⟶ ∀ x0 : ο . x0
Known ac679.. : u14 = u1 ⟶ ∀ x0 : ο . x0
Known 174d1.. : u15 = u1 ⟶ ∀ x0 : ο . x0
Known ab690.. : u16 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_2^neq_4_2 : u4 = u2 ⟶ ∀ x0 : ο . x0
Known neq_5_2^neq_5_2 : u5 = u2 ⟶ ∀ x0 : ο . x0
Known neq_6_2^neq_6_2 : u6 = u2 ⟶ ∀ x0 : ο . x0
Known neq_7_2^neq_7_2 : u7 = u2 ⟶ ∀ x0 : ο . x0
Known neq_8_2^neq_8_2 : u8 = u2 ⟶ ∀ x0 : ο . x0
Known neq_9_2^neq_9_2 : u9 = u2 ⟶ ∀ x0 : ο . x0
Known e02d9.. : u10 = u2 ⟶ ∀ x0 : ο . x0
Known 2c42c.. : u11 = u2 ⟶ ∀ x0 : ο . x0
Known 8158b.. : u12 = u2 ⟶ ∀ x0 : ο . x0
Known 40d25.. : u13 = u2 ⟶ ∀ x0 : ο . x0
Known 0bb18.. : u14 = u2 ⟶ ∀ x0 : ο . x0
Known 4d715.. : u15 = u2 ⟶ ∀ x0 : ο . x0
Known 296ac.. : u16 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_3^neq_4_3 : u4 = u3 ⟶ ∀ x0 : ο . x0
Known neq_5_3^neq_5_3 : u5 = u3 ⟶ ∀ x0 : ο . x0
Known neq_6_3^neq_6_3 : u6 = u3 ⟶ ∀ x0 : ο . x0
Known neq_7_3^neq_7_3 : u7 = u3 ⟶ ∀ x0 : ο . x0
Known neq_8_3^neq_8_3 : u8 = u3 ⟶ ∀ x0 : ο . x0
Known neq_9_3^neq_9_3 : u9 = u3 ⟶ ∀ x0 : ο . x0
Known 68152.. : u10 = u3 ⟶ ∀ x0 : ο . x0
Known b06e1.. : u11 = u3 ⟶ ∀ x0 : ο . x0
Known e015c.. : u12 = u3 ⟶ ∀ x0 : ο . x0
Known 19222.. : u13 = u3 ⟶ ∀ x0 : ο . x0
Known d0fe4.. : u14 = u3 ⟶ ∀ x0 : ο . x0
Known 70124.. : u15 = u3 ⟶ ∀ x0 : ο . x0
Known ca5c3.. : u16 = u3 ⟶ ∀ x0 : ο . x0
Known neq_5_4^neq_5_4 : u5 = u4 ⟶ ∀ x0 : ο . x0
Known neq_6_4^neq_6_4 : u6 = u4 ⟶ ∀ x0 : ο . x0
Known neq_7_4^neq_7_4 : u7 = u4 ⟶ ∀ x0 : ο . x0
Known neq_8_4^neq_8_4 : u8 = u4 ⟶ ∀ x0 : ο . x0
Known neq_9_4^neq_9_4 : u9 = u4 ⟶ ∀ x0 : ο . x0
Known 33d16.. : u10 = u4 ⟶ ∀ x0 : ο . x0
Known 6a6f1.. : u11 = u4 ⟶ ∀ x0 : ο . x0
Known 7aa79.. : u12 = u4 ⟶ ∀ x0 : ο . x0
Known 4d850.. : u13 = u4 ⟶ ∀ x0 : ο . x0
Known ffd62.. : u14 = u4 ⟶ ∀ x0 : ο . x0
Known 4b742.. : u15 = u4 ⟶ ∀ x0 : ο . x0
Known 7b2eb.. : u16 = u4 ⟶ ∀ x0 : ο . x0
Known neq_6_5^neq_6_5 : u6 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_5^neq_7_5 : u7 = u5 ⟶ ∀ x0 : ο . x0
Known neq_8_5^neq_8_5 : u8 = u5 ⟶ ∀ x0 : ο . x0
Known neq_9_5^neq_9_5 : u9 = u5 ⟶ ∀ x0 : ο . x0
Known a7d50.. : u10 = u5 ⟶ ∀ x0 : ο . x0
Known 1b659.. : u11 = u5 ⟶ ∀ x0 : ο . x0
Known 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0
Known 29333.. : u13 = u5 ⟶ ∀ x0 : ο . x0
Known d6c57.. : u14 = u5 ⟶ ∀ x0 : ο . x0
Known 24fad.. : u15 = u5 ⟶ ∀ x0 : ο . x0
Known 35bff.. : u16 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_6^neq_7_6 : u7 = u6 ⟶ ∀ x0 : ο . x0
Known neq_8_6^neq_8_6 : u8 = u6 ⟶ ∀ x0 : ο . x0
Known neq_9_6^neq_9_6 : u9 = u6 ⟶ ∀ x0 : ο . x0
Known d0401.. : u10 = u6 ⟶ ∀ x0 : ο . x0
Known 949f2.. : u11 = u6 ⟶ ∀ x0 : ο . x0
Known 0bd83.. : u12 = u6 ⟶ ∀ x0 : ο . x0
Known 02f5c.. : u13 = u6 ⟶ ∀ x0 : ο . x0
Known 62d80.. : u14 = u6 ⟶ ∀ x0 : ο . x0
Known f5ac7.. : u15 = u6 ⟶ ∀ x0 : ο . x0
Known 3bd28.. : u16 = u6 ⟶ ∀ x0 : ο . x0
Known neq_8_7^neq_8_7 : u8 = u7 ⟶ ∀ x0 : ο . x0
Known neq_9_7^neq_9_7 : u9 = u7 ⟶ ∀ x0 : ο . x0
Known 7d7a8.. : u10 = u7 ⟶ ∀ x0 : ο . x0
Known 4abfa.. : u11 = u7 ⟶ ∀ x0 : ο . x0
Known 6a15f.. : u12 = u7 ⟶ ∀ x0 : ο . x0
Known d9b35.. : u13 = u7 ⟶ ∀ x0 : ο . x0
Known 01bf6.. : u14 = u7 ⟶ ∀ x0 : ο . x0
Known 008b1.. : u15 = u7 ⟶ ∀ x0 : ο . x0
Known d3a2f.. : u16 = u7 ⟶ ∀ x0 : ο . x0
Known neq_9_8^neq_9_8 : u9 = u8 ⟶ ∀ x0 : ο . x0
Known 96175.. : u10 = u8 ⟶ ∀ x0 : ο . x0
Known b3a20.. : u11 = u8 ⟶ ∀ x0 : ο . x0
Known a6a6c.. : u12 = u8 ⟶ ∀ x0 : ο . x0
Known 0b225.. : u13 = u8 ⟶ ∀ x0 : ο . x0
Known 4f6ad.. : u14 = u8 ⟶ ∀ x0 : ο . x0
Known c0d75.. : u15 = u8 ⟶ ∀ x0 : ο . x0
Known 6c306.. : u16 = u8 ⟶ ∀ x0 : ο . x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem d6f89.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ ((λ x3 x4 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x4 x4 x4 x4 x4 x4 x4 x4) = λ x3 x4 . x3) ⟶ x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x0 = x1 (proof)