Proofgold Signed Transaction

vin
PrP4d../08007.. PUQLm../0f022..

vout

PrP4d../fed2f.. 0.08 bars
TMJVs../bbbe5.. ownership of 1b51c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMJhB../4d511.. ownership of 5383f.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMRpx../78e38.. ownership of 197a3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMcRt../f6e0d.. ownership of 77dbe.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMFoy../8af8c.. ownership of 3a874.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNox../ba79f.. ownership of d547d.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMMtG../dd0d9.. ownership of 33d05.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMWYY../8c7c9.. ownership of ba273.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMdzw../55c5f.. ownership of 32916.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMW3D../97a56.. ownership of c76ef.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMXgR../f6158.. ownership of 97fb5.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMVMV../c6fc7.. ownership of c7e2b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMKpq../df464.. ownership of fc75b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMS5N../58655.. ownership of 06617.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMPjN../01e98.. ownership of 7a4c7.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMLqB../fda1f.. ownership of d35be.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMLL8../c5ed7.. ownership of 6b13c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNrd../12556.. ownership of 2093d.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMSQH../333eb.. ownership of 3ed59.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMPWP../82c2b.. ownership of db664.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMPpg../64005.. ownership of 467ed.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMFKg../a3c15.. ownership of 09adb.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMJYy../80c7e.. ownership of d7505.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMKQn../5d5bc.. ownership of ba176.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMHi1../a1c0d.. ownership of b5b04.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMdEp../e8eab.. ownership of 898b7.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMVFV../219f7.. ownership of dea20.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMcDX../6ec47.. ownership of 7cc29.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMExT../ee7f7.. ownership of 5878b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMUCj../da549.. ownership of 6dd29.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMVkq../b6e1d.. ownership of 8239a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMSre../251ee.. ownership of 760b9.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMQhj../58faa.. ownership of eabb3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMa5h../25010.. ownership of eaca9.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
PUXbo../a6116.. doc published by PrCmT..

Known df_nfOLD__ax_gen__ax_4__ax_5__df_sb__df_sb_b__ax_6__ax_7__ax_7_b__ax_7_b1__ax_8__ax_8_b__ax_8_b1__ax_9__ax_9_b__ax_9_b1__ax_10__ax_11 : ∀ x0 : ο . ((∀ x1 : ι → ο . wb (wnfOLD x1) (∀ x2 . x1 x2 ⟶ ∀ x3 . x1 x3)) ⟶ (∀ x1 : ι → ο . (∀ x2 . x1 x2) ⟶ ∀ x2 . x1 x2) ⟶ (∀ x1 x2 : ι → ο . (∀ x3 . x1 x3 ⟶ x2 x3) ⟶ (∀ x3 . x1 x3) ⟶ ∀ x3 . x2 x3) ⟶ (∀ x1 : ο . x1 ⟶ ∀ x2 . x1) ⟶ (∀ x1 : ι → ο . ∀ x2 x3 . wb (wsb x1 x2) (wa (wceq (cv x3) (cv x2) ⟶ x1 x3) (wex (λ x4 . wa (wceq (cv x4) (cv x2)) (x1 x4))))) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wsb x1 x2) (wa (wceq (cv x2) (cv x2) ⟶ x1 x2) (wex (λ x3 . wa (wceq (cv x3) (cv x3)) (x1 x3))))) ⟶ (∀ x1 . wn (∀ x2 . wn (wceq (cv x2) (cv x1)))) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x3) ⟶ wceq (cv x2) (cv x3)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x1) ⟶ wceq (cv x2) (cv x1)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x2) ⟶ wceq (cv x2) (cv x2)) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x3) ⟶ wcel (cv x2) (cv x3)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x1) ⟶ wcel (cv x2) (cv x1)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x2) ⟶ wcel (cv x2) (cv x2)) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wcel (cv x3) (cv x1) ⟶ wcel (cv x3) (cv x2)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x1) ⟶ wcel (cv x1) (cv x2)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x2) (cv x1) ⟶ wcel (cv x2) (cv x2)) ⟶ (∀ x1 : ι → ο . wn (∀ x2 . x1 x2) ⟶ ∀ x2 . wn (∀ x3 . x1 x3)) ⟶ (∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3) ⟶ ∀ x2 x3 . x1 x3 x2) ⟶ x0) ⟶ x0
Theorem df_nfOLD : ∀ x0 : ι → ο . wb (wnfOLD x0) (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2) (proof)
Theorem ax_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1) ⟶ ∀ x1 . x0 x1 (proof)
Theorem ax_4 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . x1 x2 (proof)
Theorem ax_5 : ∀ x0 : ο . x0 ⟶ ∀ x1 . x0 (proof)
Theorem df_sb : ∀ x0 : ι → ο . ∀ x1 x2 . wb (wsb x0 x1) (wa (wceq (cv x2) (cv x1) ⟶ x0 x2) (wex (λ x3 . wa (wceq (cv x3) (cv x1)) (x0 x3)))) (proof)
Theorem df_sb_b : ∀ x0 : ι → ο . ∀ x1 . wb (wsb x0 x1) (wa (wceq (cv x1) (cv x1) ⟶ x0 x1) (wex (λ x2 . wa (wceq (cv x2) (cv x2)) (x0 x2)))) (proof)
Theorem ax_9d2 : ∀ x0 . wn (∀ x1 . wn (wceq (cv x1) (cv x0))) (proof)
Theorem ax_8d : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x2) ⟶ wceq (cv x1) (cv x2) (proof)
Theorem ax_7_b : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x0) ⟶ wceq (cv x1) (cv x0) (proof)
Theorem ax_7_b1 : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x1) ⟶ wceq (cv x1) (cv x1) (proof)
Theorem ax_8 : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x2) ⟶ wcel (cv x1) (cv x2) (proof)
Theorem ax_8_b : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x0) ⟶ wcel (cv x1) (cv x0) (proof)
Theorem ax_8_b1 : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x1) ⟶ wcel (cv x1) (cv x1) (proof)
Theorem ax_9 : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wcel (cv x2) (cv x0) ⟶ wcel (cv x2) (cv x1) (proof)
Theorem ax_9_b : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x0) ⟶ wcel (cv x0) (cv x1) (proof)
Theorem ax_9_b1 : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x1) (cv x0) ⟶ wcel (cv x1) (cv x1) (proof)
Theorem ax_10 : ∀ x0 : ι → ο . wn (∀ x1 . x0 x1) ⟶ ∀ x1 . wn (∀ x2 . x0 x2) (proof)
Theorem ax_wl_11v : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2) ⟶ ∀ x1 x2 . x0 x2 x1 (proof)