Apply df_ppi__df_mu__df_sgm__df_dchr__df_lgs__df_itv__df_lng__df_trkgc__df_trkgb__df_trkgcb__df_trkge__df_trkgld__df_trkg__df_cgrg__df_ismt__df_leg__df_hlg__df_mir with wceq cppi (cmpt (λ x0 . cr) (λ x0 . cfv (cin (co cc0 (cv x0) cicc) cprime) chash)).

Assume H0: wceq cppi (cmpt (λ x0 . cr) (λ x0 . cfv (cin (co cc0 (cv x0) cicc) cprime) chash)).

Assume H1: wceq cmu (cmpt (λ x0 . cn) (λ x0 . cif (wrex (λ x1 . wbr (co (cv x1) c2 cexp) (cv x0) cdvds) (λ x1 . cprime)) cc0 (co (cneg c1) (cfv (crab (λ x1 . wbr (cv x1) (cv x0) cdvds) (λ x1 . cprime)) chash) cexp))).

Assume H2: wceq csgm (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn) (λ x0 x1 . csu (crab (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cn)) (λ x2 . co (cv x2) (cv x0) ccxp))).

Assume H3: wceq cdchr (cmpt (λ x0 . cn) (λ x0 . csb (cfv (cv x0) czn) (λ x1 . csb (crab (λ x2 . wss (cxp (cdif (cfv (cv x1) cbs) (cfv (cv x1) cui)) (csn cc0)) (cv x2)) (λ x2 . co (cfv (cv x1) cmgp) (cfv ccnfld cmgp) cmhm)) (λ x2 . cpr (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cres (cof cmul) (cxp (cv x2) (cv x2)))))))).

Assume H4: wceq clgs (cmpt2 (λ x0 x1 . cz) (λ x0 x1 . cz) (λ x0 x1 . cif (wceq (cv x1) cc0) (cif (wceq (co (cv x0) c2 cexp) c1) c1 cc0) (co (cif (wa (wbr (cv x1) cc0 clt) (wbr (cv x0) cc0 clt)) (cneg c1) c1) (cfv (cfv (cv x1) cabs) (cseq cmul (cmpt (λ x2 . cn) (λ x2 . cif (wcel (cv x2) cprime) (co (cif (wceq (cv x2) c2) (cif (wbr c2 (cv x0) cdvds) cc0 (cif (wcel (co (cv x0) c8 cmo) (cpr c1 c7)) c1 (cneg c1))) (co (co (co (co (cv x0) (co (co (cv x2) c1 cmin) c2 cdiv) cexp) ... ...) ... ...) ... ...)) ... ...) ...)) ...)) ...))).

...

■

Proofgold Proof