Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../3e060..
PUMyn../6fc77..
vout
PrPhD../09bb3.. 102.61 bars
TMazf../ce9e7.. ownership of 76675.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMXMj../46dd9.. ownership of fe3c0.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUZHX../e53d1.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 76675.. : ∀ 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 . x38 x39 x40 ⟶ x36 x40 (x37 x41) ⟶ x35 x41 ⟶ False) ⟶ (∀ x39 x40 x41 . x38 x40 x41 ⟶ x36 x41 (x37 x39) ⟶ (x36 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x34 x40 x39 ⟶ (x36 x40 (x37 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x36 x40 (x37 x39) ⟶ (x34 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x36 x39 x40 ⟶ (x35 x40 ⟶ False) ⟶ (x38 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x34 x39 x40 ⟶ (x0 x39 x40 = x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x0 x41 (x33 x39 x40) = x33 (x0 x41 x39) (x0 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x38 x40 x39 ⟶ (x36 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x34 (x0 x39 x40) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x34 x39 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ (x32 x41 x39 x40 = x0 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ x36 x39 (x37 x41) ⟶ (x1 x41 x40 x39 = x33 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x30 (x29 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x36 (x29 x39) (x37 (x2 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x27 (x26 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x36 (x26 x39) (x37 (x2 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . x28 x39 ⟶ (x24 (x25 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x28 x39 ⟶ (x36 (x25 x39) (x37 (x2 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x35 x39 ⟶ False) ⟶ (x22 (x23 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x35 x39 ⟶ False) ⟶ (x36 (x23 x39) (x37 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . x22 (x21 x39) x39 ⟶ False) ⟶ (∀ x39 . (x36 (x21 x39) (x37 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x27 (x20 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x3 (x20 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x36 (x20 x39) (x37 (x2 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x35 (x4 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x36 (x4 x39) (x37 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x3 (x5 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x36 (x5 x39) (x37 (x2 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x35 x39 ⟶ False) ⟶ x35 (x6 x39) ⟶ False) ⟶ (∀ x39 . (x35 x39 ⟶ False) ⟶ (x36 (x6 x39) (x37 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x3 (x7 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x31 x39 ⟶ x28 x39 ⟶ (x36 (x7 x39) (x37 (x2 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x8 x40 (x8 x40 x39) = x8 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x19 x40 (x19 x40 x39) = x19 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x39 (x37 x41) ⟶ (x32 x41 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ x36 x39 (x37 x41) ⟶ (x1 x41 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x0 x39 x39 = x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x33 x39 x39 = x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x3 (x19 x40 x39) x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x31 x41 ⟶ x28 x41 ⟶ x3 x40 x41 ⟶ x36 x40 (x37 (x2 x41)) ⟶ x3 x39 x41 ⟶ x36 x39 (x37 (x2 x41)) ⟶ (x3 (x33 x40 x39) x41 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x31 x41 ⟶ x28 x41 ⟶ x3 x40 x41 ⟶ x36 x40 (x37 (x2 x41)) ⟶ x3 x39 x41 ⟶ x36 x39 (x37 (x2 x41)) ⟶ (x3 (x0 x40 x39) x41 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x31 x41 ⟶ x28 x41 ⟶ x27 x40 x41 ⟶ x36 x40 (x37 (x2 x41)) ⟶ x27 x39 x41 ⟶ x36 x39 (x37 (x2 x41)) ⟶ (x27 (x33 x40 x39) x41 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x31 x41 ⟶ x28 x41 ⟶ x27 x40 x41 ⟶ x36 x40 (x37 (x2 x41)) ⟶ x27 x39 x41 ⟶ x36 x39 (x37 (x2 x41)) ⟶ (x27 (x0 x40 x39) x41 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x27 (x8 x40 x39) x40 ⟶ False) ⟶ False) ⟶ (∀ x39 . x35 (x37 x39) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x24 x39 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x35 (x19 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 . (x36 (x9 x39) x39 ⟶ False) ⟶ False) ⟶ ((x18 x17 ⟶ False) ⟶ False) ⟶ ((x28 x10 ⟶ False) ⟶ False) ⟶ (∀ x39 . x28 x39 ⟶ (x18 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ (x36 (x32 x41 x39 x40) (x37 x41) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x36 (x16 x40 x39) (x37 (x2 x40)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ x36 x39 (x37 x41) ⟶ (x36 (x1 x41 x40 x39) (x37 x41) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x36 (x8 x40 x39) (x37 (x2 x40)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x36 (x11 x40 x39) (x37 (x2 x40)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x36 (x19 x40 x39) (x37 (x2 x40)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x36 (x12 x40 x39) (x37 (x2 x40)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x11 x40 x39 = x32 (x2 x40) x39 (x19 x40 (x8 x40 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x12 x40 x39 = x32 (x2 x40) x39 (x8 x40 (x19 x40 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x34 x39 (x1 (x2 x40) (x8 x40 (x19 x40 x39)) (x19 x40 (x8 x40 x39))) ⟶ (x15 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x15 x39 x40 ⟶ (x34 x39 (x1 (x2 x40) (x8 x40 (x19 x40 x39)) (x19 x40 (x8 x40 x39))) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ (x16 x40 x39 = x1 (x2 x40) (x12 x40 x39) (x11 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ (x32 x41 x39 x40 = x32 x41 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x36 x40 (x37 x41) ⟶ x36 x39 (x37 x41) ⟶ (x1 x41 x40 x39 = x1 x41 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x0 x40 x39 = x0 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x33 x40 x39 = x33 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x3 x39 x40 ⟶ x30 x39 x40 ⟶ (x35 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x27 x39 x40 ⟶ x24 x39 x40 ⟶ (x30 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x30 x39 x40 ⟶ (x24 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x35 x40 ⟶ x36 x39 (x37 x40) ⟶ x22 x39 x40 ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x35 x39 ⟶ (x30 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x35 x40 ⟶ False) ⟶ x36 x39 (x37 x40) ⟶ x35 x39 ⟶ (x22 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x35 x39 ⟶ (x24 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x35 x40 ⟶ False) ⟶ x36 x39 (x37 x40) ⟶ (x22 x39 x40 ⟶ False) ⟶ x35 x39 ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x35 x39 ⟶ (x27 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x31 x40 ⟶ x28 x40 ⟶ x36 x39 (x37 (x2 x40)) ⟶ x35 x39 ⟶ (x3 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x35 x40 ⟶ x36 x39 (x37 x40) ⟶ (x35 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x38 x39 x40 ⟶ x38 x40 x39 ⟶ False) ⟶ ((x14 = x16 x13 x14 ⟶ False) ⟶ (x15 x14 x13 ⟶ False) ⟶ False) ⟶ (x15 x14 x13 ⟶ x14 = x16 x13 x14 ⟶ False) ⟶ ((x36 x14 (x37 (x2 x13)) ⟶ False) ⟶ False) ⟶ ((x28 x13 ⟶ False) ⟶ False) ⟶ ((x31 x13 ⟶ False) ⟶ False) ⟶ False (proof)