Proofgold Address

Known df_met__df_bl__df_mopn__df_fbas__df_fg__df_metu__df_cnfld__df_zring__df_zrh__df_zlm__df_chr__df_zn__df_refld__df_phl__df_ipf__df_ocv__df_css__df_thl : ∀ x0 : ο . (wceq cme (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)) caddc) cle) (λ x5 . cv x1))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . co cr (cxp (cv x1) (cv x1)) cmap))) ⟶ wceq cbl (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cdm (cdm (cv x1))) (λ x2 x3 . cxr) (λ x2 x3 . crab (λ x4 . wbr (co (cv x2) (cv x4) (cv x1)) (cv x3) clt) (λ x4 . cdm (cdm (cv x1)))))) ⟶ wceq cmopn (cmpt (λ x1 . cuni (crn cxmt)) (λ x1 . cfv (crn (cfv (cv x1) cbl)) ctg)) ⟶ wceq cfbas (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . w3a (wne (cv x2) c0) (wnel c0 (cv x2)) (wral (λ x3 . wral (λ x4 . wne (cin (cv x2) (cpw (cin (cv x3) (cv x4)))) c0) (λ x4 . cv x2)) (λ x3 . cv x2))) (λ x2 . cpw (cpw (cv x1))))) ⟶ wceq cfg (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cfv (cv x1) cfbas) (λ x1 x2 . crab (λ x3 . wne (cin (cv x2) (cpw (cv x3))) c0) (λ x3 . cpw (cv x1)))) ⟶ wceq cmetu (cmpt (λ x1 . cuni (crn cpsmet)) (λ x1 . co (cxp (cdm (cdm (cv x1))) (cdm (cdm (cv x1)))) (crn (cmpt (λ x2 . crp) (λ x2 . cima (ccnv (cv x1)) (co cc0 (cv x2) cico)))) cfg)) ⟶ wceq ccnfld (cun (cun (ctp (cop (cfv cnx cbs) cc) (cop (cfv cnx cplusg) caddc) (cop (cfv cnx cmulr) cmul)) (csn (cop (cfv cnx cstv) ccj))) (cun (ctp (cop (cfv cnx cts) (cfv (ccom cabs cmin) cmopn)) (cop (cfv cnx cple) cle) (cop (cfv cnx cds) (ccom cabs cmin))) (csn (cop (cfv cnx cunif) (cfv (ccom cabs cmin) cmetu))))) ⟶ wceq zring (co ccnfld cz cress) ⟶ wceq czrh (cmpt (λ x1 . cvv) (λ x1 . cuni (co zring (cv x1) crh))) ⟶ wceq czlm (cmpt (λ x1 . cvv) (λ x1 . co (co (cv x1) (cop (cfv cnx csca) zring) csts) (cop (cfv cnx cvsca) (cfv (cv x1) cmg)) csts)) ⟶ wceq cchr (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cv x1) cur) (cfv (cv x1) cod))) ⟶ wceq czn (cmpt (λ x1 . cn0) (λ x1 . csb zring (λ x2 . csb (co (cv x2) (co (cv x2) (cfv (csn (cv x1)) (cfv (cv x2) crsp)) cqg) cqus) (λ x3 . co (cv x3) (cop (cfv cnx cple) (csb (cres (cfv (cv x3) czrh) (cif (wceq (cv x1) cc0) cz (co cc0 (cv x1) cfzo))) (λ x4 . ccom (ccom (cv x4) cle) (ccnv (cv x4))))) csts)))) ⟶ wceq crefld (co ccnfld cr cress) ⟶ wceq cphl (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wcel (cv x4) csr) (wral (λ x5 . w3a (wcel (cmpt (λ x6 . cv x2) (λ x6 . co (cv x6) (cv x5) (cv x3))) (co (cv x1) (cfv (cv x4) crglmod) clmhm)) (wceq (co (cv x5) (cv x5) (cv x3)) (cfv (cv x4) c0g) ⟶ wceq (cv x5) (cfv (cv x1) c0g)) (wral (λ x6 . wceq (cfv (co (cv x5) (cv x6) (cv x3)) (cfv (cv x4) cstv)) (co (cv x6) (cv x5) (cv x3))) (λ x6 . cv x2))) (λ x5 . cv x2))) (cfv (cv x1) csca)) (cfv (cv x1) cip)) (cfv (cv x1) cbs)) (λ x1 . clvec)) ⟶ wceq cipf (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . co (cv x2) (cv x3) (cfv (cv x1) cip)))) ⟶ wceq cocv (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . crab (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cfv (cv x1) cip)) (cfv (cfv (cv x1) csca) c0g)) (λ x4 . cv x2)) (λ x3 . cfv (cv x1) cbs)))) ⟶ wceq ccss (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wceq (cv x2) (cfv (cfv (cv x2) (cfv (cv x1) cocv)) (cfv (cv x1) cocv))))) ⟶ wceq cthl (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cfv (cv x1) ccss) cipo) (cop (cfv cnx coc) (cfv (cv x1) cocv)) csts)) ⟶ x0) ⟶ x0
Theorem df_met : wceq cme (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)) caddc) cle) (λ x4 . cv x0))) (λ x3 . cv x0)) (λ x2 . cv x0)) (λ x1 . co cr (cxp (cv x0) (cv x0)) cmap))) (proof)
Theorem df_bl : wceq cbl (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cdm (cdm (cv x0))) (λ x1 x2 . cxr) (λ x1 x2 . crab (λ x3 . wbr (co (cv x1) (cv x3) (cv x0)) (cv x2) clt) (λ x3 . cdm (cdm (cv x0)))))) (proof)
Theorem df_mopn : wceq cmopn (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . cfv (crn (cfv (cv x0) cbl)) ctg)) (proof)
Theorem df_fbas : wceq cfbas (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . w3a (wne (cv x1) c0) (wnel c0 (cv x1)) (wral (λ x2 . wral (λ x3 . wne (cin (cv x1) (cpw (cin (cv x2) (cv x3)))) c0) (λ x3 . cv x1)) (λ x2 . cv x1))) (λ x1 . cpw (cpw (cv x0))))) (proof)
Theorem df_fg : wceq cfg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cfv (cv x0) cfbas) (λ x0 x1 . crab (λ x2 . wne (cin (cv x1) (cpw (cv x2))) c0) (λ x2 . cpw (cv x0)))) (proof)
Theorem df_metu : wceq cmetu (cmpt (λ x0 . cuni (crn cpsmet)) (λ x0 . co (cxp (cdm (cdm (cv x0))) (cdm (cdm (cv x0)))) (crn (cmpt (λ x1 . crp) (λ x1 . cima (ccnv (cv x0)) (co cc0 (cv x1) cico)))) cfg)) (proof)
Theorem df_cnfld : wceq ccnfld (cun (cun (ctp (cop (cfv cnx cbs) cc) (cop (cfv cnx cplusg) caddc) (cop (cfv cnx cmulr) cmul)) (csn (cop (cfv cnx cstv) ccj))) (cun (ctp (cop (cfv cnx cts) (cfv (ccom cabs cmin) cmopn)) (cop (cfv cnx cple) cle) (cop (cfv cnx cds) (ccom cabs cmin))) (csn (cop (cfv cnx cunif) (cfv (ccom cabs cmin) cmetu))))) (proof)
Theorem df_zring : wceq zring (co ccnfld cz cress) (proof)
Theorem df_zrh : wceq czrh (cmpt (λ x0 . cvv) (λ x0 . cuni (co zring (cv x0) crh))) (proof)
Theorem df_zlm : wceq czlm (cmpt (λ x0 . cvv) (λ x0 . co (co (cv x0) (cop (cfv cnx csca) zring) csts) (cop (cfv cnx cvsca) (cfv (cv x0) cmg)) csts)) (proof)
Theorem df_chr : wceq cchr (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cur) (cfv (cv x0) cod))) (proof)
Theorem df_zn : wceq czn (cmpt (λ x0 . cn0) (λ x0 . csb zring (λ x1 . csb (co (cv x1) (co (cv x1) (cfv (csn (cv x0)) (cfv (cv x1) crsp)) cqg) cqus) (λ x2 . co (cv x2) (cop (cfv cnx cple) (csb (cres (cfv (cv x2) czrh) (cif (wceq (cv x0) cc0) cz (co cc0 (cv x0) cfzo))) (λ x3 . ccom (ccom (cv x3) cle) (ccnv (cv x3))))) csts)))) (proof)
Theorem df_refld : wceq crefld (co ccnfld cr cress) (proof)
Theorem df_phl : wceq cphl (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wcel (cv x3) csr) (wral (λ x4 . w3a (wcel (cmpt (λ x5 . cv x1) (λ x5 . co (cv x5) (cv x4) (cv x2))) (co (cv x0) (cfv (cv x3) crglmod) clmhm)) (wceq (co (cv x4) (cv x4) (cv x2)) (cfv (cv x3) c0g) ⟶ wceq (cv x4) (cfv (cv x0) c0g)) (wral (λ x5 . wceq (cfv (co (cv x4) (cv x5) (cv x2)) (cfv (cv x3) cstv)) (co (cv x5) (cv x4) (cv x2))) (λ x5 . cv x1))) (λ x4 . cv x1))) (cfv (cv x0) csca)) (cfv (cv x0) cip)) (cfv (cv x0) cbs)) (λ x0 . clvec)) (proof)
Theorem df_ipf : wceq cipf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cv x2) (cfv (cv x0) cip)))) (proof)
Theorem df_ocv : wceq cocv (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x0) cip)) (cfv (cfv (cv x0) csca) c0g)) (λ x3 . cv x1)) (λ x2 . cfv (cv x0) cbs)))) (proof)
Theorem df_css : wceq ccss (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wceq (cv x1) (cfv (cfv (cv x1) (cfv (cv x0) cocv)) (cfv (cv x0) cocv))))) (proof)
Theorem df_thl : wceq cthl (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cfv (cv x0) ccss) cipo) (cop (cfv cnx coc) (cfv (cv x0) cocv)) csts)) (proof)