Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../2ec6f..
PUT81../3b939..
vout
PrNUD../d4413.. 0.02 bars
TMH8G../d946a.. ownership of cc5f9.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMKxu../255df.. ownership of 35298.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUTNm../505ff.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem cc5f9.. : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 . ∀ x4 : ι → ι . ∀ x5 x6 : ι → ι → ι . ∀ x7 x8 : ι → ι → ο . ∀ x9 . (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ x7 x11 x10 ⟶ (x6 x11 (x5 x10 x11) = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ x7 x11 x10 ⟶ (x8 (x5 x10 x11) x9 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 x12 . x8 x12 x9 ⟶ x8 x10 x9 ⟶ x8 x11 x9 ⟶ x12 = x6 x10 x11 ⟶ (x7 x11 x12 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 x12 . x8 x12 x9 ⟶ x8 x10 x9 ⟶ x8 x11 x9 ⟶ (x0 x12 (x6 x10 x11) = x6 (x0 x12 x10) (x0 x12 x11) ⟶ False) ⟶ False) ⟶ (∀ x10 . (x8 (x4 x10) x10 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x8 (x0 x11 x10) x9 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x8 (x6 x11 x10) x9 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x7 x11 x10 ⟶ False) ⟶ (x7 x10 x11 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x0 x11 x10 = x0 x10 x11 ⟶ False) ⟶ False) ⟶ (∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x6 x11 x10 = x6 x10 x11 ⟶ False) ⟶ False) ⟶ (x7 (x0 x1 x3) (x0 x2 x3) ⟶ False) ⟶ ((x7 x1 x2 ⟶ False) ⟶ False) ⟶ ((x8 x3 x9 ⟶ False) ⟶ False) ⟶ ((x8 x2 x9 ⟶ False) ⟶ False) ⟶ ((x8 x1 x9 ⟶ False) ⟶ False) ⟶ False (proof)