Search for blocks/addresses/...

Proofgold Asset

asset id
a4375311c093047374030928e2ea52f37f34895092a1e8cc379467e345fea616
asset hash
24efaeab97a26a80124eb4d7ab4c6030f82a89fd0d2d73ea9a444049f45876e6
bday / block
36385
tx
4ed04..
preasset
doc published by PrCmT..
Known df_mpl__df_ltbag__df_opsr__df_evls__df_evl__df_mhp__df_psd__df_selv__df_algind__df_psr1__df_vr1__df_ply1__df_coe1__df_toply1__df_evls1__df_evl1__df_psmet__df_xmet : ∀ x0 : ο . (wceq cmpl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (co (cv x1) (cv x2) cmps) (λ x3 . co (cv x3) (crab (λ x4 . wbr (cv x4) (cfv (cv x2) c0g) cfsupp) (λ x4 . cfv (cv x3) cbs)) cress)))wceq cltb (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . copab (λ x3 x4 . wa (wss (cpr (cv x3) (cv x4)) (crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x2) cmap))) (wrex (λ x5 . wa (wbr (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)) clt) (wral (λ x6 . wbr (cv x5) (cv x6) (cv x1)wceq (cfv (cv x6) (cv x3)) (cfv (cv x6) (cv x4))) (λ x6 . cv x2))) (λ x5 . cv x2)))))wceq copws (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cpw (cxp (cv x1) (cv x1))) (λ x3 . csb (co (cv x1) (cv x2) cmps) (λ x4 . co (cv x4) (cop (cfv cnx cple) (copab (λ x5 x6 . wa (wss (cpr (cv x5) (cv x6)) (cfv (cv x4) cbs)) (wo (wsbc (λ x7 . wrex (λ x8 . wa (wbr (cfv (cv x8) (cv x5)) (cfv (cv x8) (cv x6)) (cfv (cv x2) cplt)) (wral (λ x9 . wbr (cv x9) (cv x8) (co (cv x3) (cv x1) cltb)wceq (cfv (cv x9) (cv x5)) (cfv (cv x9) (cv x6))) (λ x9 . cv x7))) (λ x8 . cv x7)) (crab (λ x7 . wcel (cima (ccnv (cv x7)) cn) cfn) (λ x7 . co cn0 (cv x1) cmap))) (wceq (cv x5) (cv x6)))))) csts))))wceq ces (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . ccrg) (λ x1 x2 . csb (cfv (cv x2) cbs) (λ x3 . cmpt (λ x4 . cfv (cv x2) csubrg) (λ x4 . csb (co (cv x1) (co (cv x2) (cv x4) cress) cmpl) (λ x5 . crio (λ x6 . wa (wceq (ccom (cv x6) (cfv (cv x5) cascl)) (cmpt (λ x7 . cv x4) (λ x7 . cxp (co (cv x3) (cv x1) cmap) (csn (cv x7))))) (wceq (ccom (cv x6) (co (cv x1) (co (cv x2) (cv x4) cress) cmvr)) (cmpt (λ x7 . cv x1) (λ x7 . cmpt (λ x8 . co (cv x3) (cv x1) cmap) (λ x8 . cfv (cv x7) (cv x8)))))) (λ x6 . co (cv x5) (co (cv x2) (co (cv x3) (cv x1) cmap) cpws) crh))))))wceq cevl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cfv (cfv (cv x2) cbs) (co (cv x1) (cv x2) ces)))wceq cmhp (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cn0) (λ x3 . crab (λ x4 . wss (co (cv x4) (cfv (cv x2) c0g) csupp) (crab (λ x5 . wceq (csu cn0 (λ x6 . cfv (cv x6) (cv x5))) (cv x3)) (λ x5 . crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x1) cmap)))) (λ x4 . cfv (co (cv x1) (cv x2) cmpl) cbs))))wceq cpsd (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cv x1) (λ x3 . cmpt (λ x4 . cfv (co (cv x1) (cv x2) cmps) cbs) (λ x4 . cmpt (λ x5 . crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x1) cmap)) (λ x5 . co (co (cfv (cv x3) (cv x5)) c1 caddc) (cfv (co (cv x5) (cmpt (λ x6 . cv x1) (λ x6 . cif (wceq (cv x6) (cv x3)) c1 cc0)) (cof caddc)) (cv x4)) (cfv (cv x2) cmg))))))wceq cslv (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cpw (cv x1)) (λ x3 . cmpt (λ x4 . co (cv x1) (cv x2) cmpl) (λ x4 . csb (co (cdif (cv x1) (cv x3)) (cv x2) cmpl) (λ x5 . csb (cmpt (λ x6 . cfv (cv x5) csca) (λ x6 . co (cv x6) (cfv (cv x5) cur) (cfv (cv x5) cvsca))) (λ x6 . cfv (cmpt (λ x7 . cv x1) (λ x7 . cif (wcel (cv x7) (cv x3)) (cfv (cv x7) (co (cv x3) (co (cdif (cv x1) (cv x3)) (cv x2) cmpl) cmvr)) (ccom (cv x6) (cfv (cv x7) (co (cdif (cv x1) (cv x3)) (cv x2) cmvr))))) (cfv (ccom (cv x6) (cv x4)) (cfv (co (cv x6) (cv x2) cimas) (co (cv x1) (cv x5) ces)))))))))wceq cai (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cpw (cfv (cv x1) cbs)) (λ x1 x2 . crab (λ x3 . wfun (ccnv (cmpt (λ x4 . cfv (co (cv x3) (co (cv x1) (cv x2) cress) cmpl) cbs) (λ x4 . cfv (cres cid (cv x3)) (cfv (cv x4) (cfv (cv x2) (co (cv x3) (cv x1) ces))))))) (λ x3 . cpw (cfv (cv x1) cbs))))wceq cps1 (cmpt (λ x1 . cvv) (λ x1 . cfv c0 (co c1o (cv x1) copws)))wceq cv1 (cmpt (λ x1 . cvv) (λ x1 . cfv c0 (co c1o (cv x1) cmvr)))wceq cpl1 (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cps1) (cfv (co c1o (cv x1) cmpl) cbs) cress))wceq cco1 (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cn0) (λ x2 . cfv (cxp c1o (csn (cv x2))) (cv x1))))wceq ctp1 (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . co cn0 c1o cmap) (λ x2 . cfv (cfv c0 (cv x2)) (cv x1))))wceq ces1 (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cpw (cfv (cv x1) cbs)) (λ x1 x2 . csb (cfv (cv x1) cbs) (λ x3 . ccom (cmpt (λ x4 . co (cv x3) (co (cv x3) c1o cmap) cmap) (λ x4 . ccom (cv x4) (cmpt (λ x5 . cv x3) (λ x5 . cxp c1o (csn (cv x5)))))) (cfv (cv x2) (co c1o (cv x1) ces)))))wceq ce1 (cmpt (λ x1 . cvv) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . ccom (cmpt (λ x3 . co (cv x2) (co (cv x2) c1o cmap) cmap) (λ x3 . ccom (cv x3) (cmpt (λ x4 . cv x2) (λ x4 . cxp c1o (csn (cv x4)))))) (co c1o (cv x1) cevl))))wceq cpsmet (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wa (wceq (co (cv x3) (cv x3) (cv x2)) cc0) (wral (λ x4 . wral (λ x5 . wbr (co (cv x3) (cv x4) (cv x2)) (co (co (cv x5) (cv x3) (cv x2)) (co (cv x5) (cv x4) (cv x2)) cxad) cle) (λ x5 . cv x1)) (λ x4 . cv x1))) (λ x3 . cv x1)) (λ x2 . co cxr (cxp (cv x1) (cv x1)) cmap)))wceq cxmt (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wa (wb (wceq (co (cv x3) (cv x4) (cv x2)) cc0) (wceq (cv x3) (cv x4))) (wral (λ x5 . wbr (co (cv x3) (cv x4) (cv x2)) (co (co (cv x5) (cv x3) (cv x2)) (co (cv x5) (cv x4) (cv x2)) cxad) cle) (λ x5 . cv x1))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . co cxr (cxp (cv x1) (cv x1)) cmap)))x0)x0
Theorem df_mpl : wceq cmpl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmps) (λ x2 . co (cv x2) (crab (λ x3 . wbr (cv x3) (cfv (cv x1) c0g) cfsupp) (λ x3 . cfv (cv x2) cbs)) cress))) (proof)
Theorem df_ltbag : wceq cltb (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (crab (λ x4 . wcel (cima (ccnv (cv x4)) cn) cfn) (λ x4 . co cn0 (cv x1) cmap))) (wrex (λ x4 . wa (wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) clt) (wral (λ x5 . wbr (cv x4) (cv x5) (cv x0)wceq (cfv (cv x5) (cv x2)) (cfv (cv x5) (cv x3))) (λ x5 . cv x1))) (λ x4 . cv x1))))) (proof)
Theorem df_opsr : wceq copws (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cpw (cxp (cv x0) (cv x0))) (λ x2 . csb (co (cv x0) (cv x1) cmps) (λ x3 . co (cv x3) (cop (cfv cnx cple) (copab (λ x4 x5 . wa (wss (cpr (cv x4) (cv x5)) (cfv (cv x3) cbs)) (wo (wsbc (λ x6 . wrex (λ x7 . wa (wbr (cfv (cv x7) (cv x4)) (cfv (cv x7) (cv x5)) (cfv (cv x1) cplt)) (wral (λ x8 . wbr (cv x8) (cv x7) (co (cv x2) (cv x0) cltb)wceq (cfv (cv x8) (cv x4)) (cfv (cv x8) (cv x5))) (λ x8 . cv x6))) (λ x7 . cv x6)) (crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x0) cmap))) (wceq (cv x4) (cv x5)))))) csts)))) (proof)
Theorem df_evls : wceq ces (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . ccrg) (λ x0 x1 . csb (cfv (cv x1) cbs) (λ x2 . cmpt (λ x3 . cfv (cv x1) csubrg) (λ x3 . csb (co (cv x0) (co (cv x1) (cv x3) cress) cmpl) (λ x4 . crio (λ x5 . wa (wceq (ccom (cv x5) (cfv (cv x4) cascl)) (cmpt (λ x6 . cv x3) (λ x6 . cxp (co (cv x2) (cv x0) cmap) (csn (cv x6))))) (wceq (ccom (cv x5) (co (cv x0) (co (cv x1) (cv x3) cress) cmvr)) (cmpt (λ x6 . cv x0) (λ x6 . cmpt (λ x7 . co (cv x2) (cv x0) cmap) (λ x7 . cfv (cv x6) (cv x7)))))) (λ x5 . co (cv x4) (co (cv x1) (co (cv x2) (cv x0) cmap) cpws) crh)))))) (proof)
Theorem df_evl : wceq cevl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (cfv (cv x1) cbs) (co (cv x0) (cv x1) ces))) (proof)
Theorem df_mhp : wceq cmhp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cn0) (λ x2 . crab (λ x3 . wss (co (cv x3) (cfv (cv x1) c0g) csupp) (crab (λ x4 . wceq (csu cn0 (λ x5 . cfv (cv x5) (cv x4))) (cv x2)) (λ x4 . crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x0) cmap)))) (λ x3 . cfv (co (cv x0) (cv x1) cmpl) cbs)))) (proof)
Theorem df_psd : wceq cpsd (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cv x0) (λ x2 . cmpt (λ x3 . cfv (co (cv x0) (cv x1) cmps) cbs) (λ x3 . cmpt (λ x4 . crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x0) cmap)) (λ x4 . co (co (cfv (cv x2) (cv x4)) c1 caddc) (cfv (co (cv x4) (cmpt (λ x5 . cv x0) (λ x5 . cif (wceq (cv x5) (cv x2)) c1 cc0)) (cof caddc)) (cv x3)) (cfv (cv x1) cmg)))))) (proof)
Theorem df_selv : wceq cslv (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cpw (cv x0)) (λ x2 . cmpt (λ x3 . co (cv x0) (cv x1) cmpl) (λ x3 . csb (co (cdif (cv x0) (cv x2)) (cv x1) cmpl) (λ x4 . csb (cmpt (λ x5 . cfv (cv x4) csca) (λ x5 . co (cv x5) (cfv (cv x4) cur) (cfv (cv x4) cvsca))) (λ x5 . cfv (cmpt (λ x6 . cv x0) (λ x6 . cif (wcel (cv x6) (cv x2)) (cfv (cv x6) (co (cv x2) (co (cdif (cv x0) (cv x2)) (cv x1) cmpl) cmvr)) (ccom (cv x5) (cfv (cv x6) (co (cdif (cv x0) (cv x2)) (cv x1) cmvr))))) (cfv (ccom (cv x5) (cv x3)) (cfv (co (cv x5) (cv x1) cimas) (co (cv x0) (cv x4) ces))))))))) (proof)
Theorem df_algind : wceq cai (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . crab (λ x2 . wfun (ccnv (cmpt (λ x3 . cfv (co (cv x2) (co (cv x0) (cv x1) cress) cmpl) cbs) (λ x3 . cfv (cres cid (cv x2)) (cfv (cv x3) (cfv (cv x1) (co (cv x2) (cv x0) ces))))))) (λ x2 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_psr1 : wceq cps1 (cmpt (λ x0 . cvv) (λ x0 . cfv c0 (co c1o (cv x0) copws))) (proof)
Theorem df_vr1 : wceq cv1 (cmpt (λ x0 . cvv) (λ x0 . cfv c0 (co c1o (cv x0) cmvr))) (proof)
Theorem df_ply1 : wceq cpl1 (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cps1) (cfv (co c1o (cv x0) cmpl) cbs) cress)) (proof)
Theorem df_coe1 : wceq cco1 (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cn0) (λ x1 . cfv (cxp c1o (csn (cv x1))) (cv x0)))) (proof)
Theorem df_toply1 : wceq ctp1 (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co cn0 c1o cmap) (λ x1 . cfv (cfv c0 (cv x1)) (cv x0)))) (proof)
Theorem df_evls1 : wceq ces1 (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . ccom (cmpt (λ x3 . co (cv x2) (co (cv x2) c1o cmap) cmap) (λ x3 . ccom (cv x3) (cmpt (λ x4 . cv x2) (λ x4 . cxp c1o (csn (cv x4)))))) (cfv (cv x1) (co c1o (cv x0) ces))))) (proof)
Theorem df_evl1 : wceq ce1 (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . ccom (cmpt (λ x2 . co (cv x1) (co (cv x1) c1o cmap) cmap) (λ x2 . ccom (cv x2) (cmpt (λ x3 . cv x1) (λ x3 . cxp c1o (csn (cv x3)))))) (co c1o (cv x0) cevl)))) (proof)
Theorem df_psmet : wceq cpsmet (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wceq (co (cv x2) (cv x2) (cv x1)) cc0) (wral (λ x3 . wral (λ x4 . wbr (co (cv x2) (cv x3) (cv x1)) (co (co (cv x4) (cv x2) (cv x1)) (co (cv x4) (cv x3) (cv x1)) cxad) cle) (λ x4 . cv x0)) (λ x3 . cv x0))) (λ x2 . cv x0)) (λ x1 . co cxr (cxp (cv x0) (cv x0)) cmap))) (proof)
Theorem df_xmet : wceq cxmt (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wa (wb (wceq (co (cv x2) (cv x3) (cv x1)) cc0) (wceq (cv x2) (cv x3))) (wral (λ x4 . wbr (co (cv x2) (cv x3) (cv x1)) (co (co (cv x4) (cv x2) (cv x1)) (co (cv x4) (cv x3) (cv x1)) cxad) cle) (λ x4 . cv x0))) (λ x3 . cv x0)) (λ x2 . cv x0)) (λ x1 . co cxr (cxp (cv x0) (cv x0)) cmap))) (proof)