Proofgold Signed Transaction

vin
PrJGW../6ae7b.. PUKJY../067d7..

vout

PrJGW../7aad8.. 3.00 bars
TMHKv../d77da.. negprop ownership controlledby PrGxv.. upto 0
TMRTU../9bcfd.. ownership of 732ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKsy../22adf.. ownership of 8353f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGeP../d827d.. ownership of 48046.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFka../1f3bb.. ownership of aef7b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML6U../9db16.. ownership of 2042d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXmB../24138.. ownership of b0c33.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHxx../d4d50.. ownership of 0286c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZWV../01252.. ownership of ffff6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMd5../8baa4.. ownership of db6fe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGL8../856b0.. ownership of ede72.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZWY../e2210.. ownership of 92e6a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRq8../87691.. ownership of 9a58e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTVi../98b0b.. ownership of 93754.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPzp../28b4b.. ownership of 3b556.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYHp../a994e.. ownership of 50787.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZpS../8e739.. ownership of d0954.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUaq1../227b1.. doc published by PrGxv..

Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem 50787.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x0 = x2 (proof)
Theorem 93754.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x1 = x3 (proof)
Definition False := ∀ x0 : ο . x0
Known 9aea6.. : ∀ x0 x1 . ∀ x2 : ι → ι . prim0 x0 x1 = prim1 x2 ⟶ ∀ x3 : ο . x3
Theorem 92e6a.. : ∀ x0 : ι → ι . ∀ x1 x2 . prim1 x0 = prim0 x1 x2 ⟶ False (proof)
Known b4755.. : ∀ x0 x1 : ι → ι . prim1 x0 = prim1 x1 ⟶ x0 = x1
Theorem db6fe.. : ∀ x0 x1 : ι → ι . ∀ x2 . prim1 x0 = prim1 x1 ⟶ x0 x2 = x1 x2 (proof)
Definition 236c6.. := prim1 (λ x0 . x0)
Known f558c.. : ∀ x0 x1 . 236c6.. = prim0 x0 x1 ⟶ ∀ x2 : ο . x2
Theorem 0286c.. : ∀ x0 x1 . prim0 x0 x1 = 236c6.. ⟶ False (proof)
Known 148f8.. : ∀ x0 : ι → ι → ι . 236c6.. = prim1 (λ x2 . prim1 (x0 x2)) ⟶ ∀ x1 : ο . x1
Theorem 2042d.. : ∀ x0 : ι → ι → ι . prim1 (λ x2 . prim1 (x0 x2)) = 236c6.. ⟶ False (proof)
Known f2c23.. : ∀ x0 x1 : ι → ι . 236c6.. = prim1 (λ x3 . prim0 (x0 x3) (x1 x3)) ⟶ ∀ x2 : ο . x2
Theorem 48046.. : ∀ x0 x1 : ι → ι . prim1 (λ x3 . prim0 (x0 x3) (x1 x3)) = 236c6.. ⟶ False (proof)
Known 61590.. : 236c6.. = prim1 (λ x1 . 236c6..) ⟶ False
Theorem 732ef.. : prim1 (λ x1 . 236c6..) = 236c6.. ⟶ False (proof)