Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../7d572..
PUTBB../1a032..
vout
PrNUD../035e8.. 0.00 bars
TMLRE../e0f81.. ownership of d6ffc.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMSJT../3edff.. ownership of 0df04.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUXY8../d99a0.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem d6ffc.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 . ∀ x7 : ι → ι . ∀ x8 x9 . ∀ x10 x11 : ι → ι . ∀ x12 . ∀ x13 : ι → ι → ι → ο . ∀ x14 : ι → ι → ο . ∀ x15 . ∀ x16 x17 : ι → ι → ι . ∀ x18 x19 : ι → ι → ο . ∀ x20 . (∀ x21 x22 . x19 x22 x20x19 x21 x20x18 x22 x21(x17 x22 (x16 x21 x22) = x21False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20x18 x22 x21(x19 (x16 x21 x22) x20False)False)(∀ x21 x22 x23 . x19 x23 x20x19 x21 x20x19 x22 x20(x17 x23 (x17 x21 x22) = x17 (x17 x23 x21) x22False)False)(∀ x21 x22 x23 . x0 x21 x22x19 x22 (x1 x23)x2 x23False)(∀ x21 x22 . x19 x22 x20x19 x21 x20x17 x22 x21 = x15(x22 = x15False)False)(∀ x21 x22 x23 . x0 x22 x23x19 x23 (x1 x21)(x19 x22 x21False)False)(∀ x21 x22 . x14 x22 x21(x19 x22 (x1 x21)False)False)(∀ x21 x22 . x19 x22 (x1 x21)(x14 x22 x21False)False)(∀ x21 x22 . x19 x21 x22(x2 x22False)(x0 x21 x22False)False)(∀ x21 x22 . x0 x22 x21(x19 x22 x21False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20x17 x22 x21 = x21(x22 = x15False)False)(∀ x21 . (x14 x21 x21False)False)(∀ x21 x22 x23 . (x2 x23False)(x2 x21False)x19 x21 (x1 x23)x19 x22 x21(x13 x22 x23 x21False)False)(∀ x21 x22 x23 . (x2 x23False)(x2 x21False)x19 x21 (x1 x23)x13 x22 x23 x21(x19 x22 x21False)False)((x15 = x12False)False)(∀ x21 x22 . (x2 x22False)(x2 x21False)x19 x21 (x1 x22)(x13 (x3 x21 x22) x22 x21False)False)(∀ x21 . (x19 (x11 x21) x21False)False)(∀ x21 x22 x23 . (x2 x23False)(x2 x21False)x19 x21 (x1 x23)x13 x22 x23 x21(x19 x22 x23False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20(x19 (x17 x22 x21) x20False)False)(∀ x21 x22 . x19 x22 x4x19 x21 x4(x13 (x5 x22 x21) (x1 x6) x4False)False)(∀ x21 . x19 x21 x4(x19 (x10 x21) x20False)False)(∀ x21 . x19 x21 x20(x13 (x7 x21) (x1 x6) x4False)False)((x19 x4 (x1 (x1 x6))False)False)((x19 x15 x6False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20(x21 = x15False)(x22 = x15False)(x17 x22 x21 = x10 (x5 (x7 x22) (x7 x21))False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20x22 = x15(x17 x22 x21 = x21False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20x21 = x15(x17 x22 x21 = x22False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20(x18 x22 x21False)(x18 x21 x22False)False)(∀ x21 x22 . x19 x22 x20x19 x21 x20(x17 x22 x21 = x17 x21 x22False)False)(∀ x21 x22 . x19 x22 x4x19 x21 x4(x5 x22 x21 = x5 x21 x22False)False)(∀ x21 x22 . x0 x21 x22x0 x22 x21False)(x8 = x9False)((x18 x9 x8False)False)((x18 x8 x9False)False)((x19 x9 x20False)False)((x19 x8 x20False)False)False (proof)