Proofgold Asset

Known df_zrng__df_gf__df_gfoo__df_eqp__df_rqp__df_qp__df_qpOLD__df_zp__df_qpa__df_cp__df_trpred__df_wsuc__df_wlim__df_frecs__df_no__df_slt__df_bday__df_sle : ∀ x0 : ο . (wceq czr (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (crn (cfv (cv x1) czrh)) citr)) ⟶ wceq cgf (cmpt2 (λ x1 x2 . cprime) (λ x1 x2 . cn) (λ x1 x2 . csb (cfv (cv x1) czn) (λ x3 . cfv (co (cv x3) (csn (csb (cfv (cv x3) cpl1) (λ x4 . csb (cfv (cv x3) cv1) (λ x5 . co (co (co (cv x1) (cv x2) cexp) (cv x5) (cfv (cfv (cv x4) cmgp) cmg)) (cv x5) (cfv (cv x4) csg))))) csf) c1st))) ⟶ wceq cgfo (cmpt (λ x1 . cprime) (λ x1 . csb (cfv (cv x1) czn) (λ x2 . co (cv x2) (cmpt (λ x3 . cn) (λ x3 . csn (csb (cfv (cv x2) cpl1) (λ x4 . csb (cfv (cv x2) cv1) (λ x5 . co (co (co (cv x1) (cv x3) cexp) (cv x5) (cfv (cfv (cv x4) cmgp) cmg)) (cv x5) (cfv (cv x4) csg)))))) cpsl))) ⟶ wceq ceqp (cmpt (λ x1 . cprime) (λ x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (co cz cz cmap)) (wral (λ x4 . wcel (csu (cfv (cneg (cv x4)) cuz) (λ x5 . co (co (cfv (cneg (cv x5)) (cv x2)) (cfv (cneg (cv x5)) (cv x3)) cmin) (co (cv x1) (co (cv x5) (co (cv x4) c1 caddc) caddc) cexp) cdiv)) cz) (λ x4 . cz))))) ⟶ wceq crqp (cmpt (λ x1 . cprime) (λ x1 . cin ceqp (csb (crab (λ x2 . wrex (λ x3 . wss (cima (ccnv (cv x2)) (cdif cz (csn cc0))) (cv x3)) (λ x3 . crn cuz)) (λ x2 . co cz cz cmap)) (λ x2 . cxp (cv x2) (cin (cv x2) (co cz (co cc0 (co (cv x1) c1 cmin) cfz) cmap)))))) ⟶ wceq cqp (cmpt (λ x1 . cprime) (λ x1 . csb (crab (λ x2 . wrex (λ x3 . wss (cima (ccnv (cv x2)) (cdif cz (csn cc0))) (cv x3)) (λ x3 . crn cuz)) (λ x2 . co cz (co cc0 (co (cv x1) c1 cmin) cfz) cmap)) (λ x2 . co (cun (ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cfv (co (cv x3) (cv x4) (cof caddc)) (cfv (cv x1) crqp)))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cfv (cmpt (λ x5 . cz) (λ x5 . csu cz (λ x6 . co (cfv (cv x6) (cv x3)) (cfv (co (cv x5) (cv x6) cmin) (cv x4)) cmul))) (cfv (cv x1) crqp))))) (csn (cop (cfv cnx cple) (copab (λ x3 x4 . wa (wss (cpr (cv x3) (cv x4)) (cv x2)) (wbr (csu cz (λ x5 . co (cfv (cneg (cv x5)) (cv x3)) (co (co (cv x1) c1 caddc) (cneg (cv x5)) cexp) cmul)) (csu cz (λ x5 . co (cfv (cneg (cv x5)) (cv x4)) (co (co (cv x1) c1 caddc) (cneg (cv x5)) cexp) cmul)) clt)))))) (cmpt (λ x3 . cv x2) (λ x3 . cif (wceq (cv x3) (cxp cz (csn cc0))) cc0 (co (cv x1) (cneg (cinf (cima (ccnv (cv x3)) (cdif cz (csn cc0))) cr clt)) cexp))) ctng))) ⟶ wceq cqpOLD (cmpt (λ x1 . cprime) (λ x1 . csb (crab (λ x2 . wrex (λ x3 . wss (cima (ccnv (cv x2)) (cdif cz (csn cc0))) (cv x3)) (λ x3 . crn cuz)) (λ x2 . co cz (co cc0 (co (cv x1) c1 cmin) cfz) cmap)) (λ x2 . co (cun (ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cfv (co (cv x3) (cv x4) (cof caddc)) (cfv (cv x1) crqp)))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cfv (cmpt (λ x5 . cz) (λ x5 . csu cz (λ x6 . co (cfv (cv x6) (cv x3)) (cfv (co (cv x5) (cv x6) cmin) (cv x4)) cmul))) (cfv (cv x1) crqp))))) (csn (cop (cfv cnx cple) (copab (λ x3 x4 . wa (wss (cpr (cv x3) (cv x4)) (cv x2)) (wbr (csu cz (λ x5 . co (cfv (cneg (cv x5)) (cv x3)) (co (co (cv x1) c1 caddc) (cneg (cv x5)) cexp) cmul)) (csu cz (λ x5 . co (cfv (cneg (cv x5)) (cv x4)) (co (co (cv x1) c1 caddc) (cneg (cv x5)) cexp) cmul)) clt)))))) (cmpt (λ x3 . cv x2) (λ x3 . cif (wceq (cv x3) (cxp cz (csn cc0))) cc0 (co (cv x1) (cneg (csup (cima (ccnv (cv x3)) (cdif cz (csn cc0))) cr (ccnv clt))) cexp))) ctng))) ⟶ wceq czp (ccom czr cqp) ⟶ wceq cqpa (cmpt (λ x1 . cprime) (λ x1 . csb (cfv (cv x1) cqp) (λ x2 . co (cv x2) (cmpt (λ x3 . cn) (λ x3 . crab (λ x4 . wa (wbr (co (cv x2) (cv x4) cdg1) (cv x3) cle) (wral (λ x5 . wss (cima (ccnv (cv x5)) (cdif cz (csn cc0))) (co cc0 (cv x3) cfz)) (λ x5 . crn (cfv (cv x4) cco1)))) (λ x4 . cfv (cv x2) cpl1))) cpsl))) ⟶ wceq ccp (ccom ccpms cqpa) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (ctrpred x1 x2 x3) (cuni (crn (cres (crdg (cmpt (λ x4 . cvv) (λ x4 . ciun (λ x5 . cv x4) (λ x5 . cpred x1 x2 (cv x5)))) (cpred x1 x2 x3)) com)))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cwsuc x1 x2 x3) (cinf (cpred x1 (ccnv x2) x3) x1 x2)) ⟶ (∀ x1 x2 : ι → ο . wceq (cwlim x1 x2) (crab (λ x3 . wa (wne (cv x3) (cinf x1 x1 x2)) (wceq (cv x3) (csup (cpred x1 x2 (cv x3)) x1 x2))) (λ x3 . x1))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cfrecs x1 x2 x3) (cuni (cab (λ x4 . wex (λ x5 . w3a (wfn (cv x4) (cv x5)) (wa (wss (cv x5) x1) (wral (λ x6 . wss (cpred x1 x2 (cv x6)) (cv x5)) (λ x6 . cv x5))) (wral (λ x6 . wceq (cfv (cv x6) (cv x4)) (co (cv x6) (cres (cv x4) (cpred x1 x2 (cv x6))) x3)) (λ x6 . cv x5))))))) ⟶ wceq csur (cab (λ x1 . wrex (λ x2 . wf (cv x2) (cpr c1o c2o) (cv x1)) (λ x2 . con0))) ⟶ wceq cslt (copab (λ x1 x2 . wa (wa (wcel (cv x1) csur) (wcel (cv x2) csur)) (wrex (λ x3 . wa (wral (λ x4 . wceq (cfv (cv x4) (cv x1)) (cfv (cv x4) (cv x2))) (λ x4 . cv x3)) (wbr (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) (ctp (cop c1o c0) (cop c1o c2o) (cop c0 c2o)))) (λ x3 . con0)))) ⟶ wceq cbday (cmpt (λ x1 . csur) (λ x1 . cdm (cv x1))) ⟶ wceq csle (cdif (cxp csur csur) (ccnv cslt)) ⟶ x0) ⟶ x0
Theorem df_zrng : wceq czr (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (crn (cfv (cv x0) czrh)) citr))
Theorem df_gf : wceq cgf (cmpt2 (λ x0 x1 . cprime) (λ x0 x1 . cn) (λ x0 x1 . csb (cfv (cv x0) czn) (λ x2 . cfv (co (cv x2) (csn (csb (cfv (cv x2) cpl1) (λ x3 . csb (cfv (cv x2) cv1) (λ x4 . co (co (co (cv x0) (cv x1) cexp) (cv x4) (cfv (cfv (cv x3) cmgp) cmg)) (cv x4) (cfv (cv x3) csg))))) csf) c1st)))
Theorem df_gfoo : wceq cgfo (cmpt (λ x0 . cprime) (λ x0 . csb (cfv (cv x0) czn) (λ x1 . co (cv x1) (cmpt (λ x2 . cn) (λ x2 . csn (csb (cfv (cv x1) cpl1) (λ x3 . csb (cfv (cv x1) cv1) (λ x4 . co (co (co (cv x0) (cv x2) cexp) (cv x4) (cfv (cfv (cv x3) cmgp) cmg)) (cv x4) (cfv (cv x3) csg)))))) cpsl)))
Theorem df_eqp : wceq ceqp (cmpt (λ x0 . cprime) (λ x0 . copab (λ x1 x2 . wa (wss (cpr (cv x1) (cv x2)) (co cz cz cmap)) (wral (λ x3 . wcel (csu (cfv (cneg (cv x3)) cuz) (λ x4 . co (co (cfv (cneg (cv x4)) (cv x1)) (cfv (cneg (cv x4)) (cv x2)) cmin) (co (cv x0) (co (cv x4) (co (cv x3) c1 caddc) caddc) cexp) cdiv)) cz) (λ x3 . cz)))))
Theorem df_rqp : wceq crqp (cmpt (λ x0 . cprime) (λ x0 . cin ceqp (csb (crab (λ x1 . wrex (λ x2 . wss (cima (ccnv (cv x1)) (cdif cz (csn cc0))) (cv x2)) (λ x2 . crn cuz)) (λ x1 . co cz cz cmap)) (λ x1 . cxp (cv x1) (cin (cv x1) (co cz (co cc0 (co (cv x0) c1 cmin) cfz) cmap))))))
Theorem df_qp : wceq cqp (cmpt (λ x0 . cprime) (λ x0 . csb (crab (λ x1 . wrex (λ x2 . wss (cima (ccnv (cv x1)) (cdif cz (csn cc0))) (cv x2)) (λ x2 . crn cuz)) (λ x1 . co cz (co cc0 (co (cv x0) c1 cmin) cfz) cmap)) (λ x1 . co (cun (ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . cfv (co (cv x2) (cv x3) (cof caddc)) (cfv (cv x0) crqp)))) (cop (cfv cnx cmulr) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . cfv (cmpt (λ x4 . cz) (λ x4 . csu cz (λ x5 . co (cfv (cv x5) (cv x2)) (cfv (co (cv x4) (cv x5) cmin) (cv x3)) cmul))) (cfv (cv x0) crqp))))) (csn (cop (cfv cnx cple) (copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (cv x1)) (wbr (csu cz (λ x4 . co (cfv (cneg (cv x4)) (cv x2)) (co (co (cv x0) c1 caddc) (cneg (cv x4)) cexp) cmul)) (csu cz (λ x4 . co (cfv (cneg (cv x4)) (cv x3)) (co (co (cv x0) c1 caddc) (cneg (cv x4)) cexp) cmul)) clt)))))) (cmpt (λ x2 . cv x1) (λ x2 . cif (wceq (cv x2) (cxp cz (csn cc0))) cc0 (co (cv x0) (cneg (cinf (cima (ccnv (cv x2)) (cdif cz (csn cc0))) cr clt)) cexp))) ctng)))
Theorem df_qpOLD : wceq cqpOLD (cmpt (λ x0 . cprime) (λ x0 . csb (crab (λ x1 . wrex (λ x2 . wss (cima (ccnv (cv x1)) (cdif cz (csn cc0))) (cv x2)) (λ x2 . crn cuz)) (λ x1 . co cz (co cc0 (co (cv x0) c1 cmin) cfz) cmap)) (λ x1 . co (cun (ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . cfv (co (cv x2) (cv x3) (cof caddc)) (cfv (cv x0) crqp)))) (cop (cfv cnx cmulr) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . cfv (cmpt (λ x4 . cz) (λ x4 . csu cz (λ x5 . co (cfv (cv x5) (cv x2)) (cfv (co (cv x4) (cv x5) cmin) (cv x3)) cmul))) (cfv (cv x0) crqp))))) (csn (cop (cfv cnx cple) (copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (cv x1)) (wbr (csu cz (λ x4 . co (cfv (cneg (cv x4)) (cv x2)) (co (co (cv x0) c1 caddc) (cneg (cv x4)) cexp) cmul)) (csu cz (λ x4 . co (cfv (cneg (cv x4)) (cv x3)) (co (co (cv x0) c1 caddc) (cneg (cv x4)) cexp) cmul)) clt)))))) (cmpt (λ x2 . cv x1) (λ x2 . cif (wceq (cv x2) (cxp cz (csn cc0))) cc0 (co (cv x0) (cneg (csup (cima (ccnv (cv x2)) (cdif cz (csn cc0))) cr (ccnv clt))) cexp))) ctng)))
Theorem df_zp : wceq czp (ccom czr cqp)
Theorem df_qpa : wceq cqpa (cmpt (λ x0 . cprime) (λ x0 . csb (cfv (cv x0) cqp) (λ x1 . co (cv x1) (cmpt (λ x2 . cn) (λ x2 . crab (λ x3 . wa (wbr (co (cv x1) (cv x3) cdg1) (cv x2) cle) (wral (λ x4 . wss (cima (ccnv (cv x4)) (cdif cz (csn cc0))) (co cc0 (cv x2) cfz)) (λ x4 . crn (cfv (cv x3) cco1)))) (λ x3 . cfv (cv x1) cpl1))) cpsl)))
Theorem df_cp : wceq ccp (ccom ccpms cqpa)
Theorem df_trpred : ∀ x0 x1 x2 : ι → ο . wceq (ctrpred x0 x1 x2) (cuni (crn (cres (crdg (cmpt (λ x3 . cvv) (λ x3 . ciun (λ x4 . cv x3) (λ x4 . cpred x0 x1 (cv x4)))) (cpred x0 x1 x2)) com)))
Theorem df_wsuc : ∀ x0 x1 x2 : ι → ο . wceq (cwsuc x0 x1 x2) (cinf (cpred x0 (ccnv x1) x2) x0 x1)
Theorem df_wlim : ∀ x0 x1 : ι → ο . wceq (cwlim x0 x1) (crab (λ x2 . wa (wne (cv x2) (cinf x0 x0 x1)) (wceq (cv x2) (csup (cpred x0 x1 (cv x2)) x0 x1))) (λ x2 . x0))
Theorem df_frecs : ∀ x0 x1 x2 : ι → ο . wceq (cfrecs x0 x1 x2) (cuni (cab (λ x3 . wex (λ x4 . w3a (wfn (cv x3) (cv x4)) (wa (wss (cv x4) x0) (wral (λ x5 . wss (cpred x0 x1 (cv x5)) (cv x4)) (λ x5 . cv x4))) (wral (λ x5 . wceq (cfv (cv x5) (cv x3)) (co (cv x5) (cres (cv x3) (cpred x0 x1 (cv x5))) x2)) (λ x5 . cv x4))))))
Theorem df_no : wceq csur (cab (λ x0 . wrex (λ x1 . wf (cv x1) (cpr c1o c2o) (cv x0)) (λ x1 . con0)))
Theorem df_slt : wceq cslt (copab (λ x0 x1 . wa (wa (wcel (cv x0) csur) (wcel (cv x1) csur)) (wrex (λ x2 . wa (wral (λ x3 . wceq (cfv (cv x3) (cv x0)) (cfv (cv x3) (cv x1))) (λ x3 . cv x2)) (wbr (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) (ctp (cop c1o c0) (cop c1o c2o) (cop c0 c2o)))) (λ x2 . con0))))
Theorem df_bday : wceq cbday (cmpt (λ x0 . csur) (λ x0 . cdm (cv x0)))
Theorem df_sle : wceq csle (cdif (cxp csur csur) (ccnv cslt))