Search for blocks/addresses/...

Proofgold Asset

asset id
5c8bbdcf809eacea18d1896712a9a99cc8f72bcb79f828bbffbcd22e92f1a68f
asset hash
b54885cd481e65848c2de588ea6fc595fbbff809fda8cc91062f77b4dd37518e
bday / block
36387
tx
d4238..
preasset
doc published by PrCmT..
Known df_conngr__df_eupth__df_frgr__df_plig__df_grpo__df_gid__df_ginv__df_gdiv__df_ablo__df_vc__df_nv__df_va__df_ba__df_sm__df_0v__df_vs__df_nmcv__df_ims : ∀ x0 : ο . (wceq cconngr (cab (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wex (λ x5 . wex (λ x6 . wbr (cv x5) (cv x6) (co (cv x3) (cv x4) (cfv (cv x1) cpthson))))) (λ x4 . cv x2)) (λ x3 . cv x2)) (cfv (cv x1) cvtx)))wceq ceupth (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wbr (cv x2) (cv x3) (cfv (cv x1) ctrls)) (wfo (co cc0 (cfv (cv x2) chash) cfzo) (cdm (cfv (cv x1) ciedg)) (cv x2)))))wceq cfrgr (cab (λ x1 . wa (wcel (cv x1) cusgr) (wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wreu (λ x6 . wss (cpr (cpr (cv x6) (cv x4)) (cpr (cv x6) (cv x5))) (cv x3)) (λ x6 . cv x2)) (λ x5 . cdif (cv x2) (csn (cv x4)))) (λ x4 . cv x2)) (cfv (cv x1) cedg)) (cfv (cv x1) cvtx))))wceq cplig (cab (λ x1 . w3a (wral (λ x2 . wral (λ x3 . wne (cv x2) (cv x3)wreu (λ x4 . wa (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x4))) (λ x4 . cv x1)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (wral (λ x2 . wrex (λ x3 . wrex (λ x4 . w3a (wne (cv x3) (cv x4)) (wcel (cv x3) (cv x2)) (wcel (cv x4) (cv x2))) (λ x4 . cuni (cv x1))) (λ x3 . cuni (cv x1))) (λ x2 . cv x1)) (wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wral (λ x5 . wn (w3a (wcel (cv x2) (cv x5)) (wcel (cv x3) (cv x5)) (wcel (cv x4) (cv x5)))) (λ x5 . cv x1)) (λ x4 . cuni (cv x1))) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1)))))wceq cgr (cab (λ x1 . wex (λ x2 . w3a (wf (cxp (cv x2) (cv x2)) (cv x2) (cv x1)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (co (cv x3) (cv x4) (cv x1)) (cv x5) (cv x1)) (co (cv x3) (co (cv x4) (cv x5) (cv x1)) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2)) (wrex (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cv x1)) (cv x4)) (wrex (λ x5 . wceq (co (cv x5) (cv x4) (cv x1)) (cv x3)) (λ x5 . cv x2))) (λ x4 . cv x2)) (λ x3 . cv x2)))))wceq cgi (cmpt (λ x1 . cvv) (λ x1 . crio (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x1)) (cv x3)) (wceq (co (cv x3) (cv x2) (cv x1)) (cv x3))) (λ x3 . crn (cv x1))) (λ x2 . crn (cv x1))))wceq cgn (cmpt (λ x1 . cgr) (λ x1 . cmpt (λ x2 . crn (cv x1)) (λ x2 . crio (λ x3 . wceq (co (cv x3) (cv x2) (cv x1)) (cfv (cv x1) cgi)) (λ x3 . crn (cv x1)))))wceq cgs (cmpt (λ x1 . cgr) (λ x1 . cmpt2 (λ x2 x3 . crn (cv x1)) (λ x2 x3 . crn (cv x1)) (λ x2 x3 . co (cv x2) (cfv (cv x3) (cfv (cv x1) cgn)) (cv x1))))wceq cablo (crab (λ x1 . wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cv x1)) (co (cv x3) (cv x2) (cv x1))) (λ x3 . crn (cv x1))) (λ x2 . crn (cv x1))) (λ x1 . cgr))wceq cvc (copab (λ x1 x2 . w3a (wcel (cv x1) cablo) (wf (cxp cc (crn (cv x1))) (crn (cv x1)) (cv x2)) (wral (λ x3 . wa (wceq (co c1 (cv x3) (cv x2)) (cv x3)) (wral (λ x4 . wa (wral (λ x5 . wceq (co (cv x4) (co (cv x3) (cv x5) (cv x1)) (cv x2)) (co (co (cv x4) (cv x3) (cv x2)) (co (cv x4) (cv x5) (cv x2)) (cv x1))) (λ x5 . crn (cv x1))) (wral (λ x5 . wa (wceq (co (co (cv x4) (cv x5) caddc) (cv x3) (cv x2)) (co (co (cv x4) (cv x3) (cv x2)) (co (cv x5) (cv x3) (cv x2)) (cv x1))) (wceq (co (co (cv x4) (cv x5) cmul) (cv x3) (cv x2)) (co (cv x4) (co (cv x5) (cv x3) (cv x2)) (cv x2)))) (λ x5 . cc))) (λ x4 . cc))) (λ x3 . crn (cv x1)))))wceq cnv (coprab (λ x1 x2 x3 . w3a (wcel (cop (cv x1) (cv x2)) cvc) (wf (crn (cv x1)) cr (cv x3)) (wral (λ x4 . w3a (wceq (cfv (cv x4) (cv x3)) cc0wceq (cv x4) (cfv (cv x1) cgi)) (wral (λ x5 . wceq (cfv (co (cv x5) (cv x4) (cv x2)) (cv x3)) (co (cfv (cv x5) cabs) (cfv (cv x4) (cv x3)) cmul)) (λ x5 . cc)) (wral (λ x5 . wbr (cfv (co (cv x4) (cv x5) (cv x1)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) caddc) cle) (λ x5 . crn (cv x1)))) (λ x4 . crn (cv x1)))))wceq cpv (ccom c1st c1st)wceq cba (cmpt (λ x1 . cvv) (λ x1 . crn (cfv (cv x1) cpv)))wceq cns (ccom c2nd c1st)wceq cn0v (ccom cgi cpv)wceq cnsb (ccom cgs cpv)wceq cnmcv c2ndwceq cims (cmpt (λ x1 . cnv) (λ x1 . ccom (cfv (cv x1) cnmcv) (cfv (cv x1) cnsb)))x0)x0
Theorem df_conngr : wceq cconngr (cab (λ x0 . wsbc (λ x1 . wral (λ x2 . wral (λ x3 . wex (λ x4 . wex (λ x5 . wbr (cv x4) (cv x5) (co (cv x2) (cv x3) (cfv (cv x0) cpthson))))) (λ x3 . cv x1)) (λ x2 . cv x1)) (cfv (cv x0) cvtx))) (proof)
Theorem df_eupth : wceq ceupth (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wbr (cv x1) (cv x2) (cfv (cv x0) ctrls)) (wfo (co cc0 (cfv (cv x1) chash) cfzo) (cdm (cfv (cv x0) ciedg)) (cv x1))))) (proof)
Theorem df_frgr : wceq cfrgr (cab (λ x0 . wa (wcel (cv x0) cusgr) (wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wreu (λ x5 . wss (cpr (cpr (cv x5) (cv x3)) (cpr (cv x5) (cv x4))) (cv x2)) (λ x5 . cv x1)) (λ x4 . cdif (cv x1) (csn (cv x3)))) (λ x3 . cv x1)) (cfv (cv x0) cedg)) (cfv (cv x0) cvtx)))) (proof)
Theorem df_plig : wceq cplig (cab (λ x0 . w3a (wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2)wreu (λ x3 . wa (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x3))) (λ x3 . cv x0)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (wral (λ x1 . wrex (λ x2 . wrex (λ x3 . w3a (wne (cv x2) (cv x3)) (wcel (cv x2) (cv x1)) (wcel (cv x3) (cv x1))) (λ x3 . cuni (cv x0))) (λ x2 . cuni (cv x0))) (λ x1 . cv x0)) (wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wn (w3a (wcel (cv x1) (cv x4)) (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x4)))) (λ x4 . cv x0)) (λ x3 . cuni (cv x0))) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))))) (proof)
Theorem df_grpo : wceq cgr (cab (λ x0 . wex (λ x1 . w3a (wf (cxp (cv x1) (cv x1)) (cv x1) (cv x0)) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x0)) (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x0))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)) (wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x0)) (cv x3)) (wrex (λ x4 . wceq (co (cv x4) (cv x3) (cv x0)) (cv x2)) (λ x4 . cv x1))) (λ x3 . cv x1)) (λ x2 . cv x1))))) (proof)
Theorem df_gid : wceq cgi (cmpt (λ x0 . cvv) (λ x0 . crio (λ x1 . wral (λ x2 . wa (wceq (co (cv x1) (cv x2) (cv x0)) (cv x2)) (wceq (co (cv x2) (cv x1) (cv x0)) (cv x2))) (λ x2 . crn (cv x0))) (λ x1 . crn (cv x0)))) (proof)
Theorem df_ginv : wceq cgn (cmpt (λ x0 . cgr) (λ x0 . cmpt (λ x1 . crn (cv x0)) (λ x1 . crio (λ x2 . wceq (co (cv x2) (cv x1) (cv x0)) (cfv (cv x0) cgi)) (λ x2 . crn (cv x0))))) (proof)
Theorem df_gdiv : wceq cgs (cmpt (λ x0 . cgr) (λ x0 . cmpt2 (λ x1 x2 . crn (cv x0)) (λ x1 x2 . crn (cv x0)) (λ x1 x2 . co (cv x1) (cfv (cv x2) (cfv (cv x0) cgn)) (cv x0)))) (proof)
Theorem df_ablo : wceq cablo (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cv x0)) (co (cv x2) (cv x1) (cv x0))) (λ x2 . crn (cv x0))) (λ x1 . crn (cv x0))) (λ x0 . cgr)) (proof)
Theorem df_vc : wceq cvc (copab (λ x0 x1 . w3a (wcel (cv x0) cablo) (wf (cxp cc (crn (cv x0))) (crn (cv x0)) (cv x1)) (wral (λ x2 . wa (wceq (co c1 (cv x2) (cv x1)) (cv x2)) (wral (λ x3 . wa (wral (λ x4 . wceq (co (cv x3) (co (cv x2) (cv x4) (cv x0)) (cv x1)) (co (co (cv x3) (cv x2) (cv x1)) (co (cv x3) (cv x4) (cv x1)) (cv x0))) (λ x4 . crn (cv x0))) (wral (λ x4 . wa (wceq (co (co (cv x3) (cv x4) caddc) (cv x2) (cv x1)) (co (co (cv x3) (cv x2) (cv x1)) (co (cv x4) (cv x2) (cv x1)) (cv x0))) (wceq (co (co (cv x3) (cv x4) cmul) (cv x2) (cv x1)) (co (cv x3) (co (cv x4) (cv x2) (cv x1)) (cv x1)))) (λ x4 . cc))) (λ x3 . cc))) (λ x2 . crn (cv x0))))) (proof)
Theorem df_nv : wceq cnv (coprab (λ x0 x1 x2 . w3a (wcel (cop (cv x0) (cv x1)) cvc) (wf (crn (cv x0)) cr (cv x2)) (wral (λ x3 . w3a (wceq (cfv (cv x3) (cv x2)) cc0wceq (cv x3) (cfv (cv x0) cgi)) (wral (λ x4 . wceq (cfv (co (cv x4) (cv x3) (cv x1)) (cv x2)) (co (cfv (cv x4) cabs) (cfv (cv x3) (cv x2)) cmul)) (λ x4 . cc)) (wral (λ x4 . wbr (cfv (co (cv x3) (cv x4) (cv x0)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) caddc) cle) (λ x4 . crn (cv x0)))) (λ x3 . crn (cv x0))))) (proof)
Theorem df_va : wceq cpv (ccom c1st c1st) (proof)
Theorem df_ba : wceq cba (cmpt (λ x0 . cvv) (λ x0 . crn (cfv (cv x0) cpv))) (proof)
Theorem df_sm : wceq cns (ccom c2nd c1st) (proof)
Theorem df_0v : wceq cn0v (ccom cgi cpv) (proof)
Theorem df_vs : wceq cnsb (ccom cgs cpv) (proof)
Theorem df_nmcv : wceq cnmcv c2nd (proof)
Theorem df_ims : wceq cims (cmpt (λ x0 . cnv) (λ x0 . ccom (cfv (cv x0) cnmcv) (cfv (cv x0) cnsb))) (proof)