Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../984fe..
PUPMf../86859..
vout
PrPhD../9ad7e.. 3.36 bars
TMWnV../c0908.. ownership of 41b71.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMS1W../f9f2a.. ownership of 8b824.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUbJo../7c1c6.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 41b71.. : ∀ 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 . x39 x41 ⟶ (x41 = x40 ⟶ False) ⟶ x39 x40 ⟶ False) ⟶ (∀ x40 x41 . x0 x40 x41 ⟶ x39 x41 ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ (x40 = x38 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x0 x40 x41 ⟶ x2 x41 (x1 x42) ⟶ x39 x42 ⟶ False) ⟶ (∀ x40 x41 x42 . x0 x41 x42 ⟶ x2 x42 (x1 x40) ⟶ (x2 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x3 x41 x40 ⟶ (x2 x41 (x1 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x2 x41 (x1 x40) ⟶ (x3 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x2 x40 x41 ⟶ (x39 x41 ⟶ False) ⟶ (x0 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x0 x41 x40 ⟶ (x2 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x3 x40 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x37 x40 = x1 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x2 x43 (x1 (x6 x42 x41)) ⟶ (x4 x42 x41 x43 x40 = x5 x43 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ (x35 (x36 x40) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ (x2 (x36 x40) (x1 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x35 (x34 x40) x40 ⟶ False) ⟶ (∀ x40 . (x2 (x34 x40) (x1 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x33 (x32 x40 x41) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x7 (x32 x41 x40) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x31 (x32 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ x39 (x8 x40 x41) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ (x30 (x8 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ (x33 (x8 x40 x41) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ (x7 (x8 x40 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ (x31 (x8 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ (x2 (x8 x40 x41) (x1 (x6 x41 x40)) ⟶ False) ⟶ False) ⟶ (x39 x9 ⟶ False) ⟶ (∀ x40 . (x39 (x29 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . (x2 (x29 x40) (x1 x40) ⟶ False) ⟶ False) ⟶ ((x28 x27 ⟶ False) ⟶ False) ⟶ ((x31 x27 ⟶ False) ⟶ False) ⟶ ((x39 x26 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ x39 (x10 x40) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ (x2 (x10 x40) (x1 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x33 (x11 x40 x41) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x7 (x11 x41 x40) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x31 (x11 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 (x11 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x2 (x11 x40 x41) (x1 (x6 x41 x40)) ⟶ False) ⟶ False) ⟶ ((x31 x25 ⟶ False) ⟶ False) ⟶ (x39 x25 ⟶ False) ⟶ (∀ x40 x41 . (x30 (x24 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x33 (x24 x40 x41) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x7 (x24 x41 x40) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x31 (x24 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x2 (x24 x40 x41) (x1 (x6 x41 x40)) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x2 x43 (x1 (x6 (x6 x41 x40) x42)) ⟶ (x31 (x12 x43) ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ x31 x40 ⟶ x39 (x12 x40) ⟶ False) ⟶ (∀ x40 x41 . (x31 (x6 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ (x39 (x12 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x41 ⟶ (x39 (x5 x41 x40) ⟶ False) ⟶ False) ⟶ ((x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 (x1 x40) ⟶ False) ⟶ (∀ x40 x41 . x31 x41 ⟶ x39 x40 ⟶ (x39 (x5 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x31 x41 ⟶ (x39 x40 ⟶ False) ⟶ x2 x40 (x1 (x12 x41)) ⟶ x39 (x5 x41 x40) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ x39 (x6 x41 x40) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ (x39 (x12 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . (x2 (x23 x40) x40 ⟶ False) ⟶ False) ⟶ ((x39 x13 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x2 (x37 x40) (x1 (x1 x40)) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x2 x43 (x1 (x6 x42 x41)) ⟶ (x2 (x4 x42 x41 x43 x40) (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x31 x41 ⟶ (x30 (x22 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x31 x41 ⟶ (x31 (x22 x40 x41) ⟶ False) ⟶ False) ⟶ ((x38 = x13 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x31 x42 ⟶ x31 x40 ⟶ x30 x40 ⟶ x12 x40 = x37 x41 ⟶ x14 x40 (x15 x40 x42 x41) = x5 x42 (x15 x40 x42 x41) ⟶ (x40 = x22 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x31 x42 ⟶ x31 x40 ⟶ x30 x40 ⟶ x12 x40 = x37 x41 ⟶ (x3 (x15 x40 x42 x41) x41 ⟶ False) ⟶ (x40 = x22 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x31 x43 ⟶ x31 x40 ⟶ x30 x40 ⟶ x40 = x22 x41 x43 ⟶ x3 x42 x41 ⟶ (x14 x40 x42 = x5 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x31 x42 ⟶ x31 x40 ⟶ x30 x40 ⟶ x40 = x22 x41 x42 ⟶ (x12 x40 = x37 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x40 ⟶ x33 x40 x41 ⟶ (x33 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x40 ⟶ x33 x40 x41 ⟶ (x31 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x40 ⟶ x33 x40 x41 ⟶ (x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x40 ⟶ x7 x40 x41 ⟶ (x7 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x40 ⟶ x7 x40 x41 ⟶ (x31 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x31 x40 ⟶ x7 x40 x41 ⟶ (x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x31 x42 ⟶ x33 x42 x40 ⟶ x2 x41 (x1 x42) ⟶ (x33 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x31 x42 ⟶ x7 x42 x40 ⟶ x2 x41 (x1 x42) ⟶ (x7 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x2 x40 (x1 x41) ⟶ x35 x40 x41 ⟶ False) ⟶ (∀ x40 x41 x42 . x39 x42 ⟶ x2 x40 (x1 (x6 x41 x42)) ⟶ (x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x31 x40 ⟶ (x28 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x31 x40 ⟶ (x31 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x2 x40 (x1 x41) ⟶ x39 x40 ⟶ (x35 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x39 x42 ⟶ x2 x40 (x1 (x6 x42 x41)) ⟶ (x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x31 x40 ⟶ (x16 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x31 x40 ⟶ (x31 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x2 x40 (x1 x41) ⟶ (x35 x40 x41 ⟶ False) ⟶ x39 x40 ⟶ False) ⟶ (∀ x40 x41 x42 . x2 x42 (x1 (x6 x40 x41)) ⟶ (x33 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x2 x42 (x1 (x6 x41 x40)) ⟶ (x7 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x31 x41 ⟶ x2 x40 (x1 x41) ⟶ (x31 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . (x39 x42 ⟶ False) ⟶ x39 x40 ⟶ x2 x41 (x1 (x6 x42 x40)) ⟶ x17 x41 x42 ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x2 x40 (x1 x41) ⟶ (x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x2 x42 (x1 (x6 x40 x41)) ⟶ (x31 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ (x31 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x39 x42 ⟶ x2 x40 (x1 (x6 x42 x41)) ⟶ (x17 x40 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x0 x40 x41 ⟶ x0 x41 x40 ⟶ False) ⟶ (x14 (x22 x21 x19) x20 = x4 x21 x18 x19 x20 ⟶ False) ⟶ ((x0 x20 (x12 (x22 x21 x19)) ⟶ False) ⟶ False) ⟶ ((x2 x19 (x1 (x6 x21 x18)) ⟶ False) ⟶ False) ⟶ False (proof)