Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../d7730..
PUTUW../999ed..
vout
PrPhD../5387c.. 3.40 bars
TMVNr../bcf0f.. ownership of 846a6.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMHhz../99afd.. ownership of b846f.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUVZp../5e53e.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 846a6.. : ∀ 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 . ∀ x37 : ι → ο . ∀ x38 : ι → ι . ∀ x39 x40 : ι → ι → ο . ∀ x41 : ι → ι . ∀ x42 : ι → ο . (∀ x43 x44 . x42 x44 ⟶ (x44 = x43 ⟶ False) ⟶ x42 x43 ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x6 x44 ⟶ x5 x43 (x4 (x1 x44)) ⟶ (x2 (x1 x44) x43 = x3 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x5 x43 x44 ⟶ x42 x44 ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x43 = x7 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x5 x43 x44 ⟶ x40 x44 (x41 x45) ⟶ x42 x45 ⟶ False) ⟶ (∀ x43 x44 x45 . x5 x44 x45 ⟶ x40 x45 (x41 x43) ⟶ (x40 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x39 x44 x43 ⟶ (x40 x44 (x41 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 (x41 x43) ⟶ (x39 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x43 x44 ⟶ (x42 x44 ⟶ False) ⟶ (x5 x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x5 x44 x43 ⟶ (x40 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ (x39 (x3 x44 x43) (x38 x44) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x39 x43 x43 ⟶ False) ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ (x42 x36 ⟶ False) ⟶ (∀ x43 . (x35 x43 ⟶ False) ⟶ x35 (x34 x43) ⟶ False) ⟶ (∀ x43 . (x35 x43 ⟶ False) ⟶ (x40 (x34 x43) (x41 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x35 (x33 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x42 (x33 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x40 (x33 x43) (x41 x43) ⟶ False) ⟶ False) ⟶ (x8 x9 ⟶ False) ⟶ ((x6 x9 ⟶ False) ⟶ False) ⟶ ((x0 x9 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x31 (x32 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x40 (x32 x43) (x41 x43) ⟶ False) ⟶ False) ⟶ ((x6 x30 ⟶ False) ⟶ False) ⟶ ((x10 x30 ⟶ False) ⟶ False) ⟶ ((x0 x30 ⟶ False) ⟶ False) ⟶ (x42 x30 ⟶ False) ⟶ (∀ x43 . x31 (x29 x43) x43 ⟶ False) ⟶ (∀ x43 . (x40 (x29 x43) (x41 x43) ⟶ False) ⟶ False) ⟶ ((x6 x28 ⟶ False) ⟶ False) ⟶ ((x10 x28 ⟶ False) ⟶ False) ⟶ ((x0 x28 ⟶ False) ⟶ False) ⟶ (x42 x11 ⟶ False) ⟶ (∀ x43 . (x42 (x27 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x40 (x27 x43) (x41 x43) ⟶ False) ⟶ False) ⟶ ((x10 x26 ⟶ False) ⟶ False) ⟶ ((x0 x26 ⟶ False) ⟶ False) ⟶ ((x25 x24 ⟶ False) ⟶ False) ⟶ ((x6 x24 ⟶ False) ⟶ False) ⟶ ((x0 x24 ⟶ False) ⟶ False) ⟶ ((x42 x12 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x42 (x23 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x40 (x23 x43) (x41 x43) ⟶ False) ⟶ False) ⟶ ((x0 x22 ⟶ False) ⟶ False) ⟶ (x42 x22 ⟶ False) ⟶ ((x6 x21 ⟶ False) ⟶ False) ⟶ ((x0 x21 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x0 x43 ⟶ x42 (x38 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x0 x43 ⟶ x42 (x4 x43) ⟶ False) ⟶ (∀ x43 . x35 x43 ⟶ x0 x43 ⟶ (x35 (x38 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x35 x43 ⟶ x0 x43 ⟶ (x35 (x4 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x42 x44 ⟶ x0 x44 ⟶ (x42 (x3 x44 x43) ⟶ False) ⟶ False) ⟶ ((x42 x7 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 (x41 x43) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x42 x43 ⟶ (x42 (x3 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x20 x44 ⟶ x6 x44 ⟶ (x42 (x2 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x35 x43 ⟶ False) ⟶ x0 x43 ⟶ x6 x43 ⟶ x35 (x4 x43) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ (x8 x43 ⟶ False) ⟶ x35 (x38 x43) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ x8 x43 ⟶ (x35 (x38 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x0 x44 ⟶ (x42 x43 ⟶ False) ⟶ x40 x43 (x41 (x4 x44)) ⟶ x42 (x3 x44 x43) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x42 (x38 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x0 x44 ⟶ x10 x44 ⟶ x6 x44 ⟶ x40 x43 (x4 x44) ⟶ x42 (x2 x44 x43) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x42 (x4 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x10 x43 ⟶ x6 x43 ⟶ (x19 (x38 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x40 (x13 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ (x6 (x1 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ (x0 (x1 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x5 (x18 x43 x44) x43 ⟶ (x39 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x5 (x18 x43 x44) x44 ⟶ False) ⟶ (x39 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x39 x44 x45 ⟶ x5 x43 x44 ⟶ (x5 x43 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x6 x44 ⟶ (x14 x43 x44 = x2 x44 (x15 x43 x44) ⟶ False) ⟶ (x5 (x14 x43 x44) x43 ⟶ False) ⟶ (x43 = x38 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x6 x44 ⟶ (x5 (x15 x43 x44) (x4 x44) ⟶ False) ⟶ (x5 (x14 x43 x44) x43 ⟶ False) ⟶ (x43 = x38 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x0 x45 ⟶ x6 x45 ⟶ x5 (x14 x44 x45) x44 ⟶ x5 x43 (x4 x45) ⟶ x14 x44 x45 = x2 x45 x43 ⟶ (x44 = x38 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . x0 x46 ⟶ x6 x46 ⟶ x45 = x38 x46 ⟶ x5 x43 (x4 x46) ⟶ x44 = x2 x46 x43 ⟶ (x5 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x0 x45 ⟶ x6 x45 ⟶ x44 = x38 x45 ⟶ x5 x43 x44 ⟶ (x43 = x2 x45 (x16 x43 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x0 x45 ⟶ x6 x45 ⟶ x44 = x38 x45 ⟶ x5 x43 x44 ⟶ (x5 (x16 x43 x44 x45) (x4 x45) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x37 x44 ⟶ x40 x43 (x41 x44) ⟶ (x37 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x37 x44 ⟶ x40 x43 x44 ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x37 x44 ⟶ x40 x43 x44 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x37 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x35 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x8 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x35 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x35 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x35 x44 ⟶ x40 x43 (x41 x44) ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ (x8 x43 ⟶ False) ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ (x8 x43 ⟶ False) ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x0 x43 ⟶ x6 x43 ⟶ (x8 x43 ⟶ False) ⟶ x35 x43 ⟶ False) ⟶ (∀ x43 x44 . x42 x44 ⟶ x40 x43 (x41 x44) ⟶ x31 x43 x44 ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ (x10 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x8 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x40 x43 (x41 x44) ⟶ x42 x43 ⟶ (x31 x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ (x20 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x6 x44 ⟶ x40 x43 (x41 x44) ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x40 x43 (x41 x44) ⟶ (x31 x43 x44 ⟶ False) ⟶ x42 x43 ⟶ False) ⟶ (∀ x43 x44 . x0 x44 ⟶ x40 x43 (x41 x44) ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x25 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x0 x43 ⟶ x6 x43 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x42 x44 ⟶ x40 x43 (x41 x44) ⟶ (x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x0 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x5 x43 x44 ⟶ x5 x44 x43 ⟶ False) ⟶ (x39 (x38 (x1 x17)) (x41 (x38 x17)) ⟶ False) ⟶ ((x6 x17 ⟶ False) ⟶ False) ⟶ ((x0 x17 ⟶ False) ⟶ False) ⟶ False (proof)