newton1: THEORY
BEGIN

	fb: VAR { x: posreal | x<2 };
	i: VAR nat;

	newton_init(fb): real;

	newton_x(i, fb): RECURSIVE real =
		IF (i=0) THEN newton_init(fb) 
		ELSE newton_x(i-1, fb)*(2 - fb * newton_x(i-1, fb))
		ENDIF
	MEASURE i;

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

	delta_i_lem: LEMMA delta_i(i+1, fb)=fb*delta_i(i,fb)^2;

	delta_bound: LEMMA delta_i(i+1, fb) <= 2*delta_i(i, fb)^2;

	delta_ge0: LEMMA i>=1 IMPLIES delta_i(i,fb)>=0;

END newton1