Proofgold Address

Known 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 : ∀ x0 : ο . (wceq cdioph (cmpt (λ x1 . cn0) (λ x1 . crn (cmpt2 (λ x2 x3 . cfv (cv x1) cuz) (λ x2 x3 . cfv (co c1 (cv x2) cfz) cmzp) (λ x2 x3 . cab (λ x4 . wrex (λ x5 . wa (wceq (cv x4) (cres (cv x5) (co c1 (cv x1) cfz))) (wceq (cfv (cv x5) (cv x3)) cc0)) (λ x5 . co cn0 (co c1 (cv x2) cfz) cmap)))))) ⟶ wceq csquarenn (crab (λ x1 . wcel (cfv (cv x1) csqrt) cq) (λ x1 . cn)) ⟶ wceq cpell1qr (cmpt (λ x1 . cdif cn csquarenn) (λ x1 . crab (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wceq (cv x2) (co (cv x3) (co (cfv (cv x1) csqrt) (cv x4) cmul) caddc)) (wceq (co (co (cv x3) c2 cexp) (co (cv x1) (co (cv x4) c2 cexp) cmul) cmin) c1)) (λ x4 . cn0)) (λ x3 . cn0)) (λ x2 . cr))) ⟶ wceq cpell14qr (cmpt (λ x1 . cdif cn csquarenn) (λ x1 . crab (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wceq (cv x2) (co (cv x3) (co (cfv (cv x1) csqrt) (cv x4) cmul) caddc)) (wceq (co (co (cv x3) c2 cexp) (co (cv x1) (co (cv x4) c2 cexp) cmul) cmin) c1)) (λ x4 . cz)) (λ x3 . cn0)) (λ x2 . cr))) ⟶ wceq cpell1234qr (cmpt (λ x1 . cdif cn csquarenn) (λ x1 . crab (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wceq (cv x2) (co (cv x3) (co (cfv (cv x1) csqrt) (cv x4) cmul) caddc)) (wceq (co (co (cv x3) c2 cexp) (co (cv x1) (co (cv x4) c2 cexp) cmul) cmin) c1)) (λ x4 . cz)) (λ x3 . cz)) (λ x2 . cr))) ⟶ wceq cpellfund (cmpt (λ x1 . cdif cn csquarenn) (λ x1 . cinf (crab (λ x2 . wbr c1 (cv x2) clt) (λ x2 . cfv (cv x1) cpell14qr)) cr clt)) ⟶ wceq crmx (cmpt2 (λ x1 x2 . cfv c2 cuz) (λ x1 x2 . cz) (λ x1 x2 . cfv (cfv (co (co (cv x1) (cfv (co (co (cv x1) c2 cexp) c1 cmin) csqrt) caddc) (cv x2) cexp) (ccnv (cmpt (λ x3 . cxp cn0 cz) (λ x3 . co (cfv (cv x3) c1st) (co (cfv (co (co (cv x1) c2 cexp) c1 cmin) csqrt) (cfv (cv x3) c2nd) cmul) caddc)))) c1st)) ⟶ wceq crmy (cmpt2 (λ x1 x2 . cfv c2 cuz) (λ x1 x2 . cz) (λ x1 x2 . cfv (cfv (co (co (cv x1) (cfv (co (co (cv x1) c2 cexp) c1 cmin) csqrt) caddc) (cv x2) cexp) (ccnv (cmpt (λ x3 . cxp cn0 cz) (λ x3 . co (cfv (cv x3) c1st) (co (cfv (co (co (cv x1) c2 cexp) c1 cmin) csqrt) (cfv (cv x3) c2nd) cmul) caddc)))) c2nd)) ⟶ wceq clfig (crab (λ x1 . wcel (cfv (cv x1) cbs) (cima (cfv (cv x1) clspn) (cin (cpw (cfv (cv x1) cbs)) cfn))) (λ x1 . clmod)) ⟶ wceq clnm (crab (λ x1 . wral (λ x2 . wcel (co (cv x1) (cv x2) cress) clfig) (λ x2 . cfv (cv x1) clss)) (λ x1 . clmod)) ⟶ wceq clnr (crab (λ x1 . wcel (cfv (cv x1) crglmod) clnm) (λ x1 . crg)) ⟶ wceq cldgis (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cfv (cv x1) cpl1) clidl) (λ x2 . cmpt (λ x3 . cn0) (λ x3 . cab (λ x4 . wrex (λ x5 . wa (wbr (cfv (cv x5) (cfv (cv x1) cdg1)) (cv x3) cle) (wceq (cv x4) (cfv (cv x3) (cfv (cv x5) cco1)))) (λ x5 . cv x2)))))) ⟶ wceq cmnc (cmpt (λ x1 . cpw cc) (λ x1 . crab (λ x2 . wceq (cfv (cfv (cv x2) cdgr) (cfv (cv x2) ccoe)) c1) (λ x2 . cfv (cv x1) cply))) ⟶ wceq cplylt (cmpt2 (λ x1 x2 . cpw cc) (λ x1 x2 . cn0) (λ x1 x2 . crab (λ x3 . wo (wceq (cv x3) c0p) (wbr (cfv (cv x3) cdgr) (cv x2) clt)) (λ x3 . cfv (cv x1) cply))) ⟶ wceq cdgraa (cmpt (λ x1 . caa) (λ x1 . cinf (crab (λ x2 . wrex (λ x3 . wa (wceq (cfv (cv x3) cdgr) (cv x2)) (wceq (cfv (cv x1) (cv x3)) cc0)) (λ x3 . cdif (cfv cq cply) (csn c0p))) (λ x2 . cn)) cr clt)) ⟶ wceq cmpaa (cmpt (λ x1 . caa) (λ x1 . crio (λ x2 . w3a (wceq (cfv (cv x2) cdgr) (cfv (cv x1) cdgraa)) (wceq (cfv (cv x1) (cv x2)) cc0) (wceq (cfv (cfv (cv x1) cdgraa) (cfv (cv x2) ccoe)) c1)) (λ x2 . cfv cq cply))) ⟶ wceq citgo (cmpt (λ x1 . cpw cc) (λ x1 . crab (λ x2 . wrex (λ x3 . wa (wceq (cfv (cv x2) (cv x3)) cc0) (wceq (cfv (cfv (cv x3) cdgr) (cfv (cv x3) ccoe)) c1)) (λ x3 . cfv (cv x1) cply)) (λ x2 . cc))) ⟶ wceq cza (cfv cz citgo) ⟶ x0) ⟶ x0
Theorem df_dioph : 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)))))) (proof)
Theorem df_squarenn : wceq csquarenn (crab (λ x0 . wcel (cfv (cv x0) csqrt) cq) (λ x0 . cn)) (proof)
Theorem df_pell1qr : 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))) (proof)
Theorem df_pell14qr : 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))) (proof)
Theorem df_pell1234qr : 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)) (λ x1 . cr))) (proof)
Theorem df_pellfund : wceq cpellfund (cmpt (λ x0 . cdif cn csquarenn) (λ x0 . cinf (crab (λ x1 . wbr c1 (cv x1) clt) (λ x1 . cfv (cv x0) cpell14qr)) cr clt)) (proof)
Theorem df_rmx : wceq crmx (cmpt2 (λ x0 x1 . cfv c2 cuz) (λ x0 x1 . cz) (λ x0 x1 . cfv (cfv (co (co (cv x0) (cfv (co (co (cv x0) c2 cexp) c1 cmin) csqrt) caddc) (cv x1) cexp) (ccnv (cmpt (λ x2 . cxp cn0 cz) (λ x2 . co (cfv (cv x2) c1st) (co (cfv (co (co (cv x0) c2 cexp) c1 cmin) csqrt) (cfv (cv x2) c2nd) cmul) caddc)))) c1st)) (proof)
Theorem df_rmy : wceq crmy (cmpt2 (λ x0 x1 . cfv c2 cuz) (λ x0 x1 . cz) (λ x0 x1 . cfv (cfv (co (co (cv x0) (cfv (co (co (cv x0) c2 cexp) c1 cmin) csqrt) caddc) (cv x1) cexp) (ccnv (cmpt (λ x2 . cxp cn0 cz) (λ x2 . co (cfv (cv x2) c1st) (co (cfv (co (co (cv x0) c2 cexp) c1 cmin) csqrt) (cfv (cv x2) c2nd) cmul) caddc)))) c2nd)) (proof)
Theorem df_lfig : wceq clfig (crab (λ x0 . wcel (cfv (cv x0) cbs) (cima (cfv (cv x0) clspn) (cin (cpw (cfv (cv x0) cbs)) cfn))) (λ x0 . clmod)) (proof)
Theorem df_lnm : wceq clnm (crab (λ x0 . wral (λ x1 . wcel (co (cv x0) (cv x1) cress) clfig) (λ x1 . cfv (cv x0) clss)) (λ x0 . clmod)) (proof)
Theorem df_lnr : wceq clnr (crab (λ x0 . wcel (cfv (cv x0) crglmod) clnm) (λ x0 . crg)) (proof)
Theorem df_ldgis : wceq cldgis (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cfv (cv x0) cpl1) clidl) (λ x1 . cmpt (λ x2 . cn0) (λ x2 . cab (λ x3 . wrex (λ x4 . wa (wbr (cfv (cv x4) (cfv (cv x0) cdg1)) (cv x2) cle) (wceq (cv x3) (cfv (cv x2) (cfv (cv x4) cco1)))) (λ x4 . cv x1)))))) (proof)
Theorem df_mnc : wceq cmnc (cmpt (λ x0 . cpw cc) (λ x0 . crab (λ x1 . wceq (cfv (cfv (cv x1) cdgr) (cfv (cv x1) ccoe)) c1) (λ x1 . cfv (cv x0) cply))) (proof)
Theorem df_plylt : wceq cplylt (cmpt2 (λ x0 x1 . cpw cc) (λ x0 x1 . cn0) (λ x0 x1 . crab (λ x2 . wo (wceq (cv x2) c0p) (wbr (cfv (cv x2) cdgr) (cv x1) clt)) (λ x2 . cfv (cv x0) cply))) (proof)
Theorem df_dgraa : wceq cdgraa (cmpt (λ x0 . caa) (λ x0 . cinf (crab (λ x1 . wrex (λ x2 . wa (wceq (cfv (cv x2) cdgr) (cv x1)) (wceq (cfv (cv x0) (cv x2)) cc0)) (λ x2 . cdif (cfv cq cply) (csn c0p))) (λ x1 . cn)) cr clt)) (proof)
Theorem df_mpaa : wceq cmpaa (cmpt (λ x0 . caa) (λ x0 . crio (λ x1 . w3a (wceq (cfv (cv x1) cdgr) (cfv (cv x0) cdgraa)) (wceq (cfv (cv x0) (cv x1)) cc0) (wceq (cfv (cfv (cv x0) cdgraa) (cfv (cv x1) ccoe)) c1)) (λ x1 . cfv cq cply))) (proof)
Theorem df_itgo : wceq citgo (cmpt (λ x0 . cpw cc) (λ x0 . crab (λ x1 . wrex (λ x2 . wa (wceq (cfv (cv x1) (cv x2)) cc0) (wceq (cfv (cfv (cv x2) cdgr) (cfv (cv x2) ccoe)) c1)) (λ x2 . cfv (cv x0) cply)) (λ x1 . cc))) (proof)
Theorem df_za : wceq cza (cfv cz citgo) (proof)