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

  IMPORTING ovf_unf[N, P]

  wrapped_x(x: real, mode: rounding_mode, OVFen, UNFen: bool): real =
            IF OVF(x, mode) AND OVFen
              THEN x * 2 ^ -Alpha[N]
            ELSE IF UNF(x, mode, UNFen) AND UNFen
                   THEN x * 2 ^ Alpha[N]
                 ELSE x
                 ENDIF
            ENDIF;

  rd_result(x: real, mode: rounding_mode, OVFen, UNFen: bool): real =
      round(wrapped_x(x, mode, OVFen, UNFen), mode, P);

  eta_wrapped_ovf: LEMMA FORALL(x: real, mode: rounding_mode):
		N>4 AND OVF(x, mode) IMPLIES
			eta(x * 2^-Alpha[N]) = 
				(# s:=eta(x)`s, e:=eta(x)`e-Alpha[N], f:=eta(x)`f #);

  eta_wrapped_unf: LEMMA FORALL(x: nonzero_real):
		N>4 AND TINY(x) AND abs(x)>=2^(emin[N]-Alpha[N]) IMPLIES
			eta(x * 2^Alpha[N]) = 
				(# s:=eta_hat(x)`s, e:=eta_hat(x)`e+Alpha[N], f:=eta_hat(x)`f #);

  eta_e_wrapped: LEMMA
    FORALL (x: nonzero_real, OVFen, UNFen: bool):
      LET xP =
            IF OVF_before(x) AND OVFen
              THEN x * 2 ^ -Alpha[N]
            ELSE IF TINY(x) AND UNFen THEN x * 2 ^ Alpha[N] ELSE x ENDIF
            ENDIF
        IN
        (((OVF_before(x) AND OVFen) OR (TINY(x) AND UNFen)) IMPLIES
          2 ^ emin <= abs(xP) AND abs(xP) <= 2 ^ emax)
         IMPLIES
         eta(xP)`e =
          IF TINY(x) AND NOT UNFen
            THEN emin
          ELSE eta_hat(x)`e +
                IF OVF_before(x) AND OVFen
                  THEN -Alpha[N]
                ELSE IF TINY(x) AND UNFen THEN Alpha[N] ELSE 0 ENDIF
                ENDIF
          ENDIF;

  eta_f_wrapped: LEMMA
    FORALL (x: nonzero_real, OVFen, UNFen: bool):
      LET xP =
            IF OVF_before(x) AND OVFen
              THEN x * 2 ^ -Alpha[N]
            ELSE IF TINY(x) AND UNFen THEN x * 2 ^ Alpha[N] ELSE x ENDIF
            ENDIF
        IN
        (((OVF_before(x) AND OVFen) OR (TINY(x) AND UNFen)) IMPLIES
          2 ^ emin <= abs(xP) AND abs(xP) <= 2 ^ emax)
         IMPLIES
         eta(xP)`f =
          IF TINY(x) AND NOT UNFen THEN eta(x)`f ELSE eta_hat(x)`f ENDIF;

  eta_ovf_after: LEMMA
    FORALL (x: nonzero_real, mode: rounding_mode):
      (N >= 4 AND OVF_after(x, mode)) IMPLIES
       eta(x * 2 ^ -Alpha[N]) =
        (# s := eta(x)`s, e := emax - Alpha, f := eta(x)`f #);

  eta_rd_result: LEMMA
    FORALL (x: nonzero_real, mode: rounding_mode, OVFen, UNFen: bool):
      N >= 4 IMPLIES
       LET y =
             eta(round(IF OVF_before(x) AND OVFen
                         THEN x * 2 ^ -Alpha
                       ELSE IF TINY(x) AND UNFen
                              THEN x * 2 ^ Alpha
                            ELSE x
                            ENDIF
                       ENDIF,
                       mode, P))
         IN
         eta(rd_result(x, mode, OVFen, UNFen)) =
          IF OVF_after(x, mode) AND OVFen
            THEN (# s := y`s, e := emax + 1 - Alpha, f := 1 #)
          ELSE y
          ENDIF;

  rd_result_small: LEMMA
    FORALL (x: nonzero_real, OVFen, UNFen: bool, mode: rounding_mode):
      LET xP =
            IF OVF_before(x) AND OVFen
              THEN x * 2 ^ -Alpha[N]
            ELSE IF TINY(x) AND UNFen THEN x * 2 ^ Alpha[N] ELSE x ENDIF
            ENDIF
        IN
        N >= 4 AND
         NOT (OVF(x, mode) AND NOT OVFen) AND
          (((OVF_before(x) AND OVFen) OR (TINY(x) AND UNFen)) IMPLIES
            2 ^ emin <= abs(xP) AND abs(xP) < 2 ^ emax)
         IMPLIES eta(rd_result(x, mode, OVFen, UNFen))`e <= emax;


   rd_result_rep: LEMMA
     FORALL(x: nonzero_real, OVFen, UNFen: bool, mode: rounding_mode):
         rd_result(x,mode,OVFen,UNFen) = 
			rd_result(alpha_rep[eta_hat(x)`e-P](x),mode,OVFen,UNFen);

   rd_result_eq: LEMMA
     FORALL(x1,x2: nonzero_real, OVFen, UNFen: bool, mode: rounding_mode):
       alpha_eq[eta_hat(x1)`e-P](x1,x2) IMPLIES
         rd_result(x1,mode,OVFen,UNFen) = rd_result(x2,mode,OVFen,UNFen);

 END wrapped_exp


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

  IMPORTING wrapped_exp[N, P], round_monoton[N,P], add_zero[N,P],
            fact_mul2[N,P]

   rd_result_0: LEMMA
     FORALL (mode: rounding_mode, OVFen, UNFen: bool):
       rd_result[N, P](0, mode, OVFen, UNFen) = 0;

   rd_result_pos_neg_refl: LEMMA
     FORALL (x: real, OVFen, UNFen: bool):
       rd_result[N, P](-x, to_pos, OVFen, UNFen) =
        -rd_result[N, P](x, to_neg, OVFen, UNFen);

   rd_result_neg_pos_refl: LEMMA
     FORALL (x: real, OVFen, UNFen: bool):
       rd_result[N, P](-x, to_neg, OVFen, UNFen) =
        -rd_result[N, P](x, to_pos, OVFen, UNFen);

   rd_result_nearest_refl: LEMMA
     FORALL (x: real, OVFen, UNFen: bool):
       rd_result[N, P](x, to_nearest, OVFen, UNFen) =
        -rd_result[N, P](-x, to_nearest, OVFen, UNFen);

   rd_result_zero_refl: LEMMA
     FORALL (x: real, OVFen, UNFen: bool):
       rd_result[N, P](x, to_zero, OVFen, UNFen) =
        -rd_result[N, P](-x, to_zero, OVFen, UNFen);

   round_gt_0_rd_result_gt_0: LEMMA
     FORALL (x: real, mode: rounding_mode, OVFen, UNFen: bool):
       x >= Xmin and N >= 4 AND P > 1 IMPLIES
        round[N, P](x, mode, P) > 0 IMPLIES
         rd_result[N, P](x, mode, OVFen, UNFen) > 0;

   round_lt_0_rd_result_lt_0: LEMMA
     FORALL (x: real, mode: rounding_mode, OVFen, UNFen: bool):
       x <= -Xmin and N >= 4 AND P > 1 IMPLIES
        round[N, P](x, mode, P) < 0 IMPLIES
         rd_result[N, P](x, mode, OVFen, UNFen) < 0;

   rd_result_sum_gt_0: LEMMA
     FORALL (a, b: (ff_i3e_number?[N, P]), mode: rounding_mode,
             OVFen, UNFen: bool):
       LET sum = value[N](a) + value[N](b) IN
         N >= 4 AND P > 1 IMPLIES
          sum > 0 IMPLIES rd_result[N, P](sum, mode, OVFen, UNFen) > 0;

   rd_result_sum_lt_0: LEMMA
     FORALL (a, b: (ff_i3e_number?[N, P]), mode: rounding_mode,
             OVFen, UNFen: bool):
       LET sum = value[N](a) + value[N](b) IN
         N >= 4 AND P > 1 IMPLIES
          sum < 0 IMPLIES rd_result[N, P](sum, mode, OVFen, UNFen) < 0;

   rd_result_diff_gt_0: LEMMA
     FORALL (a, b: (ff_i3e_number?[N, P]), mode: rounding_mode,
             OVFen, UNFen: bool):
       LET sum = value[N](a) - value[N](b) IN
         N >= 4 AND P > 1 IMPLIES
          sum > 0 IMPLIES rd_result[N, P](sum, mode, OVFen, UNFen) > 0;

   rd_result_diff_lt_0: LEMMA
     FORALL (a, b: (ff_i3e_number?[N, P]), mode: rounding_mode,
             OVFen, UNFen: bool):
       LET sum = value[N](a) - value[N](b) IN
         N >= 4 AND P > 1 IMPLIES
          sum < 0 IMPLIES rd_result[N, P](sum, mode, OVFen, UNFen) < 0;

end rd_result_props