Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../08043..
PUUBU../58b9d..
vout
PrPhD../b56af.. 3.38 bars
TMFob../01b59.. ownership of c2569.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMW7P../d79db.. ownership of 2aa09.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUXLE../12e16.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c2569.. : ∀ 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 . x56 x59 x57 ⟶ x56 x58 x57 ⟶ (x55 x59 x58 ⟶ False) ⟶ x53 x59 x58 = x54 ⟶ False) ⟶ (∀ x58 x59 . x0 x59 ⟶ (x59 = x58 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 x59 . x52 x58 x59 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x58 = x1 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x52 x58 x59 ⟶ x56 x59 (x51 x60) ⟶ x0 x60 ⟶ False) ⟶ (∀ x58 x59 x60 . x52 x59 x60 ⟶ x56 x60 (x51 x58) ⟶ (x56 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x50 x1 x58 = x1 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x2 x59 x58 ⟶ (x56 x59 (x51 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x59 (x51 x58) ⟶ (x2 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x50 x58 x1 = x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x52 x59 x60 ⟶ x52 x58 x60 ⟶ x52 x58 (x49 x60 x59) ⟶ False) ⟶ (∀ x58 x59 . x52 x59 x58 ⟶ (x52 (x49 x58 x59) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x58 x59 ⟶ (x0 x59 ⟶ False) ⟶ (x52 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 . x56 x58 x57 ⟶ (x58 = x54 ⟶ False) ⟶ (x52 (x4 x54 x58) x3 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x52 x59 x58 ⟶ (x56 x59 x58 ⟶ False) ⟶ False) ⟶ ((x56 x1 x5 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x48 x58 x1 = x58 ⟶ False) ⟶ False) ⟶ ((x2 x57 x3 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x47 x59 ⟶ x47 x58 ⟶ x46 x59 x58 ⟶ (x46 x58 x59 ⟶ False) ⟶ False) ⟶ ((x56 x6 x3 ⟶ False) ⟶ False) ⟶ ((x56 x6 x45 ⟶ False) ⟶ False) ⟶ ((x7 x6 x3 x45 ⟶ False) ⟶ False) ⟶ ((x44 x6 ⟶ False) ⟶ False) ⟶ (x0 x6 ⟶ False) ⟶ (∀ x58 . (x2 x58 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x0 x60 ⟶ False) ⟶ (x0 x58 ⟶ False) ⟶ x56 x58 (x51 x60) ⟶ x56 x59 x58 ⟶ (x7 x59 x60 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x0 x60 ⟶ False) ⟶ (x0 x58 ⟶ False) ⟶ x56 x58 (x51 x60) ⟶ x7 x59 x60 x58 ⟶ (x56 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x8 x58 x59 = x50 x58 x59 ⟶ False) ⟶ False) ⟶ ((x45 = x5 ⟶ False) ⟶ False) ⟶ ((x54 = x1 ⟶ False) ⟶ False) ⟶ ((x43 x42 ⟶ False) ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ ((x41 x40 ⟶ False) ⟶ False) ⟶ (x0 x40 ⟶ False) ⟶ (x39 x38 ⟶ False) ⟶ ((x9 x38 ⟶ False) ⟶ False) ⟶ ((x37 x38 ⟶ False) ⟶ False) ⟶ ((x41 x10 ⟶ False) ⟶ False) ⟶ (x36 x35 ⟶ False) ⟶ (x0 x11 ⟶ False) ⟶ ((x47 x34 ⟶ False) ⟶ False) ⟶ ((x12 x34 ⟶ False) ⟶ False) ⟶ ((x33 x34 ⟶ False) ⟶ False) ⟶ (x0 x34 ⟶ False) ⟶ ((x32 x31 ⟶ False) ⟶ False) ⟶ ((x9 x31 ⟶ False) ⟶ False) ⟶ ((x37 x31 ⟶ False) ⟶ False) ⟶ ((x36 x13 ⟶ False) ⟶ False) ⟶ (x0 x13 ⟶ False) ⟶ ((x0 x14 ⟶ False) ⟶ False) ⟶ ((x47 x30 ⟶ False) ⟶ False) ⟶ ((x9 x15 ⟶ False) ⟶ False) ⟶ ((x37 x15 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x48 x58 x58 = x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x59 x5 ⟶ x58 = x4 x59 x6 ⟶ (x52 x58 x29 ⟶ False) ⟶ False) ⟶ (∀ x58 . x52 x58 x29 ⟶ (x58 = x4 (x16 x58) x6 ⟶ False) ⟶ False) ⟶ (∀ x58 . x52 x58 x29 ⟶ (x56 (x16 x58) x5 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x56 x60 x5 ⟶ x56 x58 x5 ⟶ x59 = x4 x60 x58 ⟶ x46 x60 x58 ⟶ (x58 = x1 ⟶ False) ⟶ (x52 x59 x17 ⟶ False) ⟶ False) ⟶ (∀ x58 . x52 x58 x17 ⟶ x28 x58 = x1 ⟶ False) ⟶ (∀ x58 . x52 x58 x17 ⟶ (x46 (x18 x58) (x28 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . x52 x58 x17 ⟶ (x58 = x4 (x18 x58) (x28 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . x52 x58 x17 ⟶ (x56 (x28 x58) x5 ⟶ False) ⟶ False) ⟶ (∀ x58 . x52 x58 x17 ⟶ (x56 (x18 x58) x5 ⟶ False) ⟶ False) ⟶ (x19 x3 ⟶ False) ⟶ ((x47 x5 ⟶ False) ⟶ False) ⟶ (x0 x5 ⟶ False) ⟶ (∀ x58 x59 . (x0 x59 ⟶ False) ⟶ x0 (x48 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x0 x59 ⟶ False) ⟶ x0 (x48 x59 x58) ⟶ False) ⟶ (x0 x57 ⟶ False) ⟶ (∀ x58 x59 . x0 (x4 x58 x59) ⟶ False) ⟶ ((x0 x1 ⟶ False) ⟶ False) ⟶ (x0 x3 ⟶ False) ⟶ (∀ x58 x59 . (x0 x59 ⟶ False) ⟶ (x0 x58 ⟶ False) ⟶ x56 x58 (x51 x59) ⟶ (x7 (x27 x58 x59) x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x56 (x20 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x0 x60 ⟶ False) ⟶ (x0 x58 ⟶ False) ⟶ x56 x58 (x51 x60) ⟶ x7 x59 x60 x58 ⟶ (x56 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x56 (x8 x58 x59) (x51 x58) ⟶ False) ⟶ False) ⟶ ((x56 x45 (x51 x3) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x59 x57 ⟶ x56 x58 x57 ⟶ (x56 (x53 x59 x58) x57 ⟶ False) ⟶ False) ⟶ ((x56 x54 x26 ⟶ False) ⟶ False) ⟶ ((x26 = x48 (x8 x17 x29) x5 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x59 x57 ⟶ x56 x58 x57 ⟶ (x55 x58 x59 ⟶ False) ⟶ (x25 x59 x58 = x4 x54 (x53 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x59 x57 ⟶ x56 x58 x57 ⟶ x55 x58 x59 ⟶ (x25 x59 x58 = x53 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x56 x59 x57 ⟶ x56 x58 x57 ⟶ (x55 x59 x58 ⟶ False) ⟶ (x55 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x48 x59 x58 = x48 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x24 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x43 x59 ⟶ x56 x58 (x51 x59) ⟶ (x43 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x56 x58 x5 ⟶ (x41 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x43 x59 ⟶ x56 x58 x59 ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x43 x59 ⟶ x56 x58 x59 ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x41 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x43 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x41 x58 ⟶ (x47 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x36 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x39 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x36 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x36 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x47 x59 ⟶ x56 x58 x59 ⟶ (x47 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x37 x58 ⟶ x9 x58 ⟶ (x39 x58 ⟶ False) ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x37 x58 ⟶ x9 x58 ⟶ (x39 x58 ⟶ False) ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x37 x58 ⟶ x9 x58 ⟶ (x39 x58 ⟶ False) ⟶ x36 x58 ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x21 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x39 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x47 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x37 x59 ⟶ x9 x59 ⟶ x56 x58 (x51 x59) ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x36 x58 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . x33 x58 ⟶ x12 x58 ⟶ (x47 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x32 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ x37 x58 ⟶ x9 x58 ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x36 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x47 x58 ⟶ (x12 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x47 x58 ⟶ (x33 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x0 x58 ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x24 x59 ⟶ x56 x58 (x51 x59) ⟶ (x24 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x52 x58 x59 ⟶ x52 x59 x58 ⟶ False) ⟶ (x52 (x25 x23 x22) x3 ⟶ False) ⟶ ((x56 x22 x57 ⟶ False) ⟶ False) ⟶ ((x56 x23 x57 ⟶ False) ⟶ False) ⟶ False (proof)