Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCnV../45763..
PUXUv../a8210..
vout
PrCnV../f185c.. 67.60 bars
TMMpE../1f71a.. ownership of 88343.. as prop with payaddr PrCnV.. rights free controlledby PrCnV.. upto 0
TMMAC../dfafb.. ownership of 9f96f.. as prop with payaddr PrCnV.. rights free controlledby PrCnV.. upto 0
TMLDj../549ea.. ownership of 8ddd3.. as prop with payaddr PrCnV.. rights free controlledby PrCnV.. upto 0
TMWJM../ea89a.. ownership of a9f44.. as prop with payaddr PrCnV.. rights free controlledby PrCnV.. upto 0
PUR43../7b219.. doc published by PrCnV..
Theorem 8ddd3.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . and (not (x0 x7 (x1 x7 (x1 (x1 (x1 (x1 (x1 (x1 (x1 x6 x6) x7) x6) (x1 (x4 (x1 (x4 (x1 (x1 x6 (x1 (x4 x6) x5)) (x1 (x1 (x1 (x4 (x4 (x4 (x4 (x1 x5 (x1 (x4 (x1 x6 (x1 x6 (x4 x6)))) x6)))))) x7) x7) (x1 x6 (x4 x6))))) x5)) (x1 (x4 (x4 (x4 x7))) x6))) x5) x6) x6)))) (x6 = x6) ⟶ ∀ x8 : ο . (∀ x9 . (∀ x10 . x9 = x4 x5) ⟶ x8) ⟶ x8 (proof)
Known FalseEFalseE : False ⟶ ∀ x0 : ο . x0
Known notEnotE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known e3ec9..neq_0_1 : not (0 = 1)
Theorem 88343.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 x8 . (∀ x9 x10 . (∃ x11 . ∀ x13 . (∀ x14 . x8 = x5) ⟶ ∀ x14 : ο . (∀ x15 . (not (x3 x10) ⟶ not (x3 x15)) ⟶ x14) ⟶ x14) ⟶ x7 = x9) ⟶ x1 (x4 (x4 (x4 x6))) (x1 (x1 x8 (x4 x5)) x6) = x4 x8 (proof)