Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../5bc11..
PUWR5../2b3d3..
vout
PrNUD../90392.. 0.02 bars
TMPLt../322f3.. ownership of ea166.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMHHx../891da.. ownership of 9aabf.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PURV1../892f8.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem ea166.. : ∀ 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 . x42 x44 ⟶ (x44 = x43 ⟶ False) ⟶ x42 x43 ⟶ False) ⟶ (∀ x43 x44 . x0 x43 x44 ⟶ x42 x44 ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x43 = x41 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x0 x43 x44 ⟶ x2 x44 (x1 x45) ⟶ x42 x45 ⟶ False) ⟶ (∀ x43 x44 x45 . x0 x44 x45 ⟶ x2 x45 (x1 x43) ⟶ (x2 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x3 x44 x43 ⟶ (x2 x44 (x1 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x2 x44 (x1 x43) ⟶ (x3 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x2 x43 x44 ⟶ (x42 x44 ⟶ False) ⟶ (x0 x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 x43 ⟶ (x2 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x2 x43 (x1 (x13 x46)) ⟶ x4 x45 ⟶ x11 x45 x46 x12 ⟶ x2 x45 (x1 (x5 x46 x12)) ⟶ x10 x44 x46 ⟶ (x9 x46 x12 (x7 x46 (x8 x46 x45 x43 x44)) (x6 x46 (x7 x46 x45) x43 x44) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . x4 x46 ⟶ x11 x46 x43 x44 ⟶ x2 x46 (x1 (x5 x43 x44)) ⟶ x4 x45 ⟶ x11 x45 x43 x44 ⟶ x2 x45 (x1 (x5 x43 x44)) ⟶ x9 x43 x44 x46 x45 ⟶ (x9 x43 x44 x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . x4 x46 ⟶ x11 x46 x43 x44 ⟶ x2 x46 (x1 (x5 x43 x44)) ⟶ x4 x45 ⟶ x11 x45 x43 x44 ⟶ x2 x45 (x1 (x5 x43 x44)) ⟶ (x9 x43 x44 x46 x46 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x3 x43 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . x4 x46 ⟶ x11 x46 x43 x44 ⟶ x2 x46 (x1 (x5 x43 x44)) ⟶ x4 x45 ⟶ x11 x45 x43 x44 ⟶ x2 x45 (x1 (x5 x43 x44)) ⟶ x46 = x45 ⟶ (x9 x43 x44 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . x4 x46 ⟶ x11 x46 x43 x44 ⟶ x2 x46 (x1 (x5 x43 x44)) ⟶ x4 x45 ⟶ x11 x45 x43 x44 ⟶ x2 x45 (x1 (x5 x43 x44)) ⟶ x9 x43 x44 x46 x45 ⟶ (x46 = x45 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x14 x43 = x1 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x40 x43 = x13 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x44 x12 ⟶ x2 x43 (x1 (x5 x44 x12)) ⟶ (x7 x44 x43 = x15 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x38 (x39 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x42 (x39 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x10 (x39 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x16 (x17 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 (x17 x43) ⟶ False) ⟶ (∀ x43 . (x2 (x17 x43) (x1 (x1 (x14 x43))) ⟶ False) ⟶ False) ⟶ (x42 x37 ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x4 x19 ⟶ False) ⟶ False) ⟶ ((x20 x19 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x38 (x36 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x42 (x36 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x10 (x36 x43) x43 ⟶ False) ⟶ False) ⟶ ((x42 x21 ⟶ False) ⟶ False) ⟶ ((x35 x34 ⟶ False) ⟶ False) ⟶ ((x4 x34 ⟶ False) ⟶ False) ⟶ ((x20 x34 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x16 (x22 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x2 (x22 x43) (x1 (x1 (x14 x43))) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x44 x12 ⟶ x2 x43 (x1 (x5 x44 x12)) ⟶ (x7 x44 (x7 x44 x43) = x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x18 x43 ⟶ (x15 (x15 x43) = x43 ⟶ False) ⟶ False) ⟶ (x42 x12 ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x2 (x23 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x10 (x33 x43) x43 ⟶ False) ⟶ False) ⟶ ((x42 x24 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x10 x44 x43 ⟶ (x2 x44 (x1 (x1 x43)) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x2 (x14 x43) (x1 (x1 x43)) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x46 x12 ⟶ x2 x43 (x1 (x5 x46 x12)) ⟶ x2 x45 (x1 (x40 x46)) ⟶ x10 x44 x46 ⟶ (x2 (x6 x46 x43 x45 x44) (x1 (x5 x46 x12)) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x46 x12 ⟶ x2 x43 (x1 (x5 x46 x12)) ⟶ x2 x45 (x1 (x40 x46)) ⟶ x10 x44 x46 ⟶ (x11 (x6 x46 x43 x45 x44) x46 x12 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x46 x12 ⟶ x2 x43 (x1 (x5 x46 x12)) ⟶ x2 x45 (x1 (x40 x46)) ⟶ x10 x44 x46 ⟶ (x4 (x6 x46 x43 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x46 x12 ⟶ x2 x43 (x1 (x5 x46 x12)) ⟶ x2 x45 (x1 (x40 x46)) ⟶ x10 x44 x46 ⟶ (x2 (x8 x46 x43 x45 x44) (x1 (x5 x46 x12)) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x46 x12 ⟶ x2 x43 (x1 (x5 x46 x12)) ⟶ x2 x45 (x1 (x40 x46)) ⟶ x10 x44 x46 ⟶ (x11 (x8 x46 x43 x45 x44) x46 x12 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . (x42 x46 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x46 x12 ⟶ x2 x43 (x1 (x5 x46 x12)) ⟶ x2 x45 (x1 (x40 x46)) ⟶ x10 x44 x46 ⟶ (x4 (x8 x46 x43 x45 x44) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x2 (x40 x43) (x1 (x1 (x14 x43))) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x16 (x40 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x44 x12 ⟶ x2 x43 (x1 (x5 x44 x12)) ⟶ (x2 (x7 x44 x43) (x1 (x5 x44 x12)) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x44 x12 ⟶ x2 x43 (x1 (x5 x44 x12)) ⟶ (x11 (x7 x44 x43) x44 x12 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x4 x43 ⟶ x11 x43 x44 x12 ⟶ x2 x43 (x1 (x5 x44 x12)) ⟶ (x4 (x7 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x18 x43 ⟶ (x18 (x15 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x18 x43 ⟶ (x4 (x15 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x18 x43 ⟶ (x20 (x15 x43) ⟶ False) ⟶ False) ⟶ ((x41 = x24 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x2 x44 (x1 (x5 x43 x12)) ⟶ x4 x44 ⟶ x11 x44 x43 x12 ⟶ (x18 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x2 x44 (x1 (x5 x43 x12)) ⟶ x4 x44 ⟶ x11 x44 x43 x12 ⟶ (x11 x44 x43 x12 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x2 x44 (x1 (x5 x43 x12)) ⟶ x4 x44 ⟶ x11 x44 x43 x12 ⟶ (x4 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x42 x43 ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x42 x43 ⟶ (x4 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x42 x43 ⟶ (x20 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x2 x43 x12 ⟶ (x25 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x35 x43 ⟶ (x32 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x20 x43 ⟶ x4 x43 ⟶ x35 x43 ⟶ (x20 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x10 x44 x43 ⟶ (x38 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x31 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x10 x43 x44 ⟶ x42 x43 ⟶ False) ⟶ (∀ x43 x44 . x0 x43 x44 ⟶ x0 x44 x43 ⟶ False) ⟶ (x9 x26 x12 (x7 x26 (x8 x26 (x8 x26 x28 x29 x27) x29 x30)) (x6 x26 (x6 x26 (x7 x26 x28) x29 x27) x29 x30) ⟶ False) ⟶ ((x10 x30 x26 ⟶ False) ⟶ False) ⟶ ((x10 x27 x26 ⟶ False) ⟶ False) ⟶ ((x2 x29 (x1 (x40 x26)) ⟶ False) ⟶ False) ⟶ ((x2 x28 (x1 (x5 x26 x12)) ⟶ False) ⟶ False) ⟶ ((x11 x28 x26 x12 ⟶ False) ⟶ False) ⟶ ((x4 x28 ⟶ False) ⟶ False) ⟶ (x42 x26 ⟶ False) ⟶ False (proof)