Apply df_fallfac__df_bpoly__df_ef__df_e__df_sin__df_cos__df_tan__df_pi__df_dvds__df_bits__df_sad__df_smu__df_gcd__df_lcm__df_lcmf__df_prm__df_numer__df_denom with wceq cdvds (copab (λ x0 x1 . wa (wa (wcel (cv x0) cz) (wcel (cv x1) cz)) (wrex (λ x2 . wceq (co (cv x2) (cv x0) cmul) (cv x1)) (λ x2 . cz)))).

Assume H0: wceq cfallfac (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn0) (λ x0 x1 . cprod (λ x2 . co cc0 (co (cv x1) c1 cmin) cfz) (λ x2 . co (cv x0) (cv x2) cmin))).

Assume H1: wceq cbp (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cc) (λ x0 x1 . cfv (cv x0) (cwrecs cn0 clt (cmpt (λ x2 . cvv) (λ x2 . csb (cfv (cdm (cv x2)) chash) (λ x3 . co (co (cv x1) (cv x3) cexp) (csu (cdm (cv x2)) (λ x4 . co (co (cv x3) (cv x4) cbc) (co (cfv (cv x4) (cv x2)) (co (co (cv x3) (cv x4) cmin) c1 caddc) cdiv) cmul)) cmin)))))).

Assume H2: wceq ce (cmpt (λ x0 . cc) (λ x0 . csu cn0 (λ x1 . co (co (cv x0) (cv x1) cexp) (cfv (cv x1) cfa) cdiv))).

Assume H3: wceq ceu (cfv c1 ce).

Assume H4: wceq csin (cmpt (λ x0 . cc) (λ x0 . co (co (cfv (co ci (cv x0) cmul) ce) (cfv (co (cneg ci) (cv x0) cmul) ce) cmin) (co c2 ci cmul) cdiv)).

Assume H5: wceq ccos (cmpt (λ x0 . cc) (λ x0 . co (co (cfv (co ci (cv x0) cmul) ce) (cfv (co (cneg ci) (cv x0) cmul) ce) caddc) c2 cdiv)).

Assume H6: wceq ctan (cmpt (λ x0 . cima (ccnv ccos) (cdif cc (csn cc0))) (λ x0 . co (cfv (cv x0) csin) (cfv (cv x0) ccos) cdiv)).

Assume H7: wceq cpi (cinf (cin crp (cima (ccnv csin) (csn cc0))) cr clt).

Assume H8: wceq cdvds (copab (λ x0 x1 . wa (wa (wcel (cv x0) cz) (wcel (cv x1) cz)) (wrex (λ x2 . wceq (co ... ... ...) ...) ...))).

...

■

Proofgold Proof