a
a:
. (a)sqr 
a:. a
(a)sqra,b:. ab 
(a)sqr(b)sqr
n
wrt(n,r+1) else r fi A & c = b Aa,b,c:A. (a = b = c) Prop b < c == ab & b < ca,b,c:. a b < c Propn:. (wrt(n,0))sqr n < (wrt(n,0)+1)sqr| def | rc_loop_sqrt_sqr | (a)sqr == aa |
| THM | rc_loop_sqrt_sqr_wf | a:. (a)sqr |
| THM | rc_loop_sqrt_sqr_le | a:. a(a)sqr |
| THM | rc_loop_sqrt_sqr_mono | a,b:. ab (a)sqr(b)sqr |
| def | rc_loop_sqrt_wrt | (rec) wrt(n,r) == if (r+1)sqrn wrt(n,r+1) else r fi |
| def | rc_loop_sqrt_eqeq | a = b = c == a = b A & c = b A |
| THM | rc_loop_sqrt_eqeq_wf | a,b,c:A. (a = b = c) Prop |
| def | rc_loop_sqrt_lelt | a b < c == ab & b < c |
| THM | rc_loop_sqrt_lelt_wf | a,b,c:. a b < c Prop |
| THM | rc_loop_sqrt_SFAversion | n:. (wrt(n,0))sqr n < (wrt(n,0)+1)sqr |