Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../5cd03..
PUL1N../507bd..
vout
PrNUD../98635.. 0.02 bars
TMTnw../18fe3.. ownership of 3b01f.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMFeR../35b54.. ownership of 5af53.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUSYA../b2c47.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 3b01f.. : ∀ 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 . x40 x44 ⟶ x35 x44 ⟶ x0 x43 (x36 (x39 x44)) ⟶ (x38 (x39 x44) x43 = x37 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x44 x43 ⟶ (x2 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ (x3 (x37 x44 x43) (x36 x44) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x3 x43 x43 ⟶ False) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ (x42 x33 ⟶ False) ⟶ (∀ x43 . (x32 x43 ⟶ False) ⟶ x32 (x31 x43) ⟶ False) ⟶ (∀ x43 . (x32 x43 ⟶ False) ⟶ (x2 (x31 x43) (x1 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x32 (x30 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x42 (x30 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x2 (x30 x43) (x1 x43) ⟶ False) ⟶ False) ⟶ (x4 x5 ⟶ False) ⟶ ((x35 x5 ⟶ False) ⟶ False) ⟶ ((x40 x5 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x28 (x29 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x2 (x29 x43) (x1 x43) ⟶ False) ⟶ False) ⟶ ((x35 x27 ⟶ False) ⟶ False) ⟶ ((x6 x27 ⟶ False) ⟶ False) ⟶ ((x40 x27 ⟶ False) ⟶ False) ⟶ (x42 x27 ⟶ False) ⟶ (∀ x43 . x28 (x26 x43) x43 ⟶ False) ⟶ (∀ x43 . (x2 (x26 x43) (x1 x43) ⟶ False) ⟶ False) ⟶ ((x35 x25 ⟶ False) ⟶ False) ⟶ ((x6 x25 ⟶ False) ⟶ False) ⟶ ((x40 x25 ⟶ False) ⟶ False) ⟶ (x42 x7 ⟶ False) ⟶ (∀ x43 . (x42 (x24 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x2 (x24 x43) (x1 x43) ⟶ False) ⟶ False) ⟶ ((x6 x23 ⟶ False) ⟶ False) ⟶ ((x40 x23 ⟶ False) ⟶ False) ⟶ ((x22 x21 ⟶ False) ⟶ False) ⟶ ((x35 x21 ⟶ False) ⟶ False) ⟶ ((x40 x21 ⟶ False) ⟶ False) ⟶ ((x42 x8 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x42 (x20 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ (x2 (x20 x43) (x1 x43) ⟶ False) ⟶ False) ⟶ ((x40 x19 ⟶ False) ⟶ False) ⟶ (x42 x19 ⟶ False) ⟶ ((x35 x18 ⟶ False) ⟶ False) ⟶ ((x40 x18 ⟶ False) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x40 x43 ⟶ x42 (x17 x43) ⟶ False) ⟶ (∀ x43 . (x42 x43 ⟶ False) ⟶ x40 x43 ⟶ x42 (x36 x43) ⟶ False) ⟶ (∀ x43 . x32 x43 ⟶ x40 x43 ⟶ (x32 (x17 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x32 x43 ⟶ x40 x43 ⟶ (x32 (x36 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x42 x44 ⟶ x40 x44 ⟶ (x42 (x37 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ x42 x43 ⟶ (x42 (x37 x44 x43) ⟶ False) ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 (x1 x43) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ x16 x44 ⟶ x35 x44 ⟶ (x42 (x38 x44 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x32 x43 ⟶ False) ⟶ x40 x43 ⟶ x35 x43 ⟶ x32 (x36 x43) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ x32 (x17 x43) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ x4 x43 ⟶ (x32 (x17 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x42 (x17 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x40 x44 ⟶ x6 x44 ⟶ x35 x44 ⟶ x2 x43 (x36 x44) ⟶ x42 (x38 x44 x43) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x42 (x36 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x6 x43 ⟶ x35 x43 ⟶ (x9 (x17 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . (x2 (x15 x43) x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ (x35 (x39 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ (x40 (x39 x43) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 (x10 x43 x44) x43 ⟶ (x3 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x0 (x10 x43 x44) x44 ⟶ False) ⟶ (x3 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x3 x44 x45 ⟶ x0 x43 x44 ⟶ (x0 x43 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ x35 x44 ⟶ (x14 x43 x44 = x38 x44 (x13 x43 x44) ⟶ False) ⟶ (x0 (x14 x43 x44) x43 ⟶ False) ⟶ (x43 = x17 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ x35 x44 ⟶ (x0 (x13 x43 x44) (x36 x44) ⟶ False) ⟶ (x0 (x14 x43 x44) x43 ⟶ False) ⟶ (x43 = x17 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x40 x45 ⟶ x35 x45 ⟶ x0 (x14 x44 x45) x44 ⟶ x0 x43 (x36 x45) ⟶ x14 x44 x45 = x38 x45 x43 ⟶ (x44 = x17 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 x46 . x40 x46 ⟶ x35 x46 ⟶ x45 = x17 x46 ⟶ x0 x43 (x36 x46) ⟶ x44 = x38 x46 x43 ⟶ (x0 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x40 x45 ⟶ x35 x45 ⟶ x44 = x17 x45 ⟶ x0 x43 x44 ⟶ (x43 = x38 x45 (x12 x43 x44 x45) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 x45 . x40 x45 ⟶ x35 x45 ⟶ x44 = x17 x45 ⟶ x0 x43 x44 ⟶ (x0 (x12 x43 x44 x45) (x36 x45) ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x34 x44 ⟶ x2 x43 (x1 x44) ⟶ (x34 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x34 x44 ⟶ x2 x43 x44 ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x34 x44 ⟶ x2 x43 x44 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x34 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x32 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x32 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x32 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x32 x44 ⟶ x2 x43 (x1 x44) ⟶ (x32 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x40 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ x32 x43 ⟶ False) ⟶ (∀ x43 x44 . x42 x44 ⟶ x2 x43 (x1 x44) ⟶ x28 x43 x44 ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ (x6 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x4 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x2 x43 (x1 x44) ⟶ x42 x43 ⟶ (x28 x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ (x16 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ x35 x44 ⟶ x2 x43 (x1 x44) ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . (x42 x44 ⟶ False) ⟶ x2 x43 (x1 x44) ⟶ (x28 x43 x44 ⟶ False) ⟶ x42 x43 ⟶ False) ⟶ (∀ x43 x44 . x40 x44 ⟶ x2 x43 (x1 x44) ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x22 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ x40 x43 ⟶ x35 x43 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x42 x44 ⟶ x2 x43 (x1 x44) ⟶ (x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x40 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 . x42 x43 ⟶ (x35 x43 ⟶ False) ⟶ False) ⟶ (∀ x43 x44 . x0 x43 x44 ⟶ x0 x44 x43 ⟶ False) ⟶ (x3 (x17 (x39 x11)) (x1 (x36 x11)) ⟶ False) ⟶ ((x35 x11 ⟶ False) ⟶ False) ⟶ ((x40 x11 ⟶ False) ⟶ False) ⟶ False (proof)