Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrDeV../330f7..
PUYam../07a13..
vout
PrDeV../f1149.. 101.67 bars
TMKPG../1b8e8.. ownership of cdb7b.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TML3N../51d59.. ownership of 42bef.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUPLL../40449.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem cdb7b.. : ∀ 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 : ι → ι . ∀ x54 : ι → ο . ∀ x55 . ∀ x56 : ι → ο . ∀ x57 . ∀ x58 : ι → ο . (∀ x59 x60 . x58 x60 ⟶ (x60 = x59 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x58 x60 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x59 = x57 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x59 x60 ⟶ x2 x60 (x1 x61) ⟶ x58 x61 ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x60 x61 ⟶ x2 x61 (x1 x59) ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x3 x60 x59 ⟶ (x2 x60 (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x59) ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x59 x60 ⟶ (x58 x60 ⟶ False) ⟶ (x0 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x60 x59 ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (x58 x4 ⟶ False) ⟶ (∀ x59 . (x3 x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x59 (x1 x61) ⟶ x2 x60 x59 ⟶ (x5 x60 x61 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x59 (x1 x61) ⟶ x5 x60 x61 x59 ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 x60 ⟶ (x6 x60 x59 = x7 x59 ⟶ False) ⟶ False) ⟶ ((x56 x55 ⟶ False) ⟶ False) ⟶ (x58 x55 ⟶ False) ⟶ (∀ x59 . (x54 x59 ⟶ False) ⟶ x54 (x53 x59) ⟶ False) ⟶ (∀ x59 . (x54 x59 ⟶ False) ⟶ (x2 (x53 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x54 (x52 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ x58 (x52 x59) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x52 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (x8 x9 ⟶ False) ⟶ ((x51 x9 ⟶ False) ⟶ False) ⟶ ((x10 x9 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x49 (x50 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x50 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x48 x59 ⟶ False) ⟶ x46 x59 ⟶ x58 (x47 x59) ⟶ False) ⟶ (∀ x59 . (x48 x59 ⟶ False) ⟶ x46 x59 ⟶ (x2 (x47 x59) (x1 (x11 x59)) ⟶ False) ⟶ False) ⟶ ((x51 x45 ⟶ False) ⟶ False) ⟶ ((x12 x45 ⟶ False) ⟶ False) ⟶ ((x10 x45 ⟶ False) ⟶ False) ⟶ (x58 x45 ⟶ False) ⟶ (∀ x59 . x49 (x44 x59) x59 ⟶ False) ⟶ (∀ x59 . (x2 (x44 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x51 x43 ⟶ False) ⟶ False) ⟶ ((x12 x43 ⟶ False) ⟶ False) ⟶ ((x10 x43 ⟶ False) ⟶ False) ⟶ (x58 x13 ⟶ False) ⟶ (∀ x59 . (x58 (x42 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x42 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x12 x41 ⟶ False) ⟶ False) ⟶ ((x10 x41 ⟶ False) ⟶ False) ⟶ ((x40 x39 ⟶ False) ⟶ False) ⟶ ((x51 x39 ⟶ False) ⟶ False) ⟶ ((x10 x39 ⟶ False) ⟶ False) ⟶ (x58 x14 ⟶ False) ⟶ ((x8 x14 ⟶ False) ⟶ False) ⟶ ((x51 x14 ⟶ False) ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x15 x59 ⟶ False) ⟶ x46 x59 ⟶ x54 (x16 x59) ⟶ False) ⟶ (∀ x59 . (x15 x59 ⟶ False) ⟶ x46 x59 ⟶ (x2 (x16 x59) (x1 (x11 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x48 x59 ⟶ False) ⟶ x46 x59 ⟶ (x54 (x17 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x48 x59 ⟶ False) ⟶ x46 x59 ⟶ x58 (x17 x59) ⟶ False) ⟶ (∀ x59 . (x48 x59 ⟶ False) ⟶ x46 x59 ⟶ (x2 (x17 x59) (x1 (x11 x59)) ⟶ False) ⟶ False) ⟶ ((x58 x38 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ x58 (x18 x59) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x18 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x10 x19 ⟶ False) ⟶ False) ⟶ (x58 x19 ⟶ False) ⟶ ((x51 x20 ⟶ False) ⟶ False) ⟶ ((x10 x20 ⟶ False) ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x51 x22 ⟶ False) ⟶ False) ⟶ ((x10 x22 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x37 x59 ⟶ False) ⟶ x46 x59 ⟶ x36 (x11 x59) ⟶ False) ⟶ (∀ x59 . x37 x59 ⟶ x46 x59 ⟶ (x36 (x11 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . x15 x59 ⟶ x46 x59 ⟶ (x54 (x11 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x15 x59 ⟶ False) ⟶ x46 x59 ⟶ x54 (x11 x59) ⟶ False) ⟶ (∀ x59 . x58 (x7 x59) ⟶ False) ⟶ (∀ x59 . (x48 x59 ⟶ False) ⟶ x46 x59 ⟶ x58 (x11 x59) ⟶ False) ⟶ ((x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 (x1 x59) ⟶ False) ⟶ (∀ x59 . x48 x59 ⟶ x46 x59 ⟶ (x58 (x11 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ (x56 (x7 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ (x5 (x35 x59 x60) x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x23 x59) x59 ⟶ False) ⟶ False) ⟶ ((x46 x34 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x48 x60 ⟶ False) ⟶ x46 x60 ⟶ (x58 x59 ⟶ False) ⟶ x2 x59 (x1 (x11 x60)) ⟶ (x5 (x24 x60 x59) (x11 x60) x59 ⟶ False) ⟶ False) ⟶ ((x58 x33 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x59 (x1 x61) ⟶ x5 x60 x61 x59 ⟶ (x2 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 x60 ⟶ (x2 (x6 x60 x59) (x1 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 (x25 x59 x60) x59 ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x0 (x25 x59 x60) x60 ⟶ False) ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x3 x60 x61 ⟶ x0 x59 x60 ⟶ (x0 x59 x61 ⟶ False) ⟶ False) ⟶ ((x57 = x33 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x26 x60 x59 = x59 ⟶ False) ⟶ (x0 (x26 x60 x59) x60 ⟶ False) ⟶ (x60 = x7 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 (x26 x60 x59) x60 ⟶ x26 x60 x59 = x59 ⟶ (x60 = x7 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x60 = x7 x61 ⟶ x59 = x61 ⟶ (x0 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x60 = x7 x61 ⟶ x0 x59 x60 ⟶ (x59 = x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x3 x60 x59 ⟶ x3 x59 x60 ⟶ (x60 = x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x59 = x60 ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x60 = x59 ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x32 x59 x57 ⟶ (x48 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x56 x60 ⟶ x2 x59 (x1 x60) ⟶ (x56 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x48 x59 ⟶ (x32 x59 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x56 x60 ⟶ x2 x59 x60 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x56 x60 ⟶ x2 x59 x60 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ (x37 x59 ⟶ False) ⟶ x15 x59 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x56 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x15 x59 ⟶ (x37 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x54 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x8 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x54 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x54 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x54 x60 ⟶ x2 x59 (x1 x60) ⟶ (x54 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ (x37 x59 ⟶ False) ⟶ x37 x59 ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ (x37 x59 ⟶ False) ⟶ x48 x59 ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ (x8 x59 ⟶ False) ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ (x8 x59 ⟶ False) ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ (x8 x59 ⟶ False) ⟶ x54 x59 ⟶ False) ⟶ (∀ x59 x60 . x58 x60 ⟶ x2 x59 (x1 x60) ⟶ x49 x59 x60 ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x48 x59 ⟶ (x37 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x48 x59 ⟶ (x48 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ (x12 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x8 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ x58 x59 ⟶ (x49 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ (x31 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x10 x60 ⟶ x51 x60 ⟶ x2 x59 (x1 x60) ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ x58 x59 ⟶ (x21 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ x58 x59 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ x58 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ (x49 x59 x60 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ (x15 x59 ⟶ False) ⟶ x48 x59 ⟶ False) ⟶ (∀ x59 x60 . x10 x60 ⟶ x2 x59 (x1 x60) ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x40 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x51 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ x21 x59 ⟶ (x30 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ x21 x59 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x51 x59 ⟶ x21 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x58 x60 ⟶ x2 x59 (x1 x60) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x48 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ (x15 x59 ⟶ False) ⟶ x48 x59 ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x32 x59 x4 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ x32 x59 x4 ⟶ x48 x59 ⟶ False) ⟶ (∀ x59 . x46 x59 ⟶ (x48 x59 ⟶ False) ⟶ x15 x59 ⟶ (x32 x59 x4 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x0 x60 x59 ⟶ False) ⟶ (x27 = x6 (x11 x28) x29 ⟶ False) ⟶ ((x11 x28 = x6 (x11 x28) x29 ⟶ False) ⟶ False) ⟶ ((x2 x29 (x11 x28) ⟶ False) ⟶ False) ⟶ ((x2 x27 (x1 (x11 x28)) ⟶ False) ⟶ False) ⟶ (x58 x27 ⟶ False) ⟶ ((x46 x28 ⟶ False) ⟶ False) ⟶ (x48 x28 ⟶ False) ⟶ False (proof)