Proofgold Signed Transaction

vin
PrKjC../e3f3f.. PUXW6../7d8f1..

vout

PrKjC../d6a8e.. 0.10 bars
TMKnd../b547e.. ownership of 53760.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV2W../81e98.. ownership of 444b0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcVf../e95eb.. ownership of 6a551.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYtc../89429.. ownership of 29062.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLWU../df612.. ownership of 99f52.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdiN../45add.. ownership of 43c39.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSA4../f1060.. ownership of 33cc2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMNY../ad70d.. ownership of d14a1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXHk../69707.. ownership of d3f3c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKAf../514b4.. ownership of 49a96.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUQ52../ac385.. doc published by PrGxv..

Definition d3f3c.. := Power 0
Definition 33cc2.. := Power d3f3c..
Definition 99f52.. := Power 33cc2..
Definition 6a551.. := Power 99f52..
Known 97a83..^{atleastp_E_impred} : ∀ x0 x1 . atleastp x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known e6daf..^injE_impred : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . In x4 x0 ⟶ In (x2 x4) x1) ⟶ (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ x3) ⟶ x3
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Known 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum x0 x1)
Known f2c89..^{Empty_In_Power} : ∀ x0 . In 0 (Power x0)
Theorem 53760.. : ∀ x0 x1 x2 . atleastp (setsum 0 6a551..) 0 ⟶ False (proof)