Search for blocks/addresses/...

Proofgold Asset

asset id
3569f50bf672d4f56768df0d7a907b0b01e181de955262977bf23ed8424adb76
asset hash
a16bed14a1cf6bbc94e77e4d722d5429fd6060d79d9904a1df9348660782fe3c
bday / block
18945
tx
bf9b3..
preasset
doc published by Pr4zB..
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
Definition ChurchNum_3ary_proj_p := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι) → ο . x1 (λ x2 x3 x4 : (ι → ι)ι → ι . x2)x1 (λ x2 x3 x4 : (ι → ι)ι → ι . x3)x1 (λ x2 x3 x4 : (ι → ι)ι → ι . x4)x1 x0
Param ordsuccordsucc : ιι
Definition ChurchNums_3x8_to_u24 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x0 (x1 (λ x2 : ι → ι . λ x3 . x3) (λ x2 : ι → ι . x2) (λ x2 : ι → ι . λ x3 . x2 (x2 x3)) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 x3))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 x3)))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 x3))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 x3)))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 x3)))))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))))))))))) ordsucc 0
Definition ChurchNums_8x3_to_3_lt4_id_ge4_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)
Definition ChurchNums_8_perm_4_5_6_7_0_1_2_3 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x5 x6 x7 x8 x1 x2 x3 x4
Definition ChurchNums_8x3_to_3_lt7_id_ge7_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2)
Definition ChurchNums_8_perm_1_2_3_4_5_6_7_0 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x2 x3 x4 x5 x6 x7 x8 x1
Param andand : οοο
Definition ChurchNums_8x3_to_3_lt5_id_ge5_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)
Definition ChurchNums_8_perm_3_4_5_6_7_0_1_2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x4 x5 x6 x7 x8 x1 x2 x3
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Known neq_4_1neq_4_1 : u4 = u1∀ x0 : ο . x0
Known neq_4_2neq_4_2 : u4 = u2∀ x0 : ο . x0
Known neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0
Definition u5 := ordsucc u4
Known neq_5_4neq_5_4 : u5 = u4∀ x0 : ο . x0
Definition u6 := ordsucc u5
Known neq_6_4neq_6_4 : u6 = u4∀ x0 : ο . x0
Definition u7 := ordsucc u6
Known neq_7_4neq_7_4 : u7 = u4∀ x0 : ο . x0
Definition u8 := ordsucc u7
Known neq_8_4neq_8_4 : u8 = u4∀ x0 : ο . x0
Definition u9 := ordsucc u8
Known neq_9_4neq_9_4 : u9 = u4∀ x0 : ο . x0
Definition u10 := ordsucc u9
Known 33d16.. : u10 = u4∀ x0 : ο . x0
Definition u11 := ordsucc u10
Known 6a6f1.. : u11 = u4∀ x0 : ο . x0
Definition u12 := ordsucc u11
Known 7aa79.. : u12 = u4∀ x0 : ο . x0
Definition u13 := ordsucc u12
Known 4d850.. : u13 = u4∀ x0 : ο . x0
Definition u14 := ordsucc u13
Known ffd62.. : u14 = u4∀ x0 : ο . x0
Definition u15 := ordsucc u14
Known 4b742.. : u15 = u4∀ x0 : ο . x0
Definition u16 := ordsucc u15
Known 7b2eb.. : u16 = u4∀ x0 : ο . x0
Definition u17 := ordsucc u16
Known 506a9.. : u17 = u4∀ x0 : ο . x0
Definition u18 := ordsucc u17
Known 60e5c.. : u18 = u4∀ x0 : ο . x0
Definition u19 := ordsucc u18
Known 26e28.. : u19 = u4∀ x0 : ο . x0
Definition u20 := ordsucc u19
Known f2a22.. : u20 = u4∀ x0 : ο . x0
Definition u21 := ordsucc u20
Known ac7ac.. : u21 = u4∀ x0 : ο . x0
Definition u22 := ordsucc u21
Known 7f2f2.. : u22 = u4∀ x0 : ο . x0
Definition u23 := ordsucc u22
Known 7d70a.. : u23 = u4∀ x0 : ο . x0
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Known neq_5_1neq_5_1 : u5 = u1∀ x0 : ο . x0
Known neq_5_2neq_5_2 : u5 = u2∀ x0 : ο . x0
Known neq_5_3neq_5_3 : u5 = u3∀ x0 : ο . x0
Known neq_6_5neq_6_5 : u6 = u5∀ x0 : ο . x0
Known neq_7_5neq_7_5 : u7 = u5∀ 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 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 neq_5_0neq_5_0 : u5 = 0∀ x0 : ο . x0
Known neq_6_1neq_6_1 : u6 = u1∀ x0 : ο . x0
Known neq_6_2neq_6_2 : u6 = u2∀ x0 : ο . x0
Known neq_6_3neq_6_3 : u6 = u3∀ x0 : ο . x0
Known neq_7_6neq_7_6 : u7 = u6∀ 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 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 neq_6_0neq_6_0 : u6 = 0∀ x0 : ο . x0
Known neq_7_1neq_7_1 : u7 = u1∀ x0 : ο . x0
Known neq_7_2neq_7_2 : u7 = u2∀ x0 : ο . x0
Known neq_7_3neq_7_3 : u7 = u3∀ 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
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_7_0neq_7_0 : u7 = 0∀ x0 : ο . x0
Known neq_8_1neq_8_1 : u8 = u1∀ x0 : ο . x0
Known neq_8_2neq_8_2 : u8 = u2∀ x0 : ο . x0
Known neq_8_3neq_8_3 : u8 = u3∀ 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 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 neq_8_0neq_8_0 : u8 = 0∀ x0 : ο . x0
Known neq_9_1neq_9_1 : u9 = u1∀ x0 : ο . x0
Known neq_9_2neq_9_2 : u9 = u2∀ x0 : ο . x0
Known neq_9_3neq_9_3 : u9 = u3∀ 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 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 neq_9_0neq_9_0 : u9 = 0∀ x0 : ο . x0
Known d183f.. : u10 = u1∀ x0 : ο . x0
Known e02d9.. : u10 = u2∀ x0 : ο . x0
Known 68152.. : u10 = u3∀ 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 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 0e10e.. : u10 = 0∀ x0 : ο . x0
Known 618f7.. : u11 = u1∀ x0 : ο . x0
Known 2c42c.. : u11 = u2∀ x0 : ο . x0
Known b06e1.. : u11 = u3∀ 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 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 19f75.. : u11 = 0∀ x0 : ο . x0
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 81568.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 x2 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x1ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x2ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 (λ x4 x5 x6 : (ι → ι)ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2)and (x0 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 (λ x4 x5 x6 : (ι → ι)ι → ι . x4)) (x2 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) (proof)