Proofgold Signed Transaction

vin
PrPP6../008c8.. PUZvm../567db..

vout

PrPP6../d5c28.. 0.00 bars
TMQat../b52ee.. ownership of 900a2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXHg../18fef.. ownership of 866c0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJF1../33ed2.. ownership of bf748.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFgb../8d572.. ownership of b033c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP9J../604b6.. ownership of 09583.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKLn../46854.. ownership of 44bd2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLrY../7b8af.. ownership of b171e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM32../4f9b7.. ownership of 8d7cd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPMf../d5808.. ownership of 73af1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaZt../ddc0a.. ownership of a887f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFmp../abca7.. ownership of 12b21.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMddy../022d4.. ownership of 7a130.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJeZ../c65cc.. ownership of 340be.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFmV../2327f.. ownership of 59425.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZkH../f69c9.. ownership of 3db9b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNtU../c0b85.. ownership of ed54c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNXB../a6ca8.. ownership of daa5b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVqk../d8e81.. ownership of ae669.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdhS../4825d.. ownership of aa94a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGTA../f47b8.. ownership of 4999b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZQy../3fde4.. ownership of 62b6b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGZ6../7fc5a.. ownership of 11cf5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZuY../3ae79.. ownership of 51e8c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdH6../baaeb.. ownership of 50ca9.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML5J../14789.. ownership of ff71c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP1F../b67fa.. ownership of f824a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMapL../d528e.. ownership of 36be8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKLD../29bb7.. ownership of 190a4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcp1../64d78.. ownership of 5c14e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXbM../56f36.. ownership of 819ab.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH7D../7919f.. ownership of d091d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN1y../3b657.. ownership of 4ed0e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPHk../f1ba2.. ownership of 455bd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbiB../edc29.. ownership of 9c296.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKGy../a8c56.. ownership of 2f282.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNHU../18749.. ownership of 7bc55.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcoC../88053.. ownership of b2df9.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSkR../b1498.. ownership of 3bfe4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSgS../1afcc.. ownership of 8d0f2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUTR../6b447.. ownership of 3ef5b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYMs../4a5a5.. ownership of f6049.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQxM../bfc02.. ownership of b5deb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP2g../e7cb7.. ownership of fc3b3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGjj../91739.. ownership of 09815.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZcv../f722d.. ownership of 2a940.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG4W../05622.. ownership of 5c741.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdbQ../3617d.. ownership of 94fdb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV4X../4c202.. ownership of 6c5a3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUfV../5fdc2.. ownership of 0a59d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcX6../87e84.. ownership of 1ebcd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM8j../90923.. ownership of c036a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbDx../d4dfa.. ownership of b3b26.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcPi../05552.. ownership of 6eae3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcrN../02caf.. ownership of 6d320.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK6H../5aa6c.. ownership of e39f8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcR6../a44d8.. ownership of 4b68e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHwB../0e915.. ownership of 25bb9.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQsS../46a70.. ownership of 264b0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUUTm../c30f3.. doc published by PrGxv..

Param and : ο → ο → ο
Definition inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition surj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Param 48ef8.. : ι
Param c2e41.. : ι → ι → ο
Definition 6eae3.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (prim1 x2 48ef8..) (c2e41.. x0 x2) ⟶ x1) ⟶ x1
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition c036a.. := λ x0 . not (6eae3.. x0)
Param 14149.. : ι → ι → ι
Definition 0a59d.. := λ x0 x1 . and (and (prim1 x0 48ef8..) (prim1 x1 48ef8..)) (∀ x2 : ο . (∀ x3 . and (prim1 x3 48ef8..) (14149.. x0 x3 = x1) ⟶ x2) ⟶ x2)
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param or : ο → ο → ο
Definition 94fdb.. := λ x0 . and (and (prim1 x0 48ef8..) (prim1 (4ae4a.. 4a7ef..) x0)) (∀ x1 . prim1 x1 48ef8.. ⟶ 0a59d.. x1 x0 ⟶ or (x1 = 4ae4a.. 4a7ef..) (x1 = x0))
Param 1ad11.. : ι → ι → ι
Definition 2a940.. := λ x0 x1 . and (and (prim1 x0 48ef8..) (prim1 x1 48ef8..)) (∀ x2 . prim1 x2 (1ad11.. 48ef8.. (4ae4a.. 4a7ef..)) ⟶ 0a59d.. x2 x0 ⟶ 0a59d.. x2 x1 ⟶ x2 = 4ae4a.. 4a7ef..)
Param 616bf.. : ι → ι → ι
Definition fc3b3.. := λ x0 x1 x2 . and (and (and (prim1 x0 48ef8..) (prim1 x1 48ef8..)) (prim1 x2 48ef8..)) (or (∀ x3 : ο . (∀ x4 . and (prim1 x4 48ef8..) (616bf.. x0 (14149.. x4 x2) = x1) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 48ef8..) (616bf.. x1 (14149.. x4 x2) = x0) ⟶ x3) ⟶ x3))
Param nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition f6049.. := λ x0 . nat_primrec (4ae4a.. 4a7ef..) (λ x1 . 14149.. x0)
Definition 8d0f2.. := λ x0 . and (prim1 x0 48ef8..) (∀ x1 : ο . (∀ x2 . and (prim1 x2 48ef8..) (x0 = 14149.. (4ae4a.. (4ae4a.. 4a7ef..)) x2) ⟶ x1) ⟶ x1)
Definition b2df9.. := λ x0 . and (prim1 x0 48ef8..) (∀ x1 . prim1 x1 48ef8.. ⟶ x0 = 14149.. (4ae4a.. (4ae4a.. 4a7ef..)) x1 ⟶ ∀ x2 : ο . x2)
Definition 2f282.. := nat_primrec (4ae4a.. 4a7ef..) (λ x0 . 14149.. (4ae4a.. x0))
Param f482f.. : ι → ι → ι
Param 0fc90.. : ι → (ι → ι) → ι
Param If_i : ο → ι → ι → ι
Definition 455bd.. := λ x0 . f482f.. (nat_primrec (0fc90.. 48ef8.. (λ x1 . If_i (x1 = 4a7ef..) (4ae4a.. 4a7ef..) 4a7ef..)) (λ x1 x2 . 0fc90.. 48ef8.. (λ x3 . If_i (x3 = 4a7ef..) (4ae4a.. 4a7ef..) (616bf.. (f482f.. x2 (prim3 x3)) (f482f.. x2 x3)))) x0)
Param 1216a.. : ι → (ι → ο) → ι
Definition d091d.. := λ x0 . prim0 (λ x1 . and (prim1 x1 48ef8..) (c2e41.. x1 (1216a.. (4ae4a.. x0) (λ x2 . and (prim1 4a7ef.. x2) (2a940.. x2 x0)))))
Param 569d0.. : ι → ι → ι
Param e6316.. : ι → ι → ι
Param bc82c.. : ι → ι → ι
Param f4dc0.. : ι → ι
Definition 5c14e.. := λ x0 x1 . 569d0.. (2f282.. x0) (e6316.. (2f282.. (bc82c.. x0 (f4dc0.. x1))) (2f282.. x1))
Param a470d.. : ι
Definition 36be8.. := λ x0 x1 . and (and (prim1 x0 a470d..) (prim1 x1 a470d..)) (∀ x2 : ο . (∀ x3 . and (prim1 x3 a470d..) (e6316.. x0 x3 = x1) ⟶ x2) ⟶ x2)
Definition ff71c.. := λ x0 x1 x2 . and (and (and (prim1 x0 a470d..) (prim1 x1 a470d..)) (prim1 x2 (1ad11.. 48ef8.. (4ae4a.. 4a7ef..)))) (36be8.. (bc82c.. x0 (f4dc0.. x1)) x2)
Definition 51e8c.. := λ x0 x1 . and (and (prim1 x0 a470d..) (prim1 x1 a470d..)) (∀ x2 . prim1 x2 (1ad11.. 48ef8.. (4ae4a.. 4a7ef..)) ⟶ 36be8.. x2 x0 ⟶ 36be8.. x2 x1 ⟶ x2 = 4ae4a.. 4a7ef..)
Definition 62b6b.. := λ x0 . nat_primrec (4ae4a.. 4a7ef..) (λ x1 . e6316.. x0)
Param explicit_Nats : ι → ι → (ι → ι) → ο
Param explicit_Nats_primrec : ι → ι → (ι → ι) → ι → (ι → ι → ι) → ι → ι
Param explicit_Nats_one_plus : ι → ι → (ι → ι) → ι → ι → ι
Param explicit_Nats_one_plus : ι → ι → (ι → ι) → ι → ι → ι
Definition explicit_Nats_one_mult_alt := λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_plus x0 x1 x2 x3)
Definition explicit_Nats_lt := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x6 x3 = x4) ⟶ x5) ⟶ x5)
Definition 3db9b.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (prim1 x3 x0) (∀ x4 . prim1 x4 x0 ⟶ explicit_Nats_lt x0 x1 x2 x4 x3 ⟶ or (x4 = x1) (x4 = x3))
Definition 340be.. := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 . prim1 x5 x0 ⟶ explicit_Nats_lt x0 x1 x2 x5 x3 ⟶ explicit_Nats_lt x0 x1 x2 x5 x4 ⟶ x5 = 4ae4a.. 4a7ef..)
Definition 12b21.. := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 x5 . and (and (and (prim1 x3 x0) (prim1 x4 x0)) (prim1 x5 x0)) (or (or (x3 = x4) (∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (explicit_Nats_one_plus x0 x1 x2 x3 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x4) ⟶ x6) ⟶ x6)) (∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x3) ⟶ x6) ⟶ x6))
Definition explicit_Nats_one_lt := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4) ⟶ x5) ⟶ x5)
Definition explicit_Nats_one_le := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (or (x3 = x4) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4) ⟶ x5) ⟶ x5))
Definition 09583.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (prim1 x3 x0) (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x5) ⟶ x4) ⟶ x4)
Definition bf748.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (prim1 x3 x0) (∀ x4 . prim1 x4 x0 ⟶ x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x4 ⟶ ∀ x5 : ο . x5)
Definition 900a2.. := λ x0 x1 . λ x2 : ι → ι . explicit_Nats_primrec x0 x1 x2 x1 (λ x3 x4 . If_i (and (x3 = x1 ⟶ ∀ x5 : ο . x5) (340be.. x0 x1 x2 x3 x3)) (x2 x4) x4)