Apply df_dioph__df_squarenn__df_pell1qr__df_pell14qr__df_pell1234qr__df_pellfund__df_rmx__df_rmy__df_lfig__df_lnm__df_lnr__df_ldgis__df_mnc__df_plylt__df_dgraa__df_mpaa__df_itgo__df_za with wceq clfig (crab (λ x0 . wcel (cfv (cv x0) cbs) (cima (cfv (cv x0) clspn) (cin (cpw (cfv (cv x0) cbs)) cfn))) (λ x0 . clmod)).

Assume H0: wceq cdioph (cmpt (λ x0 . cn0) (λ x0 . crn (cmpt2 (λ x1 x2 . cfv (cv x0) cuz) (λ x1 x2 . cfv (co c1 (cv x1) cfz) cmzp) (λ x1 x2 . cab (λ x3 . wrex (λ x4 . wa (wceq (cv x3) (cres (cv x4) (co c1 (cv x0) cfz))) (wceq (cfv (cv x4) (cv x2)) cc0)) (λ x4 . co cn0 (co c1 (cv x1) cfz) cmap)))))).

Assume H1: wceq csquarenn (crab (λ x0 . wcel (cfv (cv x0) csqrt) cq) (λ x0 . cn)).

Assume H2: wceq cpell1qr (cmpt (λ x0 . cdif cn csquarenn) (λ x0 . crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (wceq (cv x1) (co (cv x2) (co (cfv (cv x0) csqrt) (cv x3) cmul) caddc)) (wceq (co (co (cv x2) c2 cexp) (co (cv x0) (co (cv x3) c2 cexp) cmul) cmin) c1)) (λ x3 . cn0)) (λ x2 . cn0)) (λ x1 . cr))).

Assume H3: wceq cpell14qr (cmpt (λ x0 . cdif cn csquarenn) (λ x0 . crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (wceq (cv x1) (co (cv x2) (co (cfv (cv x0) csqrt) (cv x3) cmul) caddc)) (wceq (co (co (cv x2) c2 cexp) (co (cv x0) (co (cv x3) c2 cexp) cmul) cmin) c1)) (λ x3 . cz)) (λ x2 . cn0)) (λ x1 . cr))).

Assume H4: wceq cpell1234qr (cmpt (λ x0 . cdif cn csquarenn) (λ x0 . crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (wceq (cv x1) (co (cv x2) (co (cfv (cv x0) csqrt) (cv x3) cmul) caddc)) (wceq (co (co (cv x2) c2 cexp) (co (cv x0) (co (cv x3) c2 cexp) cmul) cmin) c1)) (λ x3 . cz)) (λ x2 . cz)) ...)).

...

■

Proofgold Proof