div_initial: THEORY
 BEGIN

  IMPORTING lookup, newton_fin[57]

  fb: VAR bvec[53];

  reziprok_convex: LEMMA
    FORALL (x, y: {z: posreal | 1 <= z AND z < 2}, d: posreal):
      abs(x - y) <= d IMPLIES abs(1 / x - 1 / y) <= d;

  prod_pow_2: LEMMA
    FORALL (n, m: above(1), a: bvec[n], b: bvec[m]):
      bv2nat(a) * bv2nat(b) = 2 ^ (n + m - 2) IMPLIES
       (a = fill[1](TRUE) o fill[n - 1](FALSE) AND
         b = fill[1](TRUE) o fill[m - 1](FALSE));

  lookup_impl(addr: bvec[8]): bvec[8]
		= lookup_div(bv2nat(addr));
	%%%%%%%%%%%%%%%%%%
	%%%%% NOTE: this is an axiom in the sense of hardware generation,
	%%%%		since bv2nat is not synthesizable; we require the lookup-
	%%%%		ROM to obey the above definition, ie., to return the correct
	%%%%		value adressed by addr.
	%%%%%%%%%%%%%%%%%%

  initial_impl(fb): bvec[58] =
      fill[1](FALSE) o fill[1](TRUE) o lookup_impl(fb ^ (51, 44)) o fill[48](FALSE);

  initial_ok: LEMMA
    LET Fb = bv2nat(fb) / 2 ^ 52,
        init = initial_impl(fb),
        I = bv2nat(init) / 2 ^ 57
      IN
      1 <= Fb AND Fb < 2 IMPLIES
       (0 < abs(1 / Fb - I) AND abs(1 / Fb - I) <= 1 / 256);

  initial_ok2: LEMMA
    LET Fb = bv2nat(fb) / 2 ^ 52,
        init = initial_impl(fb),
        I = bv2nat(init) / 2 ^ 57
      IN
      1 <= Fb AND Fb < 2 IMPLIES
       0 < abs(delta_i(0, Fb, I)) AND
        abs(delta_i(0, Fb, I)) < 1 / 4 AND
         newton_x(0, Fb, I) > 0 AND newton_x(0, Fb, I) < 1;

  delta_bound_57: LEMMA
    LET Fb = bv2nat(fb) * 2 ^ -52,
        init = initial_impl(fb),
        I = bv2nat(init) * 2 ^ -57
      IN
      1 <= Fb AND Fb < 2 IMPLIES
       abs(delta_i(0, Fb, I)) <= 1 / 256 AND
        delta_i(1, Fb, I) < 101 / 100 * 2 ^ -15 AND
         delta_i(2, Fb, I) < 11 / 10 * 2 ^ -29 AND
          delta_i(3, Fb, I) < 2 ^ -55 AND
           0 < delta_i(2, Fb, I) AND 0 < delta_i(3, Fb, I);
 END div_initial