Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../3e5f9..
PUM6e../4c645..
vout
PrPhD../3e060.. 102.61 bars
TMdUX../2ac34.. ownership of 1a212.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMSUb../8afc4.. ownership of 10bcb.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUQ9Q../d96ba.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 1a212.. : ∀ 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 : ι → ι . ((x45 (x45 x44) = x44 ⟶ False) ⟶ False) ⟶ ((x45 x44 = x45 x44 ⟶ False) ⟶ False) ⟶ ((x42 x44 x43 ⟶ False) ⟶ False) ⟶ ((x42 x44 x0 ⟶ False) ⟶ False) ⟶ ((x41 x44 x43 x0 ⟶ False) ⟶ False) ⟶ ((x1 x44 ⟶ False) ⟶ False) ⟶ (x40 x44 ⟶ False) ⟶ (∀ x46 x47 . x2 x47 ⟶ x2 x46 ⟶ (x3 (x45 x47) (x45 x46) = x3 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x47 ⟶ x2 x46 ⟶ (x39 (x45 x47) (x45 x46) = x45 (x39 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x2 x48 ⟶ x2 x46 ⟶ x2 x47 ⟶ (x39 (x39 x48 x46) x47 = x39 x48 (x39 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x47 ⟶ x2 x46 ⟶ (x39 x47 (x45 x46) = x3 x47 x46 ⟶ False) ⟶ False) ⟶ ((x2 x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x47 ⟶ x2 x46 ⟶ (x2 (x3 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x47 ⟶ x2 x46 ⟶ (x2 (x39 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x2 x46 ⟶ (x2 (x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x2 x46 ⟶ (x45 (x45 x46) = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x47 ⟶ x2 x46 ⟶ (x39 x47 x46 = x39 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x40 x47 ⟶ (x47 = x46 ⟶ False) ⟶ x40 x46 ⟶ False) ⟶ (∀ x46 x47 . x38 x46 x47 ⟶ x40 x47 ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x46 = x5 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x46 x47 ⟶ (x40 x47 ⟶ False) ⟶ (x38 x46 x47 ⟶ False) ⟶ False) ⟶ ((x2 x6 ⟶ False) ⟶ False) ⟶ (x40 x6 ⟶ False) ⟶ (x40 x7 ⟶ False) ⟶ ((x40 x37 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x40 x46 ⟶ False) ⟶ x2 x46 ⟶ (x2 (x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x40 x46 ⟶ False) ⟶ x2 x46 ⟶ x40 (x45 x46) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x8 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x35 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x43 ⟶ (x10 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x43 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x40 x48 ⟶ False) ⟶ (x40 x46 ⟶ False) ⟶ x42 x46 (x11 x48) ⟶ x41 x47 x48 x46 ⟶ (x42 x47 x48 ⟶ False) ⟶ False) ⟶ ((x42 x0 (x11 x43) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x40 x48 ⟶ False) ⟶ (x40 x46 ⟶ False) ⟶ x42 x46 (x11 x48) ⟶ x42 x47 x46 ⟶ (x41 x47 x48 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x40 x48 ⟶ False) ⟶ (x40 x46 ⟶ False) ⟶ x42 x46 (x11 x48) ⟶ x41 x47 x48 x46 ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ ((x0 = x12 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x40 x47 ⟶ False) ⟶ (x40 x46 ⟶ False) ⟶ x42 x46 (x11 x47) ⟶ (x41 (x34 x46 x47) x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x42 (x13 x46) x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x46 x47 ⟶ x42 x47 (x11 x48) ⟶ x40 x48 ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x47 x48 ⟶ x42 x48 (x11 x46) ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x33 x47 x46 ⟶ (x42 x47 (x11 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 (x11 x46) ⟶ (x33 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 x46 ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ ((x42 x5 x12 ⟶ False) ⟶ False) ⟶ ((x36 x32 ⟶ False) ⟶ False) ⟶ (x40 x32 ⟶ False) ⟶ ((x36 x31 ⟶ False) ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ ((x35 x30 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x10 x47 ⟶ x10 x46 ⟶ (x10 (x3 x47 x46) ⟶ False) ⟶ False) ⟶ ((x35 x12 ⟶ False) ⟶ False) ⟶ (x40 x12 ⟶ False) ⟶ (∀ x46 x47 . x10 x47 ⟶ x10 x46 ⟶ (x10 (x39 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x10 x46 ⟶ (x10 (x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x10 x46 ⟶ (x2 (x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ (x15 (x3 x46 x47) ⟶ False) ⟶ False) ⟶ ((x40 x5 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ (x1 (x3 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ x15 (x45 x46) ⟶ False) ⟶ (∀ x46 . (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ (x2 (x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x1 x47 ⟶ False) ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ x1 (x39 x47 x46) ⟶ False) ⟶ (∀ x46 . x42 x46 x12 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ (x35 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x35 x47 ⟶ x42 x46 x47 ⟶ (x35 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x10 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x10 x46 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ (x10 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x35 x46 ⟶ (x16 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x35 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x8 x47 ⟶ x42 x46 (x11 x47) ⟶ (x8 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x46 x47 ⟶ x38 x47 x46 ⟶ False) ⟶ ((x29 x17 ⟶ False) ⟶ False) ⟶ ((x40 x17 ⟶ False) ⟶ False) ⟶ ((x10 x18 ⟶ False) ⟶ False) ⟶ ((x29 x18 ⟶ False) ⟶ False) ⟶ ((x2 x18 ⟶ False) ⟶ False) ⟶ ((x40 x18 ⟶ False) ⟶ False) ⟶ ((x15 x19 ⟶ False) ⟶ False) ⟶ ((x29 x19 ⟶ False) ⟶ False) ⟶ ((x10 x20 ⟶ False) ⟶ False) ⟶ ((x15 x20 ⟶ False) ⟶ False) ⟶ ((x29 x20 ⟶ False) ⟶ False) ⟶ ((x2 x20 ⟶ False) ⟶ False) ⟶ ((x1 x21 ⟶ False) ⟶ False) ⟶ ((x29 x21 ⟶ False) ⟶ False) ⟶ ((x10 x22 ⟶ False) ⟶ False) ⟶ ((x1 x22 ⟶ False) ⟶ False) ⟶ ((x29 x22 ⟶ False) ⟶ False) ⟶ ((x2 x22 ⟶ False) ⟶ False) ⟶ ((x35 x23 ⟶ False) ⟶ False) ⟶ ((x16 x23 ⟶ False) ⟶ False) ⟶ ((x28 x23 ⟶ False) ⟶ False) ⟶ (x40 x23 ⟶ False) ⟶ ((x29 x24 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x15 x47 ⟶ False) ⟶ x10 x47 ⟶ (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ x15 (x39 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . x15 x47 ⟶ x10 x47 ⟶ (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ (x1 (x3 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x15 x47 ⟶ x10 x47 ⟶ (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ (x15 (x3 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x15 x47 ⟶ False) ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ x1 (x3 x46 x47) ⟶ False) ⟶ (∀ x46 x47 . (x15 x47 ⟶ False) ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ x15 (x3 x47 x46) ⟶ False) ⟶ (∀ x46 . (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ x1 (x45 x46) ⟶ False) ⟶ (∀ x46 . (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ (x2 (x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x15 x47 ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ (x15 (x39 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x15 x47 ⟶ x10 x47 ⟶ (x1 x46 ⟶ False) ⟶ x10 x46 ⟶ (x15 (x39 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x10 x47 ⟶ (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ (x1 (x39 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x10 x47 ⟶ (x15 x46 ⟶ False) ⟶ x10 x46 ⟶ (x1 (x39 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ (x1 x46 ⟶ False) ⟶ (x15 x46 ⟶ False) ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ (x1 x46 ⟶ False) ⟶ (x15 x46 ⟶ False) ⟶ (x40 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x29 x46 ⟶ x15 x46 ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x29 x46 ⟶ x1 x46 ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x29 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x40 x46 ⟶ False) ⟶ x29 x46 ⟶ (x1 x46 ⟶ False) ⟶ (x15 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x40 x46 ⟶ False) ⟶ x29 x46 ⟶ (x1 x46 ⟶ False) ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x15 x46 ⟶ x1 x46 ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x15 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x15 x46 ⟶ x40 x46 ⟶ False) ⟶ (∀ x46 . (x40 x46 ⟶ False) ⟶ x29 x46 ⟶ (x15 x46 ⟶ False) ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x40 x46 ⟶ False) ⟶ x29 x46 ⟶ (x15 x46 ⟶ False) ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x1 x46 ⟶ x15 x46 ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x1 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x1 x46 ⟶ x40 x46 ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x16 x46 ⟶ (x35 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x33 x46 x46 ⟶ False) ⟶ False) ⟶ (x3 x25 (x3 (x45 x26) x27) = x39 (x39 x25 x26) x27 ⟶ False) ⟶ ((x2 x27 ⟶ False) ⟶ False) ⟶ ((x2 x26 ⟶ False) ⟶ False) ⟶ ((x2 x25 ⟶ False) ⟶ False) ⟶ False (proof)