Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr3ht../aa779..
PUN89../e3f65..
vout
Pr3ht../01d76.. 0.10 bars
TMbhi../5e514.. ownership of ba65a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMXd5../0f702.. ownership of cb99c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNZs../77686.. ownership of 7226f.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMW7V../b3aff.. ownership of e1fb3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMRz9../25d5b.. ownership of 0bf6a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMKn7../8dee4.. ownership of daccb.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMYZw../6d59e.. ownership of f4a0f.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMThu../6170f.. ownership of 3e7d9.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMG3n../8949b.. ownership of 93093.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMWjb../d2b5f.. ownership of 3e1da.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMTRD../2be72.. ownership of 548dc.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNAV../e205d.. ownership of ce82a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMLSt../861b0.. ownership of a4882.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMbnr../0d276.. ownership of a599e.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMY2D../b22c9.. ownership of b7718.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMZgx../b164d.. ownership of 26bb8.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMTkK../2c1bf.. ownership of 47dd3.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMWKh../cd824.. ownership of 8b5c1.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMKzQ../0d93f.. ownership of d6fdb.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMajx../e3c7b.. ownership of 5497c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMYgb../87fcc.. ownership of 969d1.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMMMf../11ae5.. ownership of 63b3d.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMQUv../34c1e.. ownership of d8fab.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMGa3../64c7b.. ownership of 80549.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNny../20bc5.. ownership of ddf1b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMQg3../61500.. ownership of aa4e0.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMUeo../0998b.. ownership of d1ee7.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMaRM../2e035.. ownership of 2bfcd.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMbiL../60ad7.. ownership of 64848.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMNqA../fc7e3.. ownership of 43d3b.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMbk8../a6bf9.. ownership of 68f57.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMZcD../978d2.. ownership of 2cfcf.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMbwZ../32180.. ownership of 8e4eb.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMc7F../7fd5a.. ownership of 02d3a.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMMPg../8f3a5.. ownership of 170ea.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
TMcby../a7744.. ownership of 97e4c.. as prop with payaddr PrCmT.. rightscost 0.00 controlledby PrCmT.. upto 0
PUNQ5../878d5.. doc published by PrCmT..
Known df_trg__df_tdrg__df_tlm__df_tvc__df_ust__df_utop__df_uss__df_usp__df_tus__df_ucn__df_cfilu__df_cusp__df_xms__df_ms__df_tms__df_nm__df_ngp__df_tng : ∀ x0 : ο . (wceq ctrg (crab (λ x1 . wcel (cfv (cv x1) cmgp) ctmd) (λ x1 . cin ctgp crg)) ⟶ wceq ctdrg (crab (λ x1 . wcel (co (cfv (cv x1) cmgp) (cfv (cv x1) cui) cress) ctgp) (λ x1 . cin ctrg cdr)) ⟶ wceq ctlm (crab (λ x1 . wa (wcel (cfv (cv x1) csca) ctrg) (wcel (cfv (cv x1) cscaf) (co (co (cfv (cfv (cv x1) csca) ctopn) (cfv (cv x1) ctopn) ctx) (cfv (cv x1) ctopn) ccn))) (λ x1 . cin ctmd clmod)) ⟶ wceq ctvc (crab (λ x1 . wcel (cfv (cv x1) csca) ctdrg) (λ x1 . ctlm)) ⟶ wceq cust (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . w3a (wss (cv x2) (cpw (cxp (cv x1) (cv x1)))) (wcel (cxp (cv x1) (cv x1)) (cv x2)) (wral (λ x3 . w3a (wral (λ x4 . wss (cv x3) (cv x4) ⟶ wcel (cv x4) (cv x2)) (λ x4 . cpw (cxp (cv x1) (cv x1)))) (wral (λ x4 . wcel (cin (cv x3) (cv x4)) (cv x2)) (λ x4 . cv x2)) (w3a (wss (cres cid (cv x1)) (cv x3)) (wcel (ccnv (cv x3)) (cv x2)) (wrex (λ x4 . wss (ccom (cv x4) (cv x4)) (cv x3)) (λ x4 . cv x2)))) (λ x3 . cv x2))))) ⟶ wceq cutop (cmpt (λ x1 . cuni (crn cust)) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cima (cv x4) (csn (cv x3))) (cv x2)) (λ x4 . cv x1)) (λ x3 . cv x2)) (λ x2 . cpw (cdm (cuni (cv x1)))))) ⟶ wceq cuss (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cunif) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) crest)) ⟶ wceq cusp (cab (λ x1 . wa (wcel (cfv (cv x1) cuss) (cfv (cfv (cv x1) cbs) cust)) (wceq (cfv (cv x1) ctopn) (cfv (cfv (cv x1) cuss) cutop)))) ⟶ wceq ctus (cmpt (λ x1 . cuni (crn cust)) (λ x1 . co (cpr (cop (cfv cnx cbs) (cdm (cuni (cv x1)))) (cop (cfv cnx cunif) (cv x1))) (cop (cfv cnx cts) (cfv (cv x1) cutop)) csts)) ⟶ wceq cucn (cmpt2 (λ x1 x2 . cuni (crn cust)) (λ x1 x2 . cuni (crn cust)) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wbr (cv x6) (cv x7) (cv x5) ⟶ wbr (cfv (cv x6) (cv x3)) (cfv (cv x7) (cv x3)) (cv x4)) (λ x7 . cdm (cuni (cv x1)))) (λ x6 . cdm (cuni (cv x1)))) (λ x5 . cv x1)) (λ x4 . cv x2)) (λ x3 . co (cdm (cuni (cv x2))) (cdm (cuni (cv x1))) cmap))) ⟶ wceq ccfilu (cmpt (λ x1 . cuni (crn cust)) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cxp (cv x4) (cv x4)) (cv x3)) (λ x4 . cv x2)) (λ x3 . cv x1)) (λ x2 . cfv (cdm (cuni (cv x1))) cfbas))) ⟶ wceq ccusp (crab (λ x1 . wral (λ x2 . wcel (cv x2) (cfv (cfv (cv x1) cuss) ccfilu) ⟶ wne (co (cfv (cv x1) ctopn) (cv x2) cflim) c0) (λ x2 . cfv (cfv (cv x1) cbs) cfil)) (λ x1 . cusp)) ⟶ wceq cxme (crab (λ x1 . wceq (cfv (cv x1) ctopn) (cfv (cres (cfv (cv x1) cds) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs))) cmopn)) (λ x1 . ctps)) ⟶ wceq cmt (crab (λ x1 . wcel (cres (cfv (cv x1) cds) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs))) (cfv (cfv (cv x1) cbs) cme)) (λ x1 . cxme)) ⟶ wceq ctmt (cmpt (λ x1 . cuni (crn cxmt)) (λ x1 . co (cpr (cop (cfv cnx cbs) (cdm (cdm (cv x1)))) (cop (cfv cnx cds) (cv x1))) (cop (cfv cnx cts) (cfv (cv x1) cmopn)) csts)) ⟶ wceq cnm (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . co (cv x2) (cfv (cv x1) c0g) (cfv (cv x1) cds)))) ⟶ wceq cngp (crab (λ x1 . wss (ccom (cfv (cv x1) cnm) (cfv (cv x1) csg)) (cfv (cv x1) cds)) (λ x1 . cin cgrp cmt)) ⟶ wceq ctng (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x1) (cop (cfv cnx cds) (ccom (cv x2) (cfv (cv x1) csg))) csts) (cop (cfv cnx cts) (cfv (ccom (cv x2) (cfv (cv x1) csg)) cmopn)) csts)) ⟶ x0) ⟶ x0
Theorem df_trg : wceq ctrg (crab (λ x0 . wcel (cfv (cv x0) cmgp) ctmd) (λ x0 . cin ctgp crg)) (proof)
Theorem df_tdrg : wceq ctdrg (crab (λ x0 . wcel (co (cfv (cv x0) cmgp) (cfv (cv x0) cui) cress) ctgp) (λ x0 . cin ctrg cdr)) (proof)
Theorem df_tlm : wceq ctlm (crab (λ x0 . wa (wcel (cfv (cv x0) csca) ctrg) (wcel (cfv (cv x0) cscaf) (co (co (cfv (cfv (cv x0) csca) ctopn) (cfv (cv x0) ctopn) ctx) (cfv (cv x0) ctopn) ccn))) (λ x0 . cin ctmd clmod)) (proof)
Theorem df_tvc : wceq ctvc (crab (λ x0 . wcel (cfv (cv x0) csca) ctdrg) (λ x0 . ctlm)) (proof)
Theorem df_ust : wceq cust (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . w3a (wss (cv x1) (cpw (cxp (cv x0) (cv x0)))) (wcel (cxp (cv x0) (cv x0)) (cv x1)) (wral (λ x2 . w3a (wral (λ x3 . wss (cv x2) (cv x3) ⟶ wcel (cv x3) (cv x1)) (λ x3 . cpw (cxp (cv x0) (cv x0)))) (wral (λ x3 . wcel (cin (cv x2) (cv x3)) (cv x1)) (λ x3 . cv x1)) (w3a (wss (cres cid (cv x0)) (cv x2)) (wcel (ccnv (cv x2)) (cv x1)) (wrex (λ x3 . wss (ccom (cv x3) (cv x3)) (cv x2)) (λ x3 . cv x1)))) (λ x2 . cv x1))))) (proof)
Theorem df_utop : wceq cutop (cmpt (λ x0 . cuni (crn cust)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cima (cv x3) (csn (cv x2))) (cv x1)) (λ x3 . cv x0)) (λ x2 . cv x1)) (λ x1 . cpw (cdm (cuni (cv x0)))))) (proof)
Theorem df_uss : wceq cuss (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cunif) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)) crest)) (proof)
Theorem df_usp : wceq cusp (cab (λ x0 . wa (wcel (cfv (cv x0) cuss) (cfv (cfv (cv x0) cbs) cust)) (wceq (cfv (cv x0) ctopn) (cfv (cfv (cv x0) cuss) cutop)))) (proof)
Theorem df_tus : wceq ctus (cmpt (λ x0 . cuni (crn cust)) (λ x0 . co (cpr (cop (cfv cnx cbs) (cdm (cuni (cv x0)))) (cop (cfv cnx cunif) (cv x0))) (cop (cfv cnx cts) (cfv (cv x0) cutop)) csts)) (proof)
Theorem df_ucn : wceq cucn (cmpt2 (λ x0 x1 . cuni (crn cust)) (λ x0 x1 . cuni (crn cust)) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wral (λ x5 . wral (λ x6 . wbr (cv x5) (cv x6) (cv x4) ⟶ wbr (cfv (cv x5) (cv x2)) (cfv (cv x6) (cv x2)) (cv x3)) (λ x6 . cdm (cuni (cv x0)))) (λ x5 . cdm (cuni (cv x0)))) (λ x4 . cv x0)) (λ x3 . cv x1)) (λ x2 . co (cdm (cuni (cv x1))) (cdm (cuni (cv x0))) cmap))) (proof)
Theorem df_cfilu : wceq ccfilu (cmpt (λ x0 . cuni (crn cust)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cxp (cv x3) (cv x3)) (cv x2)) (λ x3 . cv x1)) (λ x2 . cv x0)) (λ x1 . cfv (cdm (cuni (cv x0))) cfbas))) (proof)
Theorem df_cusp : wceq ccusp (crab (λ x0 . wral (λ x1 . wcel (cv x1) (cfv (cfv (cv x0) cuss) ccfilu) ⟶ wne (co (cfv (cv x0) ctopn) (cv x1) cflim) c0) (λ x1 . cfv (cfv (cv x0) cbs) cfil)) (λ x0 . cusp)) (proof)
Theorem df_xms : wceq cxme (crab (λ x0 . wceq (cfv (cv x0) ctopn) (cfv (cres (cfv (cv x0) cds) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs))) cmopn)) (λ x0 . ctps)) (proof)
Theorem df_ms : wceq cmt (crab (λ x0 . wcel (cres (cfv (cv x0) cds) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs))) (cfv (cfv (cv x0) cbs) cme)) (λ x0 . cxme)) (proof)
Theorem df_tms : wceq ctmt (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . co (cpr (cop (cfv cnx cbs) (cdm (cdm (cv x0)))) (cop (cfv cnx cds) (cv x0))) (cop (cfv cnx cts) (cfv (cv x0) cmopn)) csts)) (proof)
Theorem df_nm : wceq cnm (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . co (cv x1) (cfv (cv x0) c0g) (cfv (cv x0) cds)))) (proof)
Theorem df_ngp : wceq cngp (crab (λ x0 . wss (ccom (cfv (cv x0) cnm) (cfv (cv x0) csg)) (cfv (cv x0) cds)) (λ x0 . cin cgrp cmt)) (proof)
Theorem df_tng : wceq ctng (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cop (cfv cnx cds) (ccom (cv x1) (cfv (cv x0) csg))) csts) (cop (cfv cnx cts) (cfv (ccom (cv x1) (cfv (cv x0) csg)) cmopn)) csts)) (proof)