Proofgold Address

Known df_lvec__df_sra__df_rgmod__df_lidl__df_rsp__df_2idl__df_lpidl__df_lpir__df_nzr__df_rlreg__df_domn__df_idom__df_pid__df_assa__df_asp__df_ascl__df_psr__df_mvr : ∀ x0 : ο . (wceq clvec (crab (λ x1 . wcel (cfv (cv x1) csca) cdr) (λ x1 . clmod)) ⟶ wceq csra (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . co (co (co (cv x1) (cop (cfv cnx csca) (co (cv x1) (cv x2) cress)) csts) (cop (cfv cnx cvsca) (cfv (cv x1) cmulr)) csts) (cop (cfv cnx cip) (cfv (cv x1) cmulr)) csts))) ⟶ wceq crglmod (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cv x1) cbs) (cfv (cv x1) csra))) ⟶ wceq clidl (ccom clss crglmod) ⟶ wceq crsp (ccom clspn crglmod) ⟶ wceq c2idl (cmpt (λ x1 . cvv) (λ x1 . cin (cfv (cv x1) clidl) (cfv (cfv (cv x1) coppr) clidl))) ⟶ wceq clpidl (cmpt (λ x1 . crg) (λ x1 . ciun (λ x2 . cfv (cv x1) cbs) (λ x2 . csn (cfv (csn (cv x2)) (cfv (cv x1) crsp))))) ⟶ wceq clpir (crab (λ x1 . wceq (cfv (cv x1) clidl) (cfv (cv x1) clpidl)) (λ x1 . crg)) ⟶ wceq cnzr (crab (λ x1 . wne (cfv (cv x1) cur) (cfv (cv x1) c0g)) (λ x1 . crg)) ⟶ wceq crlreg (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x1) cmulr)) (cfv (cv x1) c0g) ⟶ wceq (cv x3) (cfv (cv x1) c0g)) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq cdomn (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (cv x4) (cv x5) (cfv (cv x1) cmulr)) (cv x3) ⟶ wo (wceq (cv x4) (cv x3)) (wceq (cv x5) (cv x3))) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) c0g)) (cfv (cv x1) cbs)) (λ x1 . cnzr)) ⟶ wceq cidom (cin ccrg cdomn) ⟶ wceq cpid (cin cidom clpir) ⟶ wceq casa (crab (λ x1 . wsbc (λ x2 . wa (wcel (cv x2) ccrg) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wa (wceq (co (co (cv x3) (cv x4) (cv x6)) (cv x5) (cv x7)) (co (cv x3) (co (cv x4) (cv x5) (cv x7)) (cv x6))) (wceq (co (cv x4) (co (cv x3) (cv x5) (cv x6)) (cv x7)) (co (cv x3) (co (cv x4) (cv x5) (cv x7)) (cv x6)))) (cfv (cv x1) cmulr)) (cfv (cv x1) cvsca)) (λ x5 . cfv (cv x1) cbs)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x2) cbs))) (cfv (cv x1) csca)) (λ x1 . cin clmod crg)) ⟶ wceq casp (cmpt (λ x1 . casa) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cin (cfv (cv x1) csubrg) (cfv (cv x1) clss)))))) ⟶ wceq cascl (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cfv (cv x1) csca) cbs) (λ x2 . co (cv x2) (cfv (cv x1) cur) (cfv (cv x1) cvsca)))) ⟶ wceq cmps (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (crab (λ x3 . wcel (cima (ccnv (cv x3)) cn) cfn) (λ x3 . co cn0 (cv x1) cmap)) (λ x3 . csb (co (cfv (cv x2) cbs) (cv x3) cmap) (λ x4 . cun (ctp (cop (cfv cnx cbs) (cv x4)) (cop (cfv cnx cplusg) (cres (cof (cfv (cv x2) cplusg)) (cxp (cv x4) (cv x4)))) (cop (cfv cnx cmulr) (cmpt2 (λ x5 x6 . cv x4) (λ x5 x6 . cv x4) (λ x5 x6 . cmpt (λ x7 . cv x3) (λ x7 . co (cv x2) (cmpt (λ x8 . crab (λ x9 . wbr (cv x9) (cv x7) (cofr cle)) (λ x9 . cv x3)) (λ x8 . co (cfv (cv x8) (cv x5)) (cfv (co (cv x7) (cv x8) (cof cmin)) (cv x6)) (cfv (cv x2) cmulr))) cgsu))))) (ctp (cop (cfv cnx csca) (cv x2)) (cop (cfv cnx cvsca) (cmpt2 (λ x5 x6 . cfv (cv x2) cbs) (λ x5 x6 . cv x4) (λ x5 x6 . co (cxp (cv x3) (csn (cv x5))) (cv x6) (cof (cfv (cv x2) cmulr))))) (cop (cfv cnx cts) (cfv (cxp (cv x3) (csn (cfv (cv x2) ctopn))) cpt))))))) ⟶ wceq cmvr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cv x1) (λ x3 . cmpt (λ x4 . crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x1) cmap)) (λ x4 . cif (wceq (cv x4) (cmpt (λ x5 . cv x1) (λ x5 . cif (wceq (cv x5) (cv x3)) c1 cc0))) (cfv (cv x2) cur) (cfv (cv x2) c0g))))) ⟶ x0) ⟶ x0
Theorem df_lvec : wceq clvec (crab (λ x0 . wcel (cfv (cv x0) csca) cdr) (λ x0 . clmod)) (proof)
Theorem df_sra : wceq csra (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . co (co (co (cv x0) (cop (cfv cnx csca) (co (cv x0) (cv x1) cress)) csts) (cop (cfv cnx cvsca) (cfv (cv x0) cmulr)) csts) (cop (cfv cnx cip) (cfv (cv x0) cmulr)) csts))) (proof)
Theorem df_rgmod : wceq crglmod (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cbs) (cfv (cv x0) csra))) (proof)
Theorem df_lidl : wceq clidl (ccom clss crglmod) (proof)
Theorem df_rsp : wceq crsp (ccom clspn crglmod) (proof)
Theorem df_2idl : wceq c2idl (cmpt (λ x0 . cvv) (λ x0 . cin (cfv (cv x0) clidl) (cfv (cfv (cv x0) coppr) clidl))) (proof)
Theorem df_lpidl : wceq clpidl (cmpt (λ x0 . crg) (λ x0 . ciun (λ x1 . cfv (cv x0) cbs) (λ x1 . csn (cfv (csn (cv x1)) (cfv (cv x0) crsp))))) (proof)
Theorem df_lpir : wceq clpir (crab (λ x0 . wceq (cfv (cv x0) clidl) (cfv (cv x0) clpidl)) (λ x0 . crg)) (proof)
Theorem df_nzr : wceq cnzr (crab (λ x0 . wne (cfv (cv x0) cur) (cfv (cv x0) c0g)) (λ x0 . crg)) (proof)
Theorem df_rlreg : wceq crlreg (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cfv (cv x0) cmulr)) (cfv (cv x0) c0g) ⟶ wceq (cv x2) (cfv (cv x0) c0g)) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs))) (proof)
Theorem df_domn : wceq cdomn (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cfv (cv x0) cmulr)) (cv x2) ⟶ wo (wceq (cv x3) (cv x2)) (wceq (cv x4) (cv x2))) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) c0g)) (cfv (cv x0) cbs)) (λ x0 . cnzr)) (proof)
Theorem df_idom : wceq cidom (cin ccrg cdomn) (proof)
Theorem df_pid : wceq cpid (cin cidom clpir) (proof)
Theorem df_assa : wceq casa (crab (λ x0 . wsbc (λ x1 . wa (wcel (cv x1) ccrg) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wa (wceq (co (co (cv x2) (cv x3) (cv x5)) (cv x4) (cv x6)) (co (cv x2) (co (cv x3) (cv x4) (cv x6)) (cv x5))) (wceq (co (cv x3) (co (cv x2) (cv x4) (cv x5)) (cv x6)) (co (cv x2) (co (cv x3) (cv x4) (cv x6)) (cv x5)))) (cfv (cv x0) cmulr)) (cfv (cv x0) cvsca)) (λ x4 . cfv (cv x0) cbs)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x1) cbs))) (cfv (cv x0) csca)) (λ x0 . cin clmod crg)) (proof)
Theorem df_asp : wceq casp (cmpt (λ x0 . casa) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cin (cfv (cv x0) csubrg) (cfv (cv x0) clss)))))) (proof)
Theorem df_ascl : wceq cascl (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cfv (cv x0) csca) cbs) (λ x1 . co (cv x1) (cfv (cv x0) cur) (cfv (cv x0) cvsca)))) (proof)
Theorem df_psr : wceq cmps (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (crab (λ x2 . wcel (cima (ccnv (cv x2)) cn) cfn) (λ x2 . co cn0 (cv x0) cmap)) (λ x2 . csb (co (cfv (cv x1) cbs) (cv x2) cmap) (λ x3 . cun (ctp (cop (cfv cnx cbs) (cv x3)) (cop (cfv cnx cplusg) (cres (cof (cfv (cv x1) cplusg)) (cxp (cv x3) (cv x3)))) (cop (cfv cnx cmulr) (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cmpt (λ x6 . cv x2) (λ x6 . co (cv x1) (cmpt (λ x7 . crab (λ x8 . wbr (cv x8) (cv x6) (cofr cle)) (λ x8 . cv x2)) (λ x7 . co (cfv (cv x7) (cv x4)) (cfv (co (cv x6) (cv x7) (cof cmin)) (cv x5)) (cfv (cv x1) cmulr))) cgsu))))) (ctp (cop (cfv cnx csca) (cv x1)) (cop (cfv cnx cvsca) (cmpt2 (λ x4 x5 . cfv (cv x1) cbs) (λ x4 x5 . cv x3) (λ x4 x5 . co (cxp (cv x2) (csn (cv x4))) (cv x5) (cof (cfv (cv x1) cmulr))))) (cop (cfv cnx cts) (cfv (cxp (cv x2) (csn (cfv (cv x1) ctopn))) cpt))))))) (proof)
Theorem df_mvr : wceq cmvr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cv x0) (λ x2 . cmpt (λ x3 . crab (λ x4 . wcel (cima (ccnv (cv x4)) cn) cfn) (λ x4 . co cn0 (cv x0) cmap)) (λ x3 . cif (wceq (cv x3) (cmpt (λ x4 . cv x0) (λ x4 . cif (wceq (cv x4) (cv x2)) c1 cc0))) (cfv (cv x1) cur) (cfv (cv x1) c0g))))) (proof)