Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../e0e2b..
PUWaA../cdd61..
vout
PrPhD../9541d.. 3.39 bars
TMcT1../39f47.. ownership of fc5eb.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMJLE../e93b2.. ownership of fb339.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PULNn../61f2e.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem fc5eb.. : ∀ 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 : ι → ο . (∀ x46 x47 . x45 x47 ⟶ (x47 = x46 ⟶ False) ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x45 x47 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x46 = x44 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x2 x46 x3 = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x0 x46 x47 ⟶ x42 x47 (x43 x48) ⟶ x45 x48 ⟶ False) ⟶ (∀ x46 x47 x48 . x0 x47 x48 ⟶ x42 x48 (x43 x46) ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x41 x47 x46 ⟶ (x42 x47 (x43 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 (x43 x46) ⟶ (x41 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x40 x3 x46 = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x46 x47 ⟶ (x45 x47 ⟶ False) ⟶ (x0 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x47 x46 ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ ((x42 x44 x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x1 x48 ⟶ x1 x46 ⟶ x1 x47 ⟶ (x40 (x40 x48 x46) x47 = x40 x48 (x40 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x1 x48 ⟶ x1 x46 ⟶ x1 x47 ⟶ (x40 x48 (x2 x46 x47) = x2 (x40 x48 x46) x47 ⟶ False) ⟶ False) ⟶ ((x42 x3 x39 ⟶ False) ⟶ False) ⟶ ((x42 x3 x5 ⟶ False) ⟶ False) ⟶ ((x38 x3 x39 x5 ⟶ False) ⟶ False) ⟶ ((x6 x3 ⟶ False) ⟶ False) ⟶ (x45 x3 ⟶ False) ⟶ ((x40 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x2 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x41 x46 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x45 x48 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x48) ⟶ x42 x47 x46 ⟶ (x38 x47 x48 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x45 x48 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x48) ⟶ x38 x47 x48 x46 ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ ((x5 = x4 ⟶ False) ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ (x45 x8 ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ ((x45 x10 ⟶ False) ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ ((x9 x12 ⟶ False) ⟶ False) ⟶ ((x1 x12 ⟶ False) ⟶ False) ⟶ ((x45 x12 ⟶ False) ⟶ False) ⟶ ((x7 x13 ⟶ False) ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ ((x9 x36 ⟶ False) ⟶ False) ⟶ ((x11 x35 ⟶ False) ⟶ False) ⟶ ((x37 x35 ⟶ False) ⟶ False) ⟶ ((x9 x35 ⟶ False) ⟶ False) ⟶ ((x1 x35 ⟶ False) ⟶ False) ⟶ ((x6 x34 ⟶ False) ⟶ False) ⟶ ((x9 x34 ⟶ False) ⟶ False) ⟶ ((x11 x33 ⟶ False) ⟶ False) ⟶ ((x6 x33 ⟶ False) ⟶ False) ⟶ ((x9 x33 ⟶ False) ⟶ False) ⟶ ((x1 x33 ⟶ False) ⟶ False) ⟶ ((x1 x32 ⟶ False) ⟶ False) ⟶ (x45 x32 ⟶ False) ⟶ (x45 x31 ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x30 x15 ⟶ False) ⟶ False) ⟶ ((x16 x15 ⟶ False) ⟶ False) ⟶ (x45 x15 ⟶ False) ⟶ ((x9 x17 ⟶ False) ⟶ False) ⟶ ((x11 x29 ⟶ False) ⟶ False) ⟶ ((x1 x18 ⟶ False) ⟶ False) ⟶ ((x45 x28 ⟶ False) ⟶ False) ⟶ ((x14 x19 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x1 x48 ⟶ x1 x46 ⟶ x1 x47 ⟶ (x40 (x2 x3 x48) (x2 x46 x47) = x2 x46 (x40 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x40 x47 (x2 x3 x46) = x2 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x1 x48 ⟶ x1 x46 ⟶ x1 x47 ⟶ (x40 x48 (x2 x46 x47) = x2 (x40 x48 x46) x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x1 x47 ⟶ (x45 x46 ⟶ False) ⟶ x1 x46 ⟶ x45 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . x11 x47 ⟶ x11 x46 ⟶ (x11 (x2 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x1 x47 ⟶ (x45 x46 ⟶ False) ⟶ x1 x46 ⟶ x45 (x40 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . x11 x47 ⟶ x11 x46 ⟶ (x11 (x40 x47 x46) ⟶ False) ⟶ False) ⟶ ((x14 x4 ⟶ False) ⟶ False) ⟶ (x45 x4 ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x1 (x2 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x1 (x40 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x6 x47 ⟶ False) ⟶ x11 x47 ⟶ (x6 x46 ⟶ False) ⟶ x11 x46 ⟶ x37 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x37 x47 ⟶ False) ⟶ x11 x47 ⟶ (x37 x46 ⟶ False) ⟶ x11 x46 ⟶ x37 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x37 x47 ⟶ False) ⟶ x11 x47 ⟶ (x6 x46 ⟶ False) ⟶ x11 x46 ⟶ x6 (x2 x46 x47) ⟶ False) ⟶ (∀ x46 x47 . (x37 x47 ⟶ False) ⟶ x11 x47 ⟶ (x6 x46 ⟶ False) ⟶ x11 x46 ⟶ x6 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x37 x47 ⟶ False) ⟶ x11 x47 ⟶ (x37 x46 ⟶ False) ⟶ x11 x46 ⟶ x37 (x40 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x6 x47 ⟶ False) ⟶ x11 x47 ⟶ (x6 x46 ⟶ False) ⟶ x11 x46 ⟶ x37 (x40 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x6 x47 ⟶ False) ⟶ x11 x47 ⟶ (x37 x46 ⟶ False) ⟶ x11 x46 ⟶ x6 (x40 x46 x47) ⟶ False) ⟶ (∀ x46 x47 . (x6 x47 ⟶ False) ⟶ x11 x47 ⟶ (x37 x46 ⟶ False) ⟶ x11 x46 ⟶ x6 (x40 x47 x46) ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x47) ⟶ (x38 (x27 x46 x47) x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x42 (x20 x46) x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x45 x48 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x48) ⟶ x38 x47 x48 x46 ⟶ (x42 x47 x48 ⟶ False) ⟶ False) ⟶ ((x42 x5 (x43 x39) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x40 x47 x46 = x40 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x21 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ (x6 x46 ⟶ False) ⟶ (x37 x46 ⟶ False) ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ (x6 x46 ⟶ False) ⟶ (x37 x46 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x4 ⟶ (x7 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x9 x46 ⟶ x37 x46 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x9 x46 ⟶ x6 x46 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x9 x46 ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x7 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x9 x46 ⟶ (x6 x46 ⟶ False) ⟶ (x37 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x9 x46 ⟶ (x6 x46 ⟶ False) ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x14 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ x37 x46 ⟶ x6 x46 ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ x37 x46 ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ x37 x46 ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 x47 . x14 x47 ⟶ x42 x46 x47 ⟶ (x14 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x9 x46 ⟶ (x37 x46 ⟶ False) ⟶ (x6 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x9 x46 ⟶ (x37 x46 ⟶ False) ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x11 x46 ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x22 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ x6 x46 ⟶ x37 x46 ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ x6 x46 ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x9 x46 ⟶ x6 x46 ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 . x11 x46 ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x14 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x9 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x11 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x7 x46 ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x16 x46 ⟶ x30 x46 ⟶ (x14 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x39 ⟶ (x11 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x39 ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x14 x46 ⟶ (x30 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x14 x46 ⟶ (x16 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x21 x47 ⟶ x42 x46 (x43 x47) ⟶ (x21 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x0 x47 x46 ⟶ False) ⟶ (x2 (x40 x24 x25) (x40 x26 x23) = x2 (x40 (x2 x24 x26) x25) x23 ⟶ False) ⟶ ((x1 x23 ⟶ False) ⟶ False) ⟶ ((x1 x26 ⟶ False) ⟶ False) ⟶ ((x1 x25 ⟶ False) ⟶ False) ⟶ ((x1 x24 ⟶ False) ⟶ False) ⟶ False (proof)