Proofgold Signed Transaction

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

vout

PrNHZ../e116b.. 63.99 bars
TMVcV../1972d.. ownership of 4056c.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMa2L../fbc7e.. ownership of 4a8f2.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMVgF../41bd4.. ownership of 20480.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHnM../9d53f.. ownership of 9bf31.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdYa../14764.. ownership of 2dc23.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKRW../93704.. ownership of 3900d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMU3q../b1071.. ownership of 429ac.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMawo../7ebae.. ownership of 98564.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMSxp../f4867.. ownership of 77598.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdkx../dc226.. ownership of 905c4.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHPe../35048.. ownership of 630e7.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMLhY../712d8.. ownership of 14338.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPrt../72cf8.. ownership of 9899a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZzD../0a426.. ownership of 99500.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMEyh../7293e.. ownership of b501e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWhN../c067c.. ownership of 16cc7.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHRB../a8854.. ownership of d5242.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMGMf../39bc7.. ownership of ecb82.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQDF../877dc.. ownership of ea520.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMVc4../1f72b.. ownership of 5fe69.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNNP../8add2.. ownership of fd2a6.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMT2Y../03aa5.. ownership of 8deb6.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJCb../6840a.. ownership of 71a7b.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTXK../871cf.. ownership of dbd4e.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZjB../dc5d9.. ownership of 2e3ac.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTMY../92e43.. ownership of 249a4.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQcD../a6ab8.. ownership of e6ddb.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUaq../2b4cd.. ownership of 744b2.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRc9../d1d28.. ownership of 0f074.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMYGu../712d6.. ownership of f6e76.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUHx../9236c.. ownership of 3e294.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMakM../87283.. ownership of 5ce17.. as obj with payaddr PrQUS.. rightscost 0.00 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 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (∀ x15 : ο . (∀ x16 . and (SNo x16) (x0 = bbc71.. x2 x4 x6 x8 x10 x12 x14 x16) ⟶ x15) ⟶ x15) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
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) (proof)
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 (proof)
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.. (proof)
Theorem 630e7.. : 1eb0a.. 0f074.. (proof)
Theorem 77598.. : 1eb0a.. e6ddb.. (proof)
Theorem 429ac.. : 1eb0a.. 2e3ac.. (proof)
Theorem 2dc23.. : 1eb0a.. 71a7b.. (proof)
Theorem 20480.. : 1eb0a.. fd2a6.. (proof)
Theorem 4056c.. : 1eb0a.. ea520.. (proof)