Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../ce6dc..
PUT3y../90f34..
vout
PrPhD../da9ac.. 3.39 bars
TMbwk../83328.. ownership of 9e86e.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMQU8../32a1c.. ownership of bfec8.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUa7k../981f5.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 9e86e.. : ∀ 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 x37 . x0 x35 x36 ⟶ x2 x36 (x1 x37) ⟶ x34 x37 ⟶ False) ⟶ (∀ x35 x36 x37 . x0 x36 x37 ⟶ x2 x37 (x1 x35) ⟶ (x2 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x3 x36 x35 ⟶ (x2 x36 (x1 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 x35) ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x35 x36 ⟶ (x34 x36 ⟶ False) ⟶ (x0 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x32 x36 ⟶ x32 x35 ⟶ (x3 (x31 (x30 x36 x35)) (x31 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x36 x35 ⟶ (x2 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x3 x35 x35 ⟶ False) ⟶ False) ⟶ (x4 x5 ⟶ False) ⟶ (x34 x29 ⟶ False) ⟶ ((x4 x6 ⟶ False) ⟶ False) ⟶ (x34 x6 ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ ((x34 x28 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x32 (x9 (x10 x36 x35) (x10 x38 x37)) ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x34 (x31 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x32 (x11 (x10 x36 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x34 (x27 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 (x9 x35 x36) ⟶ False) ⟶ (∀ x35 . (x4 (x11 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 (x11 x35) ⟶ False) ⟶ (∀ x35 x36 . x34 (x10 x35 x36) ⟶ False) ⟶ (∀ x35 x36 . (x7 (x10 x35 x36) ⟶ False) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x2 (x12 x35) x35 ⟶ False) ⟶ False) ⟶ ((x34 x26 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x32 (x30 x35 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x32 x37 ⟶ (x0 (x10 (x23 x37 x36 x35) (x24 x37 x36 x35)) x36 ⟶ False) ⟶ (x0 (x10 (x25 x37 x36 x35) (x24 x37 x36 x35)) x37 ⟶ False) ⟶ (x37 = x30 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x32 x37 ⟶ (x0 (x10 (x25 x37 x36 x35) (x23 x37 x36 x35)) x35 ⟶ False) ⟶ (x0 (x10 (x25 x37 x36 x35) (x24 x37 x36 x35)) x37 ⟶ False) ⟶ (x37 = x30 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x32 x38 ⟶ x0 (x10 (x25 x38 x35 x36) (x24 x38 x35 x36)) x38 ⟶ x0 (x10 (x25 x38 x35 x36) x37) x36 ⟶ x0 (x10 x37 (x24 x38 x35 x36)) x35 ⟶ (x38 = x30 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 x40 . x32 x40 ⟶ x40 = x30 x36 x35 ⟶ x0 (x10 x39 x38) x36 ⟶ x0 (x10 x38 x37) x35 ⟶ (x0 (x10 x39 x37) x40 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 . x32 x39 ⟶ x39 = x30 x36 x35 ⟶ x0 (x10 x38 x37) x39 ⟶ (x0 (x10 (x22 x37 x38 x39 x35 x36) x37) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 . x32 x39 ⟶ x39 = x30 x36 x35 ⟶ x0 (x10 x38 x37) x39 ⟶ (x0 (x10 x38 (x22 x37 x38 x39 x35 x36)) x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x10 x36 x35 = x9 (x9 x36 x35) (x11 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 (x13 x35 x36) x35 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 (x13 x35 x36) x36 ⟶ False) ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x3 x36 x37 ⟶ x0 x35 x36 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ ((x33 = x26 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 (x10 (x15 x36 x35) (x14 x36 x35)) x35 ⟶ False) ⟶ (x0 (x14 x36 x35) x36 ⟶ False) ⟶ (x36 = x31 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x0 (x14 x37 x36) x37 ⟶ x0 (x10 x35 (x14 x37 x36)) x36 ⟶ (x37 = x31 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x37 = x31 x38 ⟶ x0 (x10 x36 x35) x38 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x36 = x31 x37 ⟶ x0 x35 x36 ⟶ (x0 (x10 (x21 x35 x36 x37) x35) x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 (x10 (x16 x36 x35) (x17 x36 x35)) x35 ⟶ False) ⟶ (x0 (x16 x36 x35) x36 ⟶ False) ⟶ (x36 = x27 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x0 (x16 x37 x36) x37 ⟶ x0 (x10 (x16 x37 x36) x35) x36 ⟶ (x37 = x27 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x37 = x27 x38 ⟶ x0 (x10 x35 x36) x38 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x36 = x27 x37 ⟶ x0 x35 x36 ⟶ (x0 (x10 x35 (x20 x35 x36 x37)) x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x3 x36 x35 ⟶ x3 x35 x36 ⟶ (x36 = x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x35 = x36 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x36 = x35 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x9 x36 x35 = x9 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x4 x35 ⟶ False) ⟶ x34 x35 ⟶ False) ⟶ (∀ x35 x36 . x32 x36 ⟶ x2 x35 (x1 x36) ⟶ (x32 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x4 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x32 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x0 x36 x35 ⟶ False) ⟶ (x31 (x30 x19 x18) = x31 x18 ⟶ False) ⟶ ((x3 (x27 x18) (x31 x19) ⟶ False) ⟶ False) ⟶ ((x32 x19 ⟶ False) ⟶ False) ⟶ ((x32 x18 ⟶ False) ⟶ False) ⟶ False (proof)