Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../59945..
PUPoj../a8350..
vout
PrNUD../19d11.. 1,679.99 bars
TMasa../ade67.. ownership of 7a391.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMcWh../66f84.. ownership of 6facd.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUeZz../c8bff.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7a391.. : ∀ 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 . x40 x42 ⟶ (x42 = x41 ⟶ False) ⟶ x40 x41 ⟶ False) ⟶ (∀ x41 x42 . x0 x41 x42 ⟶ x40 x42 ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ (x41 = x39 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x0 x41 x42 ⟶ x2 x42 (x1 x43) ⟶ x40 x43 ⟶ False) ⟶ (∀ x41 x42 x43 . x0 x42 x43 ⟶ x2 x43 (x1 x41) ⟶ (x2 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x3 x42 x41 ⟶ (x2 x42 (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x42 (x1 x41) ⟶ (x3 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x7 x42 x41 x43 = x6 (x5 x42 x41) (x4 x43) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 x46 x47 x48 . (x40 x48 ⟶ False) ⟶ x2 x41 (x1 (x34 x48)) ⟶ x38 x47 x48 ⟶ x38 x42 x48 ⟶ x38 x46 x48 ⟶ x38 x43 x48 ⟶ x38 x45 x48 ⟶ x38 x44 x48 ⟶ x41 = x37 x47 x42 x46 x43 x45 x44 ⟶ (x47 = x42 ⟶ False) ⟶ (x47 = x46 ⟶ False) ⟶ (x47 = x43 ⟶ False) ⟶ (x47 = x45 ⟶ False) ⟶ (x47 = x44 ⟶ False) ⟶ (x42 = x46 ⟶ False) ⟶ (x42 = x43 ⟶ False) ⟶ (x42 = x45 ⟶ False) ⟶ (x42 = x44 ⟶ False) ⟶ (x46 = x43 ⟶ False) ⟶ (x46 = x45 ⟶ False) ⟶ (x46 = x44 ⟶ False) ⟶ (x43 = x45 ⟶ False) ⟶ (x43 = x44 ⟶ False) ⟶ (x45 = x44 ⟶ False) ⟶ (x36 x48 x43 x41 = x35 x48 (x35 x48 (x35 x48 (x35 x48 x47 x42) x46) x45) x44 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x41 x42 ⟶ (x40 x42 ⟶ False) ⟶ (x0 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x0 x42 x41 ⟶ (x2 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x6 x41 x39 = x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 x46 . (x37 x41 x42 x43 x44 x45 x46 = x6 (x7 x41 x42 x43) (x7 x44 x45 x46) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x3 x41 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x33 x41 = x1 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x38 x41 x42 ⟶ (x8 x42 x41 = x4 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x34 x41 = x32 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x10 (x9 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x2 (x9 x41) (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x12 (x11 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ x40 (x11 x41) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x38 (x11 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x10 (x31 x41) x41 ⟶ False) ⟶ (∀ x41 . (x2 (x31 x41) (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x30 (x29 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 (x29 x41) ⟶ False) ⟶ (∀ x41 . (x2 (x29 x41) (x1 (x1 (x33 x41))) ⟶ False) ⟶ False) ⟶ (x40 x13 ⟶ False) ⟶ (∀ x41 . (x40 (x28 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 (x28 x41) (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x12 (x27 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ x40 (x27 x41) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x38 (x27 x41) x41 ⟶ False) ⟶ False) ⟶ ((x40 x14 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ x40 (x26 x41) ⟶ False) ⟶ (∀ x41 . (x40 x41 ⟶ False) ⟶ (x2 (x26 x41) (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x30 (x25 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 (x25 x41) (x1 (x1 (x33 x41))) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x6 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x40 (x6 x41 x42) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 x46 . x40 (x37 x46 x41 x45 x42 x43 x44) ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x40 (x6 x42 x41) ⟶ False) ⟶ (∀ x41 x42 . x40 (x5 x41 x42) ⟶ False) ⟶ (∀ x41 . x40 (x4 x41) ⟶ False) ⟶ (∀ x41 x42 x43 . x40 (x7 x43 x42 x41) ⟶ False) ⟶ ((x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x41 . x40 (x1 x41) ⟶ False) ⟶ (∀ x41 . (x2 (x15 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x38 (x24 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x38 x42 x41 ⟶ (x2 x42 (x1 (x1 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 (x33 x41) (x1 (x1 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x40 x43 ⟶ False) ⟶ x38 x41 x43 ⟶ x2 x42 (x1 (x34 x43)) ⟶ (x38 (x36 x43 x41 x42) x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x38 x41 x42 ⟶ (x2 (x8 x42 x41) (x1 (x34 x42)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x40 x43 ⟶ False) ⟶ x38 x41 x43 ⟶ x38 x42 x43 ⟶ (x38 (x35 x43 x41 x42) x43 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 (x34 x41) (x1 (x1 (x33 x41))) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x30 (x34 x41) x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x6 x42 x41 = x6 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x5 x42 x41 = x5 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x40 x43 ⟶ False) ⟶ x38 x41 x43 ⟶ x38 x42 x43 ⟶ (x35 x43 x41 x42 = x35 x43 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x2 x41 (x1 x42) ⟶ x10 x41 x42 ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x2 x41 (x1 x42) ⟶ x40 x41 ⟶ (x10 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x2 x41 (x1 x42) ⟶ (x10 x41 x42 ⟶ False) ⟶ x40 x41 ⟶ False) ⟶ (∀ x41 x42 . x38 x42 x41 ⟶ (x12 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x40 x42 ⟶ x2 x41 (x1 x42) ⟶ (x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x40 x42 ⟶ False) ⟶ x38 x41 x42 ⟶ x40 x41 ⟶ False) ⟶ (∀ x41 x42 . x0 x41 x42 ⟶ x0 x42 x41 ⟶ False) ⟶ (x36 x18 x17 x16 = x35 x18 (x35 x18 (x35 x18 (x35 x18 x21 x22) x20) x23) x19 ⟶ False) ⟶ (x17 = x19 ⟶ False) ⟶ (x23 = x19 ⟶ False) ⟶ (x23 = x17 ⟶ False) ⟶ (x20 = x19 ⟶ False) ⟶ (x20 = x17 ⟶ False) ⟶ (x20 = x23 ⟶ False) ⟶ (x22 = x19 ⟶ False) ⟶ (x22 = x17 ⟶ False) ⟶ (x22 = x23 ⟶ False) ⟶ (x22 = x20 ⟶ False) ⟶ (x21 = x19 ⟶ False) ⟶ (x21 = x17 ⟶ False) ⟶ (x21 = x23 ⟶ False) ⟶ (x21 = x20 ⟶ False) ⟶ (x21 = x22 ⟶ False) ⟶ ((x16 = x37 x21 x22 x20 x23 x17 x19 ⟶ False) ⟶ False) ⟶ ((x38 x19 x18 ⟶ False) ⟶ False) ⟶ ((x38 x17 x18 ⟶ False) ⟶ False) ⟶ ((x38 x23 x18 ⟶ False) ⟶ False) ⟶ ((x38 x20 x18 ⟶ False) ⟶ False) ⟶ ((x38 x22 x18 ⟶ False) ⟶ False) ⟶ ((x38 x21 x18 ⟶ False) ⟶ False) ⟶ ((x2 x16 (x1 (x34 x18)) ⟶ False) ⟶ False) ⟶ (x40 x18 ⟶ False) ⟶ False (proof)