Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../d37da..
PUNKW../811c6..
vout
PrNUD../2eba7.. 0.00 bars
TMHa7../0b3cd.. ownership of 5ccec.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMYCu../a8573.. ownership of 6636e.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUcKo../da8ad.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 5ccec.. : ∀ 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 . x40 x43 ⟶ x33 x43 ⟶ x39 x42 (x38 (x37 x43)) ⟶ x39 x41 (x38 (x37 x43)) ⟶ (x36 (x37 x43) (x34 x43 (x35 x43 (x36 (x37 x43) x42 (x36 (x37 x43) (x34 x43 (x35 x43 x41)) x41)))) (x36 (x37 x43) x42 (x36 (x37 x43) (x34 x43 (x35 x43 x41)) x41)) = x36 (x37 x43) (x34 x43 (x35 x43 (x36 (x37 x43) x42 x41))) (x36 (x37 x43) x42 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x0 x42 x41 ⟶ (x39 x42 (x38 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x39 x42 (x38 x41) ⟶ (x0 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x1 (x34 x42 x41) x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x32 (x35 x42 x41) x42 ⟶ False) ⟶ False) ⟶ (∀ x41 . x2 (x38 x41) ⟶ False) ⟶ (∀ x41 . x33 x41 ⟶ (x31 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x39 x42 (x38 x43) ⟶ x39 x41 (x38 x43) ⟶ (x39 (x36 x43 x42 x41) (x38 x43) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x39 (x35 x42 x41) (x38 (x37 x42)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x39 (x34 x42 x41) (x38 (x37 x42)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x39 x42 (x38 x43) ⟶ x39 x41 (x38 x43) ⟶ (x36 x43 x42 x41 = x30 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x39 (x3 x41) x41 ⟶ False) ⟶ False) ⟶ ((x33 x29 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x39 x42 (x38 x43) ⟶ x39 x41 (x38 x43) ⟶ (x36 x43 x42 x42 = x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x39 x42 (x38 x43) ⟶ x39 x41 (x38 x43) ⟶ (x36 x43 x42 x41 = x36 x43 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x35 x42 (x35 x42 x41) = x35 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x34 x42 (x34 x42 x41) = x34 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x42 ⟶ (x42 = x41 ⟶ False) ⟶ x2 x41 ⟶ False) ⟶ (∀ x41 x42 . x28 x41 x42 ⟶ x2 x42 ⟶ False) ⟶ (∀ x41 . x2 x41 ⟶ (x41 = x4 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x39 x41 x42 ⟶ (x2 x42 ⟶ False) ⟶ (x28 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x32 (x5 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x39 (x5 x41) (x38 (x37 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x32 (x6 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x1 (x6 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x39 (x6 x41) (x38 (x37 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 (x27 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x39 (x27 x41) (x38 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x1 (x26 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x39 (x26 x41) (x38 (x37 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 x41 ⟶ False) ⟶ x2 (x25 x41) ⟶ False) ⟶ (∀ x41 . (x2 x41 ⟶ False) ⟶ (x39 (x25 x41) (x38 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x1 (x24 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x39 (x24 x41) (x38 (x37 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x40 x43 ⟶ x33 x43 ⟶ x1 x42 x43 ⟶ x39 x42 (x38 (x37 x43)) ⟶ x1 x41 x43 ⟶ x39 x41 (x38 (x37 x43)) ⟶ (x1 (x30 x42 x41) x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x40 x43 ⟶ x33 x43 ⟶ x32 x42 x43 ⟶ x39 x42 (x38 (x37 x43)) ⟶ x32 x41 x43 ⟶ x39 x41 (x38 (x37 x43)) ⟶ (x32 (x30 x42 x41) x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x42 ⟶ x39 x41 (x38 x42) ⟶ x23 x41 x42 ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x2 x41 ⟶ (x7 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x2 x42 ⟶ False) ⟶ x39 x41 (x38 x42) ⟶ x2 x41 ⟶ (x23 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x2 x41 ⟶ (x8 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x2 x41 ⟶ (x32 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x2 x41 ⟶ (x1 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x42 ⟶ x39 x41 (x38 x42) ⟶ (x2 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x2 x41 ⟶ (x9 x41 ⟶ False) ⟶ False) ⟶ ((x31 x22 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x0 x41 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x30 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x30 x42 x41 = x30 x41 x42 ⟶ False) ⟶ False) ⟶ ((x4 = x21 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x28 x41 x42 ⟶ x39 x42 (x38 x43) ⟶ x2 x43 ⟶ False) ⟶ (∀ x41 x42 x43 . x28 x42 x43 ⟶ x39 x43 (x38 x41) ⟶ (x39 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x28 x42 x41 ⟶ (x39 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x30 x41 x4 = x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x7 (x10 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ x33 x41 ⟶ (x39 (x10 x41) (x38 (x37 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . x33 x41 ⟶ (x8 (x11 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x33 x41 ⟶ (x39 (x11 x41) (x38 (x37 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 x41 ⟶ False) ⟶ (x23 (x12 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 x41 ⟶ False) ⟶ (x39 (x12 x41) (x38 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . x23 (x13 x41) x41 ⟶ False) ⟶ (∀ x41 . (x39 (x13 x41) (x38 x41) ⟶ False) ⟶ False) ⟶ ((x9 x14 ⟶ False) ⟶ False) ⟶ (x2 x14 ⟶ False) ⟶ (∀ x41 x42 . x9 x42 ⟶ x9 x41 ⟶ (x9 (x30 x42 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 ⟶ x8 x41 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x2 (x34 x42 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x1 x41 x42 ⟶ x7 x41 x42 ⟶ (x2 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x32 x41 x42 ⟶ x8 x41 x42 ⟶ (x7 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ x7 x41 x42 ⟶ (x8 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 . x2 x41 ⟶ x9 x41 ⟶ (x20 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x2 x41 ⟶ x9 x41 ⟶ (x9 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x2 x41 ⟶ x9 x41 ⟶ (x19 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x2 x41 ⟶ x9 x41 ⟶ (x9 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x2 x42 ⟶ False) ⟶ x39 x41 (x38 x42) ⟶ (x23 x41 x42 ⟶ False) ⟶ x2 x41 ⟶ False) ⟶ (∀ x41 x42 . x9 x42 ⟶ x39 x41 (x38 x42) ⟶ (x9 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x28 x41 x42 ⟶ x28 x42 x41 ⟶ False) ⟶ ((x20 x15 ⟶ False) ⟶ False) ⟶ ((x9 x15 ⟶ False) ⟶ False) ⟶ ((x2 x21 ⟶ False) ⟶ False) ⟶ (x36 (x37 x16) (x34 x16 (x35 x16 (x36 (x37 x16) (x36 (x37 x16) (x34 x16 (x35 x16 x17)) x17) x18))) (x36 (x37 x16) (x36 (x37 x16) (x34 x16 (x35 x16 x17)) x17) x18) = x36 (x37 x16) (x34 x16 (x35 x16 (x36 (x37 x16) x17 x18))) (x36 (x37 x16) x17 x18) ⟶ False) ⟶ ((x39 x18 (x38 (x37 x16)) ⟶ False) ⟶ False) ⟶ ((x39 x17 (x38 (x37 x16)) ⟶ False) ⟶ False) ⟶ ((x33 x16 ⟶ False) ⟶ False) ⟶ ((x40 x16 ⟶ False) ⟶ False) ⟶ False (proof)