Proofgold Proof

Apply df_md__df_dmd__df_at__df_dp2__df_dp__df_xdiv__ax_xrssca__ax_xrsvsca__df_omnd__df_ogrp__df_sgns__df_inftm__df_archi__df_slmd__df_orng__df_ofld__df_resv__df_smat with wceq cslmd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wa (wcel (cv x4) csrg) (wral (λ x8 . wral (λ x9 . wral (λ x10 . wral (λ x11 . wa (w3a (wcel (co (cv x9) (cv x11) (cv x3)) (cv x1)) (wceq (co (cv x9) (co (cv x11) (cv x10) (cv x2)) (cv x3)) (co (co (cv x9) (cv x11) (cv x3)) (co (cv x9) (cv x10) (cv x3)) (cv x2))) (wceq (co (co (cv x8) (cv x9) (cv x6)) (cv x11) (cv x3)) (co (co (cv x8) (cv x11) (cv x3)) (co (cv x9) (cv x11) (cv x3)) (cv x2)))) (w3a (wceq (co (co (cv x8) (cv x9) (cv x7)) (cv x11) (cv x3)) (co (cv x8) (co (cv x9) (cv x11) (cv x3)) (cv x3))) (wceq (co (cfv (cv x4) cur) (cv x11) (cv x3)) (cv x11)) (wceq (co (cfv (cv x4) c0g) (cv x11) (cv x3)) (cfv (cv x0) c0g)))) (λ x11 . cv x1)) (λ x10 . cv x1)) (λ x9 . cv x5)) (λ x8 . cv x5))) (cfv (cv x4) cmulr)) (cfv (cv x4) cplusg)) (cfv (cv x4) cbs)) (cfv (cv x0) csca)) (cfv (cv x0) cvsca)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . ccmn)).