Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../2d5b8..
PUQPW../00223..
vout
PrPhD../d2c69.. 3.40 bars
TMRTE../9e06f.. ownership of 2b1ea.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMFf7../c792c.. ownership of da987.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUeSw../df34c.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2b1ea.. : ∀ 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 . x37 x39 ⟶ (x39 = x38 ⟶ False) ⟶ x37 x38 ⟶ False) ⟶ (∀ x38 x39 . x0 x38 x39 ⟶ x37 x39 ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x38 = x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x0 x38 x39 ⟶ x2 x39 (x1 x40) ⟶ x37 x40 ⟶ False) ⟶ (∀ x38 x39 x40 . x0 x39 x40 ⟶ x2 x40 (x1 x38) ⟶ (x2 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x3 x39 x38 ⟶ (x2 x39 (x1 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x2 x39 (x1 x38) ⟶ (x3 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x2 x38 x39 ⟶ (x37 x39 ⟶ False) ⟶ (x0 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x0 x39 x38 ⟶ (x2 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ x0 x39 (x5 x40) ⟶ x38 = x7 x40 x39 ⟶ (x0 (x6 x39 x38) x40 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ x0 (x6 x39 x38) x40 ⟶ (x38 = x7 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ x0 (x6 x39 x38) x40 ⟶ (x0 x39 (x5 x40) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x4 x38 ⟶ x3 x39 x38 ⟶ (x3 (x35 x39) (x35 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x4 x38 ⟶ x3 x39 x38 ⟶ (x3 (x5 x39) (x5 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x3 x38 x38 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ (x37 x10 ⟶ False) ⟶ (x11 x12 ⟶ False) ⟶ ((x8 x12 ⟶ False) ⟶ False) ⟶ ((x4 x12 ⟶ False) ⟶ False) ⟶ ((x8 x34 ⟶ False) ⟶ False) ⟶ ((x13 x34 ⟶ False) ⟶ False) ⟶ ((x4 x34 ⟶ False) ⟶ False) ⟶ (x37 x34 ⟶ False) ⟶ ((x8 x33 ⟶ False) ⟶ False) ⟶ ((x13 x33 ⟶ False) ⟶ False) ⟶ ((x4 x33 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x4 x14 ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x8 x16 ⟶ False) ⟶ False) ⟶ ((x4 x16 ⟶ False) ⟶ False) ⟶ ((x32 x31 ⟶ False) ⟶ False) ⟶ ((x4 x17 ⟶ False) ⟶ False) ⟶ (x37 x17 ⟶ False) ⟶ ((x8 x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ x4 x38 ⟶ x37 (x35 x38) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ x4 x38 ⟶ x37 (x5 x38) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x4 (x19 (x6 x39 x38) (x6 x41 x40)) ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x37 (x35 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x4 (x20 (x6 x39 x38)) ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x37 (x5 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x21 x38 ⟶ x4 x38 ⟶ (x21 (x35 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x21 x38 ⟶ x4 x38 ⟶ (x21 (x5 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x32 (x6 x38 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x8 (x20 (x6 x39 x38)) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x22 x39 ⟶ x8 x39 ⟶ (x37 (x7 x39 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x21 x38 ⟶ False) ⟶ x4 x38 ⟶ x8 x38 ⟶ x21 (x5 x38) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x8 x39 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x9 (x19 x39 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x8 x38 ⟶ (x9 (x20 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x8 x38 ⟶ (x11 x38 ⟶ False) ⟶ x21 (x35 x38) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x8 x38 ⟶ x11 x38 ⟶ (x21 (x35 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x37 (x35 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x37 x39 ⟶ False) ⟶ x4 x39 ⟶ x13 x39 ⟶ x8 x39 ⟶ x2 x38 (x5 x39) ⟶ x37 (x7 x39 x38) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x37 (x5 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x13 x38 ⟶ x8 x38 ⟶ (x30 (x35 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x2 (x23 x38) x38 ⟶ False) ⟶ False) ⟶ ((x37 x29 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x6 x39 x38 = x19 (x19 x39 x38) (x20 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x0 (x6 (x28 x38 x39) (x27 x38 x39)) x38 ⟶ (x3 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ (x0 (x6 (x28 x38 x39) (x27 x38 x39)) x39 ⟶ False) ⟶ (x3 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x4 x41 ⟶ x3 x41 x38 ⟶ x0 (x6 x39 x40) x41 ⟶ (x0 (x6 x39 x40) x38 ⟶ False) ⟶ False) ⟶ ((x36 = x29 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ (x0 x39 (x5 x40) ⟶ False) ⟶ x38 = x36 ⟶ (x38 = x7 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ (x0 x39 (x5 x40) ⟶ False) ⟶ x38 = x7 x40 x39 ⟶ (x38 = x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ x0 x39 (x5 x40) ⟶ x0 (x6 x39 x38) x40 ⟶ (x38 = x7 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x4 x40 ⟶ x8 x40 ⟶ x0 x39 (x5 x40) ⟶ x38 = x7 x40 x39 ⟶ (x0 (x6 x39 x38) x40 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x19 x39 x38 = x19 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x9 x39 ⟶ x2 x38 (x1 x39) ⟶ (x9 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x9 x39 ⟶ x2 x38 x39 ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x9 x39 ⟶ x2 x38 x39 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x9 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x21 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x11 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x21 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x21 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x8 x38 ⟶ (x11 x38 ⟶ False) ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x8 x38 ⟶ (x11 x38 ⟶ False) ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x4 x38 ⟶ x8 x38 ⟶ (x11 x38 ⟶ False) ⟶ x21 x38 ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ (x13 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x11 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ (x22 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x8 x39 ⟶ x2 x38 (x1 x39) ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x4 x39 ⟶ x2 x38 (x1 x39) ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x15 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x4 x38 ⟶ x8 x38 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x4 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x0 x38 x39 ⟶ x0 x39 x38 ⟶ False) ⟶ (∀ x38 . x0 x38 (x5 x26) ⟶ (x7 x26 x38 = x7 x25 x38 ⟶ False) ⟶ (x3 x26 x25 ⟶ False) ⟶ False) ⟶ ((x3 (x5 x26) (x5 x25) ⟶ False) ⟶ (x3 x26 x25 ⟶ False) ⟶ False) ⟶ (x3 x26 x25 ⟶ x3 (x5 x26) (x5 x25) ⟶ x7 x26 x24 = x7 x25 x24 ⟶ False) ⟶ (x3 x26 x25 ⟶ x3 (x5 x26) (x5 x25) ⟶ (x0 x24 (x5 x26) ⟶ False) ⟶ False) ⟶ ((x8 x25 ⟶ False) ⟶ False) ⟶ ((x4 x25 ⟶ False) ⟶ False) ⟶ ((x8 x26 ⟶ False) ⟶ False) ⟶ ((x4 x26 ⟶ False) ⟶ False) ⟶ False (proof)