Search for blocks/addresses/...

Proofgold Address

address
PUUi4xGpP5xnznyyPumatdG46eDfGd3vBrH
total
0
mg
-
conjpub
-
current assets
78d6b../099c1.. bday: 18791 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 : ιι
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_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
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_0_1neq_0_1 : 0 = 1∀ x0 : ο . x0
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Known d4359.. : u17 = u1∀ x0 : ο . x0
Definition u18 := ordsucc u17
Known 9ccac.. : u18 = u1∀ x0 : ο . x0
Definition u19 := ordsucc u18
Known 70279.. : u19 = u1∀ x0 : ο . x0
Definition u20 := ordsucc u19
Known d8b53.. : u20 = u1∀ x0 : ο . x0
Definition u21 := ordsucc u20
Known db0cd.. : u21 = u1∀ x0 : ο . x0
Definition u22 := ordsucc u21
Known 9e7b1.. : u22 = u1∀ x0 : ο . x0
Definition u23 := ordsucc u22
Known 13d86.. : u23 = u1∀ x0 : ο . x0
Known neq_1_0neq_1_0 : u1 = 0∀ 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 neq_2_0neq_2_0 : u2 = 0∀ 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 neq_3_0neq_3_0 : u3 = 0∀ 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 neq_4_0neq_4_0 : u4 = 0∀ 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 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 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 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 neq_9_4neq_9_4 : u9 = u4∀ x0 : ο . x0
Known neq_9_5neq_9_5 : u9 = u5∀ x0 : ο . x0
Known neq_9_6neq_9_6 : u9 = u6∀ x0 : ο . x0
Known neq_9_7neq_9_7 : u9 = u7∀ x0 : ο . x0
Known neq_9_8neq_9_8 : u9 = u8∀ x0 : ο . x0
Known d183f.. : u10 = u1∀ x0 : ο . x0
Known e02d9.. : u10 = u2∀ x0 : ο . x0
Known 68152.. : u10 = u3∀ x0 : ο . x0
Known 33d16.. : u10 = u4∀ x0 : ο . x0
Known a7d50.. : u10 = u5∀ x0 : ο . x0
Known d0401.. : u10 = u6∀ x0 : ο . x0
Known 7d7a8.. : u10 = u7∀ x0 : ο . x0
Known 96175.. : u10 = u8∀ x0 : ο . x0
Known 618f7.. : u11 = u1∀ x0 : ο . x0
Known 2c42c.. : u11 = u2∀ x0 : ο . x0
Known b06e1.. : u11 = u3∀ x0 : ο . x0
Known 6a6f1.. : u11 = u4∀ x0 : ο . x0
Known 1b659.. : u11 = u5∀ x0 : ο . x0
Known 949f2.. : u11 = u6∀ x0 : ο . x0
Known 4abfa.. : u11 = u7∀ x0 : ο . x0
Known b3a20.. : u11 = u8∀ x0 : ο . x0
Known ce0cd.. : u12 = u1∀ x0 : ο . x0
Known 8158b.. : u12 = u2∀ x0 : ο . x0
Known e015c.. : u12 = u3∀ x0 : ο . x0
Known 7aa79.. : u12 = u4∀ x0 : ο . x0
Known 07eba.. : u12 = u5∀ x0 : ο . x0
Known 0bd83.. : u12 = u6∀ x0 : ο . x0
Known 6a15f.. : u12 = u7∀ x0 : ο . x0
Known a6a6c.. : u12 = u8∀ x0 : ο . x0
Known 16246.. : u13 = u1∀ x0 : ο . x0
Known 40d25.. : u13 = u2∀ x0 : ο . x0
Known 19222.. : u13 = u3∀ x0 : ο . x0
Known 4d850.. : u13 = u4∀ x0 : ο . x0
Known 29333.. : u13 = u5∀ x0 : ο . x0
Known 02f5c.. : u13 = u6∀ x0 : ο . x0
Known d9b35.. : u13 = u7∀ x0 : ο . x0
Known 0b225.. : u13 = u8∀ x0 : ο . x0
Known ac679.. : u14 = u1∀ x0 : ο . x0
Known 0bb18.. : u14 = u2∀ x0 : ο . x0
Known d0fe4.. : u14 = u3∀ x0 : ο . x0
Known ffd62.. : u14 = u4∀ x0 : ο . x0
Known d6c57.. : u14 = u5∀ x0 : ο . x0
Known 62d80.. : u14 = u6∀ x0 : ο . x0
Known 01bf6.. : u14 = u7∀ x0 : ο . x0
Known 4f6ad.. : u14 = u8∀ x0 : ο . x0
Known 174d1.. : u15 = u1∀ x0 : ο . x0
Known 4d715.. : u15 = u2∀ x0 : ο . x0
Known 70124.. : u15 = u3∀ x0 : ο . x0
Known 4b742.. : u15 = u4∀ x0 : ο . x0
Known 24fad.. : u15 = u5∀ x0 : ο . x0
Known f5ac7.. : u15 = u6∀ x0 : ο . x0
Known 008b1.. : u15 = u7∀ x0 : ο . x0
Known c0d75.. : u15 = u8∀ x0 : ο . x0
Known ab690.. : u16 = u1∀ x0 : ο . x0
Known 296ac.. : u16 = u2∀ x0 : ο . x0
Known ca5c3.. : u16 = u3∀ x0 : ο . x0
Known 7b2eb.. : u16 = u4∀ x0 : ο . x0
Known 35bff.. : u16 = u5∀ x0 : ο . x0
Known 3bd28.. : u16 = u6∀ x0 : ο . x0
Known d3a2f.. : u16 = u7∀ x0 : ο . x0
Known 6c306.. : u16 = u8∀ x0 : ο . x0
Known 66dfd.. : u17 = u9∀ x0 : ο . x0
Known 2e5d5.. : u17 = u10∀ x0 : ο . x0
Known 454a8.. : u17 = u11∀ x0 : ο . x0
Known 9a69f.. : u17 = u12∀ x0 : ο . x0
Known 30174.. : u17 = u13∀ x0 : ο . x0
Known 82608.. : u17 = u14∀ x0 : ο . x0
Known ac12b.. : u17 = u15∀ x0 : ο . x0
Known 7fbc8.. : u17 = u16∀ x0 : ο . x0
Known d3922.. : u18 = u9∀ x0 : ο . x0
Known a335e.. : u18 = u10∀ x0 : ο . x0
Known 8da43.. : u18 = u11∀ x0 : ο . x0
Known c1bd9.. : u18 = u12∀ x0 : ο . x0
Known 5cb8a.. : u18 = u13∀ x0 : ο . x0
Known d92fd.. : u18 = u14∀ x0 : ο . x0
Known dfba1.. : u18 = u15∀ x0 : ο . x0
Known 0eaf4.. : u18 = u16∀ x0 : ο . x0
Known 4545d.. : u19 = u9∀ x0 : ο . x0
Known 7d160.. : u19 = u10∀ x0 : ο . x0
Known 8109a.. : u19 = u11∀ x0 : ο . x0
Known a5243.. : u19 = u12∀ x0 : ο . x0
Known 8c598.. : u19 = u13∀ x0 : ο . x0
Known 35149.. : u19 = u14∀ x0 : ο . x0
Known 38ccc.. : u19 = u15∀ x0 : ο . x0
Known 0384c.. : u19 = u16∀ x0 : ο . x0
Known 6bb84.. : u20 = u9∀ x0 : ο . x0
Known 8b01c.. : u20 = u10∀ x0 : ο . x0
Known 66622.. : u20 = u11∀ x0 : ο . x0
Known 01bb6.. : u20 = u12∀ x0 : ο . x0
Known 551bd.. : u20 = u13∀ x0 : ο . x0
Known 28d21.. : u20 = u14∀ x0 : ο . x0
Known bf7ce.. : u20 = u15∀ x0 : ο . x0
Known 996e8.. : u20 = u16∀ x0 : ο . x0
Known f159f.. : u21 = u9∀ x0 : ο . x0
Known b1234.. : u21 = u10∀ x0 : ο . x0
Known 4c4e0.. : u21 = u11∀ x0 : ο . x0
Known 6371d.. : u21 = u12∀ x0 : ο . x0
Known 87a9a.. : u21 = u13∀ x0 : ο . x0
Known 25d09.. : u21 = u14∀ x0 : ο . x0
Known 17bc6.. : u21 = u15∀ x0 : ο . x0
Known 39009.. : u21 = u16∀ x0 : ο . x0
Known ac02b.. : u22 = u9∀ x0 : ο . x0
Known 4d4dd.. : u22 = u10∀ x0 : ο . x0
Known 2051a.. : u22 = u11∀ x0 : ο . x0
Known db21d.. : u22 = u12∀ x0 : ο . x0
Known 6a662.. : u22 = u13∀ x0 : ο . x0
Known bd746.. : u22 = u14∀ x0 : ο . x0
Known ac3f7.. : u22 = u15∀ x0 : ο . x0
Known e7d80.. : u22 = u16∀ x0 : ο . x0
Known b0849.. : u23 = u9∀ x0 : ο . x0
Known b7dd9.. : u23 = u10∀ x0 : ο . x0
Known 258a9.. : u23 = u11∀ x0 : ο . x0
Known 3982c.. : u23 = u12∀ x0 : ο . x0
Known 4e72c.. : u23 = u13∀ x0 : ο . x0
Known ef472.. : u23 = u14∀ x0 : ο . x0
Known eff68.. : u23 = u15∀ x0 : ο . x0
Known c26ad.. : u23 = u16∀ x0 : ο . x0
Known neq_9_0neq_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
Theorem 45827.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x2ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x3(x0 = λ x5 x6 x7 : (ι → ι)ι → ι . x1 x6 x7 x5)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) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3)∀ x4 : ο . x4 (proof)
Theorem 1eab2.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x2ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x3(x0 = λ x5 x6 x7 : (ι → ι)ι → ι . x1 x7 x5 x6)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) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3)∀ x4 : ο . x4 (proof)

previous assets