Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../d70df..
PUbeb../b8805..
vout
PrPhD../7198b.. 3.39 bars
TMF76../bd46a.. ownership of cec58.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMPwL../3a109.. ownership of 5a780.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUb3W../773a2.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem cec58.. : ∀ 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 . (x41 x45 ⟶ False) ⟶ x33 x45 ⟶ x40 x45 ⟶ x34 x45 ⟶ x39 x45 ⟶ x36 x42 (x35 x45) ⟶ x36 x44 (x35 x45) ⟶ x36 x43 (x35 x45) ⟶ x37 x45 x42 x44 ⟶ (x37 x45 (x38 x45 x42 x43) (x38 x45 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x40 x44 ⟶ x39 x44 ⟶ x36 x43 (x35 x44) ⟶ x36 x42 (x35 x44) ⟶ (x37 x44 (x0 x44 x43 x42) x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x32 x44 ⟶ x39 x44 ⟶ x36 x43 (x35 x44) ⟶ x36 x42 (x35 x44) ⟶ x30 x44 x43 (x29 x44 x42) ⟶ (x0 x44 x43 x42 = x31 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x32 x44 ⟶ x39 x44 ⟶ x36 x43 (x35 x44) ⟶ x36 x42 (x35 x44) ⟶ x0 x44 x43 x42 = x31 x44 ⟶ (x30 x44 x43 (x29 x44 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x32 x44 ⟶ x39 x44 ⟶ x36 x43 (x35 x44) ⟶ x36 x42 (x35 x44) ⟶ (x29 x44 (x0 x44 x43 x42) = x27 x44 (x29 x44 x43) (x29 x44 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x28 x43 ⟶ x32 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x0 x43 (x29 x43 x42) x42 = x31 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x28 x43 ⟶ x26 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x30 x43 (x31 x43) x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x2 x44 x42 x43 ⟶ (x2 x44 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x40 x44 ⟶ x34 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x30 x44 x42 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x2 x44 x42 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x40 x44 ⟶ x34 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x37 x44 x42 x43 ⟶ (x30 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x40 x44 ⟶ x34 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x30 x44 x42 x43 ⟶ (x37 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x42 = x43 ⟶ (x2 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x2 x44 x42 x43 ⟶ (x42 = x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x25 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x0 x44 x42 x43 = x38 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x5 x44 ⟶ x3 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x27 x44 x42 x43 = x4 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x28 x43 ⟶ x32 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x29 x43 (x29 x43 x42) = x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x28 x43 ⟶ x26 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x0 x43 (x31 x43) x42 = x31 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x28 x43 ⟶ x26 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x27 x43 (x31 x43) x42 = x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x1 x43 ⟶ x40 x43 ⟶ x34 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x0 x43 x42 x42 = x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x1 x43 ⟶ x40 x43 ⟶ x34 x43 ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x4 x43 x42 x42 = x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x36 (x6 x42) x42 ⟶ False) ⟶ False) ⟶ ((x39 x24 ⟶ False) ⟶ False) ⟶ ((x3 x7 ⟶ False) ⟶ False) ⟶ ((x23 x22 ⟶ False) ⟶ False) ⟶ ((x25 x8 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x3 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x25 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x3 x42 ⟶ (x23 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x25 x42 ⟶ (x23 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x41 x43 ⟶ False) ⟶ x39 x43 ⟶ x36 x42 (x35 x43) ⟶ (x36 (x29 x43 x42) (x35 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x25 x42 ⟶ (x36 (x31 x42) (x35 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x25 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x36 (x0 x44 x42 x43) (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x5 x44 ⟶ x3 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x36 (x27 x44 x42 x43) (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x25 x44 ⟶ x36 x43 (x35 x44) ⟶ x36 x42 (x35 x44) ⟶ (x36 (x38 x44 x43 x42) (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x3 x44 ⟶ x36 x43 (x35 x44) ⟶ x36 x42 (x35 x44) ⟶ (x36 (x4 x44 x43 x42) (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x36 (x21 x44 x42 x43) (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x30 x44 x42 x43 ⟶ x30 x44 x43 x42 ⟶ (x2 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x2 x44 x42 x43 ⟶ (x30 x44 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ x2 x44 x42 x43 ⟶ (x30 x44 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x28 x44 ⟶ x39 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x21 x44 x42 x43 = x0 x44 x42 (x29 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x39 x42 ⟶ x38 x42 (x10 x42) (x4 x42 (x12 x42) (x11 x42)) = x4 x42 (x38 x42 (x10 x42) (x12 x42)) (x38 x42 (x10 x42) (x11 x42)) ⟶ (x9 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x39 x42 ⟶ (x36 (x11 x42) (x35 x42) ⟶ False) ⟶ (x9 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x39 x42 ⟶ (x36 (x12 x42) (x35 x42) ⟶ False) ⟶ (x9 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x41 x42 ⟶ False) ⟶ x39 x42 ⟶ (x36 (x10 x42) (x35 x42) ⟶ False) ⟶ (x9 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . (x41 x45 ⟶ False) ⟶ x39 x45 ⟶ x9 x45 ⟶ x36 x42 (x35 x45) ⟶ x36 x44 (x35 x45) ⟶ x36 x43 (x35 x45) ⟶ (x38 x45 x42 (x4 x45 x44 x43) = x4 x45 (x38 x45 x42 x44) (x38 x45 x42 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x1 x44 ⟶ x25 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x0 x44 x42 x43 = x0 x44 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . (x41 x44 ⟶ False) ⟶ x5 x44 ⟶ x3 x44 ⟶ x36 x42 (x35 x44) ⟶ x36 x43 (x35 x44) ⟶ (x27 x44 x42 x43 = x27 x44 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ x9 x42 ⟶ (x20 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ x9 x42 ⟶ (x28 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ x9 x42 ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x9 x42 ⟶ x14 x42 ⟶ x13 x42 ⟶ (x32 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x9 x42 ⟶ x14 x42 ⟶ x13 x42 ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x32 x42 ⟶ (x13 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x32 x42 ⟶ (x14 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x32 x42 ⟶ (x9 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x32 x42 ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x14 x42 ⟶ (x15 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x14 x42 ⟶ (x26 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x14 x42 ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x26 x42 ⟶ x15 x42 ⟶ (x14 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x26 x42 ⟶ x15 x42 ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x5 x42 ⟶ x19 x42 ⟶ x1 x42 ⟶ x33 x42 ⟶ x40 x42 ⟶ x34 x42 ⟶ (x28 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x5 x42 ⟶ x19 x42 ⟶ x1 x42 ⟶ x33 x42 ⟶ x40 x42 ⟶ x34 x42 ⟶ x41 x42 ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ (x34 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ (x40 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ (x33 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ (x1 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ (x19 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ (x5 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x39 x42 ⟶ (x41 x42 ⟶ False) ⟶ x28 x42 ⟶ x41 x42 ⟶ False) ⟶ ((x2 x18 (x21 x18 x16 x17) x16 ⟶ False) ⟶ (x2 x18 (x0 x18 x16 x17) (x31 x18) ⟶ False) ⟶ False) ⟶ (x2 x18 (x0 x18 x16 x17) (x31 x18) ⟶ x2 x18 (x21 x18 x16 x17) x16 ⟶ False) ⟶ ((x36 x17 (x35 x18) ⟶ False) ⟶ False) ⟶ ((x36 x16 (x35 x18) ⟶ False) ⟶ False) ⟶ ((x39 x18 ⟶ False) ⟶ False) ⟶ ((x32 x18 ⟶ False) ⟶ False) ⟶ ((x28 x18 ⟶ False) ⟶ False) ⟶ (x41 x18 ⟶ False) ⟶ False (proof)