WhoCites
Definitions
SquareRootLoop
Sections
NuprlLIB
Doc
Who Cites rc
loop
sqrt
wrt?
rc_loop_sqrt_wrt
Def wrt(n,r) == if (r+1)sqr
n
wrt(n,r+1) else r fi (recursive)
rc_loop_sqrt_sqr
Def
(a)sqr == a
a
Thm*
a:
. (a)sqr
le_int
Def
i
j ==
j <
i
Thm*
i,j:
. (i
j)
lt_int
Def
i <
j == if i < j
true
; false
fi
Thm*
i,j:
. (i <
j)
bnot
Def
b == if b
false
else true
fi
Thm*
b:
.
b
Syntax:
wrt(n,r)
has structure:
rc_loop_sqrt_wrt(r; n)
About:
WhoCites
Definitions
SquareRootLoop
Sections
NuprlLIB
Doc