Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../e50e0..
PURdc../945ff..
vout
PrPhD../07507.. 3.38 bars
TMMZz../c78b2.. ownership of 595a8.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMYhh../db770.. ownership of cf16c.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUT4x../ea1b0.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 595a8.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ι → ι . ∀ x6 : ι → ι → ο . ∀ x7 : ι → ι . ∀ x8 : ι → ι → ο . ∀ x9 : ι → ι . ∀ x10 x11 . ∀ x12 : ι → ι → ι → ι . ∀ x13 : ι → ι . ∀ x14 x15 x16 x17 . ∀ x18 : ι → ι . ∀ x19 : ι → ι → ι → ι . ∀ x20 x21 x22 x23 : ι → ι . ∀ x24 : ι → ι → ι → ο . ∀ x25 : ι → ι → ο . ∀ x26 . ∀ x27 : ι → ο . (∀ x28 x29 . x27 x29 ⟶ (x29 = x28 ⟶ False) ⟶ x27 x28 ⟶ False) ⟶ (∀ x28 x29 . x0 x28 x29 ⟶ x27 x29 ⟶ False) ⟶ (∀ x28 . x27 x28 ⟶ (x28 = x26 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . x0 x28 x29 ⟶ x2 x29 (x1 x30) ⟶ x27 x30 ⟶ False) ⟶ (∀ x28 x29 x30 . x0 x29 x30 ⟶ x2 x30 (x1 x28) ⟶ (x2 x29 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x3 x29 x28 ⟶ (x2 x29 (x1 x28) ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x2 x29 (x1 x28) ⟶ (x3 x29 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ x6 x30 x28 ⟶ x2 x30 (x1 (x1 x28)) ⟶ (x27 x29 ⟶ False) ⟶ x6 x29 x28 ⟶ x2 x29 (x1 (x1 x28)) ⟶ (x4 (x5 x30 x29) x29 = x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x2 x28 x29 ⟶ (x27 x29 ⟶ False) ⟶ (x0 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x0 x29 x28 ⟶ (x2 x29 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ x24 x30 x28 x29 ⟶ (x24 x30 x29 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 . (x3 x28 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ (x24 x30 x28 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ x28 = x29 ⟶ (x24 x30 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ x24 x30 x28 x29 ⟶ (x28 = x29 ⟶ False) ⟶ False) ⟶ (∀ x28 . (x27 x28 ⟶ False) ⟶ (x8 (x7 x28) x28 ⟶ False) ⟶ False) ⟶ (∀ x28 . (x27 x28 ⟶ False) ⟶ (x2 (x7 x28) (x1 x28) ⟶ False) ⟶ False) ⟶ (∀ x28 . x8 (x9 x28) x28 ⟶ False) ⟶ (∀ x28 . (x2 (x9 x28) (x1 x28) ⟶ False) ⟶ False) ⟶ (x27 x10 ⟶ False) ⟶ (∀ x28 . (x27 (x23 x28) ⟶ False) ⟶ False) ⟶ (∀ x28 . (x2 (x23 x28) (x1 x28) ⟶ False) ⟶ False) ⟶ (∀ x28 . (x6 (x22 x28) x28 ⟶ False) ⟶ False) ⟶ (∀ x28 . x27 (x22 x28) ⟶ False) ⟶ (∀ x28 . (x2 (x22 x28) (x1 (x1 x28)) ⟶ False) ⟶ False) ⟶ ((x27 x11 ⟶ False) ⟶ False) ⟶ (∀ x28 . (x27 x28 ⟶ False) ⟶ x27 (x21 x28) ⟶ False) ⟶ (∀ x28 . (x27 x28 ⟶ False) ⟶ (x2 (x21 x28) (x1 x28) ⟶ False) ⟶ False) ⟶ (∀ x28 . (x27 x28 ⟶ False) ⟶ x27 (x20 x28) ⟶ False) ⟶ (∀ x28 . (x27 x28 ⟶ False) ⟶ (x25 (x20 x28) x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . (x27 x29 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x29 ⟶ (x2 x28 (x1 (x1 x29)) ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . (x27 x29 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x29 ⟶ (x6 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . (x27 x29 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x29 ⟶ x27 x28 ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ x27 (x12 x30 x28 x29) ⟶ False) ⟶ ((x27 x26 ⟶ False) ⟶ False) ⟶ (∀ x28 . x27 (x1 x28) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ x27 (x19 x30 x28 x29) ⟶ False) ⟶ (∀ x28 . (x2 (x13 x28) x28 ⟶ False) ⟶ False) ⟶ (∀ x28 . (x25 (x18 x28) x28 ⟶ False) ⟶ False) ⟶ ((x27 x14 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x25 x29 x28 ⟶ (x2 x29 (x1 (x1 x28)) ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ (x25 (x12 x30 x28 x29) x30 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ (x25 (x19 x30 x28 x29) x30 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ (x12 x30 x28 x29 = x4 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 x30 . (x27 x30 ⟶ False) ⟶ (x27 x28 ⟶ False) ⟶ x25 x28 x30 ⟶ (x27 x29 ⟶ False) ⟶ x25 x29 x30 ⟶ (x19 x30 x28 x29 = x5 x28 x29 ⟶ False) ⟶ False) ⟶ ((x26 = x14 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . (x5 x29 x28 = x5 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . (x4 x29 x28 = x4 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x27 x29 ⟶ x2 x28 (x1 x29) ⟶ x8 x28 x29 ⟶ False) ⟶ (∀ x28 x29 . (x27 x29 ⟶ False) ⟶ x2 x28 (x1 x29) ⟶ x27 x28 ⟶ (x8 x28 x29 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . (x27 x29 ⟶ False) ⟶ x2 x28 (x1 x29) ⟶ (x8 x28 x29 ⟶ False) ⟶ x27 x28 ⟶ False) ⟶ (∀ x28 x29 . x27 x29 ⟶ x2 x28 (x1 x29) ⟶ (x27 x28 ⟶ False) ⟶ False) ⟶ (∀ x28 x29 . x0 x28 x29 ⟶ x0 x29 x28 ⟶ False) ⟶ (x24 x15 (x12 x15 (x19 x15 x17 x16) x16) x16 ⟶ False) ⟶ ((x25 x16 x15 ⟶ False) ⟶ False) ⟶ (x27 x16 ⟶ False) ⟶ ((x25 x17 x15 ⟶ False) ⟶ False) ⟶ (x27 x17 ⟶ False) ⟶ (x27 x15 ⟶ False) ⟶ False (proof)