Apply df_gbow__df_gbo__ax_bgbltosilva__ax_tgoldbachgt__ax_hgprmladder__ax_bgbltosilvaOLD__ax_hgprmladderOLD__ax_tgoldbachgtOLD__df_upwlks__df_spr__df_mgmhm__df_submgm__df_cllaw__df_comlaw__df_asslaw__df_intop__df_clintop__df_assintop with wceq csubmgm (cmpt (λ x0 . cmgm) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wcel (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)) (λ x1 . cpw (cfv (cv x0) cbs)))).

Assume H0: wceq cgbow (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wceq (cv x0) (co (co (cv x1) (cv x2) caddc) (cv x3) caddc)) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . cprime)) (λ x0 . codd)).

Assume H1: wceq cgbo (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (w3a (wcel (cv x1) codd) (wcel (cv x2) codd) (wcel (cv x3) codd)) (wceq (cv x0) (co (co (cv x1) (cv x2) caddc) (cv x3) caddc))) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . cprime)) (λ x0 . codd)).

Assume H2: ∀ x0 : ι → ο . w3a (wcel x0 ceven) (wbr c4 x0 clt) (wbr x0 (co c4 (co (cdc c1 cc0) (cdc c1 c8) cexp) cmul) cle) ⟶ wcel x0 cgbe.

Assume H3: ∀ x0 : ι → ι → ι → ι → ι → ι → ο . ∀ x1 : ι → ι → ο . (∀ x2 . wceq (x1 x2) (crab (λ x3 . wn (wbr c2 (cv x3) cdvds)) (λ x3 . cz))) ⟶ (∀ x2 x3 x4 x5 x6 . wceq (x0 x2 x3 x4 x5 x6) (crab (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wa (w3a (wcel (cv x8) (x1 x3)) (wcel (cv x9) (x1 x3)) (wcel (cv x10) (x1 x3))) (wceq (cv x7) (co (co (cv x8) (cv x9) caddc) (cv x10) caddc))) (λ x10 . cprime)) (λ x9 . cprime)) (λ x8 . cprime)) (λ x7 . x1 x3))) ⟶ ∀ x2 x3 x4 x5 . wrex (λ x6 . wa (wbr (cv x6) (co (cdc c1 cc0) (cdc c2 c7) cexp) cle) (wral (λ x7 . wbr (cv x6) (cv x7) clt ⟶ wcel (cv x7) (x0 x2 x7 x3 x4 x5)) (λ x7 . x1 x7))) (λ x6 . cn).

Assume H4: wrex ... ....

...

■

Proofgold Proof