Apply df_rtrcl__df_relexp__df_rtrclrec__df_shft__df_sgn__df_cj__df_re__df_im__df_sqrt__df_abs__df_limsup__df_clim__df_rlim__df_o1__df_lo1__df_sum__df_prod__df_risefac with wceq cabs (cmpt (λ x0 . cc) (λ x0 . cfv (co (cv x0) (cfv (cv x0) ccj) cmul) csqrt)).

Assume H0: wceq crtcl (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . w3a (wss (cres cid (cun (cdm (cv x0)) (crn (cv x0)))) (cv x1)) (wss (cv x0) (cv x1)) (wss (ccom (cv x1) (cv x1)) (cv x1)))))).

Assume H1: wceq crelexp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . cif (wceq (cv x1) cc0) (cres cid (cun (cdm (cv x0)) (crn (cv x0)))) (cfv (cv x1) (cseq (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . ccom (cv x2) (cv x0))) (cmpt (λ x2 . cvv) (λ x2 . cv x0)) c1)))).

Assume H2: wceq crtrcl (cmpt (λ x0 . cvv) (λ x0 . ciun (λ x1 . cn0) (λ x1 . co (cv x0) (cv x1) crelexp))).

Assume H3: wceq cshi (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cc) (λ x0 x1 . copab (λ x2 x3 . wa (wcel (cv x2) cc) (wbr (co (cv x2) (cv x1) cmin) (cv x3) (cv x0))))).

Assume H4: wceq csgn (cmpt (λ x0 . cxr) (λ x0 . cif (wceq (cv x0) cc0) cc0 (cif (wbr (cv x0) cc0 clt) (cneg c1) c1))).

Assume H5: wceq ccj (cmpt (λ x0 . cc) (λ x0 . crio (λ x1 . wa (wcel (co (cv x0) (cv x1) caddc) cr) (wcel (co ci (co (cv x0) (cv x1) cmin) cmul) cr)) (λ x1 . cc))).

Assume H6: wceq cre (cmpt (λ x0 . cc) (λ x0 . co (co (cv x0) (cfv (cv x0) ccj) caddc) c2 cdiv)).

Assume H7: wceq cim (cmpt (λ x0 . cc) (λ x0 . cfv (co (cv x0) ci cdiv) cre)).

Assume H8: wceq csqrt (cmpt (λ x0 . cc) (λ x0 . crio (λ x1 . w3a (wceq (co (cv x1) c2 cexp) (cv x0)) (wbr cc0 (cfv (cv x1) cre) cle) (wnel (co ci (cv x1) ...) ...)) ...)).

...

■

Proofgold Proof