Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../bf2f7..
PUUvi../464c7..
vout
PrPhD../0421e.. 3.36 bars
TMbqA../f16c5.. ownership of 7407a.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMY1t../f8e81.. ownership of 7fb88.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUWR3../d5028.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7407a.. : ∀ 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 . x39 x41 ⟶ (x41 = x40 ⟶ False) ⟶ x39 x40 ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x0 x42 x43 ⟶ x0 x41 x40 ⟶ (x0 (x2 x42 x41) (x1 x43 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x0 (x2 x41 x43) (x1 x40 x42) ⟶ (x0 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x0 (x2 x43 x41) (x1 x42 x40) ⟶ (x0 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x0 x40 x41 ⟶ x39 x41 ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ (x40 = x3 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x0 x40 x41 ⟶ x37 x41 (x38 x42) ⟶ x39 x42 ⟶ False) ⟶ (∀ x40 x41 x42 . x0 x41 x42 ⟶ x37 x42 (x38 x40) ⟶ (x37 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x36 x41 ⟶ x33 x41 ⟶ x0 x40 (x34 x41) ⟶ x0 x40 (x35 x41) ⟶ False) ⟶ (∀ x40 x41 . x4 x41 x40 ⟶ (x37 x41 (x38 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x37 x41 (x38 x40) ⟶ (x4 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x37 x40 x41 ⟶ (x39 x41 ⟶ False) ⟶ (x0 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x0 x41 x40 ⟶ (x37 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x5 x40 x3 = x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x32 x40 x41 ⟶ (x32 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x4 x40 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ (x30 (x31 x40) x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ (x37 (x31 x40) (x38 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x30 (x29 x40) x40 ⟶ False) ⟶ (∀ x40 . (x37 (x29 x40) (x38 x40) ⟶ False) ⟶ False) ⟶ (x39 x28 ⟶ False) ⟶ (∀ x40 . (x39 (x6 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . (x37 (x6 x40) (x38 x40) ⟶ False) ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ ((x27 x8 ⟶ False) ⟶ False) ⟶ ((x39 x9 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ x39 (x26 x40) ⟶ False) ⟶ (∀ x40 . (x39 x40 ⟶ False) ⟶ (x37 (x26 x40) (x38 x40) ⟶ False) ⟶ False) ⟶ ((x27 x25 ⟶ False) ⟶ False) ⟶ (x39 x25 ⟶ False) ⟶ (∀ x40 . (x5 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x27 (x1 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x39 (x5 x40 x41) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x39 (x5 x41 x40) ⟶ False) ⟶ (∀ x40 x41 . x27 x41 ⟶ x27 x40 ⟶ (x27 (x5 x41 x40) ⟶ False) ⟶ False) ⟶ ((x39 x3 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 (x38 x40) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ (x27 (x10 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ (x39 x40 ⟶ False) ⟶ x39 (x1 x41 x40) ⟶ False) ⟶ (∀ x40 . (x37 (x11 x40) x40 ⟶ False) ⟶ False) ⟶ ((x24 x23 ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ ((x33 x22 ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ (x37 (x14 x40) (x38 (x1 (x35 x40) (x34 x40))) ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ (x37 (x21 x40) (x38 (x1 (x34 x40) (x35 x40))) ⟶ False) ⟶ False) ⟶ ((x39 x15 ⟶ False) ⟶ False) ⟶ (∀ x40 . x24 x40 ⟶ (x12 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ (x24 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . (x0 (x20 x40 x41 x42) x42 ⟶ False) ⟶ (x0 (x20 x40 x41 x42) x41 ⟶ False) ⟶ (x0 (x20 x40 x41 x42) x40 ⟶ False) ⟶ (x40 = x5 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x0 (x20 x40 x41 x42) x40 ⟶ x0 (x20 x40 x41 x42) x41 ⟶ (x40 = x5 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x0 (x20 x40 x41 x42) x40 ⟶ x0 (x20 x40 x41 x42) x42 ⟶ (x40 = x5 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x42 = x5 x40 x41 ⟶ x0 x43 x41 ⟶ (x0 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x42 = x5 x41 x40 ⟶ x0 x43 x41 ⟶ (x0 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 x43 . x43 = x5 x41 x42 ⟶ x0 x40 x43 ⟶ (x0 x40 x41 ⟶ False) ⟶ (x0 x40 x42 ⟶ False) ⟶ False) ⟶ ((x3 = x15 ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ x32 (x34 x40) (x35 x40) ⟶ x4 (x10 x40) (x5 (x1 (x34 x40) (x35 x40)) (x1 (x35 x40) (x34 x40))) ⟶ (x36 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ x36 x40 ⟶ (x4 (x10 x40) (x5 (x1 (x34 x40) (x35 x40)) (x1 (x35 x40) (x34 x40))) ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ x36 x40 ⟶ (x32 (x34 x40) (x35 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x33 x40 ⟶ (x10 x40 = x5 (x21 x40) (x14 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x5 x41 x40 = x5 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x37 x40 (x38 x41) ⟶ x30 x40 x41 ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x27 x40 ⟶ (x7 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x27 x40 ⟶ (x27 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x37 x40 (x38 x41) ⟶ x39 x40 ⟶ (x30 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x27 x40 ⟶ (x19 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ x27 x40 ⟶ (x27 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . (x39 x41 ⟶ False) ⟶ x37 x40 (x38 x41) ⟶ (x30 x40 x41 ⟶ False) ⟶ x39 x40 ⟶ False) ⟶ (∀ x40 x41 . x27 x41 ⟶ x37 x40 (x38 x41) ⟶ (x27 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x39 x41 ⟶ x37 x40 (x38 x41) ⟶ (x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x39 x40 ⟶ (x27 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x0 x40 x41 ⟶ x0 x41 x40 ⟶ False) ⟶ (x0 x16 (x34 x17) ⟶ False) ⟶ ((x0 x18 (x35 x17) ⟶ False) ⟶ False) ⟶ ((x0 (x2 x18 x16) (x10 x17) ⟶ False) ⟶ False) ⟶ ((x33 x17 ⟶ False) ⟶ False) ⟶ ((x36 x17 ⟶ False) ⟶ False) ⟶ False (proof)