Apply df_ifs__df_cgr3__df_fs__df_segle__df_outsideof__df_line2__df_ray__df_lines2__df_fwddif__df_fwddifn__df_hf__df_fne__df_3nand__df_gcdOLD__ax_prv1__ax_prv2__ax_prv3__df_ssb with ∀ x0 x1 : ι → ο . wceq (cgcdOLD x0 x1) (csup (crab (λ x2 . wa (wcel (co x0 (cv x2) cdiv) cn) (wcel (co x1 (cv x2) cdiv) cn)) (λ x2 . cn)) cn clt).

Assume H0: wceq cifs (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . w3a (wceq (cv x0) (cop (cop (cv x3) (cv x4)) (cop (cv x5) (cv x6)))) (wceq (cv x1) (cop (cop (cv x7) (cv x8)) (cop (cv x9) (cv x10)))) (w3a (wa (wbr (cv x4) (cop (cv x3) (cv x5)) cbtwn) (wbr (cv x8) (cop (cv x7) (cv x9)) cbtwn)) (wa (wbr (cop (cv x3) (cv x5)) (cop (cv x7) (cv x9)) ccgr) (wbr (cop (cv x4) (cv x5)) (cop (cv x8) (cv x9)) ccgr)) (wa (wbr (cop (cv x3) (cv x6)) (cop (cv x7) (cv x10)) ccgr) (wbr (cop (cv x5) (cv x6)) (cop (cv x9) (cv x10)) ccgr)))) (λ x10 . cfv (cv x2) cee)) (λ x9 . cfv (cv x2) cee)) (λ x8 . cfv (cv x2) cee)) (λ x7 . cfv (cv x2) cee)) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))).

Assume H1: wceq ccgr3 (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . w3a (wceq (cv x0) (cop (cv x3) (cop (cv x4) (cv x5)))) (wceq (cv x1) (cop (cv x6) (cop (cv x7) (cv x8)))) (w3a (wbr (cop (cv x3) (cv x4)) (cop (cv x6) (cv x7)) ccgr) (wbr (cop (cv x3) (cv x5)) (cop (cv x6) ...) ...) ...)) ...) ...) ...) ...) ...) ...) ...)).

...

■

Proofgold Proof