Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../54026..
PULGC../d10e6..
vout
PrPhD../e0032.. 3.40 bars
TMRtR../d4138.. ownership of 0e5d4.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMHM4../e48bc.. ownership of 7b8e9.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PULzY../2e230.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 0e5d4.. : ∀ 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 . x48 x50 ⟶ (x50 = x49 ⟶ False) ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 x50 . x0 x49 x50 ⟶ x48 x50 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x49 = x47 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x49 x50 ⟶ x2 x50 (x1 x51) ⟶ x48 x51 ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x50 x51 ⟶ x2 x51 (x1 x49) ⟶ (x2 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x3 x47 x49 = x47 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x50 x51 ⟶ x0 x50 x49 ⟶ x46 x51 x49 ⟶ False) ⟶ (∀ x49 x50 . (x46 x50 x49 ⟶ False) ⟶ (x0 (x4 x49 x50) x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x46 x49 x50 ⟶ False) ⟶ (x0 (x4 x50 x49) x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x5 x50 x49 ⟶ (x2 x50 (x1 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x2 x50 (x1 x49) ⟶ (x5 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x3 x49 x47 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x2 x49 x50 ⟶ (x48 x50 ⟶ False) ⟶ (x0 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ (x50 = x49 ⟶ False) ⟶ x0 (x8 x50 x49) x51 ⟶ (x0 x50 (x7 x51 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ x0 x50 (x7 x51 x49) ⟶ (x0 (x8 x50 x49) x51 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ x0 x49 (x7 x51 x50) ⟶ x49 = x50 ⟶ False) ⟶ (∀ x49 x50 . x0 x50 x49 ⟶ (x2 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x49 x50 ⟶ (x46 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x5 x49 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x9 x49 x50 = x3 x49 x50 ⟶ False) ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ (x48 x44 ⟶ False) ⟶ (x43 x42 ⟶ False) ⟶ ((x10 x42 ⟶ False) ⟶ False) ⟶ ((x6 x42 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x41 x11 ⟶ False) ⟶ False) ⟶ ((x6 x11 ⟶ False) ⟶ False) ⟶ (x48 x11 ⟶ False) ⟶ ((x10 x12 ⟶ False) ⟶ False) ⟶ ((x41 x12 ⟶ False) ⟶ False) ⟶ ((x6 x12 ⟶ False) ⟶ False) ⟶ ((x41 x40 ⟶ False) ⟶ False) ⟶ ((x6 x40 ⟶ False) ⟶ False) ⟶ ((x39 x38 ⟶ False) ⟶ False) ⟶ ((x10 x38 ⟶ False) ⟶ False) ⟶ ((x6 x38 ⟶ False) ⟶ False) ⟶ ((x6 x13 ⟶ False) ⟶ False) ⟶ (x48 x13 ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ ((x6 x14 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 x52 . (x6 (x15 (x8 x50 x49) (x8 x52 x51)) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x6 (x37 (x8 x50 x49)) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x6 (x3 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x48 x50 ⟶ x6 x50 ⟶ (x48 (x36 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x48 x49 ⟶ (x48 (x36 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x10 (x37 (x8 x50 x49)) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x10 x50 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x45 (x15 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x6 x49 ⟶ x10 x49 ⟶ (x45 (x37 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x2 (x16 x49) x49 ⟶ False) ⟶ False) ⟶ ((x48 x35 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x2 (x9 x49 x50) (x1 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x0 (x8 (x34 x49 x50) (x33 x49 x50)) x50 ⟶ (x32 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x0 (x8 (x33 x49 x50) (x34 x49 x50)) x50 ⟶ (x32 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x33 x49 x50 = x34 x49 x50 ⟶ (x32 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x0 (x34 x49 x50) x49 ⟶ False) ⟶ (x32 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x0 (x33 x49 x50) x49 ⟶ False) ⟶ (x32 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 x52 . x6 x52 ⟶ x32 x52 x49 ⟶ x0 x51 x49 ⟶ x0 x50 x49 ⟶ (x51 = x50 ⟶ False) ⟶ (x0 (x8 x51 x50) x52 ⟶ False) ⟶ (x0 (x8 x50 x51) x52 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x27 x50 x49 ⟶ x31 x50 x49 ⟶ x28 x50 x49 ⟶ x32 x50 x49 ⟶ x30 x50 x49 ⟶ (x29 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x29 x50 x49 ⟶ (x30 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x29 x50 x49 ⟶ (x32 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x29 x50 x49 ⟶ (x28 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x29 x50 x49 ⟶ (x31 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x29 x50 x49 ⟶ (x27 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x8 x50 x49 = x15 (x15 x50 x49) (x37 x50) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ x0 x50 (x17 x49 x51) ⟶ x46 (x7 x51 x50) (x17 x49 x51) ⟶ (x30 x51 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x17 x49 x50 = x47 ⟶ (x30 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x5 (x17 x49 x50) x49 ⟶ False) ⟶ (x30 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ x30 x51 x49 ⟶ x5 x50 x49 ⟶ (x50 = x47 ⟶ False) ⟶ (x46 (x7 x51 (x26 x50 x49 x51)) x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ x30 x51 x49 ⟶ x5 x50 x49 ⟶ (x50 = x47 ⟶ False) ⟶ (x0 (x26 x50 x49 x51) x50 ⟶ False) ⟶ False) ⟶ ((x47 = x35 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x7 x50 x49 = x9 (x18 x50 x49) (x37 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x0 (x8 (x25 x49 x50) (x25 x49 x50)) x50 ⟶ (x27 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x0 (x25 x49 x50) x49 ⟶ False) ⟶ (x27 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x6 x51 ⟶ x27 x51 x49 ⟶ x0 x50 x49 ⟶ (x0 (x8 x50 x50) x51 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ (x18 x50 x49 = x36 x50 (x37 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x15 x50 x49 = x15 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x45 x50 ⟶ x2 x49 (x1 x50) ⟶ (x45 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x45 x50 ⟶ x2 x49 x50 ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x45 x50 ⟶ x2 x49 x50 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x45 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x19 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x43 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x19 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x19 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x6 x49 ⟶ x10 x49 ⟶ (x43 x49 ⟶ False) ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x6 x49 ⟶ x10 x49 ⟶ (x43 x49 ⟶ False) ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x6 x49 ⟶ x10 x49 ⟶ (x43 x49 ⟶ False) ⟶ x19 x49 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ (x41 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x43 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ (x24 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x10 x50 ⟶ x2 x49 (x1 x50) ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 ⟶ x2 x49 (x1 x50) ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x39 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x6 x49 ⟶ x10 x49 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x6 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x0 x49 x50 ⟶ x0 x50 x49 ⟶ False) ⟶ (∀ x49 . x0 x49 x23 ⟶ x0 (x8 x49 (x22 x49)) x21 ⟶ False) ⟶ (∀ x49 . x0 x49 x23 ⟶ (x0 (x22 x49) x23 ⟶ False) ⟶ False) ⟶ (x23 = x47 ⟶ False) ⟶ ((x5 x23 x20 ⟶ False) ⟶ False) ⟶ ((x29 x21 x20 ⟶ False) ⟶ False) ⟶ ((x6 x21 ⟶ False) ⟶ False) ⟶ False (proof)