Apply df_q__df_rp__df_xneg__df_xadd__df_xmul__df_ioo__df_ioc__df_ico__df_icc__df_fz__df_fzo__df_fl__df_ceil__df_mod__df_seq__df_exp__df_fac__df_bc with wceq cmo (cmpt2 (λ x0 x1 . cr) (λ x0 x1 . crp) (λ x0 x1 . co (cv x0) (co (cv x1) (cfv (co (cv x0) (cv x1) cdiv) cfl) cmul) cmin)).

Assume H0: wceq cq (cima cdiv (cxp cz cn)).

Assume H1: wceq crp (crab (λ x0 . wbr cc0 (cv x0) clt) (λ x0 . cr)).

Assume H2: ∀ x0 : ι → ο . wceq (cxne x0) (cif (wceq x0 cpnf) cmnf (cif (wceq x0 cmnf) cpnf (cneg x0))).

Assume H3: wceq cxad (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cxr) (λ x0 x1 . cif (wceq (cv x0) cpnf) (cif (wceq (cv x1) cmnf) cc0 cpnf) (cif (wceq (cv x0) cmnf) (cif (wceq (cv x1) cpnf) cc0 cmnf) (cif (wceq (cv x1) cpnf) cpnf (cif (wceq (cv x1) cmnf) cmnf (co (cv x0) (cv x1) caddc)))))).

Assume H4: wceq cxmu (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cxr) (λ x0 x1 . cif (wo (wceq (cv x0) cc0) (wceq (cv x1) cc0)) cc0 (cif (wo (wo (wa (wbr cc0 (cv x1) clt) (wceq (cv x0) cpnf)) (wa (wbr (cv x1) cc0 clt) (wceq (cv x0) cmnf))) (wo (wa (wbr cc0 (cv x0) clt) (wceq (cv x1) cpnf)) (wa (wbr (cv x0) cc0 clt) (wceq (cv x1) cmnf)))) cpnf (cif (wo (wo (wa (wbr cc0 (cv x1) clt) (wceq (cv x0) cmnf)) (wa (wbr (cv x1) cc0 clt) (wceq (cv x0) cpnf))) (wo (wa (wbr cc0 (cv x0) clt) (wceq (cv x1) cmnf)) (wa (wbr (cv x0) cc0 clt) (wceq (cv x1) cpnf)))) cmnf (co (cv x0) (cv x1) cmul))))).

Assume H5: wceq cioo (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cxr) (λ x0 x1 . crab (λ x2 . wa (wbr (cv x0) (cv x2) clt) (wbr (cv x2) (cv x1) clt)) (λ x2 . cxr))).

...

■

Proofgold Proof