Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../39e06..
PUcTB../8d35e..
vout
PrPhD../24519.. 3.40 bars
TMK2e../3f058.. ownership of 8f193.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMMiW../d77e7.. ownership of f3b63.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUYgF../8ad7d.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 8f193.. : ∀ 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 x41 : ι → ι . ∀ x42 : ι → ο . ∀ x43 . ∀ x44 : ι → ο . ∀ x45 : ι → ι → ο . ∀ x46 : ι → ο . ∀ x47 . ∀ x48 : ι → ι → ο . ∀ x49 : ι → ι . ∀ x50 : ι → ο . (∀ x51 x52 . x50 x52(x52 = x51False)x50 x51False)(∀ x51 x52 . x0 x51 x52x50 x52False)(∀ x51 x52 . x0 x52 x51(x48 x52 (x49 x51)False)False)(∀ x51 . (x0 x51 (x1 x51)False)False)(∀ x51 . x50 x51(x51 = x47False)False)(∀ x51 x52 x53 . x0 x51 x52x3 x52 (x2 x53)x50 x53False)(∀ x51 x52 x53 . x0 x52 x53x3 x53 (x2 x51)(x3 x52 x51False)False)(∀ x51 x52 . x48 x52 x51(x3 x52 (x2 x51)False)False)(∀ x51 x52 . x3 x52 (x2 x51)(x48 x52 x51False)False)(∀ x51 x52 . x3 x51 x52(x50 x52False)(x0 x51 x52False)False)(∀ x51 x52 . x46 x52x46 x51x45 x52 x51(x0 x52 (x1 x51)False)False)(∀ x51 x52 . x46 x52x46 x51x0 x52 (x1 x51)(x45 x52 x51False)False)(∀ x51 x52 . x0 x52 x51(x3 x52 x51False)False)(∀ x51 . (x4 x51 x47 = x51False)False)(∀ x51 . (x48 x51 x51False)False)(∀ x51 x52 . x46 x52x46 x51(x45 x52 x52False)False)(∀ x51 x52 . x46 x52x46 x51x48 x52 x51(x45 x52 x51False)False)(∀ x51 x52 . x46 x52x46 x51x45 x52 x51(x48 x52 x51False)False)((x44 x43False)False)(x50 x43False)(∀ x51 . (x42 x51False)x42 (x41 x51)False)(∀ x51 . (x42 x51False)(x3 (x41 x51) (x2 x51)False)False)(∀ x51 . (x50 x51False)(x42 (x40 x51)False)False)(∀ x51 . (x50 x51False)x50 (x40 x51)False)(∀ x51 . (x50 x51False)(x3 (x40 x51) (x2 x51)False)False)((x5 x6False)False)(x50 x6False)(x7 x8False)((x39 x8False)False)((x9 x8False)False)(∀ x51 . (x50 x51False)(x37 (x38 x51) x51False)False)(∀ x51 . (x50 x51False)(x3 (x38 x51) (x2 x51)False)False)((x5 x36False)False)(∀ x51 . x37 (x10 x51) x51False)(∀ x51 . (x3 (x10 x51) (x2 x51)False)False)(x50 x11False)(∀ x51 . (x50 (x35 x51)False)False)(∀ x51 . (x3 (x35 x51) (x2 x51)False)False)((x46 x34False)False)((x12 x34False)False)((x33 x34False)False)(x50 x34False)((x32 x31False)False)((x39 x31False)False)((x9 x31False)False)(x50 x13False)((x7 x13False)False)((x39 x13False)False)((x9 x13False)False)((x50 x14False)False)(∀ x51 . (x50 x51False)x50 (x30 x51)False)(∀ x51 . (x50 x51False)(x3 (x30 x51) (x2 x51)False)False)((x46 x29False)False)((x39 x15False)False)((x9 x15False)False)((x16 x17False)False)((x39 x17False)False)((x9 x17False)False)(∀ x51 . (x4 x51 x51 = x51False)False)(∀ x51 . x46 x51x5 x51(x5 (x1 x51)False)False)(∀ x51 x52 . (x50 x52False)x50 (x4 x51 x52)False)(∀ x51 x52 . (x50 x52False)x50 (x4 x52 x51)False)(∀ x51 . x46 x51(x46 (x49 x51)False)False)(∀ x51 . x50 (x18 x51)False)(∀ x51 . x46 x51(x46 (x1 x51)False)False)(∀ x51 . x46 x51x50 (x1 x51)False)((x50 x47False)False)(∀ x51 . x50 (x2 x51)False)(∀ x51 . x50 (x1 x51)False)(∀ x51 . x9 x51x39 x51(x44 (x18 x51)False)False)(∀ x51 . (x3 (x28 x51) x51False)False)((x50 x19False)False)(∀ x51 x52 . (x0 (x27 x52 x51) x51False)(x0 (x26 x52 x51) x52False)(x52 = x49 x51False)False)(∀ x51 x52 . (x0 (x26 x52 x51) (x27 x52 x51)False)(x0 (x26 x52 x51) x52False)(x52 = x49 x51False)False)(∀ x51 x52 x53 . x0 (x26 x53 x52) x53x0 (x26 x53 x52) x51x0 x51 x52(x53 = x49 x52False)False)(∀ x51 x52 x53 x54 . x53 = x49 x54x0 x52 x51x0 x51 x54(x0 x52 x53False)False)(∀ x51 x52 x53 . x52 = x49 x53x0 x51 x52(x0 (x25 x51 x52 x53) x53False)False)(∀ x51 x52 x53 . x52 = x49 x53x0 x51 x52(x0 x51 (x25 x51 x52 x53)False)False)(∀ x51 x52 . x0 (x24 x51 x52) x51(x48 x52 x51False)False)(∀ x51 x52 . (x0 (x24 x51 x52) x52False)(x48 x52 x51False)False)(∀ x51 x52 x53 . x48 x52 x53x0 x51 x52(x0 x51 x53False)False)((x47 = x19False)False)(∀ x51 . (x1 x51 = x4 x51 (x18 x51)False)False)(∀ x51 x52 . x48 x52 x51x48 x51 x52(x52 = x51False)False)(∀ x51 x52 . x51 = x52(x48 x52 x51False)False)(∀ x51 x52 . x52 = x51(x48 x52 x51False)False)(∀ x51 x52 . x46 x52x46 x51(x45 x52 x51False)(x45 x51 x52False)False)(∀ x51 x52 . (x4 x52 x51 = x4 x51 x52False)False)(∀ x51 . x50 x51(x23 x51False)False)(∀ x51 x52 . x44 x52x3 x51 (x2 x52)(x44 x51False)False)(∀ x51 x52 . x44 x52x3 x51 x52(x39 x51False)False)(∀ x51 x52 . x44 x52x3 x51 x52(x9 x51False)False)(∀ x51 . x50 x51(x5 x51False)False)(∀ x51 . x50 x51(x44 x51False)False)(∀ x51 . x5 x51(x46 x51False)False)(∀ x51 . x42 x51x9 x51x39 x51(x7 x51False)False)(∀ x51 . x42 x51x9 x51x39 x51(x39 x51False)False)(∀ x51 . x42 x51x9 x51x39 x51(x9 x51False)False)(∀ x51 x52 . x42 x52x3 x51 (x2 x52)(x42 x51False)False)(∀ x51 x52 . x46 x52x3 x51 x52(x46 x51False)False)(∀ x51 . x9 x51x39 x51(x7 x51False)(x39 x51False)False)(∀ x51 . x9 x51x39 x51(x7 x51False)(x9 x51False)False)(∀ x51 . x9 x51x39 x51(x7 x51False)x42 x51False)(∀ x51 x52 . x50 x52x3 x51 (x2 x52)x37 x51 x52False)(∀ x51 . x50 x51(x22 x51False)False)(∀ x51 . x50 x51x9 x51x39 x51(x7 x51False)False)(∀ x51 . x50 x51x9 x51x39 x51(x39 x51False)False)(∀ x51 . x50 x51x9 x51x39 x51(x9 x51False)False)(∀ x51 x52 . (x50 x52False)x3 x51 (x2 x52)x50 x51(x37 x51 x52False)False)(∀ x51 . x50 x51(x46 x51False)False)(∀ x51 x52 . x9 x52x39 x52x3 x51 (x2 x52)(x39 x51False)False)(∀ x51 . x9 x51x39 x51x50 x51(x16 x51False)False)(∀ x51 . x9 x51x39 x51x50 x51(x39 x51False)False)(∀ x51 . x9 x51x39 x51x50 x51(x9 x51False)False)(∀ x51 x52 . (x50 x52False)x3 x51 (x2 x52)(x37 x51 x52False)x50 x51False)(∀ x51 . x33 x51x12 x51(x46 x51False)False)(∀ x51 . x50 x51x9 x51x39 x51(x32 x51False)False)(∀ x51 . x50 x51x9 x51x39 x51(x39 x51False)False)(∀ x51 . x50 x51x9 x51x39 x51(x9 x51False)False)(∀ x51 . x9 x51x39 x51x16 x51(x20 x51False)False)(∀ x51 . x9 x51x39 x51x16 x51(x39 x51False)False)(∀ x51 . x9 x51x39 x51x16 x51(x9 x51False)False)(∀ x51 x52 . x50 x52x3 x51 (x2 x52)(x50 x51False)False)(∀ x51 . x46 x51(x12 x51False)False)(∀ x51 . x46 x51(x33 x51False)False)(∀ x51 . x50 x51(x39 x51False)False)(∀ x51 x52 . x23 x52x3 x51 (x2 x52)(x23 x51False)False)(∀ x51 x52 . x0 x51 x52x0 x52 x51False)(x49 (x1 x21) = x21False)((x46 x21False)False)False (proof)