Proofgold Signed Transaction

vin
PrJGW../c89ec.. PUSBB../b9278..

vout

PrJGW../06ef8.. 2.00 bars
TMVxE../1a0f9.. BOUNTY 1.00 bars
TMFJm../e070b.. ownership of 1b30d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ7e../8f1bd.. ownership of 5b814.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS2v../c11c7.. ownership of 79006.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTJg../13df6.. ownership of 39a81.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRFf../99a33.. ownership of 5ad3b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK1L../dafd0.. ownership of 11baf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMagQ../f678e.. ownership of 70c47.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcSs../d4afd.. ownership of 7dadd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PURiK../f3334.. doc published by PrGxv..

Definition 70c47.. := λ x0 . and (nat_p x0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = mul_nat 2 x2) ⟶ x1) ⟶ x1)
Definition 5ad3b.. := nat_primrec 0 (λ x0 x1 . If_i (70c47.. x0) x1 (ordsucc x1))
Definition 79006.. := λ x0 . If_i (70c47.. x0) (5ad3b.. x0) (ordsucc (mul_nat 3 x0))
Definition 1b30d.. := λ x0 . λ x1 : ι → ι . λ x2 . nat_primrec x2 (λ x3 . x1) x0
Conjecture aa000.. : ∀ x0 . nat_p x0 ⟶ not (x0 = 0) ⟶ ∀ x1 : ο . (∀ x2 . and (nat_p x2) (1b30d.. x2 79006.. x0 = 1) ⟶ x1) ⟶ x1