Apply 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 with 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))).

Assume H0: ∀ x0 x1 x2 : ι → ο . wceq (cstrset x0 x1 x2) (cun (cres x2 (cdif cvv (csn (cfv cnx x0)))) (csn (cop (cfv cnx x0) x1))).

Assume H1: wceq cdiag2 (cmpt (λ x0 . cvv) (λ x0 . cin cid (cxp (cv x0) (cv x0)))).

Assume H2: wceq cinftyexpi (cmpt (λ x0 . co (cneg cpi) cpi cioc) (λ x0 . cop (cv x0) cc)).

Assume H3: wceq cccinfty (crn cinftyexpi).

Assume H4: wceq cccbar (cun cc cccinfty).

Assume H5: wceq cpinfty (cfv cc0 cinftyexpi).

Assume H6: wceq cminfty (cfv cpi cinftyexpi).

Assume H7: wceq crrbar (cun cr (cpr cminfty cpinfty)).

Assume H8: wceq cinfty (cpw (cuni cc)).

Assume H9: wceq ccchat (cun cc (csn cinfty)).

Assume H10: wceq crrhat (cun cr (csn cinfty)).

Assume H11: 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)))).

Assume H12: 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)))).

Assume H13: wceq cprcpal (cmpt (λ x0 . cr) (λ x0 . co (co (cv x0) (co c2 cpi cmul) cmo) ... ...)).

...

■

Proofgold Proof