Search for blocks/addresses/...

Proofgold Asset

asset id
6c2259d882e33ec0bb2fb411f73ca2bf942ce7d8ea6241efaca8fc2805ac4daa
asset hash
c2a218bfec3b034a7db43e3453b66500fb3082afd93a2d00753781e708ba36f8
bday / block
18288
tx
ff438..
preasset
doc published by Pr4zB..
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 FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0
Known neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0
Known neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Known neq_5_0neq_5_0 : u5 = 0∀ x0 : ο . x0
Known neq_6_0neq_6_0 : u6 = 0∀ x0 : ο . x0
Known neq_7_0neq_7_0 : u7 = 0∀ x0 : ο . x0
Known neq_8_0neq_8_0 : u8 = 0∀ 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
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_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 ab690.. : u16 = 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_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 296ac.. : u16 = 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_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 ca5c3.. : u16 = 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_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 7b2eb.. : u16 = 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_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 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 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 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 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1)∀ x0 : ο . x0
Theorem d6f89.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_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 u16x0 = x1 (proof)