Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../37edf..
PUbhY../fc23f..
vout
PrPhD../32b23.. 3.40 bars
TMMNG../51ddb.. ownership of 2d617.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMUm3../49408.. ownership of f864f.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUhQG../a19f2.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2d617.. : ∀ 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 . x43 x45 ⟶ (x45 = x44 ⟶ False) ⟶ x43 x44 ⟶ False) ⟶ (∀ x44 x45 . x0 x44 x45 ⟶ x43 x45 ⟶ False) ⟶ (∀ x44 x45 . x42 x45 ⟶ x42 x44 ⟶ (x38 (x37 x45 x44) = x39 (x41 (x38 x45) (x38 x44)) (x41 (x40 x45) (x40 x44)) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x42 x45 ⟶ x42 x44 ⟶ (x40 (x37 x45 x44) = x37 (x41 (x40 x45) (x38 x44)) (x41 (x38 x45) (x40 x44)) ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x44 = x36 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x0 x44 x45 ⟶ x2 x45 (x1 x46) ⟶ x43 x46 ⟶ False) ⟶ (∀ x44 x45 x46 . x0 x45 x46 ⟶ x2 x46 (x1 x44) ⟶ (x2 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x3 x45 x44 ⟶ (x2 x45 (x1 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x45 (x1 x44) ⟶ (x3 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x4 x44 ⟶ (x41 x5 x44 = x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x44 x45 ⟶ (x43 x45 ⟶ False) ⟶ (x0 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x0 x45 x44 ⟶ (x2 x45 x44 ⟶ False) ⟶ False) ⟶ ((x2 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x4 x46 ⟶ x4 x44 ⟶ x4 x45 ⟶ (x41 (x41 x46 x44) x45 = x41 x46 (x41 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x4 x46 ⟶ x4 x44 ⟶ x4 x45 ⟶ (x37 (x37 x46 x44) x45 = x37 x46 (x37 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x4 x46 ⟶ x4 x44 ⟶ x4 x45 ⟶ (x41 (x37 x46 x44) x45 = x37 (x41 x46 x45) (x41 x44 x45) ⟶ False) ⟶ False) ⟶ ((x2 x33 x34 ⟶ False) ⟶ False) ⟶ ((x2 x33 x6 ⟶ False) ⟶ False) ⟶ ((x32 x33 x34 x6 ⟶ False) ⟶ False) ⟶ ((x7 x33 ⟶ False) ⟶ False) ⟶ (x43 x33 ⟶ False) ⟶ ((x2 x5 x34 ⟶ False) ⟶ False) ⟶ ((x2 x5 x6 ⟶ False) ⟶ False) ⟶ ((x32 x5 x34 x6 ⟶ False) ⟶ False) ⟶ ((x7 x5 ⟶ False) ⟶ False) ⟶ (x43 x5 ⟶ False) ⟶ ((x41 x33 x5 = x33 ⟶ False) ⟶ False) ⟶ ((x41 x5 x33 = x33 ⟶ False) ⟶ False) ⟶ ((x41 x5 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x39 x33 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x37 x5 x5 = x33 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x3 x44 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x43 x46 ⟶ False) ⟶ (x43 x44 ⟶ False) ⟶ x2 x44 (x1 x46) ⟶ x2 x45 x44 ⟶ (x32 x45 x46 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x43 x46 ⟶ False) ⟶ (x43 x44 ⟶ False) ⟶ x2 x44 (x1 x46) ⟶ x32 x45 x46 x44 ⟶ (x2 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x45 x34 ⟶ x42 x44 ⟶ (x31 x45 x44 = x41 x45 x44 ⟶ False) ⟶ False) ⟶ ((x6 = x35 ⟶ False) ⟶ False) ⟶ (∀ x44 . x2 x44 x34 ⟶ (x30 x44 = x40 x44 ⟶ False) ⟶ False) ⟶ ((x42 x8 ⟶ False) ⟶ False) ⟶ ((x29 x8 ⟶ False) ⟶ False) ⟶ ((x4 x8 ⟶ False) ⟶ False) ⟶ ((x43 x8 ⟶ False) ⟶ False) ⟶ ((x42 x9 ⟶ False) ⟶ False) ⟶ ((x28 x9 ⟶ False) ⟶ False) ⟶ ((x29 x9 ⟶ False) ⟶ False) ⟶ ((x4 x9 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x27 x11 ⟶ False) ⟶ False) ⟶ (x43 x11 ⟶ False) ⟶ ((x42 x26 ⟶ False) ⟶ False) ⟶ ((x7 x26 ⟶ False) ⟶ False) ⟶ ((x29 x26 ⟶ False) ⟶ False) ⟶ ((x4 x26 ⟶ False) ⟶ False) ⟶ ((x27 x25 ⟶ False) ⟶ False) ⟶ (x43 x25 ⟶ False) ⟶ ((x42 x24 ⟶ False) ⟶ False) ⟶ ((x27 x12 ⟶ False) ⟶ False) ⟶ (x43 x12 ⟶ False) ⟶ (∀ x44 x45 . (x28 x45 ⟶ False) ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ x28 (x37 x45 x44) ⟶ False) ⟶ (∀ x44 x45 . x42 x45 ⟶ x42 x44 ⟶ (x42 (x39 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x42 x45 ⟶ x42 x44 ⟶ (x42 (x41 x45 x44) ⟶ False) ⟶ False) ⟶ ((x27 x35 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x42 x45 ⟶ x42 x44 ⟶ (x42 (x37 x45 x44) ⟶ False) ⟶ False) ⟶ ((x10 x35 ⟶ False) ⟶ False) ⟶ ((x10 x34 ⟶ False) ⟶ False) ⟶ (∀ x44 . x42 x44 ⟶ (x42 (x38 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x42 x44 ⟶ (x42 (x40 x44) ⟶ False) ⟶ False) ⟶ ((x23 x34 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . (x28 x45 ⟶ False) ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ x28 (x41 x45 x44) ⟶ False) ⟶ (∀ x44 x45 . (x7 x45 ⟶ False) ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ x28 (x41 x45 x44) ⟶ False) ⟶ (∀ x44 x45 . (x7 x45 ⟶ False) ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ x7 (x41 x44 x45) ⟶ False) ⟶ (∀ x44 x45 . (x7 x45 ⟶ False) ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ x7 (x41 x45 x44) ⟶ False) ⟶ (∀ x44 x45 . x28 x45 ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ (x7 (x39 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x28 x45 ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ (x28 (x39 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x7 x45 ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ (x28 (x39 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x7 x45 ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ (x7 (x39 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . (x28 x45 ⟶ False) ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ x7 (x39 x44 x45) ⟶ False) ⟶ (∀ x44 x45 . (x28 x45 ⟶ False) ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ x28 (x39 x45 x44) ⟶ False) ⟶ (∀ x44 x45 . x28 x45 ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ (x28 (x37 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x28 x45 ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ (x28 (x37 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x7 x45 ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ (x7 (x37 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x7 x45 ⟶ x42 x45 ⟶ (x28 x44 ⟶ False) ⟶ x42 x44 ⟶ (x7 (x37 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . (x7 x45 ⟶ False) ⟶ x42 x45 ⟶ (x7 x44 ⟶ False) ⟶ x42 x44 ⟶ x7 (x37 x45 x44) ⟶ False) ⟶ (∀ x44 x45 . (x43 x45 ⟶ False) ⟶ (x43 x44 ⟶ False) ⟶ x2 x44 (x1 x45) ⟶ (x32 (x22 x44 x45) x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x2 (x13 x44) x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x43 x46 ⟶ False) ⟶ (x43 x44 ⟶ False) ⟶ x2 x44 (x1 x46) ⟶ x32 x45 x46 x44 ⟶ (x2 x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x45 x34 ⟶ x42 x44 ⟶ (x2 (x31 x45 x44) x34 ⟶ False) ⟶ False) ⟶ ((x2 x6 (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x44 . x2 x44 x34 ⟶ (x2 (x30 x44) x34 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x45 x34 ⟶ x42 x44 ⟶ (x31 x45 x44 = x31 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x4 x45 ⟶ x4 x44 ⟶ (x41 x45 x44 = x41 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x4 x45 ⟶ x4 x44 ⟶ (x37 x45 x44 = x37 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 . x2 x44 (x1 x34) ⟶ (x23 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x23 x44 ⟶ (x21 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x42 x44 ⟶ (x29 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x23 x44 ⟶ (x20 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x42 x44 ⟶ (x4 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x19 x44 ⟶ (x23 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x14 x44 ⟶ (x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x18 x44 ⟶ (x19 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x10 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x2 x44 x6 ⟶ (x27 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x27 x45 ⟶ x2 x44 (x1 x45) ⟶ (x27 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x18 x45 ⟶ x2 x44 (x1 x45) ⟶ (x18 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x19 x45 ⟶ x2 x44 (x1 x45) ⟶ (x19 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x23 x45 ⟶ x2 x44 (x1 x45) ⟶ (x23 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x20 x45 ⟶ x2 x44 (x1 x45) ⟶ (x20 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x2 x44 x34 ⟶ (x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x27 x44 ⟶ (x18 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x21 x45 ⟶ x2 x44 (x1 x45) ⟶ (x21 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x27 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x27 x45 ⟶ x2 x44 x45 ⟶ (x14 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x18 x45 ⟶ x2 x44 x45 ⟶ (x15 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x19 x45 ⟶ x2 x44 x45 ⟶ (x17 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x23 x45 ⟶ x2 x44 x45 ⟶ (x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x20 x45 ⟶ x2 x44 x45 ⟶ (x29 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x21 x45 ⟶ x2 x44 x45 ⟶ (x4 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x2 x44 (x1 x6) ⟶ (x27 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x0 x44 x45 ⟶ x0 x45 x44 ⟶ False) ⟶ (x30 (x31 x33 x16) = x31 (x31 x33 (x40 x16)) (x38 x16) ⟶ False) ⟶ ((x42 x16 ⟶ False) ⟶ False) ⟶ False (proof)