Apply df_tayl__df_ana__df_ulm__df_log__df_cxp__df_logb__df_asin__df_acos__df_atan__df_area__df_em__df_zeta__df_lgam__df_gam__df_igam__df_cht__df_vma__df_chp with wceq ccht (cmpt (λ x0 . cr) (λ x0 . csu (cin (co cc0 (cv x0) cicc) cprime) (λ x1 . cfv (cv x1) clog))).

Assume H0: wceq ctayl (cmpt2 (λ x0 x1 . cpr cr cc) (λ x0 x1 . co cc (cv x0) cpm) (λ x0 x1 . cmpt2 (λ x2 x3 . cun cn0 (csn cpnf)) (λ x2 x3 . ciin (λ x4 . cin (co cc0 (cv x2) cicc) cz) (λ x4 . cdm (cfv (cv x4) (co (cv x0) (cv x1) cdvn)))) (λ x2 x3 . ciun (λ x4 . cc) (λ x4 . cxp (csn (cv x4)) (co ccnfld (cmpt (λ x5 . cin (co cc0 (cv x2) cicc) cz) (λ x5 . co (co (cfv (cv x3) (cfv (cv x5) (co (cv x0) (cv x1) cdvn))) (cfv (cv x5) cfa) cdiv) (co (co (cv x4) (cv x3) cmin) (cv x5) cexp) cmul)) ctsu))))).

Assume H1: wceq cana (cmpt (λ x0 . cpr cr cc) (λ x0 . crab (λ x1 . wral (λ x2 . wcel (cv x2) (cfv (cdm (cin (cv x1) (co cpnf (cv x2) (co (cv x0) (cv x1) ctayl)))) (cfv (co (cfv ccnfld ctopn) (cv x0) crest) cnt))) (λ x2 . cdm (cv x1))) (λ x1 . co cc (cv x0) cpm))).

Assume H2: wceq culm (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wrex (λ x3 . w3a (wf (cfv (cv x3) cuz) (co cc (cv x0) cmap) (cv x1)) (wf (cv x0) cc (cv x2)) (wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wbr (cfv (co (cfv (cv x7) (cfv (cv x6) (cv x1))) (cfv (cv x7) (cv x2)) cmin) cabs) (cv x4) clt) (λ x7 . cv x0)) (λ x6 . cfv (cv x5) cuz)) (λ x5 . cfv (cv x3) cuz)) (λ x4 . crp))) (λ x3 . cz)))).

Assume H3: wceq clog (ccnv (cres ce (cima (ccnv cim) (co (cneg cpi) cpi ...)))).

...

■

Proofgold Proof