ground	: THEORY
BEGIN

% Also defined in the NASA reals library
sqrt_newton(a:nnreal,n:nat): RECURSIVE posreal =
  IF n=0 THEN a+1
  ELSE let r=sqrt_newton(a,n-1) IN
    (1/2)*(r+a/r)
  ENDIF
  MEASURE n+1

%M-x pvsio
% <PVSio> (sqrt_newton(2,1));
% 11/6
% <PVSio> (sqrt_newton(2,3));
% 72097/50952 
%println(sqrt_newton(2,10));
%<PVSio> println(sqrt_newton2(2,10));
%1.4142135

%Has been shown to satisfy
% sqrt(a) < sqrt_newton(a, n)
% sqrt_newton(a, n+1) < sqrt_newton(a,n)
% As n --> infinity, sqrt_newton(a,n) converges to sqrt(q)

test: CONJECTURE
      2 < sqrt_newton(2, 10) * sqrt_newton(2, 10)
      AND
      sqrt_newton(2, 10) * sqrt_newton(2, 10) < 2.0000000000000001

%|- test : PROOF
%|- (eval-formula 1)
 %|- QED

% PVSio safely enables the ground evaluator in the theorem
% prover.

END ground