Proofgold Signed Transaction

vin
PrEde../0c8e9.. PUP2f../01dd9..

vout

PrEde../c0429.. 25.00 bars
TMb7y../486b6.. negprop ownership controlledby Pr8qe.. upto 0
TMPcE../0b79f.. negprop ownership controlledby Pr8qe.. upto 0
TMLSG../59b72.. ownership of fec13.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMaVX../eeab1.. ownership of 64604.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMJsX../3a242.. ownership of d8b2d.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMLSd../997e0.. ownership of a8010.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMNbt../23d5d.. ownership of 98f3c.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMHRZ../be796.. ownership of d480a.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMP7W../c1113.. ownership of 36a56.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMFCy../18fd6.. ownership of da298.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMYJc../914bb.. ownership of c93f5.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMRss../2c1e6.. ownership of e2a83.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMYXQ../f5f19.. ownership of b169a.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
TMbVK../a2f4f.. ownership of f5e61.. as prop with payaddr Pr8qe.. rights free controlledby Pr8qe.. upto 0
PUgya../c21b4.. doc published by Pr8qe..

Known False_def^False_def : False = ∀ x1 : ο . x1
Known True_def^True_def : True = ∀ x1 : ο . x1 ⟶ x1
Known not_def^not_def : not = λ x1 : ο . x1 ⟶ False
Known and_def^and_def : and = λ x1 x2 : ο . ∀ x3 : ο . (x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem FalseE^FalseE : False ⟶ ∀ x0 : ο . x0 (proof)
Theorem TrueI^TrueI : True (proof)
Theorem notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False (proof)
Theorem andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2 (proof)
Theorem and_notTrue : ∀ x0 : ο . and x0 (not True) ⟶ ∀ x1 : ο . x1 (proof)
Theorem first_bounty_thm : (∀ x0 : ι → ο . ∀ x1 : ι → ι . and ((x0 (x1 (binintersect (x1 (Power 0)) (x1 (binrep (Power (Power (Power 0))) 0)))) ⟶ TransSet (x1 0) ⟶ ∀ x2 . In x2 0 ⟶ ∀ x3 : ο . (∀ x4 . and (Subq x4 x2) (exactly2 (ordsucc (x1 x4))) ⟶ x3) ⟶ x3) ⟶ ∀ x2 : ο . (∀ x3 . and (∀ x4 : ο . (∀ x5 . and (Subq x5 x3) (x3 = x1 x3 ⟶ ∀ x6 : ο . (∀ x7 . and (Subq x7 x3) (not (x0 (setprod x5 (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0)))))) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) (not (SNo x3)) ⟶ x2) ⟶ x2) (not (x0 (x1 (x1 (x1 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0))))))) ⟶ ∀ x0 : ο . x0 (proof)