Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../4604b..
PUN3P../451f6..
vout
PrPhD../caac8.. 102.66 bars
TMTex../567e2.. ownership of 2152d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMVMs../0461c.. ownership of e70f5.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUKuA../0858b.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2152d.. : ∀ 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 . x41 x43 ⟶ (x43 = x42 ⟶ False) ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 x43 . x0 x42 x43 ⟶ x41 x43 ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x42 = x40 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x1 x42 x43 ⟶ (x41 x43 ⟶ False) ⟶ (x0 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x39 x42 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x0 x43 x42 ⟶ (x1 x43 x42 ⟶ False) ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ (x41 x37 ⟶ False) ⟶ (x36 x35 ⟶ False) ⟶ ((x2 x35 ⟶ False) ⟶ False) ⟶ ((x34 x35 ⟶ False) ⟶ False) ⟶ ((x2 x3 ⟶ False) ⟶ False) ⟶ ((x33 x3 ⟶ False) ⟶ False) ⟶ ((x34 x3 ⟶ False) ⟶ False) ⟶ (x41 x3 ⟶ False) ⟶ ((x2 x4 ⟶ False) ⟶ False) ⟶ ((x33 x4 ⟶ False) ⟶ False) ⟶ ((x34 x4 ⟶ False) ⟶ False) ⟶ (x41 x32 ⟶ False) ⟶ ((x33 x5 ⟶ False) ⟶ False) ⟶ ((x34 x5 ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ ((x2 x7 ⟶ False) ⟶ False) ⟶ ((x34 x7 ⟶ False) ⟶ False) ⟶ ((x31 x30 ⟶ False) ⟶ False) ⟶ ((x41 x8 ⟶ False) ⟶ False) ⟶ ((x34 x29 ⟶ False) ⟶ False) ⟶ (x41 x29 ⟶ False) ⟶ ((x2 x28 ⟶ False) ⟶ False) ⟶ ((x34 x28 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x39 x42 x42 = x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x34 x42 ⟶ x41 (x9 x42) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x34 x42 ⟶ x41 (x27 x42) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . (x34 (x10 (x11 x43 x42) (x11 x45 x44)) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x34 (x26 x42 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x41 (x9 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x34 (x25 (x11 x43 x42)) ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x41 (x27 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x41 (x10 x42 x43) ⟶ False) ⟶ (∀ x42 . x41 (x25 x42) ⟶ False) ⟶ (∀ x42 . x24 x42 ⟶ x34 x42 ⟶ (x24 (x9 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x24 x42 ⟶ x34 x42 ⟶ (x24 (x27 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x31 (x11 x42 x43) ⟶ False) ⟶ False) ⟶ ((x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x34 x43 ⟶ (x34 (x39 x43 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x2 (x25 (x11 x43 x42)) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x34 x43 ⟶ x22 x43 ⟶ x2 x43 ⟶ (x41 (x23 x43 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . (x24 x42 ⟶ False) ⟶ x34 x42 ⟶ x2 x42 ⟶ x24 (x27 x42) ⟶ False) ⟶ (∀ x42 x43 . x34 x43 ⟶ x2 x43 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x38 (x10 x43 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x38 (x25 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x36 x42 ⟶ False) ⟶ x24 (x9 x42) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ x36 x42 ⟶ (x24 (x9 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x41 (x9 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x34 x43 ⟶ x33 x43 ⟶ x2 x43 ⟶ x1 x42 (x27 x43) ⟶ x41 (x23 x43 x42) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ (x41 x42 ⟶ False) ⟶ x41 (x26 x43 x42) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x41 (x27 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x33 x42 ⟶ x2 x42 ⟶ (x21 (x9 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . (x1 (x12 x42) x42 ⟶ False) ⟶ False) ⟶ ((x41 x20 ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x2 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x34 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x11 x43 x42 = x10 (x10 x43 x42) (x25 x43) ⟶ False) ⟶ False) ⟶ ((x40 = x20 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ x34 x43 ⟶ x2 x43 ⟶ x27 x43 = x27 (x27 x44) ⟶ x34 x42 ⟶ x2 x42 ⟶ x23 x43 (x16 x43 x44) = x42 ⟶ x27 x42 = x9 (x39 (x27 x44) (x26 (x25 (x16 x43 x44)) (x9 (x27 x44)))) ⟶ x23 x42 (x15 x42 x43 x44) = x14 x44 (x16 x43 x44) (x15 x42 x43 x44) ⟶ (x43 = x13 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ x34 x43 ⟶ x2 x43 ⟶ x27 x43 = x27 (x27 x44) ⟶ x34 x42 ⟶ x2 x42 ⟶ x23 x43 (x16 x43 x44) = x42 ⟶ x27 x42 = x9 (x39 (x27 x44) (x26 (x25 (x16 x43 x44)) (x9 (x27 x44)))) ⟶ (x0 (x15 x42 x43 x44) (x27 x42) ⟶ False) ⟶ (x43 = x13 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x34 x43 ⟶ x2 x43 ⟶ x34 x42 ⟶ x2 x42 ⟶ x27 x42 = x27 (x27 x43) ⟶ (x0 (x16 x42 x43) (x27 (x27 x43)) ⟶ False) ⟶ (x42 = x13 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . x34 x45 ⟶ x2 x45 ⟶ x34 x44 ⟶ x2 x44 ⟶ x44 = x13 x45 ⟶ x0 x42 (x27 (x27 x45)) ⟶ x0 x43 (x27 (x19 x42 x44 x45)) ⟶ (x23 (x19 x42 x44 x45) x43 = x14 x45 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ x34 x43 ⟶ x2 x43 ⟶ x43 = x13 x44 ⟶ x0 x42 (x27 (x27 x44)) ⟶ (x27 (x19 x42 x43 x44) = x9 (x39 (x27 x44) (x26 (x25 x42) (x9 (x27 x44)))) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ x34 x43 ⟶ x2 x43 ⟶ x43 = x13 x44 ⟶ x0 x42 (x27 (x27 x44)) ⟶ (x23 x43 x42 = x19 x42 x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ x34 x43 ⟶ x2 x43 ⟶ x43 = x13 x44 ⟶ x0 x42 (x27 (x27 x44)) ⟶ (x2 (x19 x42 x43 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ x34 x43 ⟶ x2 x43 ⟶ x43 = x13 x44 ⟶ x0 x42 (x27 (x27 x44)) ⟶ (x34 (x19 x42 x43 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x34 x43 ⟶ x2 x43 ⟶ x34 x42 ⟶ x2 x42 ⟶ x42 = x13 x43 ⟶ (x27 x42 = x27 (x27 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x34 x44 ⟶ x2 x44 ⟶ (x14 x44 x42 x43 = x23 x44 (x11 x42 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x39 x43 x42 = x39 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x10 x43 x42 = x10 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x38 x43 ⟶ x1 x42 x43 ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x38 x43 ⟶ x1 x42 x43 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x38 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x24 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x36 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x24 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x24 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x36 x42 ⟶ False) ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x36 x42 ⟶ False) ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x34 x42 ⟶ x2 x42 ⟶ (x36 x42 ⟶ False) ⟶ x24 x42 ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ (x33 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x36 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ (x22 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ x34 x42 ⟶ x2 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x41 x42 ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x0 x42 x43 ⟶ x0 x43 x42 ⟶ False) ⟶ (x34 (x23 (x13 x18) x17) ⟶ x2 (x23 (x13 x18) x17) ⟶ False) ⟶ ((x0 x17 (x27 (x13 x18)) ⟶ False) ⟶ False) ⟶ ((x2 x18 ⟶ False) ⟶ False) ⟶ ((x34 x18 ⟶ False) ⟶ False) ⟶ False (proof)