Proofgold Address

Known df_nrg__df_nlm__df_nvc__df_nmo__df_nghm__df_nmhm__df_ii__df_cncf__df_htpy__df_phtpy__df_phtpc__df_pco__df_om1__df_omn__df_pi1__df_pin__df_clm__df_cvs : ∀ x0 : ο . (wceq cnrg (crab (λ x1 . wcel (cfv (cv x1) cnm) (cfv (cv x1) cabv)) (λ x1 . cngp)) ⟶ wceq cnlm (crab (λ x1 . wsbc (λ x2 . wa (wcel (cv x2) cnrg) (wral (λ x3 . wral (λ x4 . wceq (cfv (co (cv x3) (cv x4) (cfv (cv x1) cvsca)) (cfv (cv x1) cnm)) (co (cfv (cv x3) (cfv (cv x2) cnm)) (cfv (cv x4) (cfv (cv x1) cnm)) cmul)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x2) cbs))) (cfv (cv x1) csca)) (λ x1 . cin cngp clmod)) ⟶ wceq cnvc (cin cnlm clvec) ⟶ wceq cnmo (cmpt2 (λ x1 x2 . cngp) (λ x1 x2 . cngp) (λ x1 x2 . cmpt (λ x3 . co (cv x1) (cv x2) cghm) (λ x3 . cinf (crab (λ x4 . wral (λ x5 . wbr (cfv (cfv (cv x5) (cv x3)) (cfv (cv x2) cnm)) (co (cv x4) (cfv (cv x5) (cfv (cv x1) cnm)) cmul) cle) (λ x5 . cfv (cv x1) cbs)) (λ x4 . co cc0 cpnf cico)) cxr clt))) ⟶ wceq cnghm (cmpt2 (λ x1 x2 . cngp) (λ x1 x2 . cngp) (λ x1 x2 . cima (ccnv (co (cv x1) (cv x2) cnmo)) cr)) ⟶ wceq cnmhm (cmpt2 (λ x1 x2 . cnlm) (λ x1 x2 . cnlm) (λ x1 x2 . cin (co (cv x1) (cv x2) clmhm) (co (cv x1) (cv x2) cnghm))) ⟶ wceq cii (cfv (cres (ccom cabs cmin) (cxp (co cc0 c1 cicc) (co cc0 c1 cicc))) cmopn) ⟶ wceq ccncf (cmpt2 (λ x1 x2 . cpw cc) (λ x1 x2 . cpw cc) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wrex (λ x6 . wral (λ x7 . wbr (cfv (co (cv x4) (cv x7) cmin) cabs) (cv x6) clt ⟶ wbr (cfv (co (cfv (cv x4) (cv x3)) (cfv (cv x7) (cv x3)) cmin) cabs) (cv x5) clt) (λ x7 . cv x1)) (λ x6 . crp)) (λ x5 . crp)) (λ x4 . cv x1)) (λ x3 . co (cv x2) (cv x1) cmap))) ⟶ wceq chtpy (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . cmpt2 (λ x3 x4 . co (cv x1) (cv x2) ccn) (λ x3 x4 . co (cv x1) (cv x2) ccn) (λ x3 x4 . crab (λ x5 . wral (λ x6 . wa (wceq (co (cv x6) cc0 (cv x5)) (cfv (cv x6) (cv x3))) (wceq (co (cv x6) c1 (cv x5)) (cfv (cv x6) (cv x4)))) (λ x6 . cuni (cv x1))) (λ x5 . co (co (cv x1) cii ctx) (cv x2) ccn)))) ⟶ wceq cphtpy (cmpt (λ x1 . ctop) (λ x1 . cmpt2 (λ x2 x3 . co cii (cv x1) ccn) (λ x2 x3 . co cii (cv x1) ccn) (λ x2 x3 . crab (λ x4 . wral (λ x5 . wa (wceq (co cc0 (cv x5) (cv x4)) (cfv cc0 (cv x2))) (wceq (co c1 (cv x5) (cv x4)) (cfv c1 (cv x2)))) (λ x5 . co cc0 c1 cicc)) (λ x4 . co (cv x2) (cv x3) (co cii (cv x1) chtpy))))) ⟶ wceq cphtpc (cmpt (λ x1 . ctop) (λ x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (co cii (cv x1) ccn)) (wne (co (cv x2) (cv x3) (cfv (cv x1) cphtpy)) c0)))) ⟶ wceq cpco (cmpt (λ x1 . ctop) (λ x1 . cmpt2 (λ x2 x3 . co cii (cv x1) ccn) (λ x2 x3 . co cii (cv x1) ccn) (λ x2 x3 . cmpt (λ x4 . co cc0 c1 cicc) (λ x4 . cif (wbr (cv x4) (co c1 c2 cdiv) cle) (cfv (co c2 (cv x4) cmul) (cv x2)) (cfv (co (co c2 (cv x4) cmul) c1 cmin) (cv x3)))))) ⟶ wceq comi (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (cv x1)) (λ x1 x2 . ctp (cop (cfv cnx cbs) (crab (λ x3 . wa (wceq (cfv cc0 (cv x3)) (cv x2)) (wceq (cfv c1 (cv x3)) (cv x2))) (λ x3 . co cii (cv x1) ccn))) (cop (cfv cnx cplusg) (cfv (cv x1) cpco)) (cop (cfv cnx cts) (co (cv x1) cii cxko)))) ⟶ wceq comn (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (cv x1)) (λ x1 x2 . cseq (ccom (cmpt2 (λ x3 x4 . cvv) (λ x3 x4 . cvv) (λ x3 x4 . cop (co (cfv (cfv (cv x3) c1st) ctopn) (cfv (cv x3) c2nd) comi) (cxp (co cc0 c1 cicc) (csn (cfv (cv x3) c2nd))))) c1st) (cop (cpr (cop (cfv cnx cbs) (cuni (cv x1))) (cop (cfv cnx cts) (cv x1))) (cv x2)) cc0)) ⟶ wceq cpi1 (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (cv x1)) (λ x1 x2 . co (co (cv x1) (cv x2) comi) (cfv (cv x1) cphtpc) cqus)) ⟶ wceq cpin (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (cv x1)) (λ x1 x2 . cmpt (λ x3 . cn0) (λ x3 . co (cfv (cfv (cv x3) (co (cv x1) (cv x2) comn)) c1st) (cif (wceq (cv x3) cc0) (copab (λ x4 x5 . wrex (λ x6 . wa (wceq (cfv cc0 (cv x6)) (cv x4)) (wceq (cfv c1 (cv x6)) (cv x5))) (λ x6 . co cii (cv x1) ccn))) (cfv (cfv (cfv (cfv (co (cv x3) c1 cmin) (co (cv x1) (cv x2) comn)) c1st) ctopn) cphtpc)) cqus))) ⟶ wceq cclm (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wceq (cv x2) (co ccnfld (cv x3) cress)) (wcel (cv x3) (cfv ccnfld csubrg))) (cfv (cv x2) cbs)) (cfv (cv x1) csca)) (λ x1 . clmod)) ⟶ wceq ccvs (cin cclm clvec) ⟶ x0) ⟶ x0
Theorem df_nrg : wceq cnrg (crab (λ x0 . wcel (cfv (cv x0) cnm) (cfv (cv x0) cabv)) (λ x0 . cngp)) (proof)
Theorem df_nlm : wceq cnlm (crab (λ x0 . wsbc (λ x1 . wa (wcel (cv x1) cnrg) (wral (λ x2 . wral (λ x3 . wceq (cfv (co (cv x2) (cv x3) (cfv (cv x0) cvsca)) (cfv (cv x0) cnm)) (co (cfv (cv x2) (cfv (cv x1) cnm)) (cfv (cv x3) (cfv (cv x0) cnm)) cmul)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x1) cbs))) (cfv (cv x0) csca)) (λ x0 . cin cngp clmod)) (proof)
Theorem df_nvc : wceq cnvc (cin cnlm clvec) (proof)
Theorem df_nmo : wceq cnmo (cmpt2 (λ x0 x1 . cngp) (λ x0 x1 . cngp) (λ x0 x1 . cmpt (λ x2 . co (cv x0) (cv x1) cghm) (λ x2 . cinf (crab (λ x3 . wral (λ x4 . wbr (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) cnm)) (co (cv x3) (cfv (cv x4) (cfv (cv x0) cnm)) cmul) cle) (λ x4 . cfv (cv x0) cbs)) (λ x3 . co cc0 cpnf cico)) cxr clt))) (proof)
Theorem df_nghm : wceq cnghm (cmpt2 (λ x0 x1 . cngp) (λ x0 x1 . cngp) (λ x0 x1 . cima (ccnv (co (cv x0) (cv x1) cnmo)) cr)) (proof)
Theorem df_nmhm : wceq cnmhm (cmpt2 (λ x0 x1 . cnlm) (λ x0 x1 . cnlm) (λ x0 x1 . cin (co (cv x0) (cv x1) clmhm) (co (cv x0) (cv x1) cnghm))) (proof)
Theorem df_ii : wceq cii (cfv (cres (ccom cabs cmin) (cxp (co cc0 c1 cicc) (co cc0 c1 cicc))) cmopn) (proof)
Theorem df_cncf : wceq ccncf (cmpt2 (λ x0 x1 . cpw cc) (λ x0 x1 . cpw cc) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . wbr (cfv (co (cv x3) (cv x6) cmin) cabs) (cv x5) clt ⟶ wbr (cfv (co (cfv (cv x3) (cv x2)) (cfv (cv x6) (cv x2)) cmin) cabs) (cv x4) clt) (λ x6 . cv x0)) (λ x5 . crp)) (λ x4 . crp)) (λ x3 . cv x0)) (λ x2 . co (cv x1) (cv x0) cmap))) (proof)
Theorem df_htpy : wceq chtpy (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cmpt2 (λ x2 x3 . co (cv x0) (cv x1) ccn) (λ x2 x3 . co (cv x0) (cv x1) ccn) (λ x2 x3 . crab (λ x4 . wral (λ x5 . wa (wceq (co (cv x5) cc0 (cv x4)) (cfv (cv x5) (cv x2))) (wceq (co (cv x5) c1 (cv x4)) (cfv (cv x5) (cv x3)))) (λ x5 . cuni (cv x0))) (λ x4 . co (co (cv x0) cii ctx) (cv x1) ccn)))) (proof)
Theorem df_phtpy : wceq cphtpy (cmpt (λ x0 . ctop) (λ x0 . cmpt2 (λ x1 x2 . co cii (cv x0) ccn) (λ x1 x2 . co cii (cv x0) ccn) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wa (wceq (co cc0 (cv x4) (cv x3)) (cfv cc0 (cv x1))) (wceq (co c1 (cv x4) (cv x3)) (cfv c1 (cv x1)))) (λ x4 . co cc0 c1 cicc)) (λ x3 . co (cv x1) (cv x2) (co cii (cv x0) chtpy))))) (proof)
Theorem df_phtpc : wceq cphtpc (cmpt (λ x0 . ctop) (λ x0 . copab (λ x1 x2 . wa (wss (cpr (cv x1) (cv x2)) (co cii (cv x0) ccn)) (wne (co (cv x1) (cv x2) (cfv (cv x0) cphtpy)) c0)))) (proof)
Theorem df_pco : wceq cpco (cmpt (λ x0 . ctop) (λ x0 . cmpt2 (λ x1 x2 . co cii (cv x0) ccn) (λ x1 x2 . co cii (cv x0) ccn) (λ x1 x2 . cmpt (λ x3 . co cc0 c1 cicc) (λ x3 . cif (wbr (cv x3) (co c1 c2 cdiv) cle) (cfv (co c2 (cv x3) cmul) (cv x1)) (cfv (co (co c2 (cv x3) cmul) c1 cmin) (cv x2)))))) (proof)
Theorem df_om1 : wceq comi (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (cv x0)) (λ x0 x1 . ctp (cop (cfv cnx cbs) (crab (λ x2 . wa (wceq (cfv cc0 (cv x2)) (cv x1)) (wceq (cfv c1 (cv x2)) (cv x1))) (λ x2 . co cii (cv x0) ccn))) (cop (cfv cnx cplusg) (cfv (cv x0) cpco)) (cop (cfv cnx cts) (co (cv x0) cii cxko)))) (proof)
Theorem df_omn : wceq comn (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (cv x0)) (λ x0 x1 . cseq (ccom (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . cop (co (cfv (cfv (cv x2) c1st) ctopn) (cfv (cv x2) c2nd) comi) (cxp (co cc0 c1 cicc) (csn (cfv (cv x2) c2nd))))) c1st) (cop (cpr (cop (cfv cnx cbs) (cuni (cv x0))) (cop (cfv cnx cts) (cv x0))) (cv x1)) cc0)) (proof)
Theorem df_pi1 : wceq cpi1 (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (cv x0)) (λ x0 x1 . co (co (cv x0) (cv x1) comi) (cfv (cv x0) cphtpc) cqus)) (proof)
Theorem df_pin : wceq cpin (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (cv x0)) (λ x0 x1 . cmpt (λ x2 . cn0) (λ x2 . co (cfv (cfv (cv x2) (co (cv x0) (cv x1) comn)) c1st) (cif (wceq (cv x2) cc0) (copab (λ x3 x4 . wrex (λ x5 . wa (wceq (cfv cc0 (cv x5)) (cv x3)) (wceq (cfv c1 (cv x5)) (cv x4))) (λ x5 . co cii (cv x0) ccn))) (cfv (cfv (cfv (cfv (co (cv x2) c1 cmin) (co (cv x0) (cv x1) comn)) c1st) ctopn) cphtpc)) cqus))) (proof)
Theorem df_clm : wceq cclm (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wa (wceq (cv x1) (co ccnfld (cv x2) cress)) (wcel (cv x2) (cfv ccnfld csubrg))) (cfv (cv x1) cbs)) (cfv (cv x0) csca)) (λ x0 . clmod)) (proof)
Theorem df_cvs : wceq ccvs (cin cclm clvec) (proof)