Proofgold Address

Known df_strset__df_bj_diag__df_bj_inftyexpi__df_bj_ccinfty__df_bj_ccbar__df_bj_pinfty__df_bj_minfty__df_bj_rrbar__df_bj_infty__df_bj_cchat__df_bj_rrhat__df_bj_addc__df_bj_oppc__df_bj_prcpal__df_bj_arg__df_bj_mulc__df_bj_invc__df_bj_finsum : ∀ x0 : ο . ((∀ x1 x2 x3 : ι → ο . wceq (cstrset x1 x2 x3) (cun (cres x3 (cdif cvv (csn (cfv cnx x1)))) (csn (cop (cfv cnx x1) x2)))) ⟶ wceq cdiag2 (cmpt (λ x1 . cvv) (λ x1 . cin cid (cxp (cv x1) (cv x1)))) ⟶ wceq cinftyexpi (cmpt (λ x1 . co (cneg cpi) cpi cioc) (λ x1 . cop (cv x1) cc)) ⟶ wceq cccinfty (crn cinftyexpi) ⟶ wceq cccbar (cun cc cccinfty) ⟶ wceq cpinfty (cfv cc0 cinftyexpi) ⟶ wceq cminfty (cfv cpi cinftyexpi) ⟶ wceq crrbar (cun cr (cpr cminfty cpinfty)) ⟶ wceq cinfty (cpw (cuni cc)) ⟶ wceq ccchat (cun cc (csn cinfty)) ⟶ wceq crrhat (cun cr (csn cinfty)) ⟶ wceq caddcc (cmpt (λ x1 . cun (cun (cxp cc cccbar) (cxp cccbar cc)) (cun (cxp ccchat ccchat) (cfv cccinfty cdiag2))) (λ x1 . cif (wo (wceq (cfv (cv x1) c1st) cinfty) (wceq (cfv (cv x1) c2nd) cinfty)) cinfty (cif (wcel (cfv (cv x1) c1st) cc) (cif (wcel (cfv (cv x1) c2nd) cc) (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) caddc) (cfv (cv x1) c2nd)) (cfv (cv x1) c1st)))) ⟶ wceq coppcc (cmpt (λ x1 . cun cccbar ccchat) (λ x1 . cif (wceq (cv x1) cinfty) cinfty (cif (wcel (cv x1) cc) (cneg (cv x1)) (cfv (cif (wbr cc0 (cfv (cv x1) c1st) clt) (co (cfv (cv x1) c1st) cpi cmin) (co (cfv (cv x1) c1st) cpi caddc)) cinftyexpi)))) ⟶ wceq cprcpal (cmpt (λ x1 . cr) (λ x1 . co (co (cv x1) (co c2 cpi cmul) cmo) (cif (wbr (co (cv x1) (co c2 cpi cmul) cmo) cpi cle) cc0 (co c2 cpi cmul)) cmin)) ⟶ wceq carg (cmpt (λ x1 . cdif cccbar (csn cc0)) (λ x1 . cif (wcel (cv x1) cc) (cfv (cfv (cv x1) clog) cim) (cfv (cv x1) c1st))) ⟶ wceq cmulc (cmpt (λ x1 . cun (cxp cccbar cccbar) (cxp ccchat ccchat)) (λ x1 . cif (wo (wceq (cfv (cv x1) c1st) cc0) (wceq (cfv (cv x1) c2nd) cc0)) cc0 (cif (wo (wceq (cfv (cv x1) c1st) cinfty) (wceq (cfv (cv x1) c2nd) cinfty)) cinfty (cif (wcel (cv x1) (cxp cc cc)) (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cmul) (cfv (cfv (co (cfv (cfv (cv x1) c1st) carg) (cfv (cfv (cv x1) c2nd) carg) caddc) cprcpal) cinftyexpi))))) ⟶ wceq cinvc (cmpt (λ x1 . cun cccbar ccchat) (λ x1 . cif (wceq (cv x1) cc0) cinfty (cif (wcel (cv x1) cc) (co c1 (cv x1) cdiv) cc0))) ⟶ wceq cfinsum (cmpt (λ x1 . copab (λ x2 x3 . wa (wcel (cv x2) ccmn) (wrex (λ x4 . wf (cv x4) (cfv (cv x2) cbs) (cv x3)) (λ x4 . cfn)))) (λ x1 . cio (λ x2 . wrex (λ x3 . wex (λ x4 . wa (wf1o (co c1 (cv x3) cfz) (cdm (cfv (cv x1) c2nd)) (cv x4)) (wceq (cv x2) (cfv (cv x3) (cseq (cfv (cfv (cv x1) c1st) cplusg) (cmpt (λ x5 . cn) (λ x5 . cfv (cfv (cv x5) (cv x4)) (cfv (cv x1) c2nd))) c1))))) (λ x3 . cn0)))) ⟶ x0) ⟶ x0
Theorem df_strset : ∀ x0 x1 x2 : ι → ο . wceq (cstrset x0 x1 x2) (cun (cres x2 (cdif cvv (csn (cfv cnx x0)))) (csn (cop (cfv cnx x0) x1))) (proof)
Theorem df_bj_diag : wceq cdiag2 (cmpt (λ x0 . cvv) (λ x0 . cin cid (cxp (cv x0) (cv x0)))) (proof)
Theorem df_bj_inftyexpi : wceq cinftyexpi (cmpt (λ x0 . co (cneg cpi) cpi cioc) (λ x0 . cop (cv x0) cc)) (proof)
Theorem df_bj_ccinfty : wceq cccinfty (crn cinftyexpi) (proof)
Theorem df_bj_ccbar : wceq cccbar (cun cc cccinfty) (proof)
Theorem df_bj_pinfty : wceq cpinfty (cfv cc0 cinftyexpi) (proof)
Theorem df_bj_minfty : wceq cminfty (cfv cpi cinftyexpi) (proof)
Theorem df_bj_rrbar : wceq crrbar (cun cr (cpr cminfty cpinfty)) (proof)
Theorem df_bj_infty : wceq cinfty (cpw (cuni cc)) (proof)
Theorem df_bj_cchat : wceq ccchat (cun cc (csn cinfty)) (proof)
Theorem df_bj_rrhat : wceq crrhat (cun cr (csn cinfty)) (proof)
Theorem df_bj_addc : wceq caddcc (cmpt (λ x0 . cun (cun (cxp cc cccbar) (cxp cccbar cc)) (cun (cxp ccchat ccchat) (cfv cccinfty cdiag2))) (λ x0 . cif (wo (wceq (cfv (cv x0) c1st) cinfty) (wceq (cfv (cv x0) c2nd) cinfty)) cinfty (cif (wcel (cfv (cv x0) c1st) cc) (cif (wcel (cfv (cv x0) c2nd) cc) (co (cfv (cv x0) c1st) (cfv (cv x0) c2nd) caddc) (cfv (cv x0) c2nd)) (cfv (cv x0) c1st)))) (proof)
Theorem df_bj_oppc : wceq coppcc (cmpt (λ x0 . cun cccbar ccchat) (λ x0 . cif (wceq (cv x0) cinfty) cinfty (cif (wcel (cv x0) cc) (cneg (cv x0)) (cfv (cif (wbr cc0 (cfv (cv x0) c1st) clt) (co (cfv (cv x0) c1st) cpi cmin) (co (cfv (cv x0) c1st) cpi caddc)) cinftyexpi)))) (proof)
Theorem df_bj_prcpal : wceq cprcpal (cmpt (λ x0 . cr) (λ x0 . co (co (cv x0) (co c2 cpi cmul) cmo) (cif (wbr (co (cv x0) (co c2 cpi cmul) cmo) cpi cle) cc0 (co c2 cpi cmul)) cmin)) (proof)
Theorem df_bj_arg : wceq carg (cmpt (λ x0 . cdif cccbar (csn cc0)) (λ x0 . cif (wcel (cv x0) cc) (cfv (cfv (cv x0) clog) cim) (cfv (cv x0) c1st))) (proof)
Theorem df_bj_mulc : wceq cmulc (cmpt (λ x0 . cun (cxp cccbar cccbar) (cxp ccchat ccchat)) (λ x0 . cif (wo (wceq (cfv (cv x0) c1st) cc0) (wceq (cfv (cv x0) c2nd) cc0)) cc0 (cif (wo (wceq (cfv (cv x0) c1st) cinfty) (wceq (cfv (cv x0) c2nd) cinfty)) cinfty (cif (wcel (cv x0) (cxp cc cc)) (co (cfv (cv x0) c1st) (cfv (cv x0) c2nd) cmul) (cfv (cfv (co (cfv (cfv (cv x0) c1st) carg) (cfv (cfv (cv x0) c2nd) carg) caddc) cprcpal) cinftyexpi))))) (proof)
Theorem df_bj_invc : wceq cinvc (cmpt (λ x0 . cun cccbar ccchat) (λ x0 . cif (wceq (cv x0) cc0) cinfty (cif (wcel (cv x0) cc) (co c1 (cv x0) cdiv) cc0))) (proof)
Theorem df_bj_finsum : wceq cfinsum (cmpt (λ x0 . copab (λ x1 x2 . wa (wcel (cv x1) ccmn) (wrex (λ x3 . wf (cv x3) (cfv (cv x1) cbs) (cv x2)) (λ x3 . cfn)))) (λ x0 . cio (λ x1 . wrex (λ x2 . wex (λ x3 . wa (wf1o (co c1 (cv x2) cfz) (cdm (cfv (cv x0) c2nd)) (cv x3)) (wceq (cv x1) (cfv (cv x2) (cseq (cfv (cfv (cv x0) c1st) cplusg) (cmpt (λ x4 . cn) (λ x4 . cfv (cfv (cv x4) (cv x3)) (cfv (cv x0) c2nd))) c1))))) (λ x2 . cn0)))) (proof)