Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../f6ed0..
PUKn5../9753e..
vout
PrPhD../fe9c2.. 102.57 bars
TMXzU../c3c80.. ownership of fd582.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMVFc../3f531.. ownership of a2c7d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUPYb../d561f.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem fd582.. : ∀ 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 . x36 x38(x38 = x37False)x36 x37False)(∀ x37 x38 x39 x40 . x0 x39 x40x0 x38 x37(x0 (x2 x39 x38) (x1 x40 x37)False)False)(∀ x37 x38 x39 x40 . x0 (x2 x38 x40) (x1 x37 x39)(x0 x40 x39False)False)(∀ x37 x38 x39 x40 . x0 (x2 x40 x38) (x1 x39 x37)(x0 x40 x39False)False)(∀ x37 x38 . x0 x37 x38x36 x38False)(∀ x37 . x36 x37(x37 = x3False)False)(∀ x37 x38 x39 . x0 x37 x38x34 x38 (x35 x39)x36 x39False)(∀ x37 x38 x39 . x0 x38 x39x34 x39 (x35 x37)(x34 x38 x37False)False)(∀ x37 x38 . x33 x38 x37(x34 x38 (x35 x37)False)False)(∀ x37 x38 . x34 x38 (x35 x37)(x33 x38 x37False)False)(∀ x37 x38 . x34 x37 x38(x36 x38False)(x0 x37 x38False)False)(∀ x37 x38 . x0 x38 x37(x34 x38 x37False)False)(∀ x37 . (x33 x37 x37False)False)(∀ x37 x38 x39 x40 . x34 x40 (x35 (x1 x39 x38))(x4 x39 x38 x37 x40 = x5 x37 x40False)False)(∀ x37 x38 . x32 x38x31 x38 x37(x5 x37 x38 = x38False)False)(∀ x37 x38 . x32 x38(x5 x37 (x5 x37 x38) = x5 x37 x38False)False)(∀ x37 . (x36 x37False)(x29 (x30 x37) x37False)False)(∀ x37 . (x36 x37False)(x34 (x30 x37) (x35 x37)False)False)(∀ x37 . x29 (x28 x37) x37False)(∀ x37 . (x34 (x28 x37) (x35 x37)False)False)(∀ x37 x38 . (x31 (x27 x37 x38) x37False)False)(∀ x37 x38 . (x6 (x27 x38 x37) x37False)False)(∀ x37 x38 . (x32 (x27 x37 x38)False)False)(x36 x7False)(∀ x37 . (x36 (x26 x37)False)False)(∀ x37 . (x34 (x26 x37) (x35 x37)False)False)((x25 x24False)False)((x32 x24False)False)((x36 x23False)False)(∀ x37 . (x36 x37False)x36 (x8 x37)False)(∀ x37 . (x36 x37False)(x34 (x8 x37) (x35 x37)False)False)((x32 x9False)False)(x36 x9False)(∀ x37 x38 x39 x40 . (x32 (x10 (x2 x38 x37) (x2 x40 x39))False)False)(∀ x37 x38 . (x32 (x1 x37 x38)False)False)(∀ x37 x38 . (x32 (x11 (x2 x38 x37))False)False)(∀ x37 x38 . x36 (x10 x37 x38)False)(∀ x37 x38 x39 . x32 x39x31 x39 x37(x31 (x5 x38 x39) x37False)False)(∀ x37 x38 x39 . x32 x39x31 x39 x38(x31 (x5 x37 x39) x37False)False)(∀ x37 x38 x39 . x32 x39x31 x39 x38(x32 (x5 x37 x39)False)False)(∀ x37 x38 x39 . x32 x39x6 x39 x37(x6 (x5 x38 x39) x37False)False)(∀ x37 x38 x39 . x32 x39x6 x39 x38(x32 (x5 x37 x39)False)False)(∀ x37 . x36 (x11 x37)False)((x36 x3False)False)(∀ x37 . x36 (x35 x37)False)(∀ x37 x38 . x32 x38x36 x37(x32 (x5 x37 x38)False)False)(∀ x37 x38 . x32 x38x36 x37(x36 (x5 x37 x38)False)False)(∀ x37 x38 . (x36 x38False)(x36 x37False)x36 (x1 x38 x37)False)(∀ x37 . (x34 (x22 x37) x37False)False)((x36 x12False)False)(∀ x37 x38 x39 x40 . x34 x40 (x35 (x1 x39 x38))(x34 (x4 x39 x38 x37 x40) (x35 (x1 x39 x38))False)False)(∀ x37 x38 . x32 x38(x32 (x5 x37 x38)False)False)(∀ x37 x38 . (x2 x38 x37 = x10 (x10 x38 x37) (x11 x38)False)False)(∀ x37 x38 . x32 x38x0 (x2 (x13 x37 x38) (x14 x37 x38)) x37(x33 x38 x37False)False)(∀ x37 x38 . x32 x38(x0 (x2 (x13 x37 x38) (x14 x37 x38)) x38False)(x33 x38 x37False)False)(∀ x37 x38 x39 x40 . x32 x40x33 x40 x37x0 (x2 x38 x39) x40(x0 (x2 x38 x39) x37False)False)((x3 = x12False)False)(∀ x37 x38 x39 . x32 x39x32 x37(x0 (x2 (x15 x37 x39 x38) (x16 x37 x39 x38)) x39False)(x0 (x2 (x15 x37 x39 x38) (x16 x37 x39 x38)) x37False)(x37 = x5 x38 x39False)False)(∀ x37 x38 x39 . x32 x39x32 x37(x0 (x16 x37 x39 x38) x38False)(x0 (x2 (x15 x37 x39 x38) (x16 x37 x39 x38)) x37False)(x37 = x5 x38 x39False)False)(∀ x37 x38 x39 . x32 x39x32 x37x0 (x2 (x15 x37 x39 x38) (x16 x37 x39 x38)) x37x0 (x16 x37 x39 x38) x38x0 (x2 (x15 x37 x39 x38) (x16 x37 x39 x38)) x39(x37 = x5 x38 x39False)False)(∀ x37 x38 x39 x40 x41 . x32 x41x32 x37x37 = x5 x40 x41x0 x38 x40x0 (x2 x39 x38) x41(x0 (x2 x39 x38) x37False)False)(∀ x37 x38 x39 x40 x41 . x32 x41x32 x37x37 = x5 x40 x41x0 (x2 x39 x38) x37(x0 (x2 x39 x38) x41False)False)(∀ x37 x38 x39 x40 x41 . x32 x41x32 x37x37 = x5 x40 x41x0 (x2 x39 x38) x37(x0 x38 x40False)False)(∀ x37 x38 . (x10 x38 x37 = x10 x37 x38False)False)(∀ x37 x38 . x36 x38x32 x37x31 x37 x38(x31 x37 x38False)False)(∀ x37 x38 . x36 x38x32 x37x31 x37 x38(x32 x37False)False)(∀ x37 x38 . x36 x38x32 x37x31 x37 x38(x36 x37False)False)(∀ x37 x38 . x36 x38x32 x37x6 x37 x38(x6 x37 x38False)False)(∀ x37 x38 . x36 x38x32 x37x6 x37 x38(x32 x37False)False)(∀ x37 x38 . x36 x38x32 x37x6 x37 x38(x36 x37False)False)(∀ x37 x38 x39 . x32 x39x31 x39 x37x34 x38 (x35 x39)(x31 x38 x37False)False)(∀ x37 x38 x39 . x32 x39x6 x39 x37x34 x38 (x35 x39)(x6 x38 x37False)False)(∀ x37 x38 . x36 x38x34 x37 (x35 x38)x29 x37 x38False)(∀ x37 x38 x39 . x36 x39x34 x37 (x35 (x1 x38 x39))(x36 x37False)False)(∀ x37 . x36 x37x32 x37(x25 x37False)False)(∀ x37 . x36 x37x32 x37(x32 x37False)False)(∀ x37 x38 . (x36 x38False)x34 x37 (x35 x38)x36 x37(x29 x37 x38False)False)(∀ x37 x38 x39 . x36 x39x34 x37 (x35 (x1 x39 x38))(x36 x37False)False)(∀ x37 . x36 x37x32 x37(x21 x37False)False)(∀ x37 . x36 x37x32 x37(x32 x37False)False)(∀ x37 x38 . (x36 x38False)x34 x37 (x35 x38)(x29 x37 x38False)x36 x37False)(∀ x37 x38 x39 . x34 x39 (x35 (x1 x37 x38))(x31 x39 x38False)False)(∀ x37 x38 x39 . x34 x39 (x35 (x1 x38 x37))(x6 x39 x38False)False)(∀ x37 x38 . x32 x38x34 x37 (x35 x38)(x32 x37False)False)(∀ x37 x38 . x36 x38x34 x37 (x35 x38)(x36 x37False)False)(∀ x37 x38 x39 . x34 x39 (x35 (x1 x37 x38))(x32 x39False)False)(∀ x37 . x36 x37(x32 x37False)False)(∀ x37 x38 . x0 x37 x38x0 x38 x37False)(x34 (x4 x19 x20 x17 x18) (x35 (x1 x19 x17))False)((x34 x18 (x35 (x1 x19 x20))False)False)False (proof)