Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../744d7..
PURCX../dc394..
vout
PrPhD../67c54.. 102.64 bars
TMTSe../5e75c.. ownership of eb8ae.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMcLv../9a1cd.. ownership of e9854.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUbBR../18e95.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem eb8ae.. : ∀ 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 x47 . x1 x46 x47 ⟶ (x45 x47 ⟶ False) ⟶ (x0 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x43 x46 x44 = x44 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x47 x46 ⟶ (x1 x47 x46 ⟶ False) ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ (x45 x41 ⟶ False) ⟶ (x40 x39 ⟶ False) ⟶ ((x2 x39 ⟶ False) ⟶ False) ⟶ ((x38 x39 ⟶ False) ⟶ False) ⟶ ((x2 x3 ⟶ False) ⟶ False) ⟶ ((x37 x3 ⟶ False) ⟶ False) ⟶ ((x38 x3 ⟶ False) ⟶ False) ⟶ (x45 x3 ⟶ False) ⟶ ((x2 x4 ⟶ False) ⟶ False) ⟶ ((x37 x4 ⟶ False) ⟶ False) ⟶ ((x38 x4 ⟶ False) ⟶ False) ⟶ (x45 x36 ⟶ False) ⟶ ((x37 x5 ⟶ False) ⟶ False) ⟶ ((x38 x5 ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ ((x2 x7 ⟶ False) ⟶ False) ⟶ ((x38 x7 ⟶ False) ⟶ False) ⟶ ((x35 x34 ⟶ False) ⟶ False) ⟶ ((x45 x8 ⟶ False) ⟶ False) ⟶ ((x38 x33 ⟶ False) ⟶ False) ⟶ (x45 x33 ⟶ False) ⟶ ((x2 x32 ⟶ False) ⟶ False) ⟶ ((x38 x32 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x43 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x38 x46 ⟶ x45 (x9 x46) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x38 x46 ⟶ x45 (x31 x46) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . (x38 (x10 (x11 x47 x46) (x11 x49 x48)) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x38 (x30 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x45 (x9 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x38 (x29 (x11 x47 x46)) ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x45 (x31 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x45 (x10 x46 x47) ⟶ False) ⟶ (∀ x46 . x45 (x29 x46) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x38 x46 ⟶ (x28 (x9 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x38 x46 ⟶ (x28 (x31 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x35 (x11 x46 x47) ⟶ False) ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 ⟶ (x38 (x43 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x2 (x29 (x11 x47 x46)) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 ⟶ x26 x47 ⟶ x2 x47 ⟶ (x45 (x27 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x28 x46 ⟶ False) ⟶ x38 x46 ⟶ x2 x46 ⟶ x28 (x31 x46) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 ⟶ x2 x47 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x42 (x10 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x42 (x29 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x40 x46 ⟶ False) ⟶ x28 (x9 x46) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ x40 x46 ⟶ (x28 (x9 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x45 (x9 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x38 x47 ⟶ x37 x47 ⟶ x2 x47 ⟶ x1 x46 (x31 x47) ⟶ x45 (x27 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x45 (x30 x47 x46) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x45 (x31 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x37 x46 ⟶ x2 x46 ⟶ (x25 (x9 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x1 (x12 x46) x46 ⟶ False) ⟶ False) ⟶ ((x45 x24 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x2 (x13 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x38 (x13 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x11 x47 x46 = x10 (x10 x47 x46) (x29 x47) ⟶ False) ⟶ False) ⟶ ((x44 = x24 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ x38 x47 ⟶ x2 x47 ⟶ x31 x47 = x31 (x31 x48) ⟶ x38 x46 ⟶ x2 x46 ⟶ x27 x47 (x16 x47 x48) = x46 ⟶ x31 x46 = x9 (x43 (x31 x48) (x30 (x29 (x16 x47 x48)) (x9 (x31 x48)))) ⟶ x27 x46 (x15 x46 x47 x48) = x14 x48 (x16 x47 x48) (x15 x46 x47 x48) ⟶ (x47 = x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ x38 x47 ⟶ x2 x47 ⟶ x31 x47 = x31 (x31 x48) ⟶ x38 x46 ⟶ x2 x46 ⟶ x27 x47 (x16 x47 x48) = x46 ⟶ x31 x46 = x9 (x43 (x31 x48) (x30 (x29 (x16 x47 x48)) (x9 (x31 x48)))) ⟶ (x0 (x15 x46 x47 x48) (x31 x46) ⟶ False) ⟶ (x47 = x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 ⟶ x2 x47 ⟶ x38 x46 ⟶ x2 x46 ⟶ x31 x46 = x31 (x31 x47) ⟶ (x0 (x16 x46 x47) (x31 (x31 x47)) ⟶ False) ⟶ (x46 = x13 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . x38 x49 ⟶ x2 x49 ⟶ x38 x48 ⟶ x2 x48 ⟶ x48 = x13 x49 ⟶ x0 x46 (x31 (x31 x49)) ⟶ x0 x47 (x31 (x23 x46 x48 x49)) ⟶ (x27 (x23 x46 x48 x49) x47 = x14 x49 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ x38 x47 ⟶ x2 x47 ⟶ x47 = x13 x48 ⟶ x0 x46 (x31 (x31 x48)) ⟶ (x31 (x23 x46 x47 x48) = x9 (x43 (x31 x48) (x30 (x29 x46) (x9 (x31 x48)))) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ x38 x47 ⟶ x2 x47 ⟶ x47 = x13 x48 ⟶ x0 x46 (x31 (x31 x48)) ⟶ (x27 x47 x46 = x23 x46 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ x38 x47 ⟶ x2 x47 ⟶ x47 = x13 x48 ⟶ x0 x46 (x31 (x31 x48)) ⟶ (x2 (x23 x46 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ x38 x47 ⟶ x2 x47 ⟶ x47 = x13 x48 ⟶ x0 x46 (x31 (x31 x48)) ⟶ (x38 (x23 x46 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x38 x47 ⟶ x2 x47 ⟶ x38 x46 ⟶ x2 x46 ⟶ x46 = x13 x47 ⟶ (x31 x46 = x31 (x31 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x38 x48 ⟶ x2 x48 ⟶ (x14 x48 x46 x47 = x27 x48 (x11 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x0 (x11 (x17 x47 x46) (x18 x47 x46)) x46 ⟶ False) ⟶ (x0 (x17 x47 x46) x47 ⟶ False) ⟶ (x47 = x31 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x0 (x17 x48 x47) x48 ⟶ x0 (x11 (x17 x48 x47) x46) x47 ⟶ (x48 = x31 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . x48 = x31 x49 ⟶ x0 (x11 x46 x47) x49 ⟶ (x0 x46 x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x47 = x31 x48 ⟶ x0 x46 x47 ⟶ (x0 (x11 x46 (x22 x46 x47 x48)) x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x43 x47 x46 = x43 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x10 x47 x46 = x10 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 ⟶ x1 x46 x47 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 ⟶ x1 x46 x47 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x42 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x40 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x28 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x40 x46 ⟶ False) ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x40 x46 ⟶ False) ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ x2 x46 ⟶ (x40 x46 ⟶ False) ⟶ x28 x46 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ (x37 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x40 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ (x26 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x6 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x38 x46 ⟶ x2 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x0 x47 x46 ⟶ False) ⟶ (x0 x20 (x31 (x13 x19)) ⟶ x38 (x27 (x13 x19) x20) ⟶ x2 (x27 (x13 x19) x20) ⟶ False) ⟶ ((x0 (x11 x20 x21) (x31 x19) ⟶ False) ⟶ False) ⟶ ((x2 x19 ⟶ False) ⟶ False) ⟶ ((x38 x19 ⟶ False) ⟶ False) ⟶ False (proof)