Origin Definitions Sections NuprlLIB Doc

SquareRootLoop
Nuprl Section: SquareRootLoop - Stand-alone exercise: loop computing natural number square root
Selected Objects
defrc_loop_sqrt_sqr(a)sqr == aa
THMrc_loop_sqrt_sqr_wfa:. (a)sqr
THMrc_loop_sqrt_sqr_lea:. a(a)sqr
THMrc_loop_sqrt_sqr_monoa,b:. ab (a)sqr(b)sqr
defrc_loop_sqrt_wrt(rec) wrt(n,r) == if (r+1)sqrn wrt(n,r+1) else r fi
defrc_loop_sqrt_eqeqa = b = c == a = b A & c = b A
THMrc_loop_sqrt_eqeq_wfa,b,c:A. (a = b = c) Prop
defrc_loop_sqrt_lelta b < c == ab & b < c
THMrc_loop_sqrt_lelt_wfa,b,c:. a b < c Prop
THMrc_loop_sqrt_SFAversionn:. (wrt(n,0))sqr n < (wrt(n,0)+1)sqr

Contrast this program wrt(n,r) with the extract found near the bottom of Extraction.

Origin Definitions Sections NuprlLIB Doc