Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../430d9..
PUgaN../d18da..
vout
PrCit../312d9.. 5.63 bars
TMG9T../c319d.. ownership of d74be.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdKK../c7c5c.. ownership of c8f4c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUbiS../b6946.. 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_9_0neq_9_0 : u9 = 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 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 0e10e.. : u10 = 0∀ 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 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 19f75.. : u11 = 0∀ 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 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 efdfc.. : u12 = 0∀ 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 ad02f.. : u13 = u12∀ x0 : ο . x0
Known ef4da.. : u14 = u12∀ x0 : ο . x0
Known 72647.. : u15 = u12∀ x0 : ο . x0
Known fa664.. : u16 = u12∀ x0 : ο . x0
Known 733b2.. : u13 = 0∀ 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 e1947.. : u14 = u13∀ x0 : ο . x0
Known 4d8d4.. : u15 = u13∀ x0 : ο . x0
Known 4326e.. : u16 = u13∀ x0 : ο . x0
Known fc551.. : u14 = 0∀ 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 b8e82.. : u15 = u14∀ x0 : ο . x0
Known 71c5e.. : u16 = u14∀ x0 : ο . x0
Known 160ad.. : u15 = 0∀ 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 41073.. : u16 = u15∀ x0 : ο . x0
Known 86ae3.. : u16 = 0∀ 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 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1)∀ x0 : ο . x0
Theorem d74be.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1((λ x3 x4 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x3 x3 x3 x3 x3 x3 x3 x3) = λ 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)