Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../791e2..
PUK8f../1c2d6..
vout
PrPhD../82edb.. 3.39 bars
TMR1C../d8ea5.. ownership of 2e546.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMGHG../ab9d0.. ownership of 7d018.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUfzP../2cd39.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2e546.. : ∀ 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 . x38 x40 ⟶ (x40 = x39 ⟶ False) ⟶ x38 x39 ⟶ False) ⟶ (∀ x39 x40 . x0 x39 x40 ⟶ x38 x40 ⟶ False) ⟶ (∀ x39 . x38 x39 ⟶ (x39 = x37 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x0 x39 x40 ⟶ x2 x40 (x1 x41) ⟶ x38 x41 ⟶ False) ⟶ (∀ x39 x40 x41 . x0 x40 x41 ⟶ x2 x41 (x1 x39) ⟶ (x2 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x3 x40 x39 ⟶ (x2 x40 (x1 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x2 x40 (x1 x39) ⟶ (x3 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 x43 x44 x45 . (x4 x45 ⟶ False) ⟶ x9 x45 ⟶ x5 x45 ⟶ x2 x39 (x8 x45) ⟶ x2 x44 (x8 x45) ⟶ x2 x40 (x8 x45) ⟶ x2 x43 (x8 x45) ⟶ x2 x41 (x1 (x8 x45)) ⟶ x2 x42 (x1 (x8 x45)) ⟶ x0 x39 x41 ⟶ x0 x44 x41 ⟶ x0 x40 x42 ⟶ x0 x43 x42 ⟶ x7 x45 x41 x42 ⟶ (x6 x45 x39 x44 x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x4 x41 ⟶ False) ⟶ x9 x41 ⟶ x5 x41 ⟶ x2 x39 (x1 (x8 x41)) ⟶ x2 x40 (x1 (x8 x41)) ⟶ x7 x41 x39 x40 ⟶ (x36 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x4 x41 ⟶ False) ⟶ x9 x41 ⟶ x5 x41 ⟶ x2 x39 (x1 (x8 x41)) ⟶ x2 x40 (x1 (x8 x41)) ⟶ x7 x41 x39 x40 ⟶ (x36 x39 x41 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x2 x39 x40 ⟶ (x38 x40 ⟶ False) ⟶ (x0 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x0 x40 x39 ⟶ (x2 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x4 x40 ⟶ False) ⟶ x9 x40 ⟶ x5 x40 ⟶ x2 x39 (x1 (x8 x40)) ⟶ x36 x39 x40 ⟶ x35 x39 x40 = x34 x39 x40 ⟶ False) ⟶ (∀ x39 x40 . (x4 x40 ⟶ False) ⟶ x9 x40 ⟶ x5 x40 ⟶ x2 x39 (x1 (x8 x40)) ⟶ x36 x39 x40 ⟶ (x0 (x34 x39 x40) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x4 x40 ⟶ False) ⟶ x9 x40 ⟶ x5 x40 ⟶ x2 x39 (x1 (x8 x40)) ⟶ x36 x39 x40 ⟶ (x0 (x35 x39 x40) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x4 x40 ⟶ False) ⟶ x9 x40 ⟶ x5 x40 ⟶ x2 x39 (x1 (x8 x40)) ⟶ x36 x39 x40 ⟶ (x2 (x34 x39 x40) (x8 x40) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x4 x40 ⟶ False) ⟶ x9 x40 ⟶ x5 x40 ⟶ x2 x39 (x1 (x8 x40)) ⟶ x36 x39 x40 ⟶ (x2 (x35 x39 x40) (x8 x40) ⟶ False) ⟶ False) ⟶ (x38 x10 ⟶ False) ⟶ (∀ x39 . (x3 x39 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x4 x41 ⟶ False) ⟶ x9 x41 ⟶ x5 x41 ⟶ x2 x39 (x8 x41) ⟶ x2 x40 (x8 x41) ⟶ (x11 x41 x39 x40 = x12 x41 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x33 x39 ⟶ False) ⟶ x31 x39 ⟶ x38 (x32 x39) ⟶ False) ⟶ (∀ x39 . (x33 x39 ⟶ False) ⟶ x31 x39 ⟶ (x2 (x32 x39) (x1 (x8 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x4 x39 ⟶ False) ⟶ x31 x39 ⟶ x30 (x29 x39) ⟶ False) ⟶ (∀ x39 . (x4 x39 ⟶ False) ⟶ x31 x39 ⟶ (x2 (x29 x39) (x1 (x8 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x33 x39 ⟶ False) ⟶ x31 x39 ⟶ (x30 (x28 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x33 x39 ⟶ False) ⟶ x31 x39 ⟶ x38 (x28 x39) ⟶ False) ⟶ (∀ x39 . (x33 x39 ⟶ False) ⟶ x31 x39 ⟶ (x2 (x28 x39) (x1 (x8 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x4 x39 ⟶ False) ⟶ x9 x39 ⟶ x5 x39 ⟶ (x36 (x13 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x4 x39 ⟶ False) ⟶ x9 x39 ⟶ x5 x39 ⟶ (x2 (x13 x39) (x1 (x8 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 . (x4 x42 ⟶ False) ⟶ x9 x42 ⟶ x5 x42 ⟶ x2 x39 (x8 x42) ⟶ x2 x41 (x8 x42) ⟶ x2 x40 (x1 (x8 x42)) ⟶ x36 x40 x42 ⟶ x0 x39 x40 ⟶ x0 x41 x40 ⟶ (x39 = x41 ⟶ False) ⟶ (x40 = x11 x42 x39 x41 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x27 x39 ⟶ False) ⟶ x31 x39 ⟶ x26 (x8 x39) ⟶ False) ⟶ (∀ x39 . x27 x39 ⟶ x31 x39 ⟶ (x26 (x8 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . x4 x39 ⟶ x31 x39 ⟶ (x30 (x8 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x4 x39 ⟶ False) ⟶ x31 x39 ⟶ x30 (x8 x39) ⟶ False) ⟶ (∀ x39 . (x33 x39 ⟶ False) ⟶ x31 x39 ⟶ x38 (x8 x39) ⟶ False) ⟶ (∀ x39 . x33 x39 ⟶ x31 x39 ⟶ (x38 (x8 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x2 (x25 x39) x39 ⟶ False) ⟶ False) ⟶ ((x31 x14 ⟶ False) ⟶ False) ⟶ ((x5 x24 ⟶ False) ⟶ False) ⟶ (∀ x39 . x5 x39 ⟶ (x31 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x4 x41 ⟶ False) ⟶ x9 x41 ⟶ x5 x41 ⟶ x2 x39 (x8 x41) ⟶ x2 x40 (x8 x41) ⟶ (x2 (x11 x41 x39 x40) (x1 (x8 x41)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x4 x41 ⟶ False) ⟶ x9 x41 ⟶ x5 x41 ⟶ x2 x39 (x8 x41) ⟶ x2 x40 (x8 x41) ⟶ (x2 (x12 x41 x39 x40) (x1 (x8 x41)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 x43 x44 . (x4 x44 ⟶ False) ⟶ x9 x44 ⟶ x5 x44 ⟶ x2 x39 (x8 x44) ⟶ x2 x43 (x8 x44) ⟶ x2 x40 (x1 (x8 x44)) ⟶ x2 x42 (x8 x44) ⟶ x2 x41 (x8 x44) ⟶ (x42 = x41 ⟶ False) ⟶ x40 = x11 x44 x42 x41 ⟶ x6 x44 x39 x43 x42 x41 ⟶ (x23 x44 x39 x43 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 . (x4 x42 ⟶ False) ⟶ x9 x42 ⟶ x5 x42 ⟶ x2 x39 (x8 x42) ⟶ x2 x41 (x8 x42) ⟶ x2 x40 (x1 (x8 x42)) ⟶ x23 x42 x39 x41 x40 ⟶ (x6 x42 x39 x41 (x16 x40 x41 x39 x42) (x15 x40 x41 x39 x42) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 . (x4 x42 ⟶ False) ⟶ x9 x42 ⟶ x5 x42 ⟶ x2 x39 (x8 x42) ⟶ x2 x41 (x8 x42) ⟶ x2 x40 (x1 (x8 x42)) ⟶ x23 x42 x39 x41 x40 ⟶ (x40 = x11 x42 (x16 x40 x41 x39 x42) (x15 x40 x41 x39 x42) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 . (x4 x42 ⟶ False) ⟶ x9 x42 ⟶ x5 x42 ⟶ x2 x39 (x8 x42) ⟶ x2 x41 (x8 x42) ⟶ x2 x40 (x1 (x8 x42)) ⟶ x23 x42 x39 x41 x40 ⟶ x16 x40 x41 x39 x42 = x15 x40 x41 x39 x42 ⟶ False) ⟶ (∀ x39 x40 x41 x42 . (x4 x42 ⟶ False) ⟶ x9 x42 ⟶ x5 x42 ⟶ x2 x39 (x8 x42) ⟶ x2 x41 (x8 x42) ⟶ x2 x40 (x1 (x8 x42)) ⟶ x23 x42 x39 x41 x40 ⟶ (x2 (x15 x40 x41 x39 x42) (x8 x42) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 x42 . (x4 x42 ⟶ False) ⟶ x9 x42 ⟶ x5 x42 ⟶ x2 x39 (x8 x42) ⟶ x2 x41 (x8 x42) ⟶ x2 x40 (x1 (x8 x42)) ⟶ x23 x42 x39 x41 x40 ⟶ (x2 (x16 x40 x41 x39 x42) (x8 x42) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x4 x41 ⟶ False) ⟶ x9 x41 ⟶ x5 x41 ⟶ x2 x39 (x8 x41) ⟶ x2 x40 (x8 x41) ⟶ (x11 x41 x39 x40 = x11 x41 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x17 x39 x37 ⟶ (x33 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x33 x39 ⟶ (x17 x39 x37 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ (x27 x39 ⟶ False) ⟶ x4 x39 ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x4 x39 ⟶ (x27 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ (x27 x39 ⟶ False) ⟶ x27 x39 ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ (x27 x39 ⟶ False) ⟶ x33 x39 ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x33 x39 ⟶ (x27 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x33 x39 ⟶ (x33 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ (x4 x39 ⟶ False) ⟶ x33 x39 ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x33 x39 ⟶ (x4 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ (x4 x39 ⟶ False) ⟶ x33 x39 ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x17 x39 x10 ⟶ (x4 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x17 x39 x10 ⟶ x33 x39 ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ (x33 x39 ⟶ False) ⟶ x4 x39 ⟶ (x17 x39 x10 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x0 x39 x40 ⟶ x0 x40 x39 ⟶ False) ⟶ (x23 x22 x19 x20 x21 ⟶ False) ⟶ ((x7 x22 x18 x21 ⟶ False) ⟶ False) ⟶ ((x0 x20 x18 ⟶ False) ⟶ False) ⟶ ((x0 x19 x18 ⟶ False) ⟶ False) ⟶ ((x2 x21 (x1 (x8 x22)) ⟶ False) ⟶ False) ⟶ ((x2 x18 (x1 (x8 x22)) ⟶ False) ⟶ False) ⟶ ((x2 x20 (x8 x22) ⟶ False) ⟶ False) ⟶ ((x2 x19 (x8 x22) ⟶ False) ⟶ False) ⟶ ((x5 x22 ⟶ False) ⟶ False) ⟶ ((x9 x22 ⟶ False) ⟶ False) ⟶ (x4 x22 ⟶ False) ⟶ False (proof)