Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../7732c..
PUe2D../ac33e..
vout
PrPhD../31a5d.. 102.61 bars
TMHZH../c48a7.. ownership of 4dd7a.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMZXp../af97c.. ownership of 90c4d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUbFF../3de27.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 4dd7a.. : ∀ 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 . (x28 x32 ⟶ False) ⟶ x19 x32 ⟶ x27 x32 ⟶ x20 x32 ⟶ x26 x32 ⟶ x21 x32 ⟶ x24 x31 (x25 x32) ⟶ x24 x29 (x25 x32) ⟶ x24 x30 (x25 x32) ⟶ x23 x32 x31 x29 ⟶ x23 x32 x31 x30 ⟶ (x23 x32 x31 (x22 x32 x29 x30) ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x20 x31 ⟶ x21 x31 ⟶ x24 x30 (x25 x31) ⟶ x24 x29 (x25 x31) ⟶ (x0 x31 (x22 x31 x30 x29) x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x18 x31 x29 x30 ⟶ (x18 x31 x30 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x20 x31 ⟶ x26 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ (x23 x31 x29 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ (x18 x31 x29 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x20 x31 ⟶ x26 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x0 x31 x29 x30 ⟶ (x23 x31 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x20 x31 ⟶ x26 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x23 x31 x29 x30 ⟶ (x0 x31 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x29 = x30 ⟶ (x18 x31 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x18 x31 x29 x30 ⟶ (x29 = x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x1 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ (x22 x31 x29 x30 = x2 x31 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x28 x30 ⟶ False) ⟶ x19 x30 ⟶ x20 x30 ⟶ x26 x30 ⟶ x21 x30 ⟶ x24 x29 (x25 x30) ⟶ (x22 x30 x29 x29 = x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . (x24 (x3 x29) x29 ⟶ False) ⟶ False) ⟶ ((x21 x16 ⟶ False) ⟶ False) ⟶ ((x4 x5 ⟶ False) ⟶ False) ⟶ ((x15 x14 ⟶ False) ⟶ False) ⟶ ((x1 x6 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x4 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x1 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x4 x29 ⟶ (x15 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x1 x29 ⟶ (x15 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x1 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ (x24 (x22 x31 x29 x30) (x25 x31) ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x1 x31 ⟶ x24 x30 (x25 x31) ⟶ x24 x29 (x25 x31) ⟶ (x24 (x2 x31 x30 x29) (x25 x31) ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x23 x31 x29 x30 ⟶ x23 x31 x30 x29 ⟶ (x18 x31 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x18 x31 x29 x30 ⟶ (x23 x31 x30 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x17 x31 ⟶ x21 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ x18 x31 x29 x30 ⟶ (x23 x31 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 x31 ⟶ False) ⟶ x19 x31 ⟶ x1 x31 ⟶ x24 x29 (x25 x31) ⟶ x24 x30 (x25 x31) ⟶ (x22 x31 x29 x30 = x22 x31 x30 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x13 x29 ⟶ x12 x29 ⟶ x19 x29 ⟶ x27 x29 ⟶ x20 x29 ⟶ x26 x29 ⟶ (x17 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x13 x29 ⟶ x12 x29 ⟶ x19 x29 ⟶ x27 x29 ⟶ x20 x29 ⟶ x26 x29 ⟶ x28 x29 ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ (x26 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ (x20 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ (x27 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ (x19 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ (x12 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ (x13 x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . x21 x29 ⟶ (x28 x29 ⟶ False) ⟶ x17 x29 ⟶ x28 x29 ⟶ False) ⟶ (∀ x29 . x24 x29 (x25 x7) ⟶ x23 x7 x29 x10 ⟶ x23 x7 x29 x8 ⟶ (x23 x7 x29 x9 ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ False) ⟶ False) ⟶ ((x23 x7 x9 x8 ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ False) ⟶ False) ⟶ ((x23 x7 x9 x10 ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ False) ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ x23 x7 x9 x10 ⟶ x23 x7 x9 x8 ⟶ x23 x7 x11 x9 ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ x23 x7 x9 x10 ⟶ x23 x7 x9 x8 ⟶ (x23 x7 x11 x8 ⟶ False) ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ x23 x7 x9 x10 ⟶ x23 x7 x9 x8 ⟶ (x23 x7 x11 x10 ⟶ False) ⟶ False) ⟶ (x18 x7 x9 (x22 x7 x10 x8) ⟶ x23 x7 x9 x10 ⟶ x23 x7 x9 x8 ⟶ (x24 x11 (x25 x7) ⟶ False) ⟶ False) ⟶ ((x24 x8 (x25 x7) ⟶ False) ⟶ False) ⟶ ((x24 x10 (x25 x7) ⟶ False) ⟶ False) ⟶ ((x24 x9 (x25 x7) ⟶ False) ⟶ False) ⟶ ((x21 x7 ⟶ False) ⟶ False) ⟶ ((x17 x7 ⟶ False) ⟶ False) ⟶ (x28 x7 ⟶ False) ⟶ False (proof)