Proofgold Asset

Known df_ditg__df_limc__df_dv__df_dvn__df_cpn__df_mdeg__df_deg1__df_mon1__df_uc1p__df_q1p__df_r1p__df_ig1p__df_ply__df_idp__df_coe__df_dgr__df_quot__df_aa : ∀ x0 : ο . ((∀ x1 x2 x3 : ι → ι → ο . ∀ x4 . wceq (cdit x1 x2 x3) (cif (wbr (x1 x4) (x2 x4) cle) (citg (λ x5 . co (x1 x5) (x2 x5) cioo) x3) (cneg (citg (λ x5 . co (x2 x5) (x1 x5) cioo) x3)))) ⟶ wceq climc (cmpt2 (λ x1 x2 . co cc cc cpm) (λ x1 x2 . cc) (λ x1 x2 . cab (λ x3 . wsbc (λ x4 . wcel (cmpt (λ x5 . cun (cdm (cv x1)) (csn (cv x2))) (λ x5 . cif (wceq (cv x5) (cv x2)) (cv x3) (cfv (cv x5) (cv x1)))) (cfv (cv x2) (co (co (cv x4) (cun (cdm (cv x1)) (csn (cv x2))) crest) (cv x4) ccnp))) (cfv ccnfld ctopn)))) ⟶ wceq cdv (cmpt2 (λ x1 x2 . cpw cc) (λ x1 x2 . co cc (cv x1) cpm) (λ x1 x2 . ciun (λ x3 . cfv (cdm (cv x2)) (cfv (co (cfv ccnfld ctopn) (cv x1) crest) cnt)) (λ x3 . cxp (csn (cv x3)) (co (cmpt (λ x4 . cdif (cdm (cv x2)) (csn (cv x3))) (λ x4 . co (co (cfv (cv x4) (cv x2)) (cfv (cv x3) (cv x2)) cmin) (co (cv x4) (cv x3) cmin) cdiv)) (cv x3) climc)))) ⟶ wceq cdvn (cmpt2 (λ x1 x2 . cpw cc) (λ x1 x2 . co cc (cv x1) cpm) (λ x1 x2 . cseq (ccom (cmpt (λ x3 . cvv) (λ x3 . co (cv x1) (cv x3) cdv)) c1st) (cxp cn0 (csn (cv x2))) cc0)) ⟶ wceq ccpn (cmpt (λ x1 . cpw cc) (λ x1 . cmpt (λ x2 . cn0) (λ x2 . crab (λ x3 . wcel (cfv (cv x2) (co (cv x1) (cv x3) cdvn)) (co (cdm (cv x3)) cc ccncf)) (λ x3 . co cc (cv x1) cpm)))) ⟶ wceq cmdg (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmpl) cbs) (λ x3 . csup (crn (cmpt (λ x4 . co (cv x3) (cfv (cv x2) c0g) csupp) (λ x4 . co ccnfld (cv x4) cgsu))) cxr clt))) ⟶ wceq cdg1 (cmpt (λ x1 . cvv) (λ x1 . co c1o (cv x1) cmdg)) ⟶ wceq cmn1 (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wne (cv x2) (cfv (cfv (cv x1) cpl1) c0g)) (wceq (cfv (cfv (cv x2) (cfv (cv x1) cdg1)) (cfv (cv x2) cco1)) (cfv (cv x1) cur))) (λ x2 . cfv (cfv (cv x1) cpl1) cbs))) ⟶ wceq cuc1p (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wne (cv x2) (cfv (cfv (cv x1) cpl1) c0g)) (wcel (cfv (cfv (cv x2) (cfv (cv x1) cdg1)) (cfv (cv x2) cco1)) (cfv (cv x1) cui))) (λ x2 . cfv (cfv (cv x1) cpl1) cbs))) ⟶ wceq cq1p (cmpt (λ x1 . cvv) (λ x1 . csb (cfv (cv x1) cpl1) (λ x2 . csb (cfv (cv x2) cbs) (λ x3 . cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . crio (λ x6 . wbr (cfv (co (cv x4) (co (cv x6) (cv x5) (cfv (cv x2) cmulr)) (cfv (cv x2) csg)) (cfv (cv x1) cdg1)) (cfv (cv x5) (cfv (cv x1) cdg1)) clt) (λ x6 . cv x3)))))) ⟶ wceq cr1p (cmpt (λ x1 . cvv) (λ x1 . csb (cfv (cfv (cv x1) cpl1) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (co (co (cv x3) (cv x4) (cfv (cv x1) cq1p)) (cv x4) (cfv (cfv (cv x1) cpl1) cmulr)) (cfv (cfv (cv x1) cpl1) csg))))) ⟶ wceq cig1p (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cfv (cv x1) cpl1) clidl) (λ x2 . cif (wceq (cv x2) (csn (cfv (cfv (cv x1) cpl1) c0g))) (cfv (cfv (cv x1) cpl1) c0g) (crio (λ x3 . wceq (cfv (cv x3) (cfv (cv x1) cdg1)) (cinf (cima (cfv (cv x1) cdg1) (cdif (cv x2) (csn (cfv (cfv (cv x1) cpl1) c0g)))) cr clt)) (λ x3 . cin (cv x2) (cfv (cv x1) cmn1)))))) ⟶ wceq cply (cmpt (λ x1 . cpw cc) (λ x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (cmpt (λ x5 . cc) (λ x5 . csu (co cc0 (cv x3) cfz) (λ x6 . co (cfv (cv x6) (cv x4)) (co (cv x5) (cv x6) cexp) cmul)))) (λ x4 . co (cun (cv x1) (csn cc0)) cn0 cmap)) (λ x3 . cn0)))) ⟶ wceq cidp (cres cid cc) ⟶ wceq ccoe (cmpt (λ x1 . cfv cc cply) (λ x1 . crio (λ x2 . wrex (λ x3 . wa (wceq (cima (cv x2) (cfv (co (cv x3) c1 caddc) cuz)) (csn cc0)) (wceq (cv x1) (cmpt (λ x4 . cc) (λ x4 . csu (co cc0 (cv x3) cfz) (λ x5 . co (cfv (cv x5) (cv x2)) (co (cv x4) (cv x5) cexp) cmul))))) (λ x3 . cn0)) (λ x2 . co cc cn0 cmap))) ⟶ wceq cdgr (cmpt (λ x1 . cfv cc cply) (λ x1 . csup (cima (ccnv (cfv (cv x1) ccoe)) (cdif cc (csn cc0))) cn0 clt)) ⟶ wceq cquot (cmpt2 (λ x1 x2 . cfv cc cply) (λ x1 x2 . cdif (cfv cc cply) (csn c0p)) (λ x1 x2 . crio (λ x3 . wsbc (λ x4 . wo (wceq (cv x4) c0p) (wbr (cfv (cv x4) cdgr) (cfv (cv x2) cdgr) clt)) (co (cv x1) (co (cv x2) (cv x3) (cof cmul)) (cof cmin))) (λ x3 . cfv cc cply))) ⟶ wceq caa (ciun (λ x1 . cdif (cfv cz cply) (csn c0p)) (λ x1 . cima (ccnv (cv x1)) (csn cc0))) ⟶ x0) ⟶ x0
Theorem df_ditg : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 . wceq (cdit x0 x1 x2) (cif (wbr (x0 x3) (x1 x3) cle) (citg (λ x4 . co (x0 x4) (x1 x4) cioo) x2) (cneg (citg (λ x4 . co (x1 x4) (x0 x4) cioo) x2)))
Theorem df_limc : wceq climc (cmpt2 (λ x0 x1 . co cc cc cpm) (λ x0 x1 . cc) (λ x0 x1 . cab (λ x2 . wsbc (λ x3 . wcel (cmpt (λ x4 . cun (cdm (cv x0)) (csn (cv x1))) (λ x4 . cif (wceq (cv x4) (cv x1)) (cv x2) (cfv (cv x4) (cv x0)))) (cfv (cv x1) (co (co (cv x3) (cun (cdm (cv x0)) (csn (cv x1))) crest) (cv x3) ccnp))) (cfv ccnfld ctopn))))
Theorem df_dv : wceq cdv (cmpt2 (λ x0 x1 . cpw cc) (λ x0 x1 . co cc (cv x0) cpm) (λ x0 x1 . ciun (λ x2 . cfv (cdm (cv x1)) (cfv (co (cfv ccnfld ctopn) (cv x0) crest) cnt)) (λ x2 . cxp (csn (cv x2)) (co (cmpt (λ x3 . cdif (cdm (cv x1)) (csn (cv x2))) (λ x3 . co (co (cfv (cv x3) (cv x1)) (cfv (cv x2) (cv x1)) cmin) (co (cv x3) (cv x2) cmin) cdiv)) (cv x2) climc))))
Theorem df_dvn : wceq cdvn (cmpt2 (λ x0 x1 . cpw cc) (λ x0 x1 . co cc (cv x0) cpm) (λ x0 x1 . cseq (ccom (cmpt (λ x2 . cvv) (λ x2 . co (cv x0) (cv x2) cdv)) c1st) (cxp cn0 (csn (cv x1))) cc0))
Theorem df_cpn : wceq ccpn (cmpt (λ x0 . cpw cc) (λ x0 . cmpt (λ x1 . cn0) (λ x1 . crab (λ x2 . wcel (cfv (cv x1) (co (cv x0) (cv x2) cdvn)) (co (cdm (cv x2)) cc ccncf)) (λ x2 . co cc (cv x0) cpm))))
Theorem df_mdeg : wceq cmdg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmpl) cbs) (λ x2 . csup (crn (cmpt (λ x3 . co (cv x2) (cfv (cv x1) c0g) csupp) (λ x3 . co ccnfld (cv x3) cgsu))) cxr clt)))
Theorem df_deg1 : wceq cdg1 (cmpt (λ x0 . cvv) (λ x0 . co c1o (cv x0) cmdg))
Theorem df_mon1 : wceq cmn1 (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wne (cv x1) (cfv (cfv (cv x0) cpl1) c0g)) (wceq (cfv (cfv (cv x1) (cfv (cv x0) cdg1)) (cfv (cv x1) cco1)) (cfv (cv x0) cur))) (λ x1 . cfv (cfv (cv x0) cpl1) cbs)))
Theorem df_uc1p : wceq cuc1p (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wne (cv x1) (cfv (cfv (cv x0) cpl1) c0g)) (wcel (cfv (cfv (cv x1) (cfv (cv x0) cdg1)) (cfv (cv x1) cco1)) (cfv (cv x0) cui))) (λ x1 . cfv (cfv (cv x0) cpl1) cbs)))
Theorem df_q1p : wceq cq1p (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cv x0) cpl1) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . crio (λ x5 . wbr (cfv (co (cv x3) (co (cv x5) (cv x4) (cfv (cv x1) cmulr)) (cfv (cv x1) csg)) (cfv (cv x0) cdg1)) (cfv (cv x4) (cfv (cv x0) cdg1)) clt) (λ x5 . cv x2))))))
Theorem df_r1p : wceq cr1p (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cfv (cv x0) cpl1) cbs) (λ x1 . cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x2) (co (co (cv x2) (cv x3) (cfv (cv x0) cq1p)) (cv x3) (cfv (cfv (cv x0) cpl1) cmulr)) (cfv (cfv (cv x0) cpl1) csg)))))
Theorem df_ig1p : wceq cig1p (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cfv (cv x0) cpl1) clidl) (λ x1 . cif (wceq (cv x1) (csn (cfv (cfv (cv x0) cpl1) c0g))) (cfv (cfv (cv x0) cpl1) c0g) (crio (λ x2 . wceq (cfv (cv x2) (cfv (cv x0) cdg1)) (cinf (cima (cfv (cv x0) cdg1) (cdif (cv x1) (csn (cfv (cfv (cv x0) cpl1) c0g)))) cr clt)) (λ x2 . cin (cv x1) (cfv (cv x0) cmn1))))))
Theorem df_ply : wceq cply (cmpt (λ x0 . cpw cc) (λ x0 . cab (λ x1 . wrex (λ x2 . wrex (λ x3 . wceq (cv x1) (cmpt (λ x4 . cc) (λ x4 . csu (co cc0 (cv x2) cfz) (λ x5 . co (cfv (cv x5) (cv x3)) (co (cv x4) (cv x5) cexp) cmul)))) (λ x3 . co (cun (cv x0) (csn cc0)) cn0 cmap)) (λ x2 . cn0))))
Theorem df_idp : wceq cidp (cres cid cc)
Theorem df_coe : wceq ccoe (cmpt (λ x0 . cfv cc cply) (λ x0 . crio (λ x1 . wrex (λ x2 . wa (wceq (cima (cv x1) (cfv (co (cv x2) c1 caddc) cuz)) (csn cc0)) (wceq (cv x0) (cmpt (λ x3 . cc) (λ x3 . csu (co cc0 (cv x2) cfz) (λ x4 . co (cfv (cv x4) (cv x1)) (co (cv x3) (cv x4) cexp) cmul))))) (λ x2 . cn0)) (λ x1 . co cc cn0 cmap)))
Theorem df_dgr : wceq cdgr (cmpt (λ x0 . cfv cc cply) (λ x0 . csup (cima (ccnv (cfv (cv x0) ccoe)) (cdif cc (csn cc0))) cn0 clt))
Theorem df_quot : wceq cquot (cmpt2 (λ x0 x1 . cfv cc cply) (λ x0 x1 . cdif (cfv cc cply) (csn c0p)) (λ x0 x1 . crio (λ x2 . wsbc (λ x3 . wo (wceq (cv x3) c0p) (wbr (cfv (cv x3) cdgr) (cfv (cv x1) cdgr) clt)) (co (cv x0) (co (cv x1) (cv x2) (cof cmul)) (cof cmin))) (λ x2 . cfv cc cply)))
Theorem df_aa : wceq caa (ciun (λ x0 . cdif (cfv cz cply) (csn c0p)) (λ x0 . cima (ccnv (cv x0)) (csn cc0)))