Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../21564..
PUddZ../6a27a..
vout
PrPhD../6db1c.. 102.62 bars
TMUgj../30266.. ownership of 159df.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMFmZ../1b3be.. ownership of dc4e5.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUMrF../4d9c7.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 159df.. : ∀ 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 . ∀ x30 x31 : ι → ο . ∀ x32 x33 . ∀ x34 : ι → ο . (∀ x35 x36 . x34 x36 ⟶ (x36 = x35 ⟶ False) ⟶ x34 x35 ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x34 x36 ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x35 = x33 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x1 x35 x36 ⟶ (x34 x36 ⟶ False) ⟶ (x0 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x36 x35 ⟶ (x1 x36 x35 ⟶ False) ⟶ False) ⟶ (x2 x3 ⟶ False) ⟶ (x34 x32 ⟶ False) ⟶ ((x4 x5 ⟶ False) ⟶ False) ⟶ ((x31 x5 ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ ((x30 x7 ⟶ False) ⟶ False) ⟶ ((x31 x7 ⟶ False) ⟶ False) ⟶ ((x2 x29 ⟶ False) ⟶ False) ⟶ (x34 x29 ⟶ False) ⟶ ((x34 x28 ⟶ False) ⟶ False) ⟶ ((x31 x8 ⟶ False) ⟶ False) ⟶ (x34 x8 ⟶ False) ⟶ ((x30 x9 ⟶ False) ⟶ False) ⟶ ((x31 x9 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x34 x35 ⟶ False) ⟶ x31 x35 ⟶ x34 (x10 x35) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x31 (x27 (x26 x36 x35) (x26 x38 x37)) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x31 (x11 (x26 x36 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 (x27 x35 x36) ⟶ False) ⟶ (∀ x35 . (x2 (x11 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 (x11 x35) ⟶ False) ⟶ (∀ x35 . x2 x35 ⟶ x31 x35 ⟶ (x2 (x10 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 x36 ⟶ x31 x36 ⟶ (x34 (x25 x36 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x31 x36 ⟶ x34 x35 ⟶ (x34 (x25 x36 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 (x26 x35 x36) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x30 (x11 (x26 x36 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x34 (x10 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x1 (x24 x35) x35 ⟶ False) ⟶ False) ⟶ ((x34 x12 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x26 x36 x35 = x27 (x27 x36 x35) (x11 x36) ⟶ False) ⟶ False) ⟶ ((x33 = x12 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x0 (x23 x35) x35 ⟶ False) ⟶ (x34 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 x36 ⟶ x0 x35 x36 ⟶ False) ⟶ (∀ x35 x36 . (x22 x36 x35 = x35 ⟶ False) ⟶ (x0 (x22 x36 x35) x36 ⟶ False) ⟶ (x36 = x11 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 (x22 x36 x35) x36 ⟶ x22 x36 x35 = x35 ⟶ (x36 = x11 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x36 = x11 x37 ⟶ x35 = x37 ⟶ (x0 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x36 = x11 x37 ⟶ x0 x35 x36 ⟶ (x35 = x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x31 x37 ⟶ (x0 (x20 x36 x35 x37) x35 ⟶ False) ⟶ (x0 (x21 x36 x35 x37) x36 ⟶ False) ⟶ (x36 = x25 x37 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x31 x37 ⟶ (x0 (x26 (x21 x36 x35 x37) (x20 x36 x35 x37)) x37 ⟶ False) ⟶ (x0 (x21 x36 x35 x37) x36 ⟶ False) ⟶ (x36 = x25 x37 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x31 x38 ⟶ x0 (x21 x35 x36 x38) x35 ⟶ x0 (x26 (x21 x35 x36 x38) x37) x38 ⟶ x0 x37 x36 ⟶ (x35 = x25 x38 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 . x31 x39 ⟶ x35 = x25 x39 x36 ⟶ x0 (x26 x38 x37) x39 ⟶ x0 x37 x36 ⟶ (x0 x38 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x31 x38 ⟶ x35 = x25 x38 x36 ⟶ x0 x37 x35 ⟶ (x0 (x19 x37 x35 x36 x38) x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x31 x38 ⟶ x35 = x25 x38 x36 ⟶ x0 x37 x35 ⟶ (x0 (x26 x37 (x19 x37 x35 x36 x38)) x38 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 (x26 (x17 x36 x35) (x18 x36 x35)) x35 ⟶ False) ⟶ (x0 (x18 x36 x35) x36 ⟶ False) ⟶ (x36 = x10 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x0 (x18 x37 x36) x37 ⟶ x0 (x26 x35 (x18 x37 x36)) x36 ⟶ (x37 = x10 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x37 = x10 x38 ⟶ x0 (x26 x36 x35) x38 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x36 = x10 x37 ⟶ x0 x35 x36 ⟶ (x0 (x26 (x13 x35 x36 x37) x35) x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x27 x36 x35 = x27 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ (x4 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ (x31 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ (x14 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ (x31 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x2 x35 ⟶ False) ⟶ x34 x35 ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ x30 x35 ⟶ (x6 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ x30 x35 ⟶ (x30 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x31 x35 ⟶ x30 x35 ⟶ (x31 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x2 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x31 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x30 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x0 x36 x35 ⟶ False) ⟶ (x25 x16 (x11 x15) = x33 ⟶ (x0 x15 (x10 x16) ⟶ False) ⟶ False) ⟶ (x0 x15 (x10 x16) ⟶ (x25 x16 (x11 x15) = x33 ⟶ False) ⟶ False) ⟶ ((x31 x16 ⟶ False) ⟶ False) ⟶ False (proof)