Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../16bee..
PUgwa../3a126..
vout
PrNUD../c4810.. 0.04 bars
TMGE8../e07b7.. ownership of c10c0.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMd4p../a2cc0.. ownership of a60b2.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUhDf../8afcd.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c10c0.. : ∀ 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 . x24 x26 ⟶ (x26 = x25 ⟶ False) ⟶ x24 x25 ⟶ False) ⟶ (∀ x25 x26 . x0 x25 x26 ⟶ x24 x26 ⟶ False) ⟶ (∀ x25 . x24 x25 ⟶ (x25 = x23 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . x0 x25 x26 ⟶ x2 x26 (x1 x27) ⟶ x24 x27 ⟶ False) ⟶ (∀ x25 x26 x27 . x0 x26 x27 ⟶ x2 x27 (x1 x25) ⟶ (x2 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x3 x26 x25 ⟶ (x2 x26 (x1 x25) ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x2 x26 (x1 x25) ⟶ (x3 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x2 x25 x26 ⟶ (x24 x26 ⟶ False) ⟶ (x0 x25 x26 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x0 x26 x25 ⟶ (x2 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 . (x4 x25 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 . (x3 x25 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 . (x24 x25 ⟶ False) ⟶ (x6 (x5 x25) x25 ⟶ False) ⟶ False) ⟶ (∀ x25 . (x24 x25 ⟶ False) ⟶ (x2 (x5 x25) (x1 x25) ⟶ False) ⟶ False) ⟶ (∀ x25 . x6 (x7 x25) x25 ⟶ False) ⟶ (∀ x25 . (x2 (x7 x25) (x1 x25) ⟶ False) ⟶ False) ⟶ (x24 x8 ⟶ False) ⟶ (∀ x25 . (x24 (x22 x25) ⟶ False) ⟶ False) ⟶ (∀ x25 . (x2 (x22 x25) (x1 x25) ⟶ False) ⟶ False) ⟶ ((x24 x21 ⟶ False) ⟶ False) ⟶ (∀ x25 . (x24 x25 ⟶ False) ⟶ x24 (x9 x25) ⟶ False) ⟶ (∀ x25 . (x24 x25 ⟶ False) ⟶ (x2 (x9 x25) (x1 x25) ⟶ False) ⟶ False) ⟶ ((x24 x23 ⟶ False) ⟶ False) ⟶ (∀ x25 . x24 (x1 x25) ⟶ False) ⟶ (∀ x25 . (x2 (x10 x25) x25 ⟶ False) ⟶ False) ⟶ ((x24 x20 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x0 (x11 x25 x26) x25 ⟶ (x3 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . (x0 (x11 x25 x26) x26 ⟶ False) ⟶ (x3 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . x3 x26 x27 ⟶ x0 x25 x26 ⟶ (x0 x25 x27 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . x0 x26 x27 ⟶ x3 x26 (x19 x25 x27) ⟶ (x4 x27 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . (x0 (x19 x25 x26) x25 ⟶ False) ⟶ (x4 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . x4 x26 x27 ⟶ x0 x25 x27 ⟶ (x3 (x18 x25 x27 x26) x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . x4 x26 x27 ⟶ x0 x25 x27 ⟶ (x0 (x18 x25 x27 x26) x26 ⟶ False) ⟶ False) ⟶ ((x23 = x20 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x26 = x23 ⟶ x25 = x23 ⟶ (x25 = x12 x26 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x26 = x23 ⟶ x25 = x12 x26 ⟶ (x25 = x23 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . (x27 = x23 ⟶ False) ⟶ x0 x25 x27 ⟶ (x0 (x13 x26 x27) x25 ⟶ False) ⟶ (x0 (x13 x26 x27) x26 ⟶ False) ⟶ (x26 = x12 x27 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . (x26 = x23 ⟶ False) ⟶ x0 (x13 x25 x26) x25 ⟶ x0 (x13 x25 x26) (x17 x25 x26) ⟶ (x25 = x12 x26 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . (x26 = x23 ⟶ False) ⟶ x0 (x13 x25 x26) x25 ⟶ (x0 (x17 x25 x26) x26 ⟶ False) ⟶ (x25 = x12 x26 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . (x27 = x23 ⟶ False) ⟶ x25 = x12 x27 ⟶ x0 x26 (x16 x26 x25 x27) ⟶ (x0 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 . (x27 = x23 ⟶ False) ⟶ x25 = x12 x27 ⟶ (x0 (x16 x26 x25 x27) x27 ⟶ False) ⟶ (x0 x26 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 x27 x28 . (x28 = x23 ⟶ False) ⟶ x25 = x12 x28 ⟶ x0 x27 x25 ⟶ x0 x26 x28 ⟶ (x0 x27 x26 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x24 x26 ⟶ x2 x25 (x1 x26) ⟶ x6 x25 x26 ⟶ False) ⟶ (∀ x25 x26 . (x24 x26 ⟶ False) ⟶ x2 x25 (x1 x26) ⟶ x24 x25 ⟶ (x6 x25 x26 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . (x24 x26 ⟶ False) ⟶ x2 x25 (x1 x26) ⟶ (x6 x25 x26 ⟶ False) ⟶ x24 x25 ⟶ False) ⟶ (∀ x25 x26 . x24 x26 ⟶ x2 x25 (x1 x26) ⟶ (x24 x25 ⟶ False) ⟶ False) ⟶ (∀ x25 x26 . x0 x25 x26 ⟶ x0 x26 x25 ⟶ False) ⟶ (x3 (x12 x14) (x12 x15) ⟶ False) ⟶ (x15 = x23 ⟶ False) ⟶ ((x4 x14 x15 ⟶ False) ⟶ False) ⟶ False (proof)