Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../67c54..
PUg4X../e06d1..
vout
PrPhD../21564.. 102.63 bars
TMU2K../7965f.. ownership of 211c6.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMdNM../df0f1.. ownership of 278ed.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUWyg../01a1c.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 211c6.. : ∀ 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 x44 x44 = x44 ⟶ False) ⟶ False) ⟶ ((x1 x44 x0 ⟶ False) ⟶ False) ⟶ ((x1 x44 x43 ⟶ False) ⟶ False) ⟶ ((x2 x44 x0 x43 ⟶ False) ⟶ False) ⟶ ((x42 x44 ⟶ False) ⟶ False) ⟶ (x3 x44 ⟶ False) ⟶ (∀ x46 . x41 x46 ⟶ (x45 x44 x46 = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x41 x48 ⟶ x41 x46 ⟶ x41 x47 ⟶ (x45 (x45 x48 x46) x47 = x45 x48 (x45 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x41 x48 ⟶ x41 x46 ⟶ x41 x47 ⟶ (x40 (x40 x48 x46) x47 = x40 x48 (x40 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x41 x48 ⟶ x41 x46 ⟶ x41 x47 ⟶ (x45 (x40 x48 x46) x47 = x40 (x45 x48 x47) (x45 x46 x47) ⟶ False) ⟶ False) ⟶ ((x41 x39 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x41 x47 ⟶ x41 x46 ⟶ (x41 (x45 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x41 x47 ⟶ x41 x46 ⟶ (x41 (x40 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x41 x47 ⟶ x41 x46 ⟶ (x45 x47 x46 = x45 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x41 x47 ⟶ x41 x46 ⟶ (x40 x47 x46 = x40 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x3 x47 ⟶ (x47 = x46 ⟶ False) ⟶ x3 x46 ⟶ False) ⟶ (∀ x46 x47 . x38 x46 x47 ⟶ x3 x47 ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ (x46 = x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x46 x47 ⟶ (x3 x47 ⟶ False) ⟶ (x38 x46 x47 ⟶ False) ⟶ False) ⟶ ((x41 x5 ⟶ False) ⟶ False) ⟶ (x3 x5 ⟶ False) ⟶ (x3 x6 ⟶ False) ⟶ ((x3 x37 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x3 x47 ⟶ False) ⟶ x41 x47 ⟶ (x3 x46 ⟶ False) ⟶ x41 x46 ⟶ x3 (x45 x47 x46) ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ (x7 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ (x35 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ (x8 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 x0 ⟶ (x34 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 x0 ⟶ (x41 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x3 x48 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ x1 x46 (x33 x48) ⟶ x2 x47 x48 x46 ⟶ (x1 x47 x48 ⟶ False) ⟶ False) ⟶ ((x1 x43 (x33 x0) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x3 x48 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ x1 x46 (x33 x48) ⟶ x1 x47 x46 ⟶ (x2 x47 x48 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x3 x48 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ x1 x46 (x33 x48) ⟶ x2 x47 x48 x46 ⟶ (x1 x47 x46 ⟶ False) ⟶ False) ⟶ ((x43 = x32 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x3 x47 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ x1 x46 (x33 x47) ⟶ (x2 (x9 x46 x47) x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x1 (x31 x46) x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x46 x47 ⟶ x1 x47 (x33 x48) ⟶ x3 x48 ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x47 x48 ⟶ x1 x48 (x33 x46) ⟶ (x1 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x10 x47 x46 ⟶ (x1 x47 (x33 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 (x33 x46) ⟶ (x10 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 x46 ⟶ (x1 x47 x46 ⟶ False) ⟶ False) ⟶ ((x1 x4 x32 ⟶ False) ⟶ False) ⟶ ((x7 x11 ⟶ False) ⟶ False) ⟶ (x3 x11 ⟶ False) ⟶ ((x7 x12 ⟶ False) ⟶ False) ⟶ ((x34 x30 ⟶ False) ⟶ False) ⟶ ((x8 x13 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x34 x47 ⟶ x34 x46 ⟶ (x34 (x45 x47 x46) ⟶ False) ⟶ False) ⟶ ((x8 x32 ⟶ False) ⟶ False) ⟶ (x3 x32 ⟶ False) ⟶ (∀ x46 x47 . x34 x47 ⟶ x34 x46 ⟶ (x34 (x40 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x42 x47 ⟶ False) ⟶ x34 x47 ⟶ (x42 x46 ⟶ False) ⟶ x34 x46 ⟶ x29 (x45 x47 x46) ⟶ False) ⟶ ((x3 x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x42 x47 ⟶ False) ⟶ x34 x47 ⟶ (x42 x46 ⟶ False) ⟶ x34 x46 ⟶ x42 (x40 x47 x46) ⟶ False) ⟶ (∀ x46 . x1 x46 x32 ⟶ (x7 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x8 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x8 x47 ⟶ x1 x46 x47 ⟶ (x8 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x34 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x34 x46 ⟶ (x41 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x34 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x41 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x8 x46 ⟶ (x14 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x8 x46 ⟶ (x27 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x36 x47 ⟶ x1 x46 (x33 x47) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x46 x47 ⟶ x38 x47 x46 ⟶ False) ⟶ ((x28 x15 ⟶ False) ⟶ False) ⟶ ((x3 x15 ⟶ False) ⟶ False) ⟶ ((x34 x16 ⟶ False) ⟶ False) ⟶ ((x28 x16 ⟶ False) ⟶ False) ⟶ ((x41 x16 ⟶ False) ⟶ False) ⟶ ((x3 x16 ⟶ False) ⟶ False) ⟶ ((x29 x17 ⟶ False) ⟶ False) ⟶ ((x28 x17 ⟶ False) ⟶ False) ⟶ ((x34 x18 ⟶ False) ⟶ False) ⟶ ((x29 x18 ⟶ False) ⟶ False) ⟶ ((x28 x18 ⟶ False) ⟶ False) ⟶ ((x41 x18 ⟶ False) ⟶ False) ⟶ ((x42 x19 ⟶ False) ⟶ False) ⟶ ((x28 x19 ⟶ False) ⟶ False) ⟶ ((x34 x20 ⟶ False) ⟶ False) ⟶ ((x42 x20 ⟶ False) ⟶ False) ⟶ ((x28 x20 ⟶ False) ⟶ False) ⟶ ((x41 x20 ⟶ False) ⟶ False) ⟶ ((x8 x21 ⟶ False) ⟶ False) ⟶ ((x14 x21 ⟶ False) ⟶ False) ⟶ ((x27 x21 ⟶ False) ⟶ False) ⟶ (x3 x21 ⟶ False) ⟶ ((x28 x22 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x29 x47 ⟶ False) ⟶ x34 x47 ⟶ (x29 x46 ⟶ False) ⟶ x34 x46 ⟶ x29 (x40 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x29 x47 ⟶ False) ⟶ x34 x47 ⟶ (x29 x46 ⟶ False) ⟶ x34 x46 ⟶ x29 (x45 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x42 x47 ⟶ False) ⟶ x34 x47 ⟶ (x29 x46 ⟶ False) ⟶ x34 x46 ⟶ x42 (x45 x46 x47) ⟶ False) ⟶ (∀ x46 x47 . (x42 x47 ⟶ False) ⟶ x34 x47 ⟶ (x29 x46 ⟶ False) ⟶ x34 x46 ⟶ x42 (x45 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . x29 x47 ⟶ x34 x47 ⟶ (x42 x46 ⟶ False) ⟶ x34 x46 ⟶ (x29 (x40 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x29 x47 ⟶ x34 x47 ⟶ (x42 x46 ⟶ False) ⟶ x34 x46 ⟶ (x29 (x40 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 ⟶ x34 x47 ⟶ (x29 x46 ⟶ False) ⟶ x34 x46 ⟶ (x42 (x40 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 ⟶ x34 x47 ⟶ (x29 x46 ⟶ False) ⟶ x34 x46 ⟶ (x42 (x40 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ (x42 x46 ⟶ False) ⟶ (x29 x46 ⟶ False) ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ (x42 x46 ⟶ False) ⟶ (x29 x46 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ x28 x46 ⟶ x29 x46 ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ x28 x46 ⟶ x42 x46 ⟶ False) ⟶ (∀ x46 . x3 x46 ⟶ x28 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x3 x46 ⟶ False) ⟶ x28 x46 ⟶ (x42 x46 ⟶ False) ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x3 x46 ⟶ False) ⟶ x28 x46 ⟶ (x42 x46 ⟶ False) ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x29 x46 ⟶ x42 x46 ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x29 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x29 x46 ⟶ x3 x46 ⟶ False) ⟶ (∀ x46 . (x3 x46 ⟶ False) ⟶ x28 x46 ⟶ (x29 x46 ⟶ False) ⟶ (x42 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x3 x46 ⟶ False) ⟶ x28 x46 ⟶ (x29 x46 ⟶ False) ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x42 x46 ⟶ x29 x46 ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x42 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x42 x46 ⟶ x3 x46 ⟶ False) ⟶ (∀ x46 . x27 x46 ⟶ x14 x46 ⟶ (x8 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x10 x46 x46 ⟶ False) ⟶ False) ⟶ (x45 (x40 x24 x25) (x40 x26 x23) = x40 (x40 (x40 (x45 x24 x26) (x45 x24 x23)) (x45 x25 x26)) (x45 x25 x23) ⟶ False) ⟶ ((x41 x23 ⟶ False) ⟶ False) ⟶ ((x41 x26 ⟶ False) ⟶ False) ⟶ ((x41 x25 ⟶ False) ⟶ False) ⟶ ((x41 x24 ⟶ False) ⟶ False) ⟶ False (proof)