trunc[sigma: nat]: THEORY
BEGIN

  trunc(fb: real): real = floor(fb * 2 ^ sigma) * 2 ^ -sigma;

  minus_trunc: LEMMA
    FORALL (x1, x2: real): x1 - trunc(x2) < x1 - x2 + 2 ^ -sigma;

  plus_trunc: LEMMA
    FORALL (x1, x2: real, x3: nonneg_real):
      x1 + trunc(x2) * x3 <= x1 + x2 * x3;
END trunc

newton_fin[sigma: above(4)]: THEORY
 BEGIN
	 IMPORTING trunc[sigma]

  fb: VAR {x: posreal | 1 <= x AND x < 2};

  i: VAR nat;

  init: VAR real;

  newton_x(i, fb, init): RECURSIVE real =
	 IF (i = 0)
	   THEN trunc(init)
	 ELSE LET xi = newton_x(i - 1, fb, init),
			  zi = fb * xi,
			  Ai = 2 - trunc(zi) - 2 ^ -sigma
			IN trunc(xi * Ai)
	 ENDIF
	  MEASURE i;

  delta_i(i, fb, init): real = 1 / fb - newton_x(i, fb, init);

  delta_bound: LEMMA
	 0 < abs(delta_i(0, fb, init)) AND
	  abs(delta_i(0, fb, init)) < 1 / 4 AND
	   newton_x(0, fb, init) > 0 AND newton_x(0, fb, init) < 1
	  IMPLIES
	  newton_x(i, fb, init) > 0 AND
	   newton_x(i, fb, init) < 1 AND
		delta_i(i, fb, init) < 1 / 4 AND
		 (i >= 1 IMPLIES
		   delta_i(i, fb, init) > 0 AND
			delta_i(i, fb, init) <= 2 * delta_i(i - 1, fb, init) ^ 2 + 2 ^ (-sigma + 1));

 END newton_fin