Proofgold Address

Known df_mndo__df_ghomOLD__df_rngo__df_drngo__df_rngohom__df_rngoiso__df_risc__df_com2__df_fld__df_crngo__df_idl__df_pridl__df_maxidl__df_prrngo__df_dmn__df_igen__df_xrn__df_coss : ∀ x0 : ο . (wceq cmndo (cin csem cexid) ⟶ wceq cghomOLD (cmpt2 (λ x1 x2 . cgr) (λ x1 x2 . cgr) (λ x1 x2 . cab (λ x3 . wa (wf (crn (cv x1)) (crn (cv x2)) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cv x2)) (cfv (co (cv x4) (cv x5) (cv x1)) (cv x3))) (λ x5 . crn (cv x1))) (λ x4 . crn (cv x1)))))) ⟶ wceq crngo (copab (λ x1 x2 . wa (wa (wcel (cv x1) cablo) (wf (cxp (crn (cv x1)) (crn (cv x1))) (crn (cv x1)) (cv x2))) (wa (wral (λ x3 . wral (λ x4 . wral (λ x5 . w3a (wceq (co (co (cv x3) (cv x4) (cv x2)) (cv x5) (cv x2)) (co (cv x3) (co (cv x4) (cv x5) (cv x2)) (cv x2))) (wceq (co (cv x3) (co (cv x4) (cv x5) (cv x1)) (cv x2)) (co (co (cv x3) (cv x4) (cv x2)) (co (cv x3) (cv x5) (cv x2)) (cv x1))) (wceq (co (co (cv x3) (cv x4) (cv x1)) (cv x5) (cv x2)) (co (co (cv x3) (cv x5) (cv x2)) (co (cv x4) (cv x5) (cv x2)) (cv x1)))) (λ x5 . crn (cv x1))) (λ x4 . crn (cv x1))) (λ x3 . crn (cv x1))) (wrex (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cv x2)) (cv x4)) (wceq (co (cv x4) (cv x3) (cv x2)) (cv x4))) (λ x4 . crn (cv x1))) (λ x3 . crn (cv x1)))))) ⟶ wceq cdrng (copab (λ x1 x2 . wa (wcel (cop (cv x1) (cv x2)) crngo) (wcel (cres (cv x2) (cxp (cdif (crn (cv x1)) (csn (cfv (cv x1) cgi))) (cdif (crn (cv x1)) (csn (cfv (cv x1) cgi))))) cgr))) ⟶ wceq crnghom (cmpt2 (λ x1 x2 . crngo) (λ x1 x2 . crngo) (λ x1 x2 . crab (λ x3 . wa (wceq (cfv (cfv (cfv (cv x1) c2nd) cgi) (cv x3)) (cfv (cfv (cv x2) c2nd) cgi)) (wral (λ x4 . wral (λ x5 . wa (wceq (cfv (co (cv x4) (cv x5) (cfv (cv x1) c1st)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x2) c1st))) (wceq (cfv (co (cv x4) (cv x5) (cfv (cv x1) c2nd)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x2) c2nd)))) (λ x5 . crn (cfv (cv x1) c1st))) (λ x4 . crn (cfv (cv x1) c1st)))) (λ x3 . co (crn (cfv (cv x2) c1st)) (crn (cfv (cv x1) c1st)) cmap))) ⟶ wceq crngiso (cmpt2 (λ x1 x2 . crngo) (λ x1 x2 . crngo) (λ x1 x2 . crab (λ x3 . wf1o (crn (cfv (cv x1) c1st)) (crn (cfv (cv x2) c1st)) (cv x3)) (λ x3 . co (cv x1) (cv x2) crnghom))) ⟶ wceq crisc (copab (λ x1 x2 . wa (wa (wcel (cv x1) crngo) (wcel (cv x2) crngo)) (wex (λ x3 . wcel (cv x3) (co (cv x1) (cv x2) crngiso))))) ⟶ wceq ccm2 (copab (λ x1 x2 . wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cv x2)) (co (cv x4) (cv x3) (cv x2))) (λ x4 . crn (cv x1))) (λ x3 . crn (cv x1)))) ⟶ wceq cfld (cin cdrng ccm2) ⟶ wceq ccring (cin crngo ccm2) ⟶ wceq cidl (cmpt (λ x1 . crngo) (λ x1 . crab (λ x2 . wa (wcel (cfv (cfv (cv x1) c1st) cgi) (cv x2)) (wral (λ x3 . wa (wral (λ x4 . wcel (co (cv x3) (cv x4) (cfv (cv x1) c1st)) (cv x2)) (λ x4 . cv x2)) (wral (λ x4 . wa (wcel (co (cv x4) (cv x3) (cfv (cv x1) c2nd)) (cv x2)) (wcel (co (cv x3) (cv x4) (cfv (cv x1) c2nd)) (cv x2))) (λ x4 . crn (cfv (cv x1) c1st)))) (λ x3 . cv x2))) (λ x2 . cpw (crn (cfv (cv x1) c1st))))) ⟶ wceq cpridl (cmpt (λ x1 . crngo) (λ x1 . crab (λ x2 . wa (wne (cv x2) (crn (cfv (cv x1) c1st))) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wcel (co (cv x5) (cv x6) (cfv (cv x1) c2nd)) (cv x2)) (λ x6 . cv x4)) (λ x5 . cv x3) ⟶ wo (wss (cv x3) (cv x2)) (wss (cv x4) (cv x2))) (λ x4 . cfv (cv x1) cidl)) (λ x3 . cfv (cv x1) cidl))) (λ x2 . cfv (cv x1) cidl))) ⟶ wceq cmaxidl (cmpt (λ x1 . crngo) (λ x1 . crab (λ x2 . wa (wne (cv x2) (crn (cfv (cv x1) c1st))) (wral (λ x3 . wss (cv x2) (cv x3) ⟶ wo (wceq (cv x3) (cv x2)) (wceq (cv x3) (crn (cfv (cv x1) c1st)))) (λ x3 . cfv (cv x1) cidl))) (λ x2 . cfv (cv x1) cidl))) ⟶ wceq cprrng (crab (λ x1 . wcel (csn (cfv (cfv (cv x1) c1st) cgi)) (cfv (cv x1) cpridl)) (λ x1 . crngo)) ⟶ wceq cdmn (cin cprrng ccm2) ⟶ wceq cigen (cmpt2 (λ x1 x2 . crngo) (λ x1 x2 . cpw (crn (cfv (cv x1) c1st))) (λ x1 x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) cidl)))) ⟶ (∀ x1 x2 : ι → ο . wceq (cxrn x1 x2) (cin (ccom (ccnv (cres c1st (cxp cvv cvv))) x1) (ccom (ccnv (cres c2nd (cxp cvv cvv))) x2))) ⟶ (∀ x1 : ι → ο . wceq (ccoss x1) (copab (λ x2 x3 . wex (λ x4 . wa (wbr (cv x4) (cv x2) x1) (wbr (cv x4) (cv x3) x1))))) ⟶ x0) ⟶ x0
Theorem df_mndo : wceq cmndo (cin csem cexid) (proof)
Theorem df_ghomOLD : wceq cghomOLD (cmpt2 (λ x0 x1 . cgr) (λ x0 x1 . cgr) (λ x0 x1 . cab (λ x2 . wa (wf (crn (cv x0)) (crn (cv x1)) (cv x2)) (wral (λ x3 . wral (λ x4 . wceq (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cv x1)) (cfv (co (cv x3) (cv x4) (cv x0)) (cv x2))) (λ x4 . crn (cv x0))) (λ x3 . crn (cv x0)))))) (proof)
Theorem df_rngo : wceq crngo (copab (λ x0 x1 . wa (wa (wcel (cv x0) cablo) (wf (cxp (crn (cv x0)) (crn (cv x0))) (crn (cv x0)) (cv x1))) (wa (wral (λ x2 . wral (λ x3 . wral (λ x4 . w3a (wceq (co (co (cv x2) (cv x3) (cv x1)) (cv x4) (cv x1)) (co (cv x2) (co (cv x3) (cv x4) (cv x1)) (cv x1))) (wceq (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x1)) (co (co (cv x2) (cv x3) (cv x1)) (co (cv x2) (cv x4) (cv x1)) (cv x0))) (wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x1)) (co (co (cv x2) (cv x4) (cv x1)) (co (cv x3) (cv x4) (cv x1)) (cv x0)))) (λ x4 . crn (cv x0))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0))) (wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x1)) (cv x3)) (wceq (co (cv x3) (cv x2) (cv x1)) (cv x3))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0)))))) (proof)
Theorem df_drngo : wceq cdrng (copab (λ x0 x1 . wa (wcel (cop (cv x0) (cv x1)) crngo) (wcel (cres (cv x1) (cxp (cdif (crn (cv x0)) (csn (cfv (cv x0) cgi))) (cdif (crn (cv x0)) (csn (cfv (cv x0) cgi))))) cgr))) (proof)
Theorem df_rngohom : wceq crnghom (cmpt2 (λ x0 x1 . crngo) (λ x0 x1 . crngo) (λ x0 x1 . crab (λ x2 . wa (wceq (cfv (cfv (cfv (cv x0) c2nd) cgi) (cv x2)) (cfv (cfv (cv x1) c2nd) cgi)) (wral (λ x3 . wral (λ x4 . wa (wceq (cfv (co (cv x3) (cv x4) (cfv (cv x0) c1st)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) c1st))) (wceq (cfv (co (cv x3) (cv x4) (cfv (cv x0) c2nd)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) c2nd)))) (λ x4 . crn (cfv (cv x0) c1st))) (λ x3 . crn (cfv (cv x0) c1st)))) (λ x2 . co (crn (cfv (cv x1) c1st)) (crn (cfv (cv x0) c1st)) cmap))) (proof)
Theorem df_rngoiso : wceq crngiso (cmpt2 (λ x0 x1 . crngo) (λ x0 x1 . crngo) (λ x0 x1 . crab (λ x2 . wf1o (crn (cfv (cv x0) c1st)) (crn (cfv (cv x1) c1st)) (cv x2)) (λ x2 . co (cv x0) (cv x1) crnghom))) (proof)
Theorem df_risc : wceq crisc (copab (λ x0 x1 . wa (wa (wcel (cv x0) crngo) (wcel (cv x1) crngo)) (wex (λ x2 . wcel (cv x2) (co (cv x0) (cv x1) crngiso))))) (proof)
Theorem df_com2 : wceq ccm2 (copab (λ x0 x1 . wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cv x1)) (co (cv x3) (cv x2) (cv x1))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0)))) (proof)
Theorem df_fld : wceq cfld (cin cdrng ccm2) (proof)
Theorem df_crngo : wceq ccring (cin crngo ccm2) (proof)
Theorem df_idl : wceq cidl (cmpt (λ x0 . crngo) (λ x0 . crab (λ x1 . wa (wcel (cfv (cfv (cv x0) c1st) cgi) (cv x1)) (wral (λ x2 . wa (wral (λ x3 . wcel (co (cv x2) (cv x3) (cfv (cv x0) c1st)) (cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wa (wcel (co (cv x3) (cv x2) (cfv (cv x0) c2nd)) (cv x1)) (wcel (co (cv x2) (cv x3) (cfv (cv x0) c2nd)) (cv x1))) (λ x3 . crn (cfv (cv x0) c1st)))) (λ x2 . cv x1))) (λ x1 . cpw (crn (cfv (cv x0) c1st))))) (proof)
Theorem df_pridl : wceq cpridl (cmpt (λ x0 . crngo) (λ x0 . crab (λ x1 . wa (wne (cv x1) (crn (cfv (cv x0) c1st))) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wcel (co (cv x4) (cv x5) (cfv (cv x0) c2nd)) (cv x1)) (λ x5 . cv x3)) (λ x4 . cv x2) ⟶ wo (wss (cv x2) (cv x1)) (wss (cv x3) (cv x1))) (λ x3 . cfv (cv x0) cidl)) (λ x2 . cfv (cv x0) cidl))) (λ x1 . cfv (cv x0) cidl))) (proof)
Theorem df_maxidl : wceq cmaxidl (cmpt (λ x0 . crngo) (λ x0 . crab (λ x1 . wa (wne (cv x1) (crn (cfv (cv x0) c1st))) (wral (λ x2 . wss (cv x1) (cv x2) ⟶ wo (wceq (cv x2) (cv x1)) (wceq (cv x2) (crn (cfv (cv x0) c1st)))) (λ x2 . cfv (cv x0) cidl))) (λ x1 . cfv (cv x0) cidl))) (proof)
Theorem df_prrngo : wceq cprrng (crab (λ x0 . wcel (csn (cfv (cfv (cv x0) c1st) cgi)) (cfv (cv x0) cpridl)) (λ x0 . crngo)) (proof)
Theorem df_dmn : wceq cdmn (cin cprrng ccm2) (proof)
Theorem df_igen : wceq cigen (cmpt2 (λ x0 x1 . crngo) (λ x0 x1 . cpw (crn (cfv (cv x0) c1st))) (λ x0 x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cv x0) cidl)))) (proof)
Theorem df_xrn : ∀ x0 x1 : ι → ο . wceq (cxrn x0 x1) (cin (ccom (ccnv (cres c1st (cxp cvv cvv))) x0) (ccom (ccnv (cres c2nd (cxp cvv cvv))) x1)) (proof)
Theorem df_coss : ∀ x0 : ι → ο . wceq (ccoss x0) (copab (λ x1 x2 . wex (λ x3 . wa (wbr (cv x3) (cv x1) x0) (wbr (cv x3) (cv x2) x0)))) (proof)