Nuprl - Pf rc loop sqrt SFAversion

(10steps) PrintForm Definitions Lemmas SquareRootLoop Sections NuprlLIB Doc

At: rc loop sqrt SFAversion

n:. (wrt(n,0))sqr n < (wrt(n,0)+1)sqr

By: Auto

Generated subgoal:

1 1. n:
(wrt(n,0))sqr n < (wrt(n,0)+1)sqr

About:

(10steps) PrintForm Definitions Lemmas SquareRootLoop Sections NuprlLIB Doc