Proofgold Address

Definition ChurchNum_3ary_proj_p := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ο . x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x2) ⟶ x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x3) ⟶ x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) ⟶ x1 x0
Definition ChurchNum_8ary_proj_p := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ x1 x0
Param ordsucc^ordsucc : ι → ι
Param and^and : ο → ο → ο
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Definition u1 := 1
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Definition u2 := ordsucc u1
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Definition u3 := ordsucc u2
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Definition u4 := ordsucc u3
Known neq_4_0^neq_4_0 : u4 = 0 ⟶ ∀ x0 : ο . x0
Definition u5 := ordsucc u4
Known neq_5_0^neq_5_0 : u5 = 0 ⟶ ∀ x0 : ο . x0
Definition u6 := ordsucc u5
Known neq_6_0^neq_6_0 : u6 = 0 ⟶ ∀ x0 : ο . x0
Definition u7 := ordsucc u6
Known neq_7_0^neq_7_0 : u7 = 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_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_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_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_6_5^neq_6_5 : u6 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_5^neq_7_5 : u7 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_6^neq_7_6 : u7 = u6 ⟶ ∀ x0 : ο . x0
Definition u8 := ordsucc u7
Known neq_8_0^neq_8_0 : u8 = 0 ⟶ ∀ x0 : ο . x0
Definition u9 := ordsucc u8
Known neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0
Definition u10 := ordsucc u9
Known 0e10e.. : u10 = 0 ⟶ ∀ x0 : ο . x0
Definition u11 := ordsucc u10
Known 19f75.. : u11 = 0 ⟶ ∀ x0 : ο . x0
Definition u12 := ordsucc u11
Known efdfc.. : u12 = 0 ⟶ ∀ x0 : ο . x0
Definition u13 := ordsucc u12
Known 733b2.. : u13 = 0 ⟶ ∀ x0 : ο . x0
Definition u14 := ordsucc u13
Known fc551.. : u14 = 0 ⟶ ∀ x0 : ο . x0
Definition u15 := ordsucc u14
Known 160ad.. : u15 = 0 ⟶ ∀ 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 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 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 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 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 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 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
Definition u16 := ordsucc u15
Known 86ae3.. : u16 = 0 ⟶ ∀ x0 : ο . x0
Definition u17 := ordsucc u16
Known fcaf7.. : u17 = 0 ⟶ ∀ x0 : ο . x0
Definition u18 := ordsucc u17
Known 99743.. : u18 = 0 ⟶ ∀ x0 : ο . x0
Definition u19 := ordsucc u18
Known fd18a.. : u19 = 0 ⟶ ∀ x0 : ο . x0
Definition u20 := ordsucc u19
Known 4552b.. : u20 = 0 ⟶ ∀ x0 : ο . x0
Definition u21 := ordsucc u20
Known 1158c.. : u21 = 0 ⟶ ∀ x0 : ο . x0
Definition u22 := ordsucc u21
Known e8714.. : u22 = 0 ⟶ ∀ x0 : ο . x0
Definition u23 := ordsucc u22
Known c432c.. : u23 = 0 ⟶ ∀ x0 : ο . x0
Known ab690.. : u16 = u1 ⟶ ∀ x0 : ο . x0
Known d4359.. : u17 = u1 ⟶ ∀ x0 : ο . x0
Known 9ccac.. : u18 = u1 ⟶ ∀ x0 : ο . x0
Known 70279.. : u19 = u1 ⟶ ∀ x0 : ο . x0
Known d8b53.. : u20 = u1 ⟶ ∀ x0 : ο . x0
Known db0cd.. : u21 = u1 ⟶ ∀ x0 : ο . x0
Known 9e7b1.. : u22 = u1 ⟶ ∀ x0 : ο . x0
Known 13d86.. : u23 = u1 ⟶ ∀ x0 : ο . x0
Known 296ac.. : u16 = u2 ⟶ ∀ x0 : ο . x0
Known 2c536.. : u17 = u2 ⟶ ∀ x0 : ο . x0
Known ad866.. : u18 = u2 ⟶ ∀ x0 : ο . x0
Known 81672.. : u19 = u2 ⟶ ∀ x0 : ο . x0
Known c9329.. : u20 = u2 ⟶ ∀ x0 : ο . x0
Known ebee4.. : u21 = u2 ⟶ ∀ x0 : ο . x0
Known af720.. : u22 = u2 ⟶ ∀ x0 : ο . x0
Known 60a3a.. : u23 = u2 ⟶ ∀ x0 : ο . x0
Known ca5c3.. : u16 = u3 ⟶ ∀ x0 : ο . x0
Known 6c299.. : u17 = u3 ⟶ ∀ x0 : ο . x0
Known 1f012.. : u18 = u3 ⟶ ∀ x0 : ο . x0
Known 2e7b7.. : u19 = u3 ⟶ ∀ x0 : ο . x0
Known 0af1b.. : u20 = u3 ⟶ ∀ x0 : ο . x0
Known 272ed.. : u21 = u3 ⟶ ∀ x0 : ο . x0
Known 17aea.. : u22 = u3 ⟶ ∀ x0 : ο . x0
Known 3d5c1.. : u23 = u3 ⟶ ∀ x0 : ο . x0
Known 7b2eb.. : u16 = u4 ⟶ ∀ x0 : ο . x0
Known 506a9.. : u17 = u4 ⟶ ∀ x0 : ο . x0
Known 60e5c.. : u18 = u4 ⟶ ∀ x0 : ο . x0
Known 26e28.. : u19 = u4 ⟶ ∀ x0 : ο . x0
Known f2a22.. : u20 = u4 ⟶ ∀ x0 : ο . x0
Known ac7ac.. : u21 = u4 ⟶ ∀ x0 : ο . x0
Known 7f2f2.. : u22 = u4 ⟶ ∀ x0 : ο . x0
Known 7d70a.. : u23 = u4 ⟶ ∀ x0 : ο . x0
Known 35bff.. : u16 = u5 ⟶ ∀ x0 : ο . x0
Known 4ab36.. : u17 = u5 ⟶ ∀ x0 : ο . x0
Known ac512.. : u18 = u5 ⟶ ∀ x0 : ο . x0
Known dcd9d.. : u19 = u5 ⟶ ∀ x0 : ο . x0
Known 98620.. : u20 = u5 ⟶ ∀ x0 : ο . x0
Known 18fbb.. : u21 = u5 ⟶ ∀ x0 : ο . x0
Known 9a712.. : u22 = u5 ⟶ ∀ x0 : ο . x0
Known b1d7f.. : u23 = u5 ⟶ ∀ x0 : ο . x0
Known 3bd28.. : u16 = u6 ⟶ ∀ x0 : ο . x0
Known b74f3.. : u17 = u6 ⟶ ∀ x0 : ο . x0
Known 8347f.. : u18 = u6 ⟶ ∀ x0 : ο . x0
Known b1809.. : u19 = u6 ⟶ ∀ x0 : ο . x0
Known fd91d.. : u20 = u6 ⟶ ∀ x0 : ο . x0
Known 2ec13.. : u21 = u6 ⟶ ∀ x0 : ο . x0
Known f4b67.. : u22 = u6 ⟶ ∀ x0 : ο . x0
Known 51d86.. : u23 = u6 ⟶ ∀ x0 : ο . x0
Known d3a2f.. : u16 = u7 ⟶ ∀ x0 : ο . x0
Known 66c81.. : u17 = u7 ⟶ ∀ x0 : ο . x0
Known c9d3b.. : u18 = u7 ⟶ ∀ x0 : ο . x0
Known 36989.. : u19 = u7 ⟶ ∀ x0 : ο . x0
Known ae219.. : u20 = u7 ⟶ ∀ x0 : ο . x0
Known 471c9.. : u21 = u7 ⟶ ∀ x0 : ο . x0
Known 362ec.. : u22 = u7 ⟶ ∀ x0 : ο . x0
Known 49af3.. : u23 = 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 4fc31.. : u10 = u9 ⟶ ∀ x0 : ο . x0
Known 4f03f.. : u11 = u9 ⟶ ∀ x0 : ο . x0
Known 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0
Known 3f24c.. : u13 = u9 ⟶ ∀ x0 : ο . x0
Known d7730.. : u14 = u9 ⟶ ∀ x0 : ο . x0
Known 3a7bc.. : u15 = u9 ⟶ ∀ x0 : ο . x0
Known ebfb7.. : u11 = u10 ⟶ ∀ x0 : ο . x0
Known 6c583.. : u12 = u10 ⟶ ∀ x0 : ο . x0
Known 78358.. : u13 = u10 ⟶ ∀ x0 : ο . x0
Known f5ab5.. : u14 = u10 ⟶ ∀ x0 : ο . x0
Known b7f53.. : u15 = u10 ⟶ ∀ x0 : ο . x0
Known ab306.. : u12 = u11 ⟶ ∀ x0 : ο . x0
Known bf497.. : u13 = u11 ⟶ ∀ x0 : ο . x0
Known 4e1aa.. : u14 = u11 ⟶ ∀ x0 : ο . x0
Known 9c5db.. : u15 = u11 ⟶ ∀ x0 : ο . x0
Known ad02f.. : u13 = u12 ⟶ ∀ x0 : ο . x0
Known ef4da.. : u14 = u12 ⟶ ∀ x0 : ο . x0
Known 72647.. : u15 = u12 ⟶ ∀ x0 : ο . x0
Known e1947.. : u14 = u13 ⟶ ∀ x0 : ο . x0
Known 4d8d4.. : u15 = u13 ⟶ ∀ x0 : ο . x0
Known b8e82.. : u15 = u14 ⟶ ∀ x0 : ο . x0
Known 6c306.. : u16 = u8 ⟶ ∀ x0 : ο . x0
Known dc9e6.. : u17 = u8 ⟶ ∀ x0 : ο . x0
Known d47e8.. : u18 = u8 ⟶ ∀ x0 : ο . x0
Known 9b462.. : u19 = u8 ⟶ ∀ x0 : ο . x0
Known 54bdc.. : u20 = u8 ⟶ ∀ x0 : ο . x0
Known ada11.. : u21 = u8 ⟶ ∀ x0 : ο . x0
Known 9d557.. : u22 = u8 ⟶ ∀ x0 : ο . x0
Known b0bcb.. : u23 = u8 ⟶ ∀ x0 : ο . x0
Known 78b49.. : u16 = u9 ⟶ ∀ x0 : ο . x0
Known 66dfd.. : u17 = u9 ⟶ ∀ x0 : ο . x0
Known d3922.. : u18 = u9 ⟶ ∀ x0 : ο . x0
Known 4545d.. : u19 = u9 ⟶ ∀ x0 : ο . x0
Known 6bb84.. : u20 = u9 ⟶ ∀ x0 : ο . x0
Known f159f.. : u21 = u9 ⟶ ∀ x0 : ο . x0
Known ac02b.. : u22 = u9 ⟶ ∀ x0 : ο . x0
Known b0849.. : u23 = u9 ⟶ ∀ x0 : ο . x0
Known 6879f.. : u16 = u10 ⟶ ∀ x0 : ο . x0
Known 2e5d5.. : u17 = u10 ⟶ ∀ x0 : ο . x0
Known a335e.. : u18 = u10 ⟶ ∀ x0 : ο . x0
Known 7d160.. : u19 = u10 ⟶ ∀ x0 : ο . x0
Known 8b01c.. : u20 = u10 ⟶ ∀ x0 : ο . x0
Known b1234.. : u21 = u10 ⟶ ∀ x0 : ο . x0
Known 4d4dd.. : u22 = u10 ⟶ ∀ x0 : ο . x0
Known b7dd9.. : u23 = u10 ⟶ ∀ x0 : ο . x0
Known 22184.. : u16 = u11 ⟶ ∀ x0 : ο . x0
Known 454a8.. : u17 = u11 ⟶ ∀ x0 : ο . x0
Known 8da43.. : u18 = u11 ⟶ ∀ x0 : ο . x0
Known 8109a.. : u19 = u11 ⟶ ∀ x0 : ο . x0
Known 66622.. : u20 = u11 ⟶ ∀ x0 : ο . x0
Known 4c4e0.. : u21 = u11 ⟶ ∀ x0 : ο . x0
Known 2051a.. : u22 = u11 ⟶ ∀ x0 : ο . x0
Known 258a9.. : u23 = u11 ⟶ ∀ x0 : ο . x0
Known fa664.. : u16 = u12 ⟶ ∀ x0 : ο . x0
Known 9a69f.. : u17 = u12 ⟶ ∀ x0 : ο . x0
Known c1bd9.. : u18 = u12 ⟶ ∀ x0 : ο . x0
Known a5243.. : u19 = u12 ⟶ ∀ x0 : ο . x0
Known 01bb6.. : u20 = u12 ⟶ ∀ x0 : ο . x0
Known 6371d.. : u21 = u12 ⟶ ∀ x0 : ο . x0
Known db21d.. : u22 = u12 ⟶ ∀ x0 : ο . x0
Known 3982c.. : u23 = u12 ⟶ ∀ x0 : ο . x0
Known 4326e.. : u16 = u13 ⟶ ∀ x0 : ο . x0
Known 30174.. : u17 = u13 ⟶ ∀ x0 : ο . x0
Known 5cb8a.. : u18 = u13 ⟶ ∀ x0 : ο . x0
Known 8c598.. : u19 = u13 ⟶ ∀ x0 : ο . x0
Known 551bd.. : u20 = u13 ⟶ ∀ x0 : ο . x0
Known 87a9a.. : u21 = u13 ⟶ ∀ x0 : ο . x0
Known 6a662.. : u22 = u13 ⟶ ∀ x0 : ο . x0
Known 4e72c.. : u23 = u13 ⟶ ∀ x0 : ο . x0
Known 71c5e.. : u16 = u14 ⟶ ∀ x0 : ο . x0
Known 82608.. : u17 = u14 ⟶ ∀ x0 : ο . x0
Known d92fd.. : u18 = u14 ⟶ ∀ x0 : ο . x0
Known 35149.. : u19 = u14 ⟶ ∀ x0 : ο . x0
Known 28d21.. : u20 = u14 ⟶ ∀ x0 : ο . x0
Known 25d09.. : u21 = u14 ⟶ ∀ x0 : ο . x0
Known bd746.. : u22 = u14 ⟶ ∀ x0 : ο . x0
Known ef472.. : u23 = u14 ⟶ ∀ x0 : ο . x0
Known 41073.. : u16 = u15 ⟶ ∀ x0 : ο . x0
Known ac12b.. : u17 = u15 ⟶ ∀ x0 : ο . x0
Known dfba1.. : u18 = u15 ⟶ ∀ x0 : ο . x0
Known 38ccc.. : u19 = u15 ⟶ ∀ x0 : ο . x0
Known bf7ce.. : u20 = u15 ⟶ ∀ x0 : ο . x0
Known 17bc6.. : u21 = u15 ⟶ ∀ x0 : ο . x0
Known ac3f7.. : u22 = u15 ⟶ ∀ x0 : ο . x0
Known eff68.. : u23 = u15 ⟶ ∀ x0 : ο . x0
Known 7fbc8.. : u17 = u16 ⟶ ∀ x0 : ο . x0
Known 0eaf4.. : u18 = u16 ⟶ ∀ x0 : ο . x0
Known 0384c.. : u19 = u16 ⟶ ∀ x0 : ο . x0
Known 996e8.. : u20 = u16 ⟶ ∀ x0 : ο . x0
Known 39009.. : u21 = u16 ⟶ ∀ x0 : ο . x0
Known e7d80.. : u22 = u16 ⟶ ∀ x0 : ο . x0
Known c26ad.. : u23 = u16 ⟶ ∀ x0 : ο . x0
Known 82c6a.. : u18 = u17 ⟶ ∀ x0 : ο . x0
Known 3c054.. : u19 = u17 ⟶ ∀ x0 : ο . x0
Known 9ce5b.. : u20 = u17 ⟶ ∀ x0 : ο . x0
Known b821e.. : u21 = u17 ⟶ ∀ x0 : ο . x0
Known d3e26.. : u22 = u17 ⟶ ∀ x0 : ο . x0
Known e9a91.. : u23 = u17 ⟶ ∀ x0 : ο . x0
Known 97eb4.. : u19 = u18 ⟶ ∀ x0 : ο . x0
Known 75fad.. : u20 = u18 ⟶ ∀ x0 : ο . x0
Known 80a82.. : u21 = u18 ⟶ ∀ x0 : ο . x0
Known 7957c.. : u22 = u18 ⟶ ∀ x0 : ο . x0
Known 3bccb.. : u23 = u18 ⟶ ∀ x0 : ο . x0
Known 2615b.. : u20 = u19 ⟶ ∀ x0 : ο . x0
Known 44711.. : u21 = u19 ⟶ ∀ x0 : ο . x0
Known b0147.. : u22 = u19 ⟶ ∀ x0 : ο . x0
Known ad532.. : u23 = u19 ⟶ ∀ x0 : ο . x0
Known 32e25.. : u21 = u20 ⟶ ∀ x0 : ο . x0
Known c8ac0.. : u22 = u20 ⟶ ∀ x0 : ο . x0
Known 94779.. : u23 = u20 ⟶ ∀ x0 : ο . x0
Known 41315.. : u22 = u21 ⟶ ∀ x0 : ο . x0
Known 1a616.. : u23 = u21 ⟶ ∀ x0 : ο . x0
Known 3105f.. : u23 = u22 ⟶ ∀ x0 : ο . x0
Theorem bebde.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ x0 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))))))))))) ordsucc (x2 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))) ordsucc 0) = x1 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))))))))))) ordsucc (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))) ordsucc 0) ⟶ and (x0 = x1) (x2 = x3) (proof)