Search for blocks/addresses/...

Proofgold Asset

asset id
5b930e8e405c47a2b66f4bf6ba170548b4d6479f8fc575d827330366bb4b4ac1
asset hash
bfdd9d77719a5a1b49b18e095951585c701ff0ff6593d2f4f3e00c73c1baac21
bday / block
18620
tx
1aff5..
preasset
doc published by Pr4zB..
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 ordsuccordsucc : ιι
Param andand : οοο
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Definition u1 := 1
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0
Definition u2 := ordsucc u1
Known neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0
Definition u3 := ordsucc u2
Known neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0
Definition u4 := ordsucc u3
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Definition u5 := ordsucc u4
Known neq_5_0neq_5_0 : u5 = 0∀ x0 : ο . x0
Definition u6 := ordsucc u5
Known neq_6_0neq_6_0 : u6 = 0∀ x0 : ο . x0
Definition u7 := ordsucc u6
Known neq_7_0neq_7_0 : u7 = 0∀ x0 : ο . x0
Known neq_2_1neq_2_1 : u2 = u1∀ x0 : ο . x0
Known neq_3_1neq_3_1 : u3 = u1∀ x0 : ο . x0
Known neq_4_1neq_4_1 : u4 = u1∀ x0 : ο . x0
Known neq_5_1neq_5_1 : u5 = u1∀ x0 : ο . x0
Known neq_6_1neq_6_1 : u6 = u1∀ x0 : ο . x0
Known neq_7_1neq_7_1 : u7 = u1∀ x0 : ο . x0
Known neq_3_2neq_3_2 : u3 = u2∀ x0 : ο . x0
Known neq_4_2neq_4_2 : u4 = u2∀ x0 : ο . x0
Known neq_5_2neq_5_2 : u5 = u2∀ x0 : ο . x0
Known neq_6_2neq_6_2 : u6 = u2∀ x0 : ο . x0
Known neq_7_2neq_7_2 : u7 = u2∀ x0 : ο . x0
Known neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0
Known neq_5_3neq_5_3 : u5 = u3∀ x0 : ο . x0
Known neq_6_3neq_6_3 : u6 = u3∀ x0 : ο . x0
Known neq_7_3neq_7_3 : u7 = u3∀ x0 : ο . x0
Known neq_5_4neq_5_4 : u5 = u4∀ x0 : ο . x0
Known neq_6_4neq_6_4 : u6 = u4∀ x0 : ο . x0
Known neq_7_4neq_7_4 : u7 = u4∀ x0 : ο . x0
Known neq_6_5neq_6_5 : u6 = u5∀ x0 : ο . x0
Known neq_7_5neq_7_5 : u7 = u5∀ x0 : ο . x0
Known neq_7_6neq_7_6 : u7 = u6∀ x0 : ο . x0
Definition u8 := ordsucc u7
Known neq_8_0neq_8_0 : u8 = 0∀ x0 : ο . x0
Definition u9 := ordsucc u8
Known neq_9_0neq_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_1neq_8_1 : u8 = u1∀ x0 : ο . x0
Known neq_9_1neq_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_2neq_8_2 : u8 = u2∀ x0 : ο . x0
Known neq_9_2neq_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_3neq_8_3 : u8 = u3∀ x0 : ο . x0
Known neq_9_3neq_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_4neq_8_4 : u8 = u4∀ x0 : ο . x0
Known neq_9_4neq_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_5neq_8_5 : u8 = u5∀ x0 : ο . x0
Known neq_9_5neq_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_6neq_8_6 : u8 = u6∀ x0 : ο . x0
Known neq_9_6neq_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_7neq_8_7 : u8 = u7∀ x0 : ο . x0
Known neq_9_7neq_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_8neq_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 x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3x0 (λ 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)