Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../56ca9..
PUTT9../05bfd..
vout
PrNUD../654fc.. 0.02 bars
TMW1g../6a452.. ownership of 8c737.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMQoA../4a734.. ownership of 5b63a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUeon../1c080.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 8c737.. : ∀ 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 x53 . x51 x53 ⟶ (x53 = x52 ⟶ False) ⟶ x51 x52 ⟶ False) ⟶ (∀ x52 x53 . x0 x52 x53 ⟶ x51 x53 ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ (x52 = x50 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x11 x55 ⟶ x2 x55 ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ (x7 x55 x52 x54 = x50 ⟶ False) ⟶ (x7 x55 x54 x52 = x50 ⟶ False) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x4 x53 x55 x52 x54 ⟶ x5 x53 x55 x52 x54 ⟶ (x6 x53 x55 x52 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x11 x55 ⟶ x2 x55 ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ (x7 x55 x52 x54 = x50 ⟶ False) ⟶ (x7 x55 x54 x52 = x50 ⟶ False) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x6 x53 x55 x52 x54 ⟶ (x5 x53 x55 x52 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x11 x55 ⟶ x2 x55 ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ (x7 x55 x52 x54 = x50 ⟶ False) ⟶ (x7 x55 x54 x52 = x50 ⟶ False) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x6 x53 x55 x52 x54 ⟶ (x4 x53 x55 x52 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x8 x52 x53 ⟶ (x51 x53 ⟶ False) ⟶ (x0 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 x57 x58 x59 . (x1 x59 ⟶ False) ⟶ x11 x59 ⟶ x2 x59 ⟶ x3 x59 ⟶ x8 x58 (x9 x59) ⟶ x8 x52 (x9 x59) ⟶ x8 x57 (x9 x59) ⟶ x8 x53 (x9 x59) ⟶ (x7 x59 x58 x52 = x50 ⟶ False) ⟶ (x7 x59 x52 x57 = x50 ⟶ False) ⟶ (x7 x59 x57 x53 = x50 ⟶ False) ⟶ x8 x54 (x7 x59 x58 x52) ⟶ x8 x56 (x7 x59 x52 x57) ⟶ x8 x55 (x7 x59 x57 x53) ⟶ (x12 x59 x58 x57 x53 (x12 x59 x58 x52 x57 x54 x56) x55 = x12 x59 x58 x52 x53 x54 (x12 x59 x52 x57 x53 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ (x7 x55 x52 x54 = x50 ⟶ False) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ (x12 x55 x52 x54 x54 x53 (x49 x55 x54) = x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x0 x53 x52 ⟶ (x8 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x1 x53 ⟶ False) ⟶ x10 x53 ⟶ x3 x53 ⟶ x8 x52 (x9 x53) ⟶ (x0 (x49 x53 x52) (x7 x53 x52 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x11 x55 ⟶ x2 x55 ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ (x7 x55 x52 x54 = x50 ⟶ False) ⟶ (x7 x55 x54 x52 = x50 ⟶ False) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x4 x53 x55 x52 x54 ⟶ (x13 x53 x55 x52 x54 ⟶ False) ⟶ False) ⟶ ((x48 x47 ⟶ False) ⟶ False) ⟶ (x51 x47 ⟶ False) ⟶ (x46 x45 ⟶ False) ⟶ ((x14 x45 ⟶ False) ⟶ False) ⟶ ((x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x15 x52 ⟶ False) ⟶ x51 (x16 x52) ⟶ False) ⟶ (∀ x52 . (x15 x52 ⟶ False) ⟶ (x8 (x16 x52) x52 ⟶ False) ⟶ False) ⟶ (x17 x18 ⟶ False) ⟶ (x51 x43 ⟶ False) ⟶ (x15 x19 ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ ((x14 x41 ⟶ False) ⟶ False) ⟶ ((x44 x41 ⟶ False) ⟶ False) ⟶ ((x17 x20 ⟶ False) ⟶ False) ⟶ (x51 x20 ⟶ False) ⟶ ((x51 x21 ⟶ False) ⟶ False) ⟶ ((x14 x40 ⟶ False) ⟶ False) ⟶ ((x44 x40 ⟶ False) ⟶ False) ⟶ ((x51 x50 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x8 (x22 x52) x52 ⟶ False) ⟶ False) ⟶ ((x3 x39 ⟶ False) ⟶ False) ⟶ ((x23 x24 ⟶ False) ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ (∀ x52 . x3 x52 ⟶ (x38 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x38 x52 ⟶ (x23 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x1 x53 ⟶ False) ⟶ x10 x53 ⟶ x3 x53 ⟶ x8 x52 (x9 x53) ⟶ (x8 (x49 x53 x52) (x7 x53 x52 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 x57 . (x1 x57 ⟶ False) ⟶ x3 x57 ⟶ x8 x56 (x9 x57) ⟶ x8 x52 (x9 x57) ⟶ x8 x55 (x9 x57) ⟶ x8 x53 (x7 x57 x56 x52) ⟶ x8 x54 (x7 x57 x52 x55) ⟶ (x8 (x12 x57 x56 x52 x55 x53 x54) (x7 x57 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x3 x55 ⟶ x8 x54 (x9 x55) ⟶ x8 x52 (x9 x55) ⟶ x8 x53 (x7 x55 x54 x52) ⟶ x26 x53 x52 x54 x55 = x25 x53 x52 x54 x55 ⟶ (x13 x53 x55 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x3 x55 ⟶ x8 x54 (x9 x55) ⟶ x8 x52 (x9 x55) ⟶ x8 x53 (x7 x55 x54 x52) ⟶ (x12 x55 x54 x52 (x36 x53 x52 x54 x55) x53 (x26 x53 x52 x54 x55) = x12 x55 x54 x52 (x36 x53 x52 x54 x55) x53 (x25 x53 x52 x54 x55) ⟶ False) ⟶ (x13 x53 x55 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x3 x55 ⟶ x8 x54 (x9 x55) ⟶ x8 x52 (x9 x55) ⟶ x8 x53 (x7 x55 x54 x52) ⟶ (x8 (x25 x53 x52 x54 x55) (x7 x55 x52 (x36 x53 x52 x54 x55)) ⟶ False) ⟶ (x13 x53 x55 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x3 x55 ⟶ x8 x54 (x9 x55) ⟶ x8 x52 (x9 x55) ⟶ x8 x53 (x7 x55 x54 x52) ⟶ (x8 (x26 x53 x52 x54 x55) (x7 x55 x52 (x36 x53 x52 x54 x55)) ⟶ False) ⟶ (x13 x53 x55 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x3 x55 ⟶ x8 x54 (x9 x55) ⟶ x8 x52 (x9 x55) ⟶ x8 x53 (x7 x55 x54 x52) ⟶ x7 x55 x52 (x36 x53 x52 x54 x55) = x50 ⟶ (x13 x53 x55 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x3 x55 ⟶ x8 x54 (x9 x55) ⟶ x8 x52 (x9 x55) ⟶ x8 x53 (x7 x55 x54 x52) ⟶ (x8 (x36 x53 x52 x54 x55) (x9 x55) ⟶ False) ⟶ (x13 x53 x55 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 x57 x58 . (x1 x58 ⟶ False) ⟶ x3 x58 ⟶ x8 x57 (x9 x58) ⟶ x8 x52 (x9 x58) ⟶ x8 x56 (x7 x58 x57 x52) ⟶ x13 x56 x58 x57 x52 ⟶ x8 x55 (x9 x58) ⟶ (x7 x58 x52 x55 = x50 ⟶ False) ⟶ x8 x54 (x7 x58 x52 x55) ⟶ x8 x53 (x7 x58 x52 x55) ⟶ x12 x58 x57 x52 x55 x56 x54 = x12 x58 x57 x52 x55 x56 x53 ⟶ (x54 = x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 . (x1 x56 ⟶ False) ⟶ x10 x56 ⟶ x3 x56 ⟶ x8 x52 (x9 x56) ⟶ x8 x55 (x9 x56) ⟶ x8 x53 (x7 x56 x52 x55) ⟶ x8 x54 (x7 x56 x55 x52) ⟶ x35 x56 x55 x52 x54 x53 ⟶ (x5 x53 x56 x52 x55 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x5 x53 x55 x52 x54 ⟶ (x35 x55 x54 x52 (x27 x53 x54 x52 x55) x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x5 x53 x55 x52 x54 ⟶ (x8 (x27 x53 x54 x52 x55) (x7 x55 x54 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 . (x1 x56 ⟶ False) ⟶ x10 x56 ⟶ x3 x56 ⟶ x8 x52 (x9 x56) ⟶ x8 x55 (x9 x56) ⟶ x8 x53 (x7 x56 x52 x55) ⟶ x8 x54 (x7 x56 x55 x52) ⟶ x35 x56 x52 x55 x53 x54 ⟶ (x4 x53 x56 x52 x55 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x4 x53 x55 x52 x54 ⟶ (x35 x55 x52 x54 x53 (x34 x53 x54 x52 x55) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x1 x55 ⟶ False) ⟶ x10 x55 ⟶ x3 x55 ⟶ x8 x52 (x9 x55) ⟶ x8 x54 (x9 x55) ⟶ x8 x53 (x7 x55 x52 x54) ⟶ x4 x53 x55 x52 x54 ⟶ (x8 (x34 x53 x54 x52 x55) (x7 x55 x54 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 . (x1 x56 ⟶ False) ⟶ x10 x56 ⟶ x3 x56 ⟶ x8 x52 (x9 x56) ⟶ x8 x55 (x9 x56) ⟶ x8 x53 (x7 x56 x52 x55) ⟶ x8 x54 (x7 x56 x55 x52) ⟶ x12 x56 x55 x52 x55 x54 x53 = x49 x56 x55 ⟶ (x35 x56 x52 x55 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 . (x1 x56 ⟶ False) ⟶ x10 x56 ⟶ x3 x56 ⟶ x8 x52 (x9 x56) ⟶ x8 x55 (x9 x56) ⟶ x8 x53 (x7 x56 x52 x55) ⟶ x8 x54 (x7 x56 x55 x52) ⟶ x35 x56 x52 x55 x53 x54 ⟶ (x12 x56 x55 x52 x55 x54 x53 = x49 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x1 x54 ⟶ False) ⟶ x10 x54 ⟶ x3 x54 ⟶ x8 x52 (x9 x54) ⟶ x8 x53 (x7 x54 x52 x52) ⟶ x12 x54 x52 x52 (x32 x53 x52 x54) x53 (x33 x53 x52 x54) = x33 x53 x52 x54 ⟶ (x53 = x49 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x1 x54 ⟶ False) ⟶ x10 x54 ⟶ x3 x54 ⟶ x8 x52 (x9 x54) ⟶ x8 x53 (x7 x54 x52 x52) ⟶ (x8 (x33 x53 x52 x54) (x7 x54 x52 (x32 x53 x52 x54)) ⟶ False) ⟶ (x53 = x49 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x1 x54 ⟶ False) ⟶ x10 x54 ⟶ x3 x54 ⟶ x8 x52 (x9 x54) ⟶ x8 x53 (x7 x54 x52 x52) ⟶ x7 x54 x52 (x32 x53 x52 x54) = x50 ⟶ (x53 = x49 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x1 x54 ⟶ False) ⟶ x10 x54 ⟶ x3 x54 ⟶ x8 x52 (x9 x54) ⟶ x8 x53 (x7 x54 x52 x52) ⟶ (x8 (x32 x53 x52 x54) (x9 x54) ⟶ False) ⟶ (x53 = x49 x54 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 x56 . (x1 x56 ⟶ False) ⟶ x10 x56 ⟶ x3 x56 ⟶ x8 x52 (x9 x56) ⟶ x8 x55 (x7 x56 x52 x52) ⟶ x55 = x49 x56 x52 ⟶ x8 x54 (x9 x56) ⟶ (x7 x56 x52 x54 = x50 ⟶ False) ⟶ x8 x53 (x7 x56 x52 x54) ⟶ (x12 x56 x52 x52 x54 x55 x53 = x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x48 x53 ⟶ x8 x52 x53 ⟶ (x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x48 x53 ⟶ x8 x52 x53 ⟶ (x44 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ (x48 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x17 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x46 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x17 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x17 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x44 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x44 x52 ⟶ x14 x52 ⟶ (x46 x52 ⟶ False) ⟶ (x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x44 x52 ⟶ x14 x52 ⟶ (x46 x52 ⟶ False) ⟶ (x44 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x44 x52 ⟶ x14 x52 ⟶ (x46 x52 ⟶ False) ⟶ x17 x52 ⟶ False) ⟶ (∀ x52 . (x17 x52 ⟶ False) ⟶ x15 x52 ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x46 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x44 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x17 x52 ⟶ False) ⟶ x51 x52 ⟶ False) ⟶ (∀ x52 . (x15 x52 ⟶ False) ⟶ x51 x52 ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x42 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x44 x52 ⟶ x14 x52 ⟶ (x44 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ (x17 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ (x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x0 x52 x53 ⟶ x0 x53 x52 ⟶ False) ⟶ (x6 x31 x28 x29 x30 ⟶ False) ⟶ (x7 x28 x30 x29 = x50 ⟶ False) ⟶ (x7 x28 x29 x30 = x50 ⟶ False) ⟶ ((x8 x31 (x7 x28 x29 x30) ⟶ False) ⟶ False) ⟶ ((x8 x30 (x9 x28) ⟶ False) ⟶ False) ⟶ ((x8 x29 (x9 x28) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x8 x54 (x9 x28) ⟶ x8 x52 (x9 x28) ⟶ x8 x53 (x7 x28 x54 x52) ⟶ (x4 x53 x28 x54 x52 ⟶ False) ⟶ False) ⟶ ((x3 x28 ⟶ False) ⟶ False) ⟶ ((x10 x28 ⟶ False) ⟶ False) ⟶ ((x2 x28 ⟶ False) ⟶ False) ⟶ ((x11 x28 ⟶ False) ⟶ False) ⟶ (x1 x28 ⟶ False) ⟶ False (proof)