Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../ef1b4..
PUTCV../7cce7..
vout
PrPhD../c42f0.. 102.63 bars
TMLyx../f8c61.. ownership of ff3aa.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMFC5../59e11.. ownership of b55fb.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUa2J../d8336.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem ff3aa.. : ∀ 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 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x26 x27 x25 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x25 x24 x26 x27 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x27 x26 x24 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x26 x25 x27 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x24 x25 x27 x26 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x27 x24 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x24 x27 x25 x26 ⟶ (x21 x28 x25 x26 x24 x27 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x23 x27 ⟶ False) ⟶ x18 x27 ⟶ x22 x27 ⟶ x20 x24 (x19 x27) ⟶ x20 x26 (x19 x27) ⟶ x20 x25 (x19 x27) ⟶ (x21 x27 x24 x26 x25 (x0 x25 x26 x24 x27) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x23 x27 ⟶ False) ⟶ x18 x27 ⟶ x22 x27 ⟶ x20 x24 (x19 x27) ⟶ x20 x26 (x19 x27) ⟶ x20 x25 (x19 x27) ⟶ (x20 (x0 x25 x26 x24 x27) (x19 x27) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 x29 . (x23 x29 ⟶ False) ⟶ x18 x29 ⟶ x22 x29 ⟶ x20 x24 (x19 x29) ⟶ x20 x28 (x19 x29) ⟶ x20 x25 (x19 x29) ⟶ x20 x27 (x19 x29) ⟶ x20 x26 (x19 x29) ⟶ x21 x29 x24 x28 x25 x27 ⟶ x21 x29 x24 x28 x25 x26 ⟶ (x27 = x26 ⟶ False) ⟶ False) ⟶ ((x18 x17 ⟶ False) ⟶ False) ⟶ (x23 x17 ⟶ False) ⟶ ((x22 x17 ⟶ False) ⟶ False) ⟶ (∀ x24 . (x1 x24 ⟶ False) ⟶ x3 x24 ⟶ x2 (x19 x24) ⟶ False) ⟶ (∀ x24 . x1 x24 ⟶ x3 x24 ⟶ (x2 (x19 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 . x4 x24 ⟶ x3 x24 ⟶ (x5 (x19 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 . (x4 x24 ⟶ False) ⟶ x3 x24 ⟶ x5 (x19 x24) ⟶ False) ⟶ (∀ x24 . (x23 x24 ⟶ False) ⟶ x3 x24 ⟶ x6 (x19 x24) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ x3 x24 ⟶ (x6 (x19 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 . (x20 (x7 x24) x24 ⟶ False) ⟶ False) ⟶ ((x3 x16 ⟶ False) ⟶ False) ⟶ ((x22 x8 ⟶ False) ⟶ False) ⟶ (∀ x24 . x22 x24 ⟶ (x3 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x23 x27 ⟶ False) ⟶ x18 x27 ⟶ x22 x27 ⟶ x20 x24 (x19 x27) ⟶ x20 x26 (x19 x27) ⟶ x20 x25 (x19 x27) ⟶ (x20 (x9 x27 x24 x26 x25) (x19 x27) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x21 x28 x25 x24 x27 x26 ⟶ (x26 = x9 x28 x24 x27 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 x28 . (x23 x28 ⟶ False) ⟶ x18 x28 ⟶ x22 x28 ⟶ x20 x24 (x19 x28) ⟶ x20 x27 (x19 x28) ⟶ x20 x25 (x19 x28) ⟶ x20 x26 (x19 x28) ⟶ x26 = x9 x28 x24 x27 x25 ⟶ (x21 x28 x25 x24 x27 x26 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x14 x24 x15 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x23 x24 ⟶ (x14 x24 x15 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ (x1 x24 ⟶ False) ⟶ x4 x24 ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x4 x24 ⟶ (x1 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ (x1 x24 ⟶ False) ⟶ x1 x24 ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ (x1 x24 ⟶ False) ⟶ x23 x24 ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x23 x24 ⟶ (x1 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x23 x24 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ (x4 x24 ⟶ False) ⟶ x23 x24 ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x23 x24 ⟶ (x4 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ (x4 x24 ⟶ False) ⟶ x23 x24 ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x14 x24 x10 ⟶ (x4 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ x14 x24 x10 ⟶ x23 x24 ⟶ False) ⟶ (∀ x24 . x3 x24 ⟶ (x23 x24 ⟶ False) ⟶ x4 x24 ⟶ (x14 x24 x10 ⟶ False) ⟶ False) ⟶ (∀ x24 . x20 x24 (x19 x13) ⟶ x9 x13 x11 x24 x12 = x12 ⟶ False) ⟶ ((x20 x12 (x19 x13) ⟶ False) ⟶ False) ⟶ ((x20 x11 (x19 x13) ⟶ False) ⟶ False) ⟶ ((x22 x13 ⟶ False) ⟶ False) ⟶ ((x18 x13 ⟶ False) ⟶ False) ⟶ (x23 x13 ⟶ False) ⟶ False (proof)