Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrMSx../d8eb5..
PUN9b../3de95..
vout
PrMSx../0e15b.. 0.10 bars
TMV81../20e10.. ownership of 83f09.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMKH8../93880.. ownership of 8fba3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMEmb../6f3c1.. ownership of 39054.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMaXR../548de.. ownership of bbfa6.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMdaB../fed92.. ownership of c759b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMWt1../4d937.. ownership of 341a3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMSHr../4868a.. ownership of 6c53b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMWuC../c16b4.. ownership of 406e3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMKd6../98595.. ownership of e9dc9.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMFk9../a4c66.. ownership of 7812e.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMaAC../f4186.. ownership of 0d2a7.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMRhf../9e2bb.. ownership of 040c5.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMM2K../6401e.. ownership of 1b37e.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMYDi../927c5.. ownership of b922a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMZtG../c0b48.. ownership of 6ec07.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMU8G../c2213.. ownership of 53a24.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMF4u../5439e.. ownership of 62e18.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMHE1../3d9d6.. ownership of 30976.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMYFf../91375.. ownership of a7942.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMEzD../891e0.. ownership of 85425.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMGzo../8ab26.. ownership of 23cf0.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMZ3b../91d1c.. ownership of 818d2.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMahk../a1617.. ownership of dec58.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMYXh../1da0b.. ownership of a69d6.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMcjC../6263b.. ownership of fc27c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMVaE../201e7.. ownership of f446c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMRJ5../f42aa.. ownership of 4edb8.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMZZb../bb640.. ownership of ca40f.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMRLc../8b442.. ownership of ed56a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMWnf../06cc8.. ownership of fc411.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMFkD../224e2.. ownership of f211f.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMRyb../19d1f.. ownership of b67a2.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMd1H../ee75d.. ownership of 787b4.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNFN../50378.. ownership of 64751.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNsR../81530.. ownership of d3af4.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMbMM../eaa6d.. ownership of e3127.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
PUKaw../9f5bb.. doc published by PrCmT..
Known df_cart__df_img__df_domain__df_range__df_cup__df_cap__df_restrict__df_succf__df_apply__df_funpart__df_fullfun__df_ub__df_lb__df_altop__df_altxp__df_ofs__df_transport__df_colinear : ∀ x0 : ο . (wceq ccart (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cpprod cep cep) cvv)))) ⟶ wceq cimg (ccom (cimage (cres (ccom c2nd c1st) (cres c1st (cxp cvv cvv)))) ccart) ⟶ wceq cdomain (cimage (cres c1st (cxp cvv cvv))) ⟶ wceq crange (cimage (cres c2nd (cxp cvv cvv))) ⟶ wceq ccup (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cun (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) ⟶ wceq ccap (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cin (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) ⟶ wceq crestrict (ccom ccap (ctxp c1st (ccom ccart (ctxp c2nd (ccom crange c1st))))) ⟶ wceq csuccf (ccom ccup (ctxp cid csingle)) ⟶ wceq capply (ccom (ccom cbigcup cbigcup) (ccom (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cres cep csingles) cvv)))) (ccom (ccom csingle cimg) (cpprod cid csingle)))) ⟶ (∀ x1 : ι → ο . wceq (cfunpart x1) (cres x1 (cdm (cin (ccom (cimage x1) csingle) (cxp cvv csingles))))) ⟶ (∀ x1 : ι → ο . wceq (cfullfn x1) (cun (cfunpart x1) (cxp (cdif cvv (cdm (cfunpart x1))) (csn c0)))) ⟶ (∀ x1 : ι → ο . wceq (cub x1) (cdif (cxp cvv cvv) (ccom (cdif cvv x1) (ccnv cep)))) ⟶ (∀ x1 : ι → ο . wceq (clb x1) (cub (ccnv x1))) ⟶ (∀ x1 x2 : ι → ο . wceq (caltop x1 x2) (cpr (csn x1) (cpr x1 (csn x2)))) ⟶ (∀ x1 x2 : ι → ο . wceq (caltxp x1 x2) (cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (caltop (cv x4) (cv x5))) (λ x5 . x2)) (λ x4 . x1)))) ⟶ wceq cofs (copab (λ x1 x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . w3a (wceq (cv x1) (cop (cop (cv x4) (cv x5)) (cop (cv x6) (cv x7)))) (wceq (cv x2) (cop (cop (cv x8) (cv x9)) (cop (cv x10) (cv x11)))) (w3a (wa (wbr (cv x5) (cop (cv x4) (cv x6)) cbtwn) (wbr (cv x9) (cop (cv x8) (cv x10)) cbtwn)) (wa (wbr (cop (cv x4) (cv x5)) (cop (cv x8) (cv x9)) ccgr) (wbr (cop (cv x5) (cv x6)) (cop (cv x9) (cv x10)) ccgr)) (wa (wbr (cop (cv x4) (cv x7)) (cop (cv x8) (cv x11)) ccgr) (wbr (cop (cv x5) (cv x7)) (cop (cv x9) (cv x11)) ccgr)))) (λ x11 . cfv (cv x3) cee)) (λ x10 . cfv (cv x3) cee)) (λ x9 . cfv (cv x3) cee)) (λ x8 . cfv (cv x3) cee)) (λ x7 . cfv (cv x3) cee)) (λ x6 . cfv (cv x3) cee)) (λ x5 . cfv (cv x3) cee)) (λ x4 . cfv (cv x3) cee)) (λ x3 . cn))) ⟶ wceq ctransport (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x1) (cxp (cfv (cv x4) cee) (cfv (cv x4) cee))) (wcel (cv x2) (cxp (cfv (cv x4) cee) (cfv (cv x4) cee))) (wne (cfv (cv x2) c1st) (cfv (cv x2) c2nd))) (wceq (cv x3) (crio (λ x5 . wa (wbr (cfv (cv x2) c2nd) (cop (cfv (cv x2) c1st) (cv x5)) cbtwn) (wbr (cop (cfv (cv x2) c2nd) (cv x5)) (cv x1) ccgr)) (λ x5 . cfv (cv x4) cee)))) (λ x4 . cn))) ⟶ wceq ccolin (ccnv (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x3) (cfv (cv x4) cee)) (wcel (cv x1) (cfv (cv x4) cee)) (wcel (cv x2) (cfv (cv x4) cee))) (w3o (wbr (cv x3) (cop (cv x1) (cv x2)) cbtwn) (wbr (cv x1) (cop (cv x2) (cv x3)) cbtwn) (wbr (cv x2) (cop (cv x3) (cv x1)) cbtwn))) (λ x4 . cn)))) ⟶ x0) ⟶ x0
Theorem df_cart : wceq ccart (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cpprod cep cep) cvv)))) (proof)
Theorem df_img : wceq cimg (ccom (cimage (cres (ccom c2nd c1st) (cres c1st (cxp cvv cvv)))) ccart) (proof)
Theorem df_domain : wceq cdomain (cimage (cres c1st (cxp cvv cvv))) (proof)
Theorem df_range : wceq crange (cimage (cres c2nd (cxp cvv cvv))) (proof)
Theorem df_cup : wceq ccup (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cun (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) (proof)
Theorem df_cap : wceq ccap (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cin (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) (proof)
Theorem df_restrict : wceq crestrict (ccom ccap (ctxp c1st (ccom ccart (ctxp c2nd (ccom crange c1st))))) (proof)
Theorem df_succf : wceq csuccf (ccom ccup (ctxp cid csingle)) (proof)
Theorem df_apply : wceq capply (ccom (ccom cbigcup cbigcup) (ccom (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cres cep csingles) cvv)))) (ccom (ccom csingle cimg) (cpprod cid csingle)))) (proof)
Theorem df_funpart : ∀ x0 : ι → ο . wceq (cfunpart x0) (cres x0 (cdm (cin (ccom (cimage x0) csingle) (cxp cvv csingles)))) (proof)
Theorem df_fullfun : ∀ x0 : ι → ο . wceq (cfullfn x0) (cun (cfunpart x0) (cxp (cdif cvv (cdm (cfunpart x0))) (csn c0))) (proof)
Theorem df_ub : ∀ x0 : ι → ο . wceq (cub x0) (cdif (cxp cvv cvv) (ccom (cdif cvv x0) (ccnv cep))) (proof)
Theorem df_lb : ∀ x0 : ι → ο . wceq (clb x0) (cub (ccnv x0)) (proof)
Theorem df_altop : ∀ x0 x1 : ι → ο . wceq (caltop x0 x1) (cpr (csn x0) (cpr x0 (csn x1))) (proof)
Theorem df_altxp : ∀ x0 x1 : ι → ο . wceq (caltxp x0 x1) (cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (caltop (cv x3) (cv x4))) (λ x4 . x1)) (λ x3 . x0))) (proof)
Theorem df_ofs : wceq cofs (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . w3a (wceq (cv x0) (cop (cop (cv x3) (cv x4)) (cop (cv x5) (cv x6)))) (wceq (cv x1) (cop (cop (cv x7) (cv x8)) (cop (cv x9) (cv x10)))) (w3a (wa (wbr (cv x4) (cop (cv x3) (cv x5)) cbtwn) (wbr (cv x8) (cop (cv x7) (cv x9)) cbtwn)) (wa (wbr (cop (cv x3) (cv x4)) (cop (cv x7) (cv x8)) ccgr) (wbr (cop (cv x4) (cv x5)) (cop (cv x8) (cv x9)) ccgr)) (wa (wbr (cop (cv x3) (cv x6)) (cop (cv x7) (cv x10)) ccgr) (wbr (cop (cv x4) (cv x6)) (cop (cv x8) (cv x10)) ccgr)))) (λ x10 . cfv (cv x2) cee)) (λ x9 . cfv (cv x2) cee)) (λ x8 . cfv (cv x2) cee)) (λ x7 . cfv (cv x2) cee)) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))) (proof)
Theorem df_transport : wceq ctransport (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x0) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee))) (wcel (cv x1) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee))) (wne (cfv (cv x1) c1st) (cfv (cv x1) c2nd))) (wceq (cv x2) (crio (λ x4 . wa (wbr (cfv (cv x1) c2nd) (cop (cfv (cv x1) c1st) (cv x4)) cbtwn) (wbr (cop (cfv (cv x1) c2nd) (cv x4)) (cv x0) ccgr)) (λ x4 . cfv (cv x3) cee)))) (λ x3 . cn))) (proof)
Theorem df_colinear : wceq ccolin (ccnv (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x2) (cfv (cv x3) cee)) (wcel (cv x0) (cfv (cv x3) cee)) (wcel (cv x1) (cfv (cv x3) cee))) (w3o (wbr (cv x2) (cop (cv x0) (cv x1)) cbtwn) (wbr (cv x0) (cop (cv x1) (cv x2)) cbtwn) (wbr (cv x1) (cop (cv x2) (cv x0)) cbtwn))) (λ x3 . cn)))) (proof)