Proofgold Signed Transaction

vin
PrEvg../b0998.. PUPap../ab134..

vout

PrEvg../9ee0b.. 0.34 bars
TMEmU../5e2a7.. ownership of 6c266.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEhG../999fd.. ownership of cfa38.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGE3../8f438.. ownership of c3a5b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZNU../a26f1.. ownership of 87135.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHyL../a61d8.. ownership of 6231b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQnR../96b14.. ownership of 6b2a2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVJ8../a9daa.. ownership of 7e37c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMait../b56cd.. ownership of 81e24.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXZe../48605.. ownership of 9bba6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZQ9../3a7a1.. ownership of fcc45.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcg5../53fa3.. ownership of 25303.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMjh../4e6ff.. ownership of 547d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMe1G../8c88e.. ownership of f6630.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMReV../ff403.. ownership of 9b0ff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQhF../0318d.. ownership of d10d0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaFj../383d8.. ownership of d965d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZUW../a9737.. ownership of 9a431.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcC3../9f3c9.. ownership of 9c79f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZMf../e20ee.. ownership of 438d4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG4f../55e9c.. ownership of fb729.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMScc../80235.. ownership of 4326e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN1g../274a3.. ownership of 8a009.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY8G../801dc.. ownership of 10f71.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMWW../5935e.. ownership of 5adfc.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUanJ../7bc05.. doc published by PrGxv..

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Definition empty_p := λ x0 . ∀ x1 . nIn x1 x0
Known 0117f.. : ∀ x0 : ο . (∀ x1 . (∀ x2 . nIn x2 x1) ⟶ x0) ⟶ x0
Theorem 438d4.. : ∀ x0 : ο . (∀ x1 . empty_p x1 ⟶ x0) ⟶ x0 (proof)
Param 4a7ef.. : ι
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 9a431.. : empty_p 4a7ef.. (proof)
Param iff : ο → ο → ο
Known 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ x0 = x1
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Theorem d10d0.. : ∀ x0 . empty_p x0 ⟶ x0 = 4a7ef.. (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition 4326e.. := λ x0 x1 . or (prim1 x1 x0) (and (empty_p x0) (empty_p x1))
Known xm : ∀ x0 : ο . or x0 (not x0)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem f6630.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . 4326e.. x0 x2 ⟶ x1) ⟶ x1 (proof)
Theorem 25303.. : ∀ x0 x1 . prim1 x1 x0 ⟶ 4326e.. x0 x1 (proof)
Theorem 9bba6.. : ∀ x0 . empty_p x0 ⟶ 4326e.. x0 4a7ef.. (proof)
Theorem 7e37c.. : ∀ x0 . not (empty_p x0) ⟶ ∀ x1 . 4326e.. x0 x1 ⟶ prim1 x1 x0 (proof)
Theorem 6231b.. : ∀ x0 . empty_p x0 ⟶ ∀ x1 . 4326e.. x0 x1 ⟶ x1 = 4a7ef.. (proof)
Definition c2f57.. := λ x0 : ι → ο . ∀ x1 : ο . (∀ x2 . (∀ x3 . iff (prim1 x3 x2) (x0 x3)) ⟶ x1) ⟶ x1
Param 91630.. : ι → ι
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Theorem c3a5b.. : ∀ x0 . c2f57.. (4326e.. x0) (proof)
Param 707e2.. : (ι → ο) → ι
Known 477e8.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . prim1 x1 (707e2.. x0) ⟶ x0 x1
Known bbc77.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . x0 x1 ⟶ prim1 x1 (707e2.. x0)
Theorem 6c266.. : ∀ x0 . not (empty_p x0) ⟶ 707e2.. (4326e.. x0) = x0 (proof)