Proofgold Signed Transaction

vin
PrNHZ../f2b2d.. PUbgW../aefda..

vout

PrNHZ../e116b.. 63.99 bars
TMVcV../1972d.. ownership of 4056c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMa2L../fbc7e.. ownership of 4a8f2.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVgF../41bd4.. ownership of 20480.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHnM../9d53f.. ownership of 9bf31.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMdYa../14764.. ownership of 2dc23.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMKRW../93704.. ownership of 3900d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMU3q../b1071.. ownership of 429ac.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMawo../7ebae.. ownership of 98564.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSxp../f4867.. ownership of 77598.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMdkx../dc226.. ownership of 905c4.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHPe../35048.. ownership of 630e7.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLhY../712d8.. ownership of 14338.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPrt../72cf8.. ownership of 9899a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMZzD../0a426.. ownership of 99500.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMEyh../7293e.. ownership of b501e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWhN../c067c.. ownership of 16cc7.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHRB../a8854.. ownership of d5242.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGMf../39bc7.. ownership of ecb82.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMQDF../877dc.. ownership of ea520.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVc4../1f72b.. ownership of 5fe69.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNNP../8add2.. ownership of fd2a6.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMT2Y../03aa5.. ownership of 8deb6.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJCb../6840a.. ownership of 71a7b.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTXK../871cf.. ownership of dbd4e.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMZjB../dc5d9.. ownership of 2e3ac.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTMY../92e43.. ownership of 249a4.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMQcD../a6ab8.. ownership of e6ddb.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUaq../2b4cd.. ownership of 744b2.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRc9../d1d28.. ownership of 0f074.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMYGu../712d6.. ownership of f6e76.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUHx../9236c.. ownership of 3e294.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMakM../87283.. ownership of 5ce17.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
PURE5../af73b.. doc published by PrQUS..

Param SNo^SNo : ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param bbc71.. : ι → ι → ι → ι → ι → ι → ι → ι → ι
Definition 1eb0a.. := λ x0 . ∃ x1 . and (SNo x1) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (∃ x15 . and (SNo x15) (x0 = bbc71.. x1 x3 x5 x7 x9 x11 x13 x15))))))))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem d5242.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 1eb0a.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7)

...

Theorem b501e.. : ∀ x0 . 1eb0a.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 x4 x5 x6 x7 x8 x9 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ x0 = bbc71.. x2 x3 x4 x5 x6 x7 x8 x9 ⟶ x1 (bbc71.. x2 x3 x4 x5 x6 x7 x8 x9)) ⟶ x1 x0

...

Param ordsucc^ordsucc : ι → ι
Definition 3e294.. := bbc71.. 0 1 0 0 0 0 0 0
Definition 0f074.. := bbc71.. 0 0 1 0 0 0 0 0
Definition e6ddb.. := bbc71.. 0 0 0 1 0 0 0 0
Definition 2e3ac.. := bbc71.. 0 0 0 0 1 0 0 0
Definition 71a7b.. := bbc71.. 0 0 0 0 0 1 0 0
Definition fd2a6.. := bbc71.. 0 0 0 0 0 0 1 0
Definition ea520.. := bbc71.. 0 0 0 0 0 0 0 1
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Theorem 9899a.. : 1eb0a.. 3e294..

...

Theorem 630e7.. : 1eb0a.. 0f074..

...

Theorem 77598.. : 1eb0a.. e6ddb..

...

Theorem 429ac.. : 1eb0a.. 2e3ac..

...

Theorem 2dc23.. : 1eb0a.. 71a7b..

...

Theorem 20480.. : 1eb0a.. fd2a6..

...

Theorem 4056c.. : 1eb0a.. ea520..

...