round_fact2 [ N:above(1), P: posnat ] : THEORY
BEGIN

  IMPORTING alpha_rd_lem[N], round_correct[N,P], xmin[N,P];

  x, x2: VAR real;
  y: VAR factoring;

  mode: VAR rounding_mode;

  rnd_repr_l1: Lemma y=eta(x) IMPLIES
    eta(x)`e = eta(alpha_rep[y`e-P](x))`e;

  rnd_repr__l1: LEMMA FORALL(x: posreal, s: sign_rep):
      NOT integer?(x) IMPLIES
      floor(sign(s)*x) = floor(sign(s) * (1/4 + 1/2*floor(2*x)));

  rnd_repr__l2: LEMMA FORALL(x: posreal, s: sign_rep):
      NOT integer?(x) IMPLIES
      ceiling(sign(s)*x) = ceiling(sign(s) * (1/4 + 1/2*floor(2*x)));

	%%%% the next to lemmas also hold for x:real
  rnd_repr___l3a: LEMMA forall (x: posreal, s: sign_rep): NOT integer?(2*x) IMPLIES
    LET X=sign(s)*x IN
    (ceiling(X) - X > X - floor(X)
         IFF ceiling(X) - sign(s)*(floor(2*x)*1/2+1/4) >
           sign(s)*(floor(2*x)*1/2+1/4) - floor(X));

  rnd_repr___l3b: LEMMA forall (x: posreal, s: sign_rep): NOT integer?(2*x) IMPLIES
    LET X=sign(s)*x IN
    (ceiling(X) - X < X - floor(X)
         IFF ceiling(X) - sign(s)*(floor(2*x)*1/2+1/4) <
           sign(s)*(floor(2*x)*1/2+1/4) - floor(X));



  
rnd_repr_lem: LEMMA y=eta(x) AND (mode=to_pos OR mode=to_nearest) IMPLIES 
    round(x, mode, P) = round(alpha_rep[y`e-P](x), mode, P);

  rnd_repr: LEMMA y=eta(x) IMPLIES 
    round(x, mode, P) = round(alpha_rep[y`e-P](x), mode, P);

  rnd_equiv: LEMMA (y=eta(x) AND alpha_eq[y`e-P](x, x2)) IMPLIES 
    round(x, mode, P) = round(x2, mode, P);

  rnd_repr_hat: LEMMA (x/=0 AND y=eta_hat(x)) IMPLIES
    round(x, mode, P) = round(alpha_rep[y`e-P](x), mode, P);

  rnd_equiv_hat: LEMMA (x/=0 AND x2/=0 AND y=eta_hat(x) AND alpha_eq[y`e-P](x, x2)) 
    IMPLIES round(x, mode, P) = round(x2, mode, P);


  alpha_rep_real_fprec: Lemma  %% cb
    Forall (a: nonneg_real):
      real_fprec?[N,P](alpha_rep[-P-1](a)) Implies
        alpha_rep[-P-1](a) = a;

END round_fact2