Proofgold Address

Known df_vrgp__df_cmn__df_abl__df_cyg__df_dprd__df_dpj__df_mgp__df_ur__df_srg__df_ring__df_cring__df_oppr__df_dvdsr__df_unit__df_irred__df_invr__df_dvr__df_rprm : ∀ x0 : ο . (wceq cvrgp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cv x1) (λ x2 . cec (cs1 (cop (cv x2) c0)) (cfv (cv x1) cefg)))) ⟶ wceq ccmn (crab (λ x1 . wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x1) cplusg)) (co (cv x3) (cv x2) (cfv (cv x1) cplusg))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)) (λ x1 . cmnd)) ⟶ wceq cabl (cin cgrp ccmn) ⟶ wceq ccyg (crab (λ x1 . wrex (λ x2 . wceq (crn (cmpt (λ x3 . cz) (λ x3 . co (cv x3) (cv x2) (cfv (cv x1) cmg)))) (cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)) (λ x1 . cgrp)) ⟶ wceq cdprd (cmpt2 (λ x1 x2 . cgrp) (λ x1 x2 . cab (λ x3 . wa (wf (cdm (cv x3)) (cfv (cv x1) csubg) (cv x3)) (wral (λ x4 . wa (wral (λ x5 . wss (cfv (cv x4) (cv x3)) (cfv (cfv (cv x5) (cv x3)) (cfv (cv x1) ccntz))) (λ x5 . cdif (cdm (cv x3)) (csn (cv x4)))) (wceq (cin (cfv (cv x4) (cv x3)) (cfv (cuni (cima (cv x3) (cdif (cdm (cv x3)) (csn (cv x4))))) (cfv (cfv (cv x1) csubg) cmrc))) (csn (cfv (cv x1) c0g)))) (λ x4 . cdm (cv x3))))) (λ x1 x2 . crn (cmpt (λ x3 . crab (λ x4 . wbr (cv x4) (cfv (cv x1) c0g) cfsupp) (λ x4 . cixp (λ x5 . cdm (cv x2)) (λ x5 . cfv (cv x5) (cv x2)))) (λ x3 . co (cv x1) (cv x3) cgsu)))) ⟶ wceq cdpj (cmpt2 (λ x1 x2 . cgrp) (λ x1 x2 . cima (cdm cdprd) (csn (cv x1))) (λ x1 x2 . cmpt (λ x3 . cdm (cv x2)) (λ x3 . co (cfv (cv x3) (cv x2)) (co (cv x1) (cres (cv x2) (cdif (cdm (cv x2)) (csn (cv x3)))) cdprd) (cfv (cv x1) cpj1)))) ⟶ wceq cmgp (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (cop (cfv cnx cplusg) (cfv (cv x1) cmulr)) csts)) ⟶ wceq cur (ccom c0g cmgp) ⟶ wceq csrg (crab (λ x1 . wa (wcel (cfv (cv x1) cmgp) cmnd) (wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wral (λ x6 . wa (wral (λ x7 . wral (λ x8 . wa (wceq (co (cv x6) (co (cv x7) (cv x8) (cv x3)) (cv x4)) (co (co (cv x6) (cv x7) (cv x4)) (co (cv x6) (cv x8) (cv x4)) (cv x3))) (wceq (co (co (cv x6) (cv x7) (cv x3)) (cv x8) (cv x4)) (co (co (cv x6) (cv x8) (cv x4)) (co (cv x7) (cv x8) (cv x4)) (cv x3)))) (λ x8 . cv x2)) (λ x7 . cv x2)) (wa (wceq (co (cv x5) (cv x6) (cv x4)) (cv x5)) (wceq (co (cv x6) (cv x5) (cv x4)) (cv x5)))) (λ x6 . cv x2)) (cfv (cv x1) c0g)) (cfv (cv x1) cmulr)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs))) (λ x1 . ccmn)) ⟶ wceq crg (crab (λ x1 . wa (wcel (cfv (cv x1) cmgp) cmnd) (wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wa (wceq (co (cv x5) (co (cv x6) (cv x7) (cv x3)) (cv x4)) (co (co (cv x5) (cv x6) (cv x4)) (co (cv x5) (cv x7) (cv x4)) (cv x3))) (wceq (co (co (cv x5) (cv x6) (cv x3)) (cv x7) (cv x4)) (co (co (cv x5) (cv x7) (cv x4)) (co (cv x6) (cv x7) (cv x4)) (cv x3)))) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (cfv (cv x1) cmulr)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs))) (λ x1 . cgrp)) ⟶ wceq ccrg (crab (λ x1 . wcel (cfv (cv x1) cmgp) ccmn) (λ x1 . crg)) ⟶ wceq coppr (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (cop (cfv cnx cmulr) (ctpos (cfv (cv x1) cmulr))) csts)) ⟶ wceq cdsr (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wcel (cv x2) (cfv (cv x1) cbs)) (wrex (λ x4 . wceq (co (cv x4) (cv x2) (cfv (cv x1) cmulr)) (cv x3)) (λ x4 . cfv (cv x1) cbs))))) ⟶ wceq cui (cmpt (λ x1 . cvv) (λ x1 . cima (ccnv (cin (cfv (cv x1) cdsr) (cfv (cfv (cv x1) coppr) cdsr))) (csn (cfv (cv x1) cur)))) ⟶ wceq cir (cmpt (λ x1 . cvv) (λ x1 . csb (cdif (cfv (cv x1) cbs) (cfv (cv x1) cui)) (λ x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wne (co (cv x4) (cv x5) (cfv (cv x1) cmulr)) (cv x3)) (λ x5 . cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2)))) ⟶ wceq cinvr (cmpt (λ x1 . cvv) (λ x1 . cfv (co (cfv (cv x1) cmgp) (cfv (cv x1) cui) cress) cminusg)) ⟶ wceq cdvr (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cui) (λ x2 x3 . co (cv x2) (cfv (cv x3) (cfv (cv x1) cinvr)) (cfv (cv x1) cmulr)))) ⟶ wceq crpm (cmpt (λ x1 . cvv) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wsbc (λ x6 . wbr (cv x3) (co (cv x4) (cv x5) (cfv (cv x1) cmulr)) (cv x6) ⟶ wo (wbr (cv x3) (cv x4) (cv x6)) (wbr (cv x3) (cv x5) (cv x6))) (cfv (cv x1) cdsr)) (λ x5 . cv x2)) (λ x4 . cv x2)) (λ x3 . cdif (cv x2) (cun (cfv (cv x1) cui) (csn (cfv (cv x1) c0g))))))) ⟶ x0) ⟶ x0
Theorem df_vrgp : wceq cvrgp (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cv x0) (λ x1 . cec (cs1 (cop (cv x1) c0)) (cfv (cv x0) cefg)))) (proof)
Theorem df_cmn : wceq ccmn (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cfv (cv x0) cplusg)) (co (cv x2) (cv x1) (cfv (cv x0) cplusg))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cmnd)) (proof)
Theorem df_abl : wceq cabl (cin cgrp ccmn) (proof)
Theorem df_cyg : wceq ccyg (crab (λ x0 . wrex (λ x1 . wceq (crn (cmpt (λ x2 . cz) (λ x2 . co (cv x2) (cv x1) (cfv (cv x0) cmg)))) (cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cgrp)) (proof)
Theorem df_dprd : wceq cdprd (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cab (λ x2 . wa (wf (cdm (cv x2)) (cfv (cv x0) csubg) (cv x2)) (wral (λ x3 . wa (wral (λ x4 . wss (cfv (cv x3) (cv x2)) (cfv (cfv (cv x4) (cv x2)) (cfv (cv x0) ccntz))) (λ x4 . cdif (cdm (cv x2)) (csn (cv x3)))) (wceq (cin (cfv (cv x3) (cv x2)) (cfv (cuni (cima (cv x2) (cdif (cdm (cv x2)) (csn (cv x3))))) (cfv (cfv (cv x0) csubg) cmrc))) (csn (cfv (cv x0) c0g)))) (λ x3 . cdm (cv x2))))) (λ x0 x1 . crn (cmpt (λ x2 . crab (λ x3 . wbr (cv x3) (cfv (cv x0) c0g) cfsupp) (λ x3 . cixp (λ x4 . cdm (cv x1)) (λ x4 . cfv (cv x4) (cv x1)))) (λ x2 . co (cv x0) (cv x2) cgsu)))) (proof)
Theorem df_dpj : wceq cdpj (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cima (cdm cdprd) (csn (cv x0))) (λ x0 x1 . cmpt (λ x2 . cdm (cv x1)) (λ x2 . co (cfv (cv x2) (cv x1)) (co (cv x0) (cres (cv x1) (cdif (cdm (cv x1)) (csn (cv x2)))) cdprd) (cfv (cv x0) cpj1)))) (proof)
Theorem df_mgp : wceq cmgp (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cop (cfv cnx cplusg) (cfv (cv x0) cmulr)) csts)) (proof)
Theorem df_ur : wceq cur (ccom c0g cmgp) (proof)
Theorem df_srg : wceq csrg (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) cmnd) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wa (wral (λ x6 . wral (λ x7 . wa (wceq (co (cv x5) (co (cv x6) (cv x7) (cv x2)) (cv x3)) (co (co (cv x5) (cv x6) (cv x3)) (co (cv x5) (cv x7) (cv x3)) (cv x2))) (wceq (co (co (cv x5) (cv x6) (cv x2)) (cv x7) (cv x3)) (co (co (cv x5) (cv x7) (cv x3)) (co (cv x6) (cv x7) (cv x3)) (cv x2)))) (λ x7 . cv x1)) (λ x6 . cv x1)) (wa (wceq (co (cv x4) (cv x5) (cv x3)) (cv x4)) (wceq (co (cv x5) (cv x4) (cv x3)) (cv x4)))) (λ x5 . cv x1)) (cfv (cv x0) c0g)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . ccmn)) (proof)
Theorem df_ring : wceq crg (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) cmnd) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wa (wceq (co (cv x4) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (co (co (cv x4) (cv x5) (cv x3)) (co (cv x4) (cv x6) (cv x3)) (cv x2))) (wceq (co (co (cv x4) (cv x5) (cv x2)) (cv x6) (cv x3)) (co (co (cv x4) (cv x6) (cv x3)) (co (cv x5) (cv x6) (cv x3)) (cv x2)))) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . cgrp)) (proof)
Theorem df_cring : wceq ccrg (crab (λ x0 . wcel (cfv (cv x0) cmgp) ccmn) (λ x0 . crg)) (proof)
Theorem df_oppr : wceq coppr (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cop (cfv cnx cmulr) (ctpos (cfv (cv x0) cmulr))) csts)) (proof)
Theorem df_dvdsr : wceq cdsr (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wcel (cv x1) (cfv (cv x0) cbs)) (wrex (λ x3 . wceq (co (cv x3) (cv x1) (cfv (cv x0) cmulr)) (cv x2)) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_unit : wceq cui (cmpt (λ x0 . cvv) (λ x0 . cima (ccnv (cin (cfv (cv x0) cdsr) (cfv (cfv (cv x0) coppr) cdsr))) (csn (cfv (cv x0) cur)))) (proof)
Theorem df_irred : wceq cir (cmpt (λ x0 . cvv) (λ x0 . csb (cdif (cfv (cv x0) cbs) (cfv (cv x0) cui)) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wne (co (cv x3) (cv x4) (cfv (cv x0) cmulr)) (cv x2)) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)))) (proof)
Theorem df_invr : wceq cinvr (cmpt (λ x0 . cvv) (λ x0 . cfv (co (cfv (cv x0) cmgp) (cfv (cv x0) cui) cress) cminusg)) (proof)
Theorem df_dvr : wceq cdvr (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cui) (λ x1 x2 . co (cv x1) (cfv (cv x2) (cfv (cv x0) cinvr)) (cfv (cv x0) cmulr)))) (proof)
Theorem df_rprm : wceq crpm (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wsbc (λ x5 . wbr (cv x2) (co (cv x3) (cv x4) (cfv (cv x0) cmulr)) (cv x5) ⟶ wo (wbr (cv x2) (cv x3) (cv x5)) (wbr (cv x2) (cv x4) (cv x5))) (cfv (cv x0) cdsr)) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cdif (cv x1) (cun (cfv (cv x0) cui) (csn (cfv (cv x0) c0g))))))) (proof)