%Patch files loaded: (patch2) version 2.376

$$$IEEE_854.pvs
IEEE_854 [b,p:above(1),alpha,E_max,E_min:integer]: THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  This theory defines the representation and basic operations for 
%    arbitrary precision IEEE-854 floating point numbers.  It also 
%    introduces the required assumption for arbitrary precision
%    IEEE-854 floating point numbers.
%
%  Example use:
%
%   To define IEEE-754 single-precision operations use the following
%     importing:
%   
%     IMPORTING IEEE_854[2,24,192,127,-126]
%
%  Author: 
%  Paul S. Miner                | email: p.s.miner@larc.nasa.gov
%  1 South Wright St. / MS 130  |   fax: (804) 864-4234
%  NASA Langley Research Center | phone: (804) 864-6201
%  Hampton, Virginia 23681      |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  BEGIN

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Representation assumptions (from section 3.1 of IEEE-854)
  ASSUMING

    Base_values: ASSUMPTION b=2 or b=10

    Exponent_range: ASSUMPTION (E_max - E_min)/p > 5 %10 % may be 5

    Significand_size: ASSUMPTION b^(p-1)>=10^5 

%  Uncomment the following, if you wish to include the suggestion
%   about exponent balance .

    E_balance: ASSUMPTION
        IF b < 4 THEN E_max + E_min = 1 ELSE E_max + E_min = 0 ENDIF

% Although not mentioned explicitly as a parameter.  We need the following 
% value for adjusting the exponent of overflow and underflow results when the 
% corresponing traps are enabled.

% Section 7.3 of IEEE-854 states: `` The exponent adjustment $\alpha$
% for a precision shall be chosen to be approximately 
% $3\times(\Emax - \Emin)/4$ for that precision and should be
% divisible by twelve.''

    Exponent_Adjustment: ASSUMPTION
         abs(alpha - (3 * (E_max - E_min) / 4)) <= 6 
          & integer?(alpha / 12) 

  ENDASSUMING
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Assumption about balanced exponents as given in standard
%  (comment out if you do not desire this constraint)

  Exponent_balance: LEMMA b^(E_max+E_min) <4 & 4<=b^(E_max+E_min+1)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  A useful consequence of the assumptions

  E_max_gt_E_min: lemma E_max > E_min

% An illustrative example for HUG95 paper
  HUG_example: lemma 5*p < E_max-E_min  => E_min < E_max

% Simple examples showing how importing tccs may be automatically proven
  ex754_2:lemma (127 - (-126))/24 > 5

  ex754_3: lemma 2^23 >=10^5

% Some beneficial consequences of assumption E_balance
%  (These cannot be proven without E_balance)

  E_min_neg: lemma E_min<0

  E_max_pos: lemma E_max>0

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  Importing IEEE_854_defs[b,p,alpha,E_max,E_min]

  

  END IEEE_854

$$$IEEE_854.prf
(IEEE_854 (|Exponent_range_TCC1| "" (TCC) NIL)
 (|Significand_size_TCC1| "" (TCC :DEFS !) NIL)
 (|Exponent_balance_TCC1| "" (TCC :DEFS !) NIL)
 (|Exponent_balance_TCC2| "" (TCC :DEFS !) NIL)
 (|Exponent_balance| "" (LEMMA "E_balance")
  (("" (LEMMA "expt_x1")
    (("" (INST?)
      (("" (LEMMA "expt_x0")
        (("" (INST?)
          (("" (GROUND)
            (("" (LEMMA "expt_plus")
              (("" (INST - "1" "E_max+E_min" "b")
                (("" (ASSERT)
                  (("" (TYPEPRED "b")
                    (("" (CASE "forall (i:above(1)): 4<=i*i")
                      (("1" (INST?) (("1" (ASSERT) NIL)))
                       ("2" (INDUCT "i" 1 "above_induction[1]")
                        (("1" (ASSERT) NIL)
                         ("2" (SKOSIMP*)
                          (("2" (ASSERT)
                            NIL)))))))))))))))))))))))))))
 (|E_max_gt_E_min| "" (LEMMA "Exponent_range")
  (("" (REWRITE "div_mult_pos_gt2") (("" (ASSERT) NIL)))))
 (|HUG_example| "" (GROUND) NIL) (|ex754_2| "" (ASSERT) NIL)
 (|ex754_3| "" (GRIND) NIL)
 (|E_min_neg| "" (LEMMA "E_balance")
  (("" (LEMMA "Exponent_range")
    (("" (REWRITE "div_mult_pos_gt2") (("" (GROUND) NIL)))))))
 (|E_max_pos| "" (LEMMA "E_balance")
  (("" (LEMMA "Exponent_range")
    (("" (REWRITE "div_mult_pos_gt2") (("" (GROUND) NIL)))))))
 (IMPORTING1_TCC1 "" (REWRITE "E_max_gt_E_min") NIL)
 (IMPORTING1_TCC2 "" (INST 1 "E_max - 1") NIL))
$$$IEEE_854_defs.pvs
IEEE_854_defs 
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min],
            IEEE_854_remainder[b,p,alpha,E_max,E_min],
            IEEE_854_fp_int[b,p,alpha,E_max,E_min],
            arithmetic_ops[b,p,alpha,E_max,E_min],
            comparison1[b,p,E_max,E_min],
            infinity_arithmetic[b,p,E_max,E_min],
            NaN_ops[b,p,E_max,E_min],
            enumerated_type_defs,
            sqrt

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% basic instruction schemata, ignoring exceptions for now
%  These functions are listed in section 5.1 of IEEE-854

  fp,fp1,fp2: var fp_num
  mode: var rounding_mode

% Addition operator
  fp_add(fp1, fp2, mode): fp_num =
    IF finite?(fp1) & finite?(fp2)
      THEN fp_op(add, fp1, fp2, mode)
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(add, fp1, fp2)
    ELSE fp_add_inf(fp1, fp2)
    ENDIF

% Addition operator with exceptions
  fp_add_x(fp1, fp2, mode): [fp_num, exception] =
    IF finite?(fp1) & finite?(fp2)
      THEN fp_op_x(add, fp1, fp2, mode)
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan_x(add, fp1, fp2)
    ELSE fp_add_inf_x(fp1, fp2)
    ENDIF

  fp_add_x_correct: lemma fp_add(fp1,fp2,mode) = proj_1(fp_add_x(fp1,fp2,mode))

% Subtraction Operator
  fp_sub(fp1, fp2, mode): fp_num =
    IF finite?(fp1) & finite?(fp2)
      THEN fp_op(sub, fp1, fp2, mode)
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(sub, fp1, fp2)
    ELSE fp_sub_inf(fp1, fp2)
    ENDIF

% Subtraction Operator with exceptions
  fp_sub_x(fp1, fp2, mode): [fp_num, exception] =
    IF finite?(fp1) & finite?(fp2)
      THEN fp_op_x(sub, fp1, fp2, mode)
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan_x(sub, fp1, fp2)
    ELSE fp_sub_inf_x(fp1, fp2)
    ENDIF

% Excluding NaN operands, we should be able to prove a - b = a + (-b)
%  independent of the rounding mode  
  fsub_alt_def: LEMMA
        NOT (NaN?(fp1) OR NaN?(fp2))
          => fp_sub(fp1, fp2, mode) = fp_add(fp1, toggle_sign(fp2), mode)

% Multiplication
  fp_mul(fp1, fp2, mode): fp_num =
    IF finite?(fp1) & finite?(fp2)
      THEN fp_op(mult, fp1, fp2, mode)
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(mult, fp1, fp2)
    ELSE fp_mul_inf(fp1, fp2)
    ENDIF
  
% Division
  fp_div(fp1, fp2, mode): fp_num =
    IF finite?(fp1) & finite?(fp2)
      THEN IF zero?(fp2)
        THEN IF zero?(fp1)
          THEN invalid
        ELSE infinite(mult_sign(fp1, fp2))
        ENDIF
      ELSE fp_op(div, fp1, fp2, mode)
      ENDIF
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(div, fp1, fp2)
    ELSE fp_div_inf(fp1, fp2)
    ENDIF

% Remainder (independent of rounding mode)
  fp_rem(fp1, fp2): fp_num =
    IF finite?(fp1) & finite?(fp2)
      THEN IF zero?(fp2)
        THEN invalid
      ELSE REM(fp1, fp2)
      ENDIF
    ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(div, fp1, fp2)
    ELSIF infinite?(fp1) THEN invalid
    ELSE fp1
    ENDIF

% Square root

  fp_sqrt(fp, mode): fp_num =
    IF NaN?(fp) THEN NaN_sqrt(fp)
    ELSIF zero?(fp) THEN fp
    ELSIF finite?(fp)
      THEN IF sign(fp) = pos
        THEN real_to_fp(fp_round(sqrt(value(fp)), mode))
      ELSE invalid
      ENDIF
    ELSIF i_sign(fp) = pos THEN fp
    ELSE invalid
    ENDIF

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% bug test spec, won't typecheck, 
%% cannot determine full theory instance
%  fp_id(fp):fp_num =
%    cases fp of
%      finite(s,e,d): fp,
%      infinite(s): fp,
%      NaN(sig,data):fp
%    endcases
  
  END IEEE_854_defs

$$$IEEE_854_defs.prf
(|IEEE_854_defs| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
 (|fp_add_TCC1| "" (SKOSIMP*) NIL) (|fp_add_TCC2| "" (SKOSIMP*) NIL)
 (|fp_add_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|fp_add_TCC4| "" (SKOSIMP*) (("" (GROUND) NIL)))
 (|fp_add_x_correct| "" (SKOSIMP*)
  (("" (EXPAND "fp_add")
    (("" (EXPAND "fp_add_x")
      (("" (LIFT-IF)
        (("" (EXPAND "fp_nan")
          (("" (EXPAND "fp_nan_x")
            (("" (EXPAND "fp_add_inf")
              (("" (EXPAND "fp_add_inf_x")
                (("" (GROUND)
                  (("" (EXPAND "fp_op")
                    (("" (EXPAND "fp_op_x")
                      (("" (EXPAND "real_to_fp_x")
                        (("" (EXPAND "fp_round")
                          (("" (EXPAND "fp_round_x")
                            ((""
                              (LIFT-IF)
                              ((""
                                (EXPAND "round_exceptions")
                                ((""
                                  (PROPAX)
                                  NIL)))))))))))))))))))))))))))))))))
 (|fsub_alt_def| "" (SKOSIMP*)
  (("" (EXPAND "fp_sub")
    (("" (EXPAND "fp_add")
      (("" (REWRITE "toggle_finite")
        (("" (REWRITE "toggle_NaN")
          (("" (LIFT-IF)
            (("" (ASSERT)
              (("" (SPLIT)
                (("1" (FLATTEN)
                  (("1" (EXPAND "fp_op")
                    (("1" (EXPAND "apply")
                      (("1" (REWRITE "value_toggle")
                        (("1" (ASSERT)
                          (("1" (LIFT-IF)
                            (("1"
                              (ASSERT)
                              (("1"
                                (GROUND)
                                (("1"
                                  (EXPAND "signed_zero")
                                  (("1"
                                    (CASE
                                     "forall fp: zero?(toggle_sign(fp)) iff zero?(fp)")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (REPLACE -1)
                                        (("1"
                                          (CASE
                                           "forall (fin1,fin2: (finite?)): (sign(fin1) = sign(toggle_sign(fin2))) iff (sign(fin1) /= sign(fin2))")
                                          (("1"
                                            (INST?)
                                            (("1"
                                              (REPLACE -1)
                                              (("1" (PROPAX) NIL)))))
                                           ("2"
                                            (HIDE -1 -2 -3 -4 2 3 4)
                                            (("2"
                                              (SKOSIMP*)
                                              (("2"
                                                (EXPAND
                                                 "toggle_sign")
                                                (("2"
                                                  (TYPEPRED
                                                   "sign(fin1!1)")
                                                  (("2"
                                                    (TYPEPRED
                                                     "sign(fin2!1)")
                                                    (("2"
                                                      (GROUND)
                                                      NIL)))))))))))
                                           ("3"
                                            (HIDE -1 -2 -3 -4 2 3 4)
                                            (("3"
                                              (SKOSIMP*)
                                              (("3"
                                                (REWRITE
                                                 "toggle_finite")
                                                NIL)))))))))))
                                     ("2"
                                      (HIDE -1 -2 -3 2 3 4)
                                      (("2"
                                        (SKOSIMP*)
                                        (("2"
                                          (EXPAND "zero?")
                                          (("2"
                                            (REWRITE "toggle_finite")
                                            (("2"
                                              (REWRITE
                                               "value_toggle")
                                              (("2"
                                                (GROUND)
                                                NIL)))))))))))))))))))))))))))))))
                 ("2" (FLATTEN)
                  (("2" (REWRITE "fp_sub_inf_def")
                    (("1" (GROUND) NIL)
                     ("2" (GROUND) NIL)))))))))))))))))))))
 (|fp_div_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|fp_sqrt_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "value_positive") (("" (INST?) (("" (ASSERT) NIL)))))))
 (|fp_sqrt_TCC2| "" (TCC) NIL))
$$$IEEE_854_values.pvs
IEEE_854_values 
  [b,p:above(1),
   E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This file defines the set of values that must be represented in each
% supported precision of an instance of IEEE-854
% 
% Author:
%  Paul S. Miner                | email: p.s.miner@larc.nasa.gov
%  1 South Wright St. / MS 130  |   fax: (804) 864-4234
%  NASA Langley Research Center | phone: (804) 864-6201
%  Hampton, Virginia 23681      |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  BEGIN

  IMPORTING sum_hack, %for use until we have good summation library
            sum_lemmas[b], % these are more specialized
            enumerated_type_defs

  Exponent: type = {i:int| E_min <= i & i <= E_max}

  digits: type = [below(p)->below(b)]

 
  fp_num: datatype
   begin
    finite(sign:sign_rep,Exp:Exponent,d:digits):finite?
    infinite(i_sign:sign_rep): infinite?
    NaN(status:NaN_type, data:NaN_data): NaN?
   end fp_num

% A mapping from finite floating point numbers to real numbers
%  This corresponds to the interpretation given in the standard
%  section 3.1
  fin : var (finite?)

  value_digit(d:digits)(n:nat):nonneg_real = 
     if n<p then d(n)*b^(-n) else 0 endif

  value(fin): real =
    (-1) ^ sign(fin) * b ^ Exp(fin) * Sum(p, value_digit(d(fin)))

% Predicate testing whether an fp_num is 0
  zero?(fp:fp_num):bool = if finite?(fp) then value(fp)=0 else false endif

  shift_left((d: digits)): digits =
    LAMBDA (i: below(p)): IF (i + 1 = p) THEN 0 ELSE d(i + 1) ENDIF

% Function normalize takes a finite and returns the finite of 
% equivalent value with the smallest possible exponent.
  normalize(fin:(finite?)): recursive (finite?) = 
     IF Exp(fin) = E_min or d(fin)(0) /= 0 then
        fin
     ELSE
        normalize(finite(sign(fin),Exp(fin)-1,shift_left(d(fin))))
     ENDIF
  measure lambda (fin:(finite?)): Exp(fin) - E_min

  normalize_idempotent: FACT
        FORALL (fin: (finite?)): normalize(normalize(fin)) = normalize(fin)

% Predicate testing whether an fp_num is subnormal:
% Section 2 of the standard defines a subnormal (denormal in IEEE-754)
% number as a nonzero finite number whose exponent is the precision's 
% minimum and whose leading significant digit is zero.
  subnormal?(fp: fp_num): bool =
    IF finite?(fp)  THEN 
        not zero?(fp)
        & Exp(normalize(fp)) = E_min
        & d(normalize(fp))(0) = 0
    ELSE FALSE
    ENDIF

% Predicate testing whether an fp_num is normal:
% Section 2 of the standard defines a normal number as 
% a nonzero finite number that is not subnormal
  normal?((fp: fp_num)): bool =
    IF finite?(fp) THEN d(normalize(fp))(0) > 0 ELSE FALSE ENDIF

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some definitions and theorems to help illustrate the correctness
%  of the definition of value.

% Maximum and Minimum representable values
  max_significand:digits = 
    (lambda (i:below(p)): b-1)
  min_significand: digits =
    (LAMBDA (i: below(p)): IF i < p - 1 THEN 0 ELSE 1 ENDIF)
  d_zero: digits = LAMBDA (i: below(p)): 0

  m,n: var nat

  Sum_value0: lemma Sum(n,value_digit(d_zero)) = 0

  s: var sign_rep
  E: var Exponent

  zero_finite_d_zero: lemma zero?(finite(s,E,d_zero))

  max_fp_pos : fp_num = finite(pos,E_max,max_significand)
  min_fp_pos : fp_num = finite(pos,E_min,min_significand)
  pos_zero   : {fin|zero?(fin)}= finite(pos,E_min,d_zero)

  max_fp_neg : fp_num = finite(neg,E_max,max_significand)
  min_fp_neg : fp_num = finite(neg,E_min,min_significand)
  neg_zero   : {fin|zero?(fin)} = finite(neg,E_min,d_zero)

  max_pos: posreal = value(max_fp_pos)
  min_pos: posreal = value(min_fp_pos)

  max_neg: negreal = value(max_fp_neg)
  min_neg: negreal = value(min_fp_neg)

  max_fp_correct: THEOREM 
     max_pos = b ^ (E_max +1) - b ^ (E_max + 1 - p)

  min_fp_correct: THEOREM 
     value(min_fp_pos) = b ^ (E_min + 1 - p)

% Value of zero

  value0: lemma value(fin)=0 iff d(fin)=d_zero

  value_of_zero: THEOREM 
     value(pos_zero) = 0

% Normalization preserves the value

  normal_value: lemma 
     value(fin) = value(normalize(fin))

% sign determines algebraic sign of value
  value_positive: lemma

    (sign(fin)=pos & not zero?(fin)) <=> value(fin)>0

  value_negative: lemma
    (sign(fin)=neg & not zero?(fin)) <=> value(fin)<0

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  finite_cover: lemma zero?(fin) or normal?(fin) or subnormal?(fin)

  finite_disjoint1: lemma not (zero?(fin) & normal?(fin))

  finite_disjoint2: lemma not (zero?(fin) & subnormal?(fin))

  finite_disjoint3: lemma not (normal?(fin) & subnormal?(fin))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 
  fp,fp1,fp2: var fp_num

% reverse the sign of a floating point number
  toggle_sign(fp): fp_num
    =
    cases fp of
      finite(s,e,d): finite(1-s,e,d),
      infinite(s): infinite(1-s),
      NaN(sig,data): fp
    endcases

  toggle_finite: lemma finite?(toggle_sign(fp)) iff finite?(fp)
  toggle_infinite: lemma infinite?(toggle_sign(fp)) iff infinite?(fp)
  toggle_NaN: lemma NaN?(toggle_sign(fp)) iff NaN?(fp)

  value_toggle: lemma value(toggle_sign(fin)) = -value(fin) 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  toggle_d_normalize: lemma 
     d(normalize(toggle_sign(fin))) = d(normalize(fin))

  toggle_Exp_normalize: lemma 
     Exp(normalize(toggle_sign(fin))) = Exp(normalize(fin))

  toggle_zero?: lemma zero?(toggle_sign(fin)) iff zero?(fin)

  toggle_normal?: lemma normal?(toggle_sign(fin)) iff normal?(fin)

  toggle_subnormal?: lemma subnormal?(toggle_sign(fin)) iff subnormal?(fin)

% Sum lemmas

  d: var digits

  j : var nat

  value_digit_le: lemma value_digit(d)(j) <= (b-1) * b^(-j)

  Sum_d_lt_b: lemma Sum(j+1,value_digit(d)) <= b - b^(-j)

  Sum_d_lt1: lemma d(0)=0 => Sum(j+1,value_digit(d)) <= 1-b^(-j)

  Sum_d_ge1: lemma d(0)>0 => Sum(j+1,value_digit(d)) >= 1

  value_sig_lt_b: lemma Sum(p,value_digit(d)) < b

  value_sig_lt1: lemma d(0)=0 => Sum(p,value_digit(d)) < 1

  value_sig_ge1: lemma d(0)>0 => Sum(p,value_digit(d)) >= 1

  abs_value_fin: lemma 
      abs(value(fin)) = b^(Exp(fin)) * Sum(p,value_digit(d(fin)))

  min_significand_min: lemma d/=d_zero => 
            Sum(p,value_digit(min_significand))<= Sum(p,value_digit(d))

  sign_normal: lemma sign(fin) = sign(normalize(fin))

  value_normal: lemma normal?(fin) => 
            b^E_min <= abs(value(fin)) & abs(value(fin)) <= max_pos

  value_subnormal: lemma subnormal?(fin) => 
            min_pos <= abs(value(fin)) & abs(value(fin)) < b^E_min 

  value_nonzero: lemma not zero?(fin) =>
            min_pos <= abs(value(fin)) & abs(value(fin)) <= max_pos

%mod(floor(Sum(p, value_digit(d(normalize(fin!1)))) * b ^ x!1), b)
%        = d(normalize(fin!1))(x!1)

    scale_value(d,m)(n): nonneg_real = value_digit(d)(n) * b^m

    scaled_Sum_int: lemma forall d,n:
       forall (m:upto(n+1)): integer?(Sum(m,scale_value(d,n)))

    scale_value_p(d)(n): nat = scale_value(d,p-1)(n)

    i: var below(p)

    scaled_Sum_i: lemma 
        Sum(n,value_digit(d))*b^(i) = Sum(n,scale_value(d,i))

    scaled_Sum: lemma 
        Sum(n,value_digit(d))*b^(p-1) = Sum(n,scale_value_p(d))

    floor_Sum: lemma 
        floor(Sum(p,value_digit(d)) * b^i) = 
             Sum(i+1,scale_value(d,i))

    mod_Sum: lemma mod(Sum(i+1,scale_value(d,i)),b)=d(i)

%%%%%%%%%
%
%  The next two declarations are here for importing purposes.

% A dummy fp_num to be used as a place holder.  Any definition that 
% returns holder is not yet finished.
  holder:fp_num

% An undefined NaN for functions to return when the invalid exception
% should be raised.  This serves as a placeholder until this specification 
% accounts for exceptions.
%
  invalid: (NaN?) = NaN(quiet,invalid_data)

  END IEEE_854_values

$$$IEEE_854_values.prf
(|IEEE_854_values| (|digits_TCC1| "" (SUBTYPE-TCC) NIL)
 (|digits_TCC2| "" (SUBTYPE-TCC) NIL)
 (|value_digit_TCC1| "" (TCC :DEFS !) NIL)
 (|value_digit_TCC2| "" (SKOSIMP*)
  (("" (TYPEPRED "d!1(n!1)")
    (("1" (LEMMA "expt_pos")
      (("1" (INST?)
        (("1" (REWRITE "pos_times_ge") (("1" (ASSERT) NIL)))
         ("2" (ASSERT) NIL)))))
     ("2" (PROPAX) NIL)))))
 (|value_TCC1| "" (TCC :DEFS !) NIL)
 (|shift_left_TCC1| "" (TCC :DEFS !) NIL)
 (|shift_left_TCC2| "" (TCC :DEFS !) NIL)
 (|normalize_TCC1| "" (TCC :DEFS !) NIL)
 (|normalize_TCC2| "" (TCC :DEFS !) NIL)
 (|normalize_TCC3| "" (TCC :DEFS !) NIL)
 (|normalize_TCC4| "" (TCC :DEFS !) NIL)
 (|normalize_idempotent| "" (SKOSIMP*)
  (("" (CASE-REPLACE "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
    (("1" (HIDE -1)
      (("1"
        (CASE "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
     normalize(normalize(finite(s,n+E_min,d)))=normalize(finite(s,n+E_min,d))")
        (("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
          (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
         ("2" (HIDE 2)
          (("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
            (("1" (SKOSIMP*)
              (("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))))
             ("2" (SKOSIMP*)
              (("2" (REWRITE "normalize" +)
                (("2" (LIFT-IF)
                  (("2" (GROUND)
                    (("1" (REWRITE "normalize") NIL)
                     ("2" (INST?) NIL)))))))))))))
         ("3" (ASSERT) NIL)))))
     ("2" (ASSERT) (("2" (REWRITE "fp_num_finite_eta") NIL)))))))
 (|subnormal?_TCC1| "" (TCC :DEFS !) NIL)
 (|normal?_TCC1| "" (TCC :DEFS !) NIL)
 (|max_significand_TCC1| "" (TCC :DEFS !) NIL)
 (|min_significand_TCC1| "" (TCC :DEFS !) NIL)
 (|min_significand_TCC2| "" (TCC :DEFS !) NIL)
 (|d_zero_TCC1| "" (TCC :DEFS !) NIL)
 (|Sum_value0| "" (INDUCT-AND-SIMPLIFY "n") (("" (GRIND) NIL)))
 (|zero_finite_d_zero| "" (GRIND :REWRITES "Sum_value0") NIL)
 (|max_fp_pos_TCC1| "" (TCC :DEFS !) NIL)
 (|min_fp_pos_TCC1| "" (TCC :DEFS !) NIL)
 (|pos_zero_TCC1| "" (REWRITE "zero_finite_d_zero") NIL)
 (|neg_zero_TCC1| "" (REWRITE "zero_finite_d_zero") NIL)
 (|max_pos_TCC1| "" (TCC :DEFS !) NIL)
 (|max_pos_TCC2| "" (EXPAND "value")
  (("" (EXPAND "max_fp_pos")
    (("" (EXPAND "pos")
      (("" (REWRITE "expt_x0")
        (("" (LEMMA "pos_times_gt")
          (("" (ASSERT)
            (("" (INST?)
              (("" (ASSERT)
                (("" (LEMMA "expt_pos")
                  (("" (INST?)
                    (("" (ASSERT)
                      ((""
                        (CASE "Sum(p, value_digit(max_significand)) > 0")
                        (("1" (GROUND) NIL)
                         ("2" (HIDE -1 -2 2)
                          (("2" (EXPAND "Sum")
                            (("2"
                              (ASSERT)
                              (("2"
                                (LEMMA "Sum_nonneg")
                                (("2"
                                  (INST?)
                                  (("2"
                                    (REWRITE "value_digit")
                                    (("2"
                                      (REWRITE "max_significand")
                                      (("2"
                                        (LEMMA "expt_pos")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (LEMMA "pos_times_gt")
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (GROUND)
                                                NIL)))))))))))))))))))))))))))))))))))))))))))))))
 (|min_pos_TCC1| "" (TCC) NIL)
 (|min_pos_TCC2| "" (EXPAND "min_fp_pos")
  (("" (EXPAND "value")
    (("" (EXPAND "pos")
      (("" (REWRITE "expt_x0")
        (("" (LEMMA "expt_pos")
          (("" (INST?)
            (("1" (ASSERT)
              (("1" (LEMMA "pos_times_gt")
                (("1" (INST?)
                  (("1" (ASSERT)
                    (("1"
                      (CASE "Sum(p, value_digit(min_significand)) > 0")
                      (("1" (ASSERT) (("1" (ASSERT) NIL)))
                       ("2" (HIDE -1 -2 2)
                        (("2" (EXPAND "Sum")
                          (("2" (LEMMA "Sum_nonneg")
                            (("2"
                              (INST?)
                              (("2"
                                (REWRITE "value_digit")
                                (("2"
                                  (REWRITE "min_significand")
                                  (("2"
                                    (LEMMA "expt_pos")
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))
             ("2" (ASSERT)
              (("2" (SPLIT)
                (("1" (ASSERT) NIL)
                 ("2" (ASSERT) NIL)))))))))))))))))
 (|max_neg_TCC1| "" (TCC :DEFS !) NIL)
 (|max_neg_TCC2| "" (EXPAND "max_fp_neg")
  (("" (EXPAND "value")
    (("" (EXPAND "neg")
      (("" (REWRITE "expt_x1")
        (("" (LEMMA "expt_pos")
          (("" (INST?)
            (("1" (LEMMA "Sum_pos")
              (("1" (INST?)
                (("1" (ASSERT)
                  (("1" (LEMMA "pos_times_gt")
                    (("1" (INST?)
                      (("1" (GROUND)
                        (("1" (INST + "0")
                          (("1" (REWRITE "value_digit")
                            (("1"
                              (REWRITE "expt_x0")
                              (("1"
                                (REWRITE "max_significand")
                                (("1" (ASSERT) NIL)))))))))
                         ("2" (INST + "0")
                          (("2" (REWRITE "value_digit")
                            (("2"
                              (REWRITE "expt_x0")
                              (("2"
                                (REWRITE "max_significand")
                                (("2" (ASSERT) NIL)))))))))))))))))
                 ("2" (ASSERT) NIL)))))
             ("2" (SPLIT 1)
              (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))))
 (|min_neg_TCC1| "" (TCC :DEFS !) NIL)
 (|min_neg_TCC2| "" (EXPAND "min_fp_neg")
  (("" (EXPAND "value")
    (("" (EXPAND "neg")
      (("" (REWRITE "expt_x1")
        (("" (ASSERT)
          (("" (LEMMA "expt_pos")
            (("" (INST?)
              (("" (LEMMA "Sum_pos")
                (("" (INST?)
                  (("" (LEMMA "pos_times_gt")
                    (("" (INST?)
                      (("" (GROUND)
                        (("1" (INST + "p-1")
                          (("1" (REWRITE "value_digit")
                            (("1"
                              (REWRITE "min_significand")
                              (("1"
                                (HIDE 1 3 4 5 6)
                                (("1"
                                  (HIDE -1)
                                  (("1"
                                    (LEMMA "expt_pos")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (ASSERT)
                                        NIL)))))))))))))))
                         ("2" (HIDE -1 1 3 4 5 6)
                          (("2" (INST + "p-1")
                            (("2"
                              (EXPAND "value_digit")
                              (("2"
                                (EXPAND "min_significand")
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (LEMMA "expt_pos")
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|max_fp_correct_TCC1| "" (TCC :DEFS !) NIL)
 (|max_fp_correct_TCC2| "" (TCC :DEFS !) NIL)
 (|max_fp_correct| "" (REWRITE "max_pos")
  (("" (REWRITE "max_fp_pos")
    (("" (REWRITE "value")
      (("" (REWRITE "pos")
        (("" (REWRITE "expt_x0")
          (("" (ASSERT)
            ((""
              (CASE "forall (i:upto(p)):Sum(i,
          (LAMBDA (n: nat):
             IF n < p THEN max_significand(n) * (b ^ (-n)) ELSE 0 ENDIF))
        * b ^ E_max
        = b ^ (1 + E_max) - b ^ (1 + E_max - i)")
              (("1" (INST?)
                (("1" (EXPAND "value_digit") (("1" (PROPAX) NIL)))))
               ("2" (HIDE 2)
                (("2" (INDUCT "i" 1 "upto_induction[p]")
                  (("1" (REWRITE "Sum") (("1" (ASSERT) NIL)))
                   ("2" (SKOSIMP*)
                    (("2" (EXPAND "Sum" +)
                      (("2" (REPLACE -2)
                        (("2" (HIDE -2)
                          (("2" (ASSERT)
                            (("2"
                              (REWRITE "max_significand")
                              (("2"
                                (LEMMA "expt_plus")
                                (("2"
                                  (INST-CP - "1" "E_max - jt!1" "b")
                                  (("2"
                                    (INST - "E_max" "-jt!1" "b")
                                    (("2"
                                      (REPLACE -1)
                                      (("2"
                                        (HIDE -1)
                                        (("2"
                                          (REPLACE -1)
                                          (("2"
                                            (HIDE -1)
                                            (("2"
                                              (REWRITE "expt_x1")
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))))))))))))))))))))))))))))))))))
 (|min_fp_correct_TCC1| "" (TCC :DEFS !) NIL)
 (|min_fp_correct| "" (EXPAND "min_fp_pos")
  (("" (EXPAND "value")
    (("" (EXPAND "pos")
      (("" (REWRITE "expt_x0")
        (("" (ASSERT)
          ((""
            (CASE-REPLACE
             "Sum(p,value_digit(min_significand))= b^(1-p)")
            (("1" (HIDE -1)
              (("1" (LEMMA "expt_plus")
                (("1" (INST - "(1 - p)" "E_min" "b")
                  (("1" (ASSERT) NIL)))))))
             ("2" (HIDE 2)
              (("2" (EXPAND "Sum")
                (("2" (EXPAND "value_digit")
                  (("2" (EXPAND "min_significand")
                    (("2"
                      (CASE "forall (i:below(p)):Sum(i,
          LAMBDA (n: nat):
            IF n < p THEN IF n < p - 1 THEN 0 ELSE 1 ENDIF * b ^ (-n)
            ELSE 0
            ENDIF)
        = 0")
                      (("1" (INST?) NIL)
                       ("2" (HIDE 2)
                        (("2" (INDUCT-AND-REWRITE "i" 1 "Sum")
                          NIL)))))))))))))))))))))))))
 (|value0| "" (SKOSIMP*)
  (("" (EXPAND "value")
    (("" (REWRITE "zero_times3")
      (("1" (REWRITE "zero_times3")
        (("1" (LEMMA "expt_nonzero")
          (("1" (INST? :COPY? T)
            (("1" (ASSERT)
              (("1" (HIDE -2)
                (("1" (INST?)
                  (("1" (ASSERT)
                    (("1" (HIDE -1)
                      (("1" (REWRITE "Sum_zero")
                        (("1" (PROP)
                          (("1" (EXPAND "d_zero")
                            (("1"
                              (APPLY-EXTENSIONALITY)
                              (("1"
                                (EXPAND "value_digit")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (REWRITE "zero_times3")
                                    (("1"
                                      (LEMMA "expt_nonzero")
                                      (("1"
                                        (INST?)
                                        (("1"
                                          (ASSERT)
                                          NIL)))))))))))))))
                           ("2" (REPLACE -1)
                            (("2"
                              (EXPAND "d_zero")
                              (("2"
                                (EXPAND "value_digit")
                                (("2"
                                  (PROPAX)
                                  NIL)))))))))))))))))))))))))))
       ("2" (ASSERT) NIL)))))))
 (|value_of_zero| "" (REWRITE "value0")
  (("" (EXPAND "pos_zero") (("" (PROPAX) NIL)))))
 (|normal_value| "" (SKOSIMP*)
  (("" (CASE-REPLACE "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
    (("1" (HIDE -1)
      (("1"
        (CASE "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
     value(finite(s,n+E_min,d))=value(normalize(finite(s,n+E_min,d)))")
        (("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
          (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
         ("2" (HIDE 2)
          (("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
            (("1" (SKOSIMP*)
              (("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))))
             ("2" (SKOSIMP*)
              (("2" (REWRITE "normalize")
                (("2" (LIFT-IF)
                  (("2" (GROUND)
                    (("2" (INST?)
                      (("2" (REPLACE -3 :DIR RL)
                        (("2" (HIDE -3)
                          (("2" (EXPAND "value")
                            (("2"
                              (EXPAND "value_digit")
                              (("2"
                                (CASE-REPLACE
                                 "Sum(p,(LAMBDA (n: nat):
               IF n < p THEN shift_left(d!1)(n) * (b ^ (-n))
               ELSE 0
               ENDIF))=b*Sum(p,(LAMBDA (n: nat): IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))")
                                (("1"
                                  (HIDE -1)
                                  (("1"
                                    (LEMMA "expt_plus")
                                    (("1"
                                      (INST - "1" "E_min+jt!1" "b")
                                      (("1"
                                        (REPLACE -1)
                                        (("1"
                                          (HIDE -1)
                                          (("1"
                                            (REWRITE "expt_x1")
                                            (("1"
                                              (ASSERT)
                                              NIL)))))))))))))
                                 ("2"
                                  (HIDE 2)
                                  (("2"
                                    (REWRITE "Sum")
                                    (("2"
                                      (ASSERT)
                                      (("2"
                                        (REWRITE "shift_left")
                                        (("2"
                                          (ASSERT)
                                          (("2"
                                            (CASE
                                             "forall (i:below(p)): Sum(i,
          (LAMBDA (n: nat):
             IF n < p THEN shift_left(d!1)(n) * (b ^ (-n)) ELSE 0 ENDIF))
        = b
            *
            Sum(i+1,
                (LAMBDA (n: nat):
                   IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))")
                                            (("1"
                                              (INST?)
                                              (("1" (ASSERT) NIL)))
                                             ("2"
                                              (HIDE 2)
                                              (("2"
                                                (INDUCT
                                                 "i"
                                                 1
                                                 "below_induction[p]")
                                                (("1"
                                                  (EXPAND "Sum")
                                                  (("1"
                                                    (EXPAND "Sum")
                                                    (("1"
                                                      (ASSERT)
                                                      NIL)))))
                                                 ("2"
                                                  (SKOSIMP*)
                                                  (("2"
                                                    (EXPAND "Sum" +)
                                                    (("2"
                                                      (REPLACE -2)
                                                      (("2"
                                                        (HIDE -2)
                                                        (("2"
                                                          (ASSERT)
                                                          (("2"
                                                            (EXPAND
                                                             "shift_left")
                                                            (("2"
                                                              (LEMMA
                                                               "expt_plus")
                                                              (("2"
                                                                (INST
                                                                 -
                                                                 "1"
                                                                 "-(1+jb!1)"
                                                                 "b")
                                                                (("2"
                                                                  (REPLACE
                                                                   -1)
                                                                  (("2"
                                                                    (REWRITE
                                                                     "expt_x1")
                                                                    (("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))))))))))))))))))))))))
                                 ("3"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))
         ("3" (REWRITE "fp_num_finite_eta") (("3" (ASSERT) NIL)))))))
     ("2" (REWRITE "fp_num_finite_eta") NIL)))))
 (|value_positive| "" (SKOSIMP*)
  (("" (EXPAND "zero?")
    (("" (EXPAND "pos")
      (("" (GROUND)
        (("1" (EXPAND "value")
          (("1" (REPLACE -1)
            (("1" (REWRITE "expt_x0")
              (("1" (ASSERT)
                (("1" (LEMMA "pos_times_ge")
                  (("1" (INST?)
                    (("1" (LEMMA "expt_pos")
                      (("1" (INST?)
                        (("1" (GROUND) NIL)))))))))))))))))
         ("2" (EXPAND "value")
          (("2" (TYPEPRED "sign(fin!1)")
            (("2" (ASSERT)
              (("2" (REPLACE -1)
                (("2" (REWRITE "expt_x1")
                  (("2" (LEMMA "expt_pos")
                    (("2" (INST?)
                      (("2" (ASSERT)
                        (("2" (LEMMA "Sum_nonneg")
                          (("2" (INST?)
                            (("2"
                              (LEMMA "pos_times_ge")
                              (("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|value_negative| "" (ASSERT)
  (("" (SKOSIMP*)
    (("" (EXPAND "neg")
      (("" (EXPAND "zero?")
        (("" (EXPAND "value")
          (("" (LEMMA "expt_pos")
            (("" (INST - "Exp(fin!1)" "b")
              (("1" (LEMMA "Sum_nonneg")
                (("1" (INST?)
                  (("1" (LEMMA "pos_times_ge")
                    (("1" (GROUND)
                      (("1" (REPLACE -1)
                        (("1" (REWRITE "expt_x1")
                          (("1" (ASSERT)
                            (("1" (INST?) (("1" (ASSERT) NIL)))))))))
                       ("2" (TYPEPRED "sign(fin!1)")
                        (("2" (ASSERT)
                          (("2" (REPLACE -1)
                            (("2"
                              (REWRITE "expt_x0")
                              (("2"
                                (ASSERT)
                                (("2"
                                  (INST?)
                                  (("2" (ASSERT) NIL)))))))))))))))))
                   ("2" (ASSERT) NIL)))))
               ("2" (ASSERT)
                (("2" (SPLIT)
                  (("1" (ASSERT) NIL)
                   ("2" (ASSERT) NIL)))))))))))))))))))
 (|finite_cover| "" (SKOSIMP*)
  (("" (EXPAND "normal?")
    (("" (EXPAND "subnormal?")
      (("" (GROUND)
        (("" (HIDE 2)
          ((""
            (CASE "forall (n:upto(E_max-E_min)),(s:sign_rep),(d:digits):
              Exp(normalize(finite(s,n+E_min,d))) = E_min or
              d(normalize(finite(s,n+E_min,d)))(0) > 0")
            (("1"
              (INST - "Exp(fin!1)-E_min" "sign(fin!1)" "d(fin!1)")
              (("1" (ASSERT)
                (("1" (REWRITE "fp_num_finite_eta")
                  (("1" (ASSERT) NIL)))))
               ("2" (ASSERT)
                (("2" (HIDE 2 3) (("2" (GROUND) NIL)))))))
             ("2" (HIDE 2 3)
              (("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
                (("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))
                 ("2" (SKOSIMP*)
                  (("2" (REWRITE "normalize")
                    (("2" (LIFT-IF)
                      (("2" (GROUND)
                        (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
                 ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))
             ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))))))))))
 (|finite_disjoint1| "" (SKOSIMP*)
  (("" (EXPAND "normal?")
    (("" (EXPAND "zero?")
      (("" (GROUND)
        (("" (REWRITE "normal_value")
          (("" (REWRITE "value0")
            (("" (REPLACE -2)
              (("" (EXPAND "d_zero")
                (("" (ASSERT) NIL)))))))))))))))))
 (|finite_disjoint2| "" (SKOSIMP*)
  (("" (EXPAND "subnormal?") (("" (GROUND) NIL)))))
 (|finite_disjoint3| "" (SKOSIMP*)
  (("" (EXPAND "subnormal?")
    (("" (EXPAND "normal?") (("" (GROUND) NIL)))))))
 (|toggle_sign_TCC1| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|toggle_sign_TCC2| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|toggle_finite| "" (TCC :DEFS !) NIL)
 (|toggle_infinite| "" (TCC :DEFS !) NIL)
 (|toggle_NaN| "" (TCC :DEFS !) NIL)
 (|value_toggle_TCC1| "" (TCC :DEFS !) NIL)
 (|value_toggle| "" (SKOSIMP*)
  (("" (EXPAND "toggle_sign")
    (("" (EXPAND "value")
      (("" (TYPEPRED "sign(fin!1)")
        (("" (GROUND)
          (("1" (REPLACE -1)
            (("1" (REWRITE "expt_x0")
              (("1" (REWRITE "expt_x1") (("1" (ASSERT) NIL)))))))
           ("2" (REPLACE -1)
            (("2" (REWRITE "expt_x1")
              (("2" (REWRITE "expt_x0")
                (("2" (ASSERT) NIL)))))))))))))))))
 (|toggle_d_normalize| "" (SKOSIMP*)
  ((""
    (CASE-REPLACE "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))")
    (("1" (EXPAND "toggle_sign")
      (("1"
        (CASE "forall (s:sign_rep),(d1:digits),(n:upto(E_max-E_min)):
      d(normalize(finite(s,n+E_min,d1))) = d(normalize(finite(1-s,n+E_min,d1)))")
        (("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
          (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
         ("2" (HIDE -1 2)
          (("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
            (("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))
             ("2" (SKOSIMP*)
              (("2" (EXPAND "normalize" +)
                (("2" (LIFT-IF)
                  (("2" (ASSERT)
                    (("2" (GROUND) (("2" (INST?) NIL)))))))))))
             ("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))))
         ("3" (HIDE -1 2)
          (("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))
         ("4" (ASSERT) NIL)))))
     ("2" (REWRITE "fp_num_finite_eta") NIL)))))
 (|toggle_Exp_normalize| "" (SKOSIMP*)
  ((""
    (CASE-REPLACE "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))")
    (("1" (EXPAND "toggle_sign")
      (("1"
        (CASE "forall (s:sign_rep),(d1:digits),(n:upto(E_max-E_min)):
      Exp(normalize(finite(s,n+E_min,d1))) = Exp(normalize(finite(1-s,n+E_min,d1)))")
        (("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
          (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
         ("2" (HIDE -1 2)
          (("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
            (("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))
             ("2" (SKOSIMP*)
              (("2" (EXPAND "normalize" +)
                (("2" (LIFT-IF)
                  (("2" (ASSERT)
                    (("2" (GROUND) (("2" (INST?) NIL)))))))))))
             ("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))))
         ("3" (HIDE -1 2)
          (("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))
         ("4" (ASSERT) NIL)))))
     ("2" (REWRITE "fp_num_finite_eta") NIL)))))
 (|toggle_zero?| "" (SKOSIMP*)
  (("" (EXPAND "zero?")
    (("" (REWRITE "toggle_finite")
      (("" (REWRITE "value_toggle") (("" (GROUND) NIL)))))))))
 (|toggle_normal?| "" (SKOSIMP*)
  (("" (EXPAND "normal?")
    (("" (REWRITE "toggle_d_normalize")
      (("" (REWRITE "toggle_finite") (("" (ASSERT) NIL)))))))))
 (|toggle_subnormal?| "" (SKOSIMP*)
  (("" (EXPAND "subnormal?")
    (("" (REWRITE "toggle_d_normalize")
      (("" (REWRITE "toggle_Exp_normalize")
        (("" (REWRITE "toggle_zero?")
          (("" (REWRITE "toggle_finite")
            (("" (ASSERT) NIL)))))))))))))
 (|value_digit_le_TCC1| "" (TCC :DEFS !) NIL)
 (|value_digit_le| "" (SKOSIMP*)
  (("" (REWRITE "value_digit")
    (("" (LIFT-IF)
      (("" (SPLIT)
        (("1" (FLATTEN)
          (("1" (REWRITE "both_sides_times_pos_le1")
            (("1" (ASSERT) NIL)
             ("2" (LEMMA "expt_pos")
              (("2" (INST?) (("2" (ASSERT) NIL)))))))))
         ("2" (FLATTEN)
          (("2" (LEMMA "expt_pos")
            (("2" (INST?)
              (("1" (REWRITE "pos_times_le") (("1" (ASSERT) NIL)))
               ("2" (ASSERT) NIL)))))))))))))))
 (|Sum_d_lt_b| "" (INDUCT "j")
  (("1" (EXPAND "Sum")
    (("1" (EXPAND "Sum")
      (("1" (EXPAND "value_digit")
        (("1" (REWRITE "expt_x0")
          (("1" (SKOSIMP*)
            (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))))))))
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST?)
        (("2" (LEMMA "value_digit_le")
          (("2" (INST?)
            (("2" (ASSERT)
              (("2" (CASE-REPLACE "b ^ (-(1 + j!1)) * b = b^(-j!1)")
                (("1" (HIDE -1) (("1" (ASSERT) NIL)))
                 ("2" (HIDE -1 -2 2)
                  (("2" (LEMMA "expt_plus")
                    (("2" (INST - "-(1+j!1)" "1" "b")
                      (("2" (REWRITE "expt_x1")
                        (("2" (ASSERT) NIL)))))))))))))))))))))))
   ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
 (|Sum_d_lt1_TCC1| "" (TCC :DEFS !) NIL)
 (|Sum_d_lt1_TCC2| "" (TCC :DEFS !) NIL)
 (|Sum_d_lt1| "" (INDUCT "j")
  (("1" (EXPAND "Sum")
    (("1" (EXPAND "Sum")
      (("1" (EXPAND "value_digit")
        (("1" (REWRITE "expt_x0")
          (("1" (LIFT-IF)
            (("1" (ASSERT)
              (("1" (GROUND)
                (("1" (SKOSIMP*) (("1" (ASSERT) NIL)))))))))))))))))
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (LEMMA "value_digit_le")
            (("2" (INST?)
              (("2" (ASSERT)
                (("2"
                  (CASE-REPLACE "b ^ (-(1 + j!1)) * b = b^(-j!1)")
                  (("1" (ASSERT) NIL)
                   ("2" (HIDE -1 -2 -3 2)
                    (("2" (LEMMA "expt_plus")
                      (("2" (INST - "-(1+j!1)" "1" "b")
                        (("2" (REWRITE "expt_x1")
                          (("2" (ASSERT) NIL)))))))))))))))))))))))))
   ("3" (SKOSIMP*) (("3" (ASSERT) NIL))) ("4" (ASSERT) NIL)))
 (|Sum_d_ge1| "" (INDUCT "j")
  (("1" (EXPAND "Sum")
    (("1" (SKOSIMP*)
      (("1" (REWRITE "value_digit")
        (("1" (LIFT-IF)
          (("1" (ASSERT)
            (("1" (REWRITE "expt_x0")
              (("1" (ASSERT)
                (("1" (LEMMA "Sum_nonneg")
                  (("1" (INST?) (("1" (ASSERT) NIL)))))))))))))))))))
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum") (("2" (INST?) (("2" (ASSERT) NIL)))))))
   ("3" (ASSERT) NIL)))
 (|value_sig_lt_b| "" (SKOSIMP*)
  (("" (LEMMA "Sum_d_lt_b")
    (("" (INST - "d!1" "p-1")
      (("1" (ASSERT)
        (("1" (LEMMA "expt_pos")
          (("1" (INST?) (("1" (ASSERT) NIL)))))))
       ("2" (ASSERT) NIL)))))))
 (|value_sig_lt1| "" (SKOSIMP*)
  (("" (LEMMA "Sum_d_lt1")
    (("" (INST - "d!1" "p-1")
      (("1" (LEMMA "expt_pos")
        (("1" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))
       ("2" (ASSERT) NIL)))))))
 (|value_sig_ge1| "" (SKOSIMP*)
  (("" (LEMMA "Sum_d_ge1")
    (("" (INST - "d!1" "p-1")
      (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
 (|abs_value_fin| "" (SKOSIMP*)
  (("" (EXPAND "value")
    ((""
      (CASE "b ^ (Exp(fin!1)) * Sum(p, value_digit(d(fin!1))) >=0")
      (("1" (TYPEPRED "sign(fin!1)")
        (("1" (PROP)
          (("1" (REPLACE -1)
            (("1" (REWRITE "expt_x0")
              (("1" (EXPAND "abs") (("1" (ASSERT) NIL)))))))
           ("2" (REPLACE -1)
            (("2" (REWRITE "expt_x1")
              (("2" (EXPAND "abs")
                (("2" (ASSERT)
                  (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))))
       ("2" (HIDE 2)
        (("2" (LEMMA "expt_pos")
          (("2" (INST?)
            (("1" (LEMMA "Sum_nonneg")
              (("1" (INST?)
                (("1" (REWRITE "pos_times_ge") (("1" (ASSERT) NIL)))
                 ("2" (ASSERT) NIL)))))
             ("2" (ASSERT) NIL)))))))
       ("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))))))
 (|min_significand_min| "" (SKOSIMP*)
  (("" (EXPAND "Sum" + 1)
    (("" (GROUND)
      (("" (LIFT-IF)
        (("" (GROUND)
          (("" (REWRITE "value_digit")
            (("" (REWRITE "min_significand")
              (("" (ASSERT)
                ((""
                  (CASE-REPLACE
                   "Sum(p - 1, value_digit(min_significand))=0")
                  (("1" (HIDE -1)
                    (("1" (ASSERT)
                      (("1" (LEMMA "Sum_pos")
                        (("1" (INST?)
                          (("1" (GROUND)
                            (("1"
                              (SKOSIMP*)
                              (("1"
                                (LEMMA "Sum_ge")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (INST - "value_digit(d!1)(i!1)")
                                    (("1"
                                      (GROUND)
                                      (("1"
                                        (REWRITE "value_digit")
                                        (("1"
                                          (TYPEPRED "i!1")
                                          (("1"
                                            (CASE
                                             "d!1(i!1) * b ^ (-i!1) >= b ^ (-(p - 1))")
                                            (("1" (ASSERT) NIL)
                                             ("2"
                                              (LEMMA
                                               "ge_times_ge_pos")
                                              (("2"
                                                (INST
                                                 -
                                                 "b ^ (-(p - 1))"
                                                 "1"
                                                 "d!1(i!1)"
                                                 "b ^ (-i!1)")
                                                (("2"
                                                  (GROUND)
                                                  (("2"
                                                    (HIDE
                                                     -3
                                                     -4
                                                     -5
                                                     2
                                                     3
                                                     4
                                                     5)
                                                    (("2"
                                                      (LEMMA
                                                       "both_sides_expt_gt1_le")
                                                      (("2"
                                                        (INST
                                                         -
                                                         "b"
                                                         "-(p-1)"
                                                         "-i!1")
                                                        (("2"
                                                          (ASSERT)
                                                          NIL)))))))))))))))))))
                                       ("2"
                                        (INST?)
                                        (("2"
                                          (ASSERT)
                                          NIL)))))))))))))
                             ("2"
                              (CASE "d!1=d_zero")
                              (("1" (PROPAX) NIL)
                               ("2"
                                (APPLY-EXTENSIONALITY)
                                (("2"
                                  (EXPAND "d_zero")
                                  (("2"
                                    (INST?)
                                    (("2"
                                      (HIDE 2 4 5 6 7)
                                      (("2"
                                        (EXPAND "value_digit")
                                        (("2"
                                          (REWRITE "pos_times_gt")
                                          (("2"
                                            (LEMMA "expt_pos")
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))))))))))))))))
                   ("2" (HIDE 2 3 4)
                    (("2"
                      (CASE "forall (i:below(p)): Sum(i,value_digit(min_significand)) = 0")
                      (("1" (INST?) NIL)
                       ("2" (HIDE 2)
                        (("2" (INDUCT "i" 1 "below_induction[p]")
                          (("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))
                           ("2" (SKOSIMP*)
                            (("2"
                              (REWRITE "Sum" +)
                              (("2"
                                (REWRITE "value_digit")
                                (("2"
                                  (REWRITE "min_significand")
                                  (("2"
                                    (GROUND)
                                    NIL)))))))))))))))))))))))))))))))))))
 (|sign_normal| "" (SKOSIMP*)
  ((""
    (CASE "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
              s=sign(normalize(finite(s,n+E_min,d)))")
    (("1"
      (CASE-REPLACE
       "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))")
      (("1" (ASSERT)
        (("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
          (("1" (ASSERT) NIL)))))
       ("2" (ASSERT) (("2" (REWRITE "fp_num_finite_eta") NIL)))))
     ("2" (HIDE 2)
      (("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
        (("1" (SKOSIMP*)
          (("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))))
         ("2" (SKOSIMP*)
          (("2" (REWRITE "normalize")
            (("2" (LIFT-IF)
              (("2" (GROUND) (("2" (INST?) NIL)))))))))))))
     ("3" (ASSERT) NIL)))))
 (|value_normal_TCC1| "" (TCC :DEFS !) NIL)
 (|value_normal| "" (SKOSIMP*)
  (("" (REWRITE "normal_value")
    (("" (REWRITE "abs_value_fin")
      (("" (EXPAND "normal?")
        (("" (ASSERT)
          (("" (EXPAND "max_pos")
            (("" (EXPAND "value")
              (("" (EXPAND "max_fp_pos")
                (("" (EXPAND "pos")
                  (("" (REWRITE "expt_x0")
                    (("" (ASSERT)
                      (("" (PROP)
                        (("1" (LEMMA "value_sig_ge1")
                          (("1" (INST?)
                            (("1"
                              (ASSERT)
                              (("1"
                                (LEMMA "both_sides_expt_gt1_le")
                                (("1"
                                  (INST
                                   -
                                   "b"
                                   "E_min"
                                   "(Exp(normalize(fin!1)))")
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (LEMMA "le_times_le_pos")
                                      (("1"
                                        (INST
                                         -
                                         "b^E_min"
                                         "1"
                                         "Sum(p, value_digit(d(normalize(fin!1))))"
                                         "b ^ (Exp(normalize(fin!1)))")
                                        (("1" (ASSERT) NIL)
                                         ("2"
                                          (LEMMA "expt_pos")
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (ASSERT)
                                              NIL)))))))))))))))))))))
                         ("2" (LEMMA "both_sides_expt_gt1_le")
                          (("2"
                            (INST - "b" "(Exp(normalize(fin!1)))"
                             "E_max")
                            (("2"
                              (ASSERT)
                              (("2"
                                (LEMMA "le_times_le_pos")
                                (("2"
                                  (INST
                                   -
                                   "b ^ (Exp(normalize(fin!1)))"
                                   "Sum(p, value_digit(d(normalize(fin!1))))"
                                   "Sum(p, value_digit(max_significand))"
                                   " b ^ E_max")
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (HIDE -1 2)
                                      (("1"
                                        (REWRITE "Sum_le")
                                        (("1"
                                          (HIDE -1 2)
                                          (("1"
                                            (SKOSIMP*)
                                            (("1"
                                              (EXPAND "value_digit")
                                              (("1"
                                                (LEMMA "expt_pos")
                                                (("1"
                                                  (INST?)
                                                  (("1"
                                                    (REWRITE
                                                     "both_sides_times_pos_le1")
                                                    (("1"
                                                      (EXPAND
                                                       "max_significand")
                                                      (("1"
                                                        (ASSERT)
                                                        NIL)))))))))))))))))))))
                                   ("2"
                                    (LEMMA "expt_pos")
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|value_subnormal_TCC1| "" (TCC :DEFS !) NIL)
 (|value_subnormal| "" (SKOSIMP*)
  (("" (REWRITE "normal_value")
    (("" (REWRITE "abs_value_fin")
      (("" (EXPAND "min_pos")
        (("" (EXPAND "value")
          (("" (EXPAND "min_fp_pos")
            (("" (EXPAND "pos")
              (("" (REWRITE "expt_x0")
                (("" (ASSERT)
                  (("" (EXPAND "subnormal?")
                    (("" (ASSERT)
                      (("" (GROUND)
                        (("1" (EXPAND "zero?")
                          (("1" (LEMMA "both_sides_times_pos_le1")
                            (("1"
                              (INST
                               -
                               "b ^ (Exp(normalize(fin!1)))"
                               "Sum(p, value_digit(min_significand))"
                               "Sum(p, value_digit(d(normalize(fin!1))))")
                              (("1"
                                (GROUND)
                                (("1"
                                  (HIDE 2 3)
                                  (("1"
                                    (REWRITE "normal_value")
                                    (("1"
                                      (REWRITE "value0")
                                      (("1"
                                        (REWRITE
                                         "min_significand_min")
                                        NIL)))))))))
                               ("2"
                                (LEMMA "expt_pos")
                                (("2"
                                  (INST?)
                                  (("2" (ASSERT) NIL)))))))))))
                         ("2" (LEMMA "value_sig_lt1")
                          (("2" (INST?)
                            (("2"
                              (ASSERT)
                              (("2"
                                (ASSERT)
                                (("2"
                                  (LEMMA "expt_pos")
                                  (("2"
                                    (INST?)
                                    (("2"
                                      (LEMMA
                                       "both_sides_times_pos_lt1")
                                      (("2"
                                        (INST
                                         -
                                         "b ^ (Exp(normalize(fin!1)))"
                                         "Sum(p, value_digit(d(normalize(fin!1))))"
                                         "1")
                                        (("1" (ASSERT) NIL)
                                         ("2"
                                          (ASSERT)
                                          NIL)))))))))))))))))))))))))))))))))))))))))
 (|value_nonzero| "" (SKOSIMP*)
  (("" (LEMMA "value_normal")
    (("" (INST?)
      (("" (LEMMA "value_subnormal")
        (("" (INST?)
          (("" (LEMMA "finite_cover")
            (("" (INST?)
              (("" (GROUND)
                (("1" (EXPAND "min_pos")
                  (("1" (REWRITE "min_fp_correct")
                    (("1" (LEMMA "both_sides_expt_gt1_le")
                      (("1" (INST - "b" "(1 + E_min - p)" "E_min")
                        (("1" (GROUND) NIL)))))))))
                 ("2" (LEMMA "both_sides_expt_gt1_le")
                  (("2" (REWRITE "max_fp_correct")
                    (("2" (INST - "b" "E_min" "E_max")
                      (("2" (GROUND)
                        (("2"
                          (CASE "b^E_max < b ^ (1 + E_max) - b ^ (1 + E_max - p)")
                          (("1" (GROUND) NIL)
                           ("2" (HIDE -1 -2 -3 -4 -5 2 3 4)
                            (("2"
                              (LEMMA "exponent_adjust")
                              (("2"
                                (INST - "b" "E_max" "p-1")
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|scale_value_TCC1| "" (TCC)
  (("1" (REWRITE "pos_times_ge")
    (("1" (ASSERT)
      (("1" (LEMMA "expt_pos")
        (("1" (EXPAND "^")
          (("1" (INST?) (("1" (ASSERT) NIL)))))))))))
   ("2" (LEMMA "expt_pos")
    (("2" (EXPAND "^")
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (LEMMA "expt_pos")
            (("2" (ASSERT)
              (("2" (INST -1 "-n!1" "b")
                (("2" (ASSERT)
                  (("2" (LEMMA "pos_times_gt")
                    (("2"
                      (INST -1 "d!1(n!1)"
                       "expt(b, m!1) * (1 / (b * expt(b, -(-n!1) - 1)))")
                      (("1" (ASSERT)
                        (("1" (PROP)
                          (("1" (LEMMA "pos_times_gt")
                            (("1"
                              (INST
                               -1
                               "expt(b, m!1)"
                               "(1 / (b * expt(b, -(-n!1) - 1)))")
                              (("1" (ASSERT) NIL)
                               ("2"
                                (LEMMA "zero_times3")
                                (("2"
                                  (INST?)
                                  (("2"
                                    (ASSERT)
                                    (("2"
                                      (LEMMA "expt_nonzero_aux")
                                      (("2"
                                        (INST?)
                                        (("2"
                                          (ASSERT)
                                          NIL)))))))))))))))))))
                       ("2" (LEMMA "zero_times3")
                        (("2" (INST?)
                          (("2" (ASSERT)
                            (("2"
                              (LEMMA "zero_times3")
                              (("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (LEMMA "expt_nonzero_aux")
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|scaled_Sum_int| "" (SKOLEM!)
  (("" (INDUCT "m" 1 "upto_induction[n!1+1]")
    (("1" (REWRITE "Sum")
      (("1" (EXPAND "integer?") (("1" (PROPAX) NIL)))))
     ("2" (SKOSIMP*)
      (("2" (REWRITE "Sum" +)
        (("2" (REWRITE "scale_value")
          (("2" (REWRITE "value_digit")
            (("2" (LIFT-IF)
              (("2" (GROUND)
                (("2" (CASE "FORALL (i,j:int): integer?(i+j)")
                  (("1" (INST?)
                    (("1" (HIDE -3 2)
                      (("1" (REWRITE "associative_mult" :DIR RL)
                        (("1" (REWRITE "expt_plus" :DIR RL)
                          (("1"
                            (CASE "FORALL (i,j:int): integer?(i*j)")
                            (("1"
                              (INST?)
                              (("1" (ASSERT) NIL)
                               ("2"
                                (ASSERT)
                                (("2"
                                  (HIDE 2)
                                  (("2"
                                    (CASE
                                     "forall (n:nat): integer?(b^n)")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (EXPAND "integer?")
                                        (("1" (PROPAX) NIL)))))
                                     ("2"
                                      (SKOSIMP*)
                                      (("2"
                                        (EXPAND "integer?")
                                        (("2"
                                          (PROPAX)
                                          NIL)))))))))))))
                             ("2"
                              (EXPAND "integer?")
                              (("2" (PROPAX) NIL)))))))))))
                     ("2" (EXPAND "integer?") (("2" (PROPAX) NIL)))))
                   ("2" (EXPAND "integer?" 1)
                    (("2" (PROPAX) NIL)))))))))))))))))))))
 (|scale_value_p_TCC1| "" (TCC :DEFS !) NIL)
 (|scale_value_p_TCC2| "" (SKOSIMP*)
  (("" (CASE "integer?(scale_value(d!1, p - 1)(n!1))")
    (("1" (EXPAND "integer?") (("1" (ASSERT) NIL)))
     ("2" (HIDE 2)
      (("2" (REWRITE "scale_value")
        (("2" (REWRITE "value_digit")
          (("2" (LIFT-IF)
            (("2" (GROUND)
              (("1"
                (CASE-REPLACE
                 "(d!1(n!1) * b ^ (p - 1) * b ^ (-n!1))=(d!1(n!1) * b ^ (p - 1 - n!1))")
                (("1" (HIDE -1)
                  (("1" (CASE "FORALL (i,j:int): integer?(i*j)")
                    (("1" (INST?)
                      (("1" (ASSERT)
                        (("1" (HIDE 2)
                          (("1" (EXPAND "^")
                            (("1"
                              (ASSERT)
                              (("1"
                                (CASE
                                 "FORALL (n:nat): integer_pred(expt(b, n))")
                                (("1" (INST?) NIL)
                                 ("2"
                                  (HIDE -1 2)
                                  (("2"
                                    (INDUCT "n")
                                    (("2"
                                      (SKOSIMP*)
                                      NIL)))))))))))))))))
                     ("2" (EXPAND "integer?")
                      (("2" (PROPAX) NIL)))))))
                 ("2" (LEMMA "expt_plus")
                  (("2" (INST?)
                    (("2" (INST -1 "-n!1")
                      (("2" (ASSERT) NIL)))))))))
               ("2" (EXPAND "integer?")
                (("2" (PROPAX) NIL)))))))))))))
     ("3" (ASSERT) NIL)))))
 (|scaled_Sum_i| "" (INDUCT "n")
  (("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "Sum" +)
      (("2" (INST?)
        (("2" (REWRITE "scale_value") (("2" (ASSERT) NIL)))))))))))
 (|scaled_Sum| "" (SKOSIMP*)
  (("" (REWRITE "scaled_Sum_i")
    (("" (REWRITE "scale_value_p")
      (("" (REPLACE-ETA "scale_value(d!1, (p - 1))") NIL)))))))
 (|floor_Sum| "" (SKOSIMP*)
  (("" (REWRITE "scaled_Sum_i")
    (("" (LEMMA "Sum_split")
      (("" (INST - "scale_value(d!1, i!1)" "p" "i!1+1")
        (("" (REPLACE -1)
          (("" (HIDE -1)
            (("" (LEMMA "floor_plus_int")
              ((""
                (INST - "Sum(i!1 + 1, scale_value(d!1, i!1))"
                 "Sum(p - (i!1 + 1),
                  LAMBDA (k: nat):
                    scale_value(d!1, i!1)(k + (i!1 + 1)))")
                (("1" (REPLACE -1)
                  (("1" (HIDE -1)
                    (("1" (ASSERT)
                      (("1" (LEMMA "floor_Sum_mant")
                        (("1" (INST?)
                          (("1" (HIDE 2)
                            (("1"
                              (SKOSIMP*)
                              (("1"
                                (REWRITE "scale_value")
                                (("1"
                                  (REWRITE "value_digit")
                                  (("1"
                                    (LIFT-IF)
                                    (("1"
                                      (GROUND)
                                      (("1"
                                        (LEMMA "expt_plus")
                                        (("1"
                                          (INST
                                           -
                                           "(-(1 + i!1 + i!2))"
                                           "i!1"
                                           "b")
                                          (("1"
                                            (LEMMA
                                             "both_sides_times_pos_le1")
                                            (("1"
                                              (INST
                                               -
                                               "b ^ (-i!2 - 1)"
                                               "d!1(1 + i!1 + i!2)"
                                               "(b-1)")
                                              (("1" (ASSERT) NIL)
                                               ("2"
                                                (HIDE -1 -2 2)
                                                (("2"
                                                  (LEMMA "expt_pos")
                                                  (("2"
                                                    (INST?)
                                                    (("2"
                                                      (ASSERT)
                                                      NIL)))))))))))))))
                                       ("2"
                                        (LEMMA "pos_times_le")
                                        (("2"
                                          (INST
                                           -
                                           "(b-1)"
                                           "b ^ (-i!2 - 1)")
                                          (("2"
                                            (LEMMA "expt_pos")
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))))))))))))))))))
                 ("2" (HIDE 2)
                  (("2" (LEMMA "scaled_Sum_int")
                    (("2" (EXPAND "integer?")
                      (("2" (INST?) NIL)))))))))))))))))))))))
 (|mod_Sum_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "scaled_Sum_int")
    (("" (EXPAND "integer?") (("" (INST?) NIL)))))))
 (|mod_Sum_TCC2| "" (ASSERT) NIL)
 (|mod_Sum| "" (SKOSIMP*)
  (("" (REWRITE "Sum")
    (("" (REWRITE "scale_value")
      (("" (REWRITE "value_digit")
        ((""
          (CASE-REPLACE
           "(d!1(i!1) * b ^ (-i!1) * b ^ i!1) = d!1(i!1) * (b ^ (-i!1) * b ^ i!1)")
          (("1" (HIDE -1)
            (("1" (LEMMA "expt_plus")
              (("1" (INST?)
                (("1" (REPLACE -1 :DIR RL)
                  (("1" (HIDE -1)
                    (("1" (REWRITE "expt_x0")
                      (("1" (ASSERT)
                        (("1" (LEMMA "mod_of_mod")
                          (("1" (INST?)
                            (("1"
                              (REPLACE -1 :DIR RL)
                              (("1"
                                (HIDE -1)
                                (("1"
                                  (CASE-REPLACE
                                   "mod(Sum(i!1, scale_value(d!1, i!1)),b) = 0")
                                  (("1"
                                    (HIDE -1)
                                    (("1"
                                      (REWRITE "mod_lt_nat")
                                      NIL)))
                                   ("2"
                                    (HIDE 2)
                                    (("2"
                                      (CASE
                                       "forall (j:upto(i!1)): mod(Sum(j,scale_value(d!1,i!1)),b) = 0")
                                      (("1" (INST?) NIL)
                                       ("2"
                                        (HIDE 2)
                                        (("2"
                                          (INDUCT
                                           "j"
                                           1
                                           "upto_induction[i!1]")
                                          (("1"
                                            (EXPAND "Sum")
                                            (("1"
                                              (REWRITE "mod_zero")
                                              NIL)))
                                           ("2"
                                            (SKOSIMP*)
                                            (("2"
                                              (EXPAND "Sum" +)
                                              (("2"
                                                (REWRITE
                                                 "scale_value")
                                                (("2"
                                                  (REWRITE
                                                   "value_digit")
                                                  (("2"
                                                    (CASE-REPLACE
                                                     "d!1(jt!1) * b ^ (-jt!1) * b ^ i!1 = d!1(jt!1) * (b ^ (-jt!1) * b ^ i!1)")
                                                    (("1"
                                                      (HIDE -1)
                                                      (("1"
                                                        (LEMMA
                                                         "expt_plus")
                                                        (("1"
                                                          (INST?)
                                                          (("1"
                                                            (REPLACE
                                                             -1
                                                             :DIR
                                                             RL)
                                                            (("1"
                                                              (HIDE
                                                               -1)
                                                              (("1"
                                                                (LEMMA
                                                                 "mod_of_mod")
                                                                (("1"
                                                                  (INST?)
                                                                  (("1"
                                                                    (REPLACE
                                                                     -1
                                                                     :DIR
                                                                     RL)
                                                                    (("1"
                                                                      (HIDE
                                                                       -1)
                                                                      (("1"
                                                                        (REPLACE
                                                                         -2)
                                                                        (("1"
                                                                          (HIDE
                                                                           -2)
                                                                          (("1"
                                                                            (CASE-REPLACE
                                                                             "d!1(jt!1) * b ^ ((-jt!1) + i!1) = (d!1(jt!1) * b ^ ((-jt!1) + i!1-1))*b")
                                                                            (("1"
                                                                              (HIDE
                                                                               -1)
                                                                              (("1"
                                                                                (LEMMA
                                                                                 "mod_sum")
                                                                                (("1"
                                                                                  (INST
                                                                                   -
                                                                                   "0"
                                                                                   "b"
                                                                                   "_")
                                                                                  (("1"
                                                                                    (REWRITE
                                                                                     "mod_zero")
                                                                                    (("1"
                                                                                      (INST?)
                                                                                      (("1"
                                                                                        (ASSERT)
                                                                                        NIL)
                                                                                       ("2"
                                                                                        (REWRITE
                                                                                         "closed_times")
                                                                                        (("2"
                                                                                          (CASE
                                                                                           "forall (n:nat):integer_pred(b^n)")
                                                                                          (("1"
                                                                                            (INST?)
                                                                                            NIL)
                                                                                           ("2"
                                                                                            (SKOSIMP*)
                                                                                            (("2"
                                                                                              (ASSERT)
                                                                                              NIL)))))))))))))))))
                                                                             ("2"
                                                                              (HIDE
                                                                               2)
                                                                              (("2"
                                                                                (CASE
                                                                                 "b ^ ((-jt!1) + i!1 - 1) * b = b^(i!1-jt!1)")
                                                                                (("1"
                                                                                  (ASSERT)
                                                                                  NIL)
                                                                                 ("2"
                                                                                  (HIDE
                                                                                   2)
                                                                                  (("2"
                                                                                    (LEMMA
                                                                                     "expt_plus")
                                                                                    (("2"
                                                                                      (INST
                                                                                       -
                                                                                       "i!1-jt!1"
                                                                                       "(-1)"
                                                                                       "b")
                                                                                      (("2"
                                                                                        (REPLACE
                                                                                         -1)
                                                                                        (("2"
                                                                                          (REWRITE
                                                                                           "expt_inverse")
                                                                                          (("2"
                                                                                            (REWRITE
                                                                                             "expt_x1")
                                                                                            (("2"
                                                                                              (ASSERT)
                                                                                              NIL)))))))))))))))))))))))))))
                                                                   ("2"
                                                                    (LEMMA
                                                                     "scaled_Sum_int")
                                                                    (("2"
                                                                      (INST?)
                                                                      (("2"
                                                                        (ASSERT)
                                                                        (("2"
                                                                          (EXPAND
                                                                           "integer?")
                                                                          (("2"
                                                                            (PROPAX)
                                                                            NIL)))))))))
                                                                   ("3"
                                                                    (HIDE
                                                                     -2
                                                                     2)
                                                                    (("3"
                                                                      (REWRITE
                                                                       "closed_times")
                                                                      (("3"
                                                                        (CASE
                                                                         "forall (n:nat):integer_pred(b^n)")
                                                                        (("1"
                                                                          (INST?)
                                                                          NIL)
                                                                         ("2"
                                                                          (SKOSIMP*)
                                                                          (("2"
                                                                            (ASSERT)
                                                                            NIL)))))))))))))))))))))))
                                                     ("2"
                                                      (ASSERT)
                                                      NIL)))))))))))
                                           ("3"
                                            (LEMMA "scaled_Sum_int")
                                            (("3"
                                              (INST?)
                                              (("3"
                                                (EXPAND "integer?")
                                                (("3"
                                                  (ASSERT)
                                                  NIL)))))))
                                           ("4"
                                            (LEMMA "scaled_Sum_int")
                                            (("4"
                                              (INST?)
                                              (("4"
                                                (EXPAND "integer?")
                                                (("4"
                                                  (ASSERT)
                                                  NIL)))))))))))
                                       ("3"
                                        (SKOSIMP*)
                                        (("3"
                                          (LEMMA "scaled_Sum_int")
                                          (("3"
                                            (INST?)
                                            (("3"
                                              (ASSERT)
                                              (("3"
                                                (EXPAND "integer?")
                                                (("3"
                                                  (PROPAX)
                                                  NIL)))))))))))))))
                                   ("3"
                                    (LEMMA "scaled_Sum_int")
                                    (("3"
                                      (INST?)
                                      (("3"
                                        (ASSERT)
                                        (("3"
                                          (EXPAND "integer?")
                                          (("3"
                                            (PROPAX)
                                            NIL)))))))))))))))
                             ("2"
                              (LEMMA "scaled_Sum_int")
                              (("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (EXPAND "integer?")
                                    (("2"
                                      (PROPAX)
                                      NIL)))))))))))))))))))))))))))
           ("2" (ASSERT) NIL))))))))))))
$$$sum_hack.pvs
sum_hack  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some stuff that will eventually be loaded from a library,
%  once the PVS library mechanism works.
  i,j,k:var nat
  F: var [nat->real]

  Sum(j,F):recursive real =
   if j=0 then 0 else F(j-1)+Sum(j-1,F) endif
   measure j

  F1,F2: var [nat->nonneg_real]

  Sum_nonneg: lemma  Sum(j,F1)>=0

  JUDGEMENT Sum HAS_TYPE [nat,[nat->nonneg_real]->nonneg_real]
  

  Sum_zero: lemma Sum(j,F1)=0 iff forall (i:below(j)): F1(i)=0

  Sum_pos: lemma  Sum(j,F1)>0 iff (exists (i:below(j)): F1(i)>0)

  Sum_le:  lemma (forall (i:below(j)): F1(i) <= F2(i)) => Sum(j,F1)<=Sum(j,F2)

  Sum_ge1: lemma (exists (i:below(j)): F1(i)>=1) => Sum(j,F1)>=1

  pz: var posreal

  Sum_ge: lemma (exists (i:below(j)): F1(i)>= pz) => Sum(j,F1)>=pz

  Sum_split: lemma forall (i:upto(j)):
    Sum(j,F) = Sum(i,F) + Sum(j-i,lambda k: F(k+i)) 

  END sum_hack

$$$sum_hack.prf
(|sum_hack| (|Sum_TCC1| "" (TCC :DEFS !) NIL)
 (|Sum_TCC2| "" (TCC :DEFS !) NIL)
 (|Sum_nonneg| "" (INDUCT-AND-REWRITE "j" 1 "Sum") NIL)
 (|Sum_TCC3| "" (SKOSIMP*) (("" (REWRITE "Sum_nonneg") NIL)))
 (|Sum_zero| "" (INDUCT "j")
  (("1" (EXPAND "Sum") (("1" (ASSERT) (("1" (SKOSIMP*) NIL)))))
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST?)
        (("2" (PROP)
          (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))
           ("2" (INST?) (("2" (ASSERT) NIL)))
           ("3" (TYPEPRED "Sum(j!1,F1!1)")
            (("3" (TYPEPRED "F1!1(j!1)") (("3" (ASSERT) NIL)))))
           ("4" (SKOSIMP*) (("4" (INST?) NIL)))))))))))))
 (|Sum_pos| "" (INDUCT "j")
  (("1" (EXPAND "Sum")
    (("1" (SKOSIMP*) (("1" (GROUND) (("1" (SKOSIMP*) NIL)))))))
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST?)
        (("2" (LEMMA "Sum_nonneg")
          (("2" (INST?)
            (("2" (PROP)
              (("1" (SKOSIMP*) (("1" (INST?) NIL)))
               ("2" (ASSERT) NIL)
               ("3" (INST + "j!1") (("3" (ASSERT) NIL)))
               ("4" (SKOSIMP*)
                (("4" (INST?) (("4" (ASSERT) NIL)))))))))))))))))))
 (|Sum_le| "" (INDUCT "j")
  (("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "Sum" +)
      (("2" (INST - "F1!1 " "F2!1")
        (("2" (PROP)
          (("1" (INST?) (("1" (ASSERT) NIL)))
           ("2" (SKOSIMP*) (("2" (INST?) NIL)))))))))))))
 (|Sum_ge1| "" (INDUCT "j")
  (("1" (SKOSIMP*) NIL)
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (LEMMA "Sum_nonneg")
            (("2" (INST?)
              (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))
 (|Sum_ge| "" (INDUCT "j")
  (("1" (SKOSIMP*) NIL)
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST - "F1!1" "pz!1")
        (("2" (PROP)
          (("1" (ASSERT) NIL)
           ("2" (INST?)
            (("2" (ASSERT)
              (("2" (GROUND)
                (("2" (LEMMA "Sum_nonneg")
                  (("2" (INST?)
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|Sum_split_TCC1| "" (TCC) NIL)
 (|Sum_split| "" (INDUCT "j")
  (("1" (SKOSIMP*) (("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))))
   ("2" (SKOSIMP*)
    (("2" (TYPEPRED "i!1")
      (("2" (EXPAND "Sum" + (1 3))
        (("2" (LIFT-IF)
          (("2" (GROUND)
            (("1" (EXPAND "Sum" + 2) (("1" (PROPAX) NIL)))
             ("2" (INST - "F!1" "i!1")
              (("2" (ASSERT) NIL))))))))))))))))
$$$sum_lemmas.pvs
sum_lemmas [b:above(1)]: THEORY

  BEGIN

  importing sum_hack

  i: var nat

  F1: var [nat->nonneg_real]

  mant_digit_fun: type = {F1| forall i: F1(i)<=(b-1)*b^(-i-1)}

  d: var mant_digit_fun

  Sum_pos_less_1: lemma
      0<=Sum(i,d) & Sum(i,d)<= 1-b^(-i)

  floor_Sum_mant: lemma 
     floor(Sum(i,d))=0

  END sum_lemmas

$$$sum_lemmas.prf
(|sum_lemmas| (|mant_digit_fun_TCC1| "" (TCC) NIL)
 (|Sum_pos_less_1_TCC1| "" (TCC) NIL)
 (|Sum_pos_less_1| "" (INDUCT "i")
  (("1" (EXPAND "Sum")
    (("1" (REWRITE "expt_x0") (("1" (ASSERT) NIL)))))
   ("2" (SKOSIMP*)
    (("2" (REWRITE "Sum")
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (TYPEPRED "d!1")
            (("2" (INST?)
              (("2" (ASSERT)
                (("2" (CASE-REPLACE "b ^ (-j!1 - 1) * b = b^(-j!1)")
                  (("1" (ASSERT) NIL)
                   ("2" (HIDE -1 -2 2)
                    (("2" (LEMMA "expt_plus")
                      (("2" (INST - "(-(j!1+1))" "1" "b")
                        (("2" (REWRITE "expt_x1")
                          (("2" (ASSERT) NIL)))))))))))))))))))))))))
   ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
   ("4" (SKOSIMP*) (("4" (ASSERT) NIL)))))
 (|floor_Sum_mant| "" (SKOSIMP*)
  (("" (LEMMA "Sum_pos_less_1")
    (("" (INST?)
      (("" (LEMMA "expt_pos")
        (("" (INST?)
          (("1" (CASE "1-b^(-i!1)<1")
            (("1" (CASE "Sum(i!1, d!1) < 1")
              (("1" (FLATTEN)
                (("1" (HIDE -2 -3 -5)
                  (("1" (ASSERT)
                    (("1"
                      (CASE "forall (r:real): floor(r)=0 iff 0<=r & r<1")
                      (("1" (INST?) (("1" (ASSERT) NIL)))
                       ("2" (HIDE -1 -2 2) (("2" (TCC) NIL)))))))))))
               ("2" (ASSERT) NIL)))
             ("2" (ASSERT) NIL) ("3" (ASSERT) NIL)))
           ("2" (SPLIT)
            (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))
$$$enumerated_type_defs.pvs
enumerated_type_defs: THEORY

  BEGIN

  sign_rep: type = {n:nat| n = 0 or n = 1}
  pos:sign_rep = 0
  neg:sign_rep = 1

  NaN_type: type = {signal,quiet}
  NaN_data: NONEMPTY_TYPE
  invalid_data: NaN_data

  fp_ops        : type = {add,sub,mult,div}
  rounding_mode : type = {to_nearest,to_zero,to_pos,to_neg}  

   exception: DATATYPE
     BEGIN
       invalid_operation      : invalid?
       division_by_zero       : div_by_zero?
       overflow               : overflow?
       underflow(exact?:bool) : underflow?
       inexact                : inexact?
       no_exceptions          : no_exceptions?
     END exception

  trap_enabled?(e:exception) : bool

  END enumerated_type_defs

$$$enumerated_type_defs.prf
(|enumerated_type_defs| (|pos_TCC1| "" (ASSERT) NIL)
 (|neg_TCC1| "" (ASSERT) NIL))
$$$IEEE_854_remainder.pvs
IEEE_854_remainder
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min],
            real_to_fp[b,p,alpha,E_max,E_min],
            round

  fin, fin1, fin2: var (finite?)

  REM(fin1, (fin2:{fin|not zero?(fin)})): fp_num =
     let x = value(fin1),
         y = value(fin2) in
     if (x - y * round_to_even(x/y)) = 0
        then finite(sign(fin1),E_min,d_zero)
        else real_to_fp(x - y * round_to_even(x/y))
     endif

  END IEEE_854_remainder

$$$IEEE_854_remainder.prf
(|IEEE_854_remainder| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
 (REM_TCC1 "" (SKOLEM-TYPEPRED)
  (("" (SKOSIMP*)
    (("" (REPLACE -6)
      (("" (EXPAND "zero?") (("" (PROPAX) NIL)))))))))
 (REM_TCC2 "" (SKOSIMP*) (("" (ASSERT) NIL))))
$$$real_to_fp.pvs
real_to_fp
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min], 
            over_under[b,p,alpha,E_max,E_min],
            fp_round_aux[b,p],
            round

  r: var real
  mode: var rounding_mode
  op: var fp_ops
  fin, fin1, fin2: var (finite?)

  px: var posreal
  E: var integer

  JUDGEMENT truncate has_type [integer,nonneg_real -> digits]

  truncate_zero: lemma truncate(E,0)=d_zero

  digits_of_finite: lemma truncate(Exp(fin),abs(value(fin))) = d(fin)

  real_to_fp(r): fp_num =
    IF abs(r) >= b^(E_max+1) THEN 
       infinite(sign_of(r))
    ELSIF abs(r) < b^E_min THEN 
       finite(sign_of(r), E_min, truncate(E_min, abs(r)))
    ELSE 
       finite(sign_of(r), Exp_of(abs(r)), truncate(Exp_of(abs(r)), abs(r)))
    ENDIF    

  real_to_fp_x(r:real,e:exception): [fp_num,exception] = (real_to_fp(r),e)

  real_to_fp_zero: lemma real_to_fp(0) = pos_zero

  sign_of_value: lemma not zero?(fin) =>(sign_of(value(fin))= sign(fin))

  Exp_of_value_normal: LEMMA
         normal?(fin)
          => Exp_of(abs(value(fin))) = Exp(normalize(fin))

  real_to_fp_normal: LEMMA 
	        normal?(fin) 
          => real_to_fp(value(fin)) = normalize(fin)

  real_to_fp_subnormal: LEMMA 
        subnormal?(fin) 
          => real_to_fp(value(fin)) = normalize(fin)

  real_to_fp_inverts_value: LEMMA 
       not zero?(fin) => real_to_fp(value(fin)) = normalize(fin)

  round_exceptions_x(x:(over_under?),mode:rounding_mode): [real,exception] =
    IF abs(x)>max_pos THEN 
            overflow(x,mode)
       ELSE underflow(x,mode)
       ENDIF

  round_exceptions(r:(over_under?),mode): real 
      = proj_1(round_exceptions_x(r,mode))

  fp_round(r, mode): real =
    IF r = 0 THEN 0
    ELSIF over_under?(r) then
      round_exceptions(r,mode)
    ELSE round_scaled(r,mode)
    ENDIF

  is_exact?(r:nzreal,mode):exception =
    IF round_scaled(r,mode) = r then no_exceptions ELSE inexact ENDIF
  
  fp_round_x(r, mode): [real,exception] =
    IF r = 0 THEN (0,no_exceptions)
    ELSIF over_under?(r) then
      round_exceptions_x(r,mode)
    ELSE (round_scaled(r,mode),is_exact?(r,mode))
    ENDIF

  round_value: lemma not over_under?(value(fin)) =>
                 fp_round(value(fin),mode) = value(fin)

  round_value2: lemma not trap_enabled?(underflow(FALSE)) =>
                 fp_round(value(fin),mode) = value(fin)

  round_0: lemma fp_round(0,mode)=0

  round_value3: lemma not trap_enabled?(underflow(FALSE)) =>
                 not zero?(fin) =>
                 real_to_fp(fp_round(value(fin),mode)) = normalize(fin)

  round_error: lemma r/=0 & not over_under?(r)
            => abs(r-fp_round(r,mode))<b^(Exp_of(abs(r))-(p-1))

  round_near: LEMMA
        r /= 0 & not over_under?(r)
          => abs(r - fp_round(r, to_nearest))
               <= b ^ (Exp_of(abs(r)) - (p - 1)) / 2

  round_pos: lemma not over_under?(r) => fp_round(r,to_pos)>=r

  round_neg: lemma not over_under?(r) => fp_round(r,to_neg)<=r

  round_zero: lemma not over_under?(r) => abs(fp_round(r,to_zero))<=abs(r)
  
  END real_to_fp

$$$real_to_fp.prf
(|real_to_fp|
 (|truncate_zero| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY)
    (("" (EXPAND "truncate")
      (("" (EXPAND "d_zero")
        (("" (ASSERT)
          (("" (LEMMA "div_eq_zero")
            (("" (ASSERT)
              (("" (REWRITE "floor_int")
                (("" (REWRITE "mod_zero") NIL)))))))))))))))))
 (|digits_of_finite| "" (SKOSIMP*)
  (("" (REWRITE "abs_value_fin")
    (("" (CASE "b ^ (Exp(fin!1)) * Sum(p, value_digit(d(fin!1))) >=0")
      (("1" (APPLY-EXTENSIONALITY)
        (("1" (HIDE 2)
          (("1" (REWRITE "truncate")
            (("1" (ASSERT)
              (("1"
                (CASE-REPLACE "(b ^ (x!1 - Exp(fin!1))
                  *
                  (b ^ (Exp(fin!1))
                     * Sum(p, value_digit(d(fin!1))))) =
Sum(p, value_digit(d(fin!1)))*b^x!1")
                (("1" (HIDE -1 -2)
                  (("1" (LEMMA "floor_Sum")
                    (("1" (INST?)
                      (("1" (REPLACE -1)
                        (("1" (HIDE -1)
                          (("1" (LEMMA "mod_Sum")
                            (("1" (INST?) NIL)))))))))))))
                 ("2" (HIDE -1 2)
                  (("2" (ASSERT)
                    (("2" (LEMMA "expt_plus")
                      (("2" (INST?)
                        (("2" (INST - "Exp(fin!1)")
                          (("2" (ASSERT) NIL)))))))))))))))))))))
       ("2" (LEMMA "expt_pos")
        (("2" (INST?)
          (("2" (LEMMA "Sum_nonneg")
            (("2" (INST?)
              (("2" (REWRITE "pos_times_ge")
                (("2" (ASSERT) NIL)))))))))))))))))
 (|real_to_fp_TCC1| "" (TCC :DEFS !) NIL)
 (|real_to_fp_TCC2| "" (TCC :DEFS !) NIL)
 (|real_to_fp_TCC3| "" (TCC :DEFS !) NIL)
 (|real_to_fp_TCC4| "" (SKOSIMP*)
  (("" (HIDE 1)
    (("" (LEMMA "expt_pos")
      (("" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))
 (|real_to_fp_TCC5| "" (SKOSIMP)
  (("" (CASE "abs(r!1)>0")
    (("1" (TYPEPRED "Exp_of(abs(r!1))")
      (("1" (GROUND)
        (("1" (CASE "b^E_min<= abs(r!1)")
          (("1" (LEMMA "both_sides_expt_gt1_lt")
            (("1" (INST - "b" "E_min" "(1 + Exp_of(abs(r!1)))")
              (("1" (ASSERT) NIL)))))
           ("2" (ASSERT) NIL)))
         ("2" (CASE "abs(r!1)<b^(1+E_max)")
          (("1" (LEMMA "both_sides_expt_gt1_lt")
            (("1" (INST - "b" "Exp_of(abs(r!1))" "1+E_max")
              (("1" (ASSERT) NIL)))))
           ("2" (ASSERT) NIL)))))
       ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
       ("3" (SKOSIMP*) (("3" (ASSERT) NIL))) ("4" (PROPAX) NIL)))
     ("2" (LEMMA "expt_pos")
      (("2" (INST - "E_min" "b")
        (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))
 (|real_to_fp_zero| "" (REWRITE "real_to_fp")
  (("" (EXPAND "abs")
    (("" (LEMMA "expt_pos")
      (("" (INST-CP - "(1+E_max)" "b")
        (("" (ASSERT)
          (("" (HIDE -2)
            (("" (INST?)
              (("" (ASSERT)
                (("" (REWRITE "truncate_zero")
                  (("" (EXPAND "sign_of")
                    (("" (EXPAND "pos_zero")
                      (("" (PROPAX) NIL)))))))))))))))))))))))
 (|sign_of_value| "" (SKOSIMP*)
  (("" (EXPAND "sign_of")
    (("" (LIFT-IF)
      (("" (LEMMA "value_negative")
        (("" (INST?)
          (("" (GROUND)
            (("" (EXPAND "neg")
              (("" (EXPAND "pos")
                (("" (ASSERT)
                  (("" (TYPEPRED "sign(fin!1)")
                    (("" (ASSERT) NIL)))))))))))))))))))))
 (|Exp_of_value_normal_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "abs")
    (("" (LIFT-IF)
      (("" (GROUND)
        (("" (LEMMA "finite_disjoint1")
          (("" (INST?) (("" (EXPAND "zero?") (("" (PROPAX) NIL)))))))))))))))
 (|Exp_of_value_normal| "" (SKOSIMP*)
  (("" (REWRITE "normal_value")
    (("" (REWRITE "abs_value_fin")
      (("" (LEMMA "value_sig_lt_b")
        (("" (LEMMA "value_sig_ge1")
          (("" (EXPAND "normal?")
            (("" (ASSERT)
              (("" (INST?)
                (("" (ASSERT)
                  (("" (INST?)
                    (("" (LEMMA "expt_pos")
                      (("" (INST?)
                        ((""
                          (CASE "(b ^ (Exp(normalize(fin!1)))
               * Sum(p, value_digit(d(normalize(fin!1)))))>0")
                          (("1" (ASSERT)
                            (("1"
                              (TYPEPRED "Exp_of(b ^ (Exp(normalize(fin!1)))
               * Sum(p, value_digit(d(normalize(fin!1)))))")
                              (("1" (LEMMA "div_mult_pos_lt2")
                                (("1"
                                  (INST - "b ^ (Exp(normalize(fin!1)))"
                                   "Sum(p, value_digit(d(normalize(fin!1))))"
                                   "b
            ^
            (1
               +
               Exp_of(b ^ (Exp(normalize(fin!1)))
                        * Sum(p, value_digit(d(normalize(fin!1))))))")
                                  (("1" (REPLACE -1 :DIR RL)
                                    (("1" (HIDE -1)
                                      (("1"
                                        (LEMMA "div_mult_pos_le1")
                                        (("1"
                                          (INST
                                           -
                                           "b ^ (Exp(normalize(fin!1)))"
                                           "Sum(p, value_digit(d(normalize(fin!1))))"
                                           "b
            ^
            ( Exp_of(b ^ (Exp(normalize(fin!1)))
                        * Sum(p, value_digit(d(normalize(fin!1))))))")
                                          (("1"
                                            (REPLACE -1 :DIR RL)
                                            (("1"
                                              (HIDE -1)
                                              (("1"
                                                (REWRITE "expt_div")
                                                (("1"
                                                  (REWRITE "expt_div")
                                                  (("1"
                                                    (CASE
                                                     "(Exp_of(b ^ (Exp(normalize(fin!1)))
                   * Sum(p, value_digit(d(normalize(fin!1))))))
           > (Exp(normalize(fin!1)))")
                                                    (("1"
                                                      (LEMMA "expt_gt1_pos")
                                                      (("1"
                                                        (INST
                                                         -
                                                         "b"
                                                         "(Exp_of(b ^ (Exp(normalize(fin!1)))
                   * Sum(p, value_digit(d(normalize(fin!1))))))
           - (Exp(normalize(fin!1)))")
                                                        (("1" (ASSERT) NIL)
                                                         ("2"
                                                          (ASSERT)
                                                          NIL)))))
                                                     ("2"
                                                      (LEMMA
                                                       "expt_gt1_nonpos")
                                                      (("2"
                                                        (INST
                                                         -
                                                         "b"
                                                         "-((1
                +
                Exp_of(b ^ (Exp(normalize(fin!1)))
                         * Sum(p, value_digit(d(normalize(fin!1))))))
               - (Exp(normalize(fin!1))))")
                                                        (("1" (ASSERT) NIL)
                                                         ("2"
                                                          (ASSERT)
                                                          NIL)))))))))))))))))))))))))))))))
                           ("2" (REWRITE "pos_times_gt")
                            (("2" (ASSERT) NIL)))))))))))))))))))))))))))))
 (|real_to_fp_normal| "" (SKOSIMP*)
  (("" (REWRITE "real_to_fp")
    (("" (LIFT-IF)
      (("" (LEMMA "value_normal")
        (("" (INST?)
          (("" (ASSERT)
            (("" (FLATTEN)
              (("" (ASSERT)
                (("" (CASE "max_pos < b^(1+E_max)")
                  (("1" (ASSERT)
                    (("1" (HIDE -1 -2 -3)
                      (("1" (REWRITE "Exp_of_value_normal")
                        (("1" (LEMMA "finite_disjoint1")
                          (("1" (INST?)
                            (("1" (ASSERT)
                              (("1" (REWRITE "normal_value")
                                (("1" (REWRITE "sign_of_value")
                                  (("1" (ASSERT)
                                    (("1" (REWRITE "digits_of_finite")
                                      (("1"
                                        (REWRITE "fp_num_finite_eta")
                                        NIL)))))
                                   ("2" (EXPAND "zero?")
                                    (("2" (REWRITE "normal_value" +)
                                      NIL)))))))))))))))))))
                   ("2" (HIDE 2)
                    (("2" (HIDE -1 -2 -3)
                      (("2" (LEMMA "max_fp_correct")
                        (("2" (LEMMA "expt_pos")
                          (("2" (INST - "(E_max-(p-1))" "b")
                            (("2" (ASSERT) NIL)))))))))))))))))))))))))))))
 (|real_to_fp_subnormal| "" (SKOSIMP*)
  (("" (REWRITE "real_to_fp")
    (("" (LEMMA "value_subnormal")
      (("" (INST?)
        (("" (ASSERT)
          (("" (FLATTEN)
            (("" (ASSERT)
              (("" (CASE "b^E_min < b^(1+E_max)")
                (("1" (ASSERT)
                  (("1" (REWRITE "normal_value")
                    (("1" (REWRITE "sign_of_value")
                      (("1" (HIDE -1)
                        (("1" (EXPAND "subnormal?")
                          (("1" (ASSERT)
                            (("1" (GROUND)
                              (("1" (LEMMA "digits_of_finite")
                                (("1" (INST?)
                                  (("1" (LEMMA "fp_num_finite_eta")
                                    (("1" (INST?)
                                      (("1"
                                        (REPLACE -5)
                                        (("1"
                                          (REPLACE -2)
                                          (("1"
                                            (PROPAX)
                                            NIL)))))))))))))))))))))
                       ("2" (EXPAND "subnormal?")
                        (("2" (GROUND)
                          (("2" (EXPAND "zero?")
                            (("2" (ASSERT)
                              (("2" (REWRITE "normal_value" +)
                                NIL)))))))))))))))
                 ("2" (HIDE -1 -2 -3 2)
                  (("2" (REWRITE "both_sides_expt_gt1_lt")
                    NIL)))))))))))))))))))
 (|real_to_fp_inverts_value| "" (SKOSIMP*)
  (("" (LEMMA "finite_cover")
    (("" (INST?)
      (("" (GROUND)
        (("1" (REWRITE "real_to_fp_normal") NIL)
         ("2" (REWRITE "real_to_fp_subnormal") NIL)))))))))
 (|round_exceptions_x_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "over_under?") (("" (GROUND) NIL)))))
 (|round_exceptions_x_TCC2| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "over_under?") (("" (GROUND) NIL)))))
 (|fp_round_TCC1| "" (TCC :DEFS !) NIL)
 (|round_value| "" (SKOSIMP*)
  (("" (EXPAND "fp_round")
    (("" (EXPAND "round_scaled")
      (("" (ASSERT)
        (("" (LIFT-IF)
          (("" (ASSERT)
            (("" (GROUND)
              (("" (EXPAND "scale")
                (("" (REWRITE "Exp_of_value_normal")
                  (("1" (REWRITE "round_int")
                    (("1" (REWRITE "expt_inverse") (("1" (ASSERT) NIL)))
                     ("2" (HIDE 2 3 4)
                      (("2"
                        (CASE "integer?(value(fin!1)*b^(-(1 + Exp(normalize(fin!1)) - p)))")
                        (("1" (EXPAND "integer?")
                          (("1" (ASSERT) (("1" (GROUND) NIL)))))
                         ("2" (HIDE 2)
                          (("2" (REWRITE "normal_value")
                            (("2" (EXPAND "value")
                              (("2"
                                (CASE-REPLACE
                                 "(Sum(p, value_digit(d(normalize(fin!1))))
                     * (-1) ^ sign(normalize(fin!1))
                     * b ^ Exp(normalize(fin!1))
                     * b ^ (-(1 + Exp(normalize(fin!1)) - p))) =
(-1) ^ sign(normalize(fin!1))
                     * Sum(p, value_digit(d(normalize(fin!1))))
                     * b ^ (p-1)")
                                (("1" (HIDE -1)
                                  (("1"
                                    (CASE-REPLACE
                                     "((-1) ^ sign(normalize(fin!1))
                     * Sum(p, value_digit(d(normalize(fin!1))))
                     * b ^ (p - 1)) = ((-1) ^ sign(normalize(fin!1))
                     * Sum(p, scale_value_p(d(normalize(fin!1)))))")
                                    (("1" (HIDE -1)
                                      (("1"
                                        (CASE
                                         "FORALL (i,j:int): integer?(i*j)")
                                        (("1"
                                          (INST?)
                                          (("1"
                                            (HIDE 2)
                                            (("1"
                                              (CASE
                                               "forall (n:nat),(d:digits): integer?(Sum(n,scale_value_p(d)))")
                                              (("1"
                                                (EXPAND "integer?")
                                                (("1" (INST?) NIL)))
                                               ("2"
                                                (HIDE 2)
                                                (("2"
                                                  (INDUCT "n")
                                                  (("1"
                                                    (EXPAND "Sum")
                                                    (("1"
                                                      (EXPAND "integer?")
                                                      (("1" (PROPAX) NIL)))))
                                                   ("2"
                                                    (SKOSIMP*)
                                                    (("2"
                                                      (REWRITE "Sum")
                                                      (("2"
                                                        (INST?)
                                                        (("2"
                                                          (CASE
                                                           "FORALL (i,j:int): integer?(i+j)")
                                                          (("1"
                                                            (INST?)
                                                            (("1"
                                                              (EXPAND
                                                               "integer?")
                                                              (("1"
                                                                (PROPAX)
                                                                NIL)))))
                                                           ("2"
                                                            (HIDE -1 2)
                                                            (("2"
                                                              (SKOSIMP*)
                                                              (("2"
                                                                (EXPAND
                                                                 "integer?")
                                                                (("2"
                                                                  (PROPAX)
                                                                  NIL)))))))))))))))))))))))))
                                         ("2"
                                          (HIDE 2)
                                          (("2"
                                            (SKOSIMP*)
                                            (("2"
                                              (EXPAND "integer?")
                                              (("2" (PROPAX) NIL)))))))))))
                                     ("2" (HIDE 2)
                                      (("2"
                                        (ASSERT)
                                        (("2"
                                          (LEMMA "scaled_Sum")
                                          (("2"
                                            (INST?)
                                            (("2" (ASSERT) NIL)))))))))))))
                                 ("2" (HIDE 2)
                                  (("2" (ASSERT)
                                    (("2" (LEMMA "expt_plus")
                                      (("2"
                                        (INST
                                         -
                                         "Exp(normalize(fin!1))"
                                         "(-(1+Exp(normalize(fin!1)) - p))"
                                         "b")
                                        (("2"
                                          (ASSERT)
                                          NIL)))))))))))))))))))))))
                   ("2" (HIDE 3)
                    (("2" (EXPAND "over_under?")
                      (("2" (LEMMA "value_subnormal")
                        (("2" (INST?)
                          (("2" (GROUND)
                            (("2" (LEMMA "finite_cover")
                              (("2" (INST?)
                                (("2" (EXPAND "zero?")
                                  (("2" (PROPAX)
                                    NIL)))))))))))))))))))))))))))))))))))
 (|round_value2| "" (SKOSIMP*)
  (("" (REWRITE "round_value")
    (("" (EXPAND "fp_round")
      (("" (LIFT-IF)
        (("" (ASSERT)
          (("" (PROP)
            (("" (EXPAND "round_exceptions")
              (("" (EXPAND "round_exceptions_x")
                (("" (LEMMA "value_nonzero")
                  (("" (INST?)
                    (("" (ASSERT)
                      (("" (EXPAND "zero?")
                        (("" (LIFT-IF)
                          (("" (PROP)
                            (("1" (ASSERT) NIL)
                             ("2" (EXPAND "over_under?")
                              (("2" (ASSERT)
                                (("2" (EXPAND "underflow")
                                  (("2" (LIFT-IF)
                                    (("2" (ASSERT)
                                      (("2"
                                        (REWRITE "round_under_value")
                                        (("2"
                                          (LEMMA "finite_cover")
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (EXPAND "zero?")
                                              (("2"
                                                (LEMMA "value_normal")
                                                (("2"
                                                  (INST?)
                                                  (("2"
                                                    (ASSERT)
                                                    NIL)))))))))))))))))))))))))))))))))))))))))))))))))))
 (|round_0| "" (SKOSIMP*) (("" (EXPAND "fp_round") (("" (PROPAX) NIL)))))
 (|round_value3| "" (SKOSIMP*)
  (("" (REWRITE "round_value2")
    (("" (REWRITE "real_to_fp_inverts_value") NIL)))))
 (|round_error_TCC1| "" (TCC :DEFS !) NIL)
 (|round_error_TCC2| "" (TCC :DEFS !) NIL)
 (|round_error| "" (SKOSIMP*)
  (("" (EXPAND "fp_round")
    (("" (EXPAND "round_scaled")
      (("" (LIFT-IF)
        (("" (GROUND)
          ((""
            (CASE-REPLACE "r!1
            - b ^ scale(abs(r!1))
                * round(r!1 * b ^ (-scale(abs(r!1))), mode!1)=
b^scale(abs(r!1))*(r!1*b ^ (-scale(abs(r!1))) -round(r!1 * b ^ (-scale(abs(r!1))), mode!1))")
            (("1" (HIDE -1)
              (("1" (REWRITE "abs_mult")
                (("1" (LEMMA "div_mult_pos_lt2")
                  (("1"
                    (INST - "abs(b ^ scale(abs(r!1)))"
                     "abs((r!1 * b ^ (-scale(abs(r!1)))
               - round(r!1 * b ^ (-scale(abs(r!1))), mode!1)))"
                     "b ^ (1 + Exp_of(abs(r!1)) - p)")
                    (("1" (REPLACE -1 :DIR RL)
                      (("1" (HIDE -1)
                        (("1"
                          (CASE-REPLACE
                           "b ^ (1 + Exp_of(abs(r!1)) - p) / abs(b ^ scale(abs(r!1)))=1")
                          (("1" (REWRITE "round1") NIL)
                           ("2" (HIDE 3)
                            (("2" (HIDE 2)
                              (("2" (LEMMA "expt_pos")
                                (("2" (REWRITE "abs")
                                  (("2" (LIFT-IF)
                                    (("2" (GROUND)
                                      (("1"
                                        (REWRITE "abs")
                                        (("1"
                                          (LIFT-IF)
                                          (("1"
                                            (INST?)
                                            (("1"
                                              (ASSERT)
                                              (("1"
                                                (EXPAND "scale")
                                                (("1" (ASSERT) NIL)))))))))))
                                       ("2"
                                        (REWRITE "abs")
                                        (("2"
                                          (LIFT-IF)
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (ASSERT)
                                              (("2"
                                                (EXPAND "scale")
                                                (("2"
                                                  (ASSERT)
                                                  NIL)))))))))))))))))))))))
                           ("3" (HIDE 3)
                            (("3" (EXPAND "abs" + 1)
                              (("3" (LEMMA "expt_pos")
                                (("3" (INST?)
                                  (("3" (ASSERT) NIL)))))))))))))))
                     ("2" (HIDE 3)
                      (("2" (LEMMA "expt_pos")
                        (("2" (INST?)
                          (("2" (EXPAND "abs" + 1)
                            (("2" (ASSERT) NIL)))))))))))))))))
             ("2" (HIDE 3)
              (("2" (ASSERT)
                (("2" (REWRITE "expt_inverse")
                  (("2" (ASSERT) NIL)))))))))))))))))))
 (|round_near| "" (SKOSIMP*)
  (("" (EXPAND "fp_round")
    (("" (EXPAND "round_scaled")
      (("" (ASSERT)
        (("" (CASE "abs(r!1)>0")
          (("1"
            (CASE-REPLACE "(r!1
            - b ^ scale(abs(r!1))
                * round(r!1 * b ^ (-scale(abs(r!1))), to_nearest)) =
b^scale(abs(r!1))*(r!1*b^(-scale(abs(r!1))) - round(r!1 * b ^ (-scale(abs(r!1))), to_nearest))")
            (("1" (HIDE -1)
              (("1" (REWRITE "abs_mult")
                (("1" (LEMMA "div_mult_pos_le2")
                  (("1"
                    (INST - "abs(b ^ scale(abs(r!1)))"
                     "abs((r!1 * b ^ (-scale(abs(r!1)))
               - round(r!1 * b ^ (-scale(abs(r!1))), to_nearest)))"
                     "b ^ (1 + Exp_of(abs(r!1)) - p) / 2")
                    (("1" (REPLACE -1 :DIR RL)
                      (("1" (HIDE -1)
                        (("1"
                          (CASE-REPLACE
                           "b ^ (1 + Exp_of(abs(r!1)) - p) / 2 / abs(b ^ scale(abs(r!1)))=1/2")
                          (("1" (EXPAND "round")
                            (("1" (REWRITE "round_to_even1") NIL)))
                           ("2" (HIDE 3)
                            (("2" (REWRITE "div_div2")
                              (("1" (EXPAND "scale")
                                (("1" (EXPAND "abs" + 2)
                                  (("1" (LIFT-IF)
                                    (("1" (LEMMA "expt_pos")
                                      (("1"
                                        (INST?)
                                        (("1" (ASSERT) NIL)))))))))))
                               ("2" (HIDE 2)
                                (("2" (LEMMA "expt_pos")
                                  (("2" (INST?)
                                    (("2" (EXPAND "abs" + 1)
                                      (("2" (ASSERT) NIL)))))))))))))
                           ("3" (HIDE 3)
                            (("3" (LEMMA "expt_pos")
                              (("3" (INST?)
                                (("3" (EXPAND "abs" + 1)
                                  (("3" (ASSERT) NIL)))))))))))))))
                     ("2" (HIDE 3)
                      (("2" (LEMMA "expt_pos")
                        (("2" (INST?)
                          (("2" (EXPAND "abs" + 1)
                            (("2" (ASSERT) NIL)))))))))))))))))
             ("2" (ASSERT)
              (("2" (HIDE 3)
                (("2" (REWRITE "expt_inverse") (("2" (ASSERT) NIL)))))))))
           ("2" (HIDE 3)
            (("2" (EXPAND "abs")
              (("2" (LIFT-IF) (("2" (ASSERT) NIL)))))))))))))))))
 (|round_pos| "" (SKOSIMP*)
  (("" (EXPAND "fp_round")
    (("" (EXPAND "round_scaled")
      (("" (LIFT-IF)
        (("" (ASSERT)
          (("" (GROUND)
            (("" (EXPAND "round")
              (("" (ASSERT)
                (("" (LEMMA "div_mult_pos_ge2")
                  ((""
                    (INST - "b ^ scale(abs(r!1))"
                     "ceiling(r!1 * b ^ (-scale(abs(r!1))))" "r!1")
                    (("1" (REPLACE -1 :DIR RL)
                      (("1" (REWRITE "expt_inverse") (("1" (ASSERT) NIL)))))
                     ("2" (LEMMA "expt_pos")
                      (("2" (INST?)
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|round_neg| "" (SKOSIMP*)
  (("" (EXPAND "fp_round")
    (("" (EXPAND "round_scaled")
      (("" (LIFT-IF)
        (("" (GROUND)
          (("" (EXPAND "round")
            (("" (LEMMA "div_mult_pos_le2")
              ((""
                (INST - "b ^ scale(abs(r!1))"
                 "floor(r!1 * b ^ (-scale(abs(r!1))))" "r!1")
                (("1" (REPLACE -1 :DIR RL)
                  (("1" (REWRITE "expt_inverse")
                    (("1" (HIDE -1)
                      (("1"
                        (TYPEPRED "floor(r!1 * (1 / (b ^ scale(abs(r!1)))))")
                        (("1" (ASSERT) NIL)
                         ("2" (SKOSIMP)
                          (("2" (LEMMA "expt_pos")
                            (("2" (INST?) (("2" (ASSERT) NIL)))))))
                         ("3" (SKOSIMP*)
                          (("3" (LEMMA "expt_nonzero")
                            (("3" (INST?) (("3" (ASSERT) NIL)))))))
                         ("4" (REWRITE "expt_nonzero") NIL)))))))))
                 ("2" (LEMMA "expt_pos")
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|round_zero| "" (SKOSIMP*)
  (("" (EXPAND "fp_round")
    (("" (ASSERT)
      (("" (LIFT-IF)
        (("" (PROP)
          (("1" (ASSERT) NIL)
           ("2" (CASE "abs(r!1)>0")
            (("1" (HIDE 3)
              (("1" (EXPAND "round_scaled")
                (("1" (REWRITE "abs_mult")
                  (("1" (NAME-REPLACE "sr!1" "scale(abs(r!1))")
                    (("1" (REWRITE "expt_inverse")
                      (("1" (LEMMA "expt_pos")
                        (("1" (INST?)
                          (("1" (NAME-REPLACE "s!1" "b^sr!1")
                            (("1" (CASE "abs(s!1)>0")
                              (("1" (LEMMA "div_mult_pos_le2")
                                (("1"
                                  (INST - "abs(s!1)"
                                   "abs(round(r!1/s!1,to_zero))" "abs(r!1)")
                                  (("1" (REPLACE -1 :DIR RL)
                                    (("1" (HIDE -1)
                                      (("1"
                                        (CASE-REPLACE
                                         "abs(r!1) / abs(s!1) = abs(r!1/s!1)")
                                        (("1"
                                          (HIDE -1)
                                          (("1"
                                            (NAME-REPLACE "r!2" "r!1/s!1")
                                            (("1"
                                              (HIDE -1 -2 -3 1)
                                              (("1" (GRIND) NIL)))
                                             ("2" (ASSERT) NIL)))))
                                         ("2"
                                          (HIDE -3 2 3)
                                          (("2"
                                            (GRIND)
                                            (("1" (REWRITE "neg_div_lt") NIL)
                                             ("2"
                                              (REWRITE "neg_div_lt")
                                              NIL)))))
                                         ("3" (ASSERT) NIL)
                                         ("4" (ASSERT) NIL)))))))
                                   ("2" (ASSERT) NIL)))))
                               ("2" (HIDE -2 2 3)
                                (("2" (EXPAND "abs")
                                  (("2" (LIFT-IF)
                                    (("2" (ASSERT)
                                      NIL)))))))))))))))))))))))))
             ("2" (HIDE 3 4) (("2" (GRIND) NIL))))))))))))))))
$$$over_under.pvs
over_under
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min], 
            fp_round_aux[b,p],
            enumerated_type_defs,
            round

  over_under?(r:real): bool = (r/=0 & (abs(r)>max_pos or abs(r)<b^E_min))

% A real number that real_to_fp maps to infinity
  infinity: real = b^(E_max+1)

  trap_over((r1:nzreal), (r2: real), (mode: rounding_mode)): real =
    IF trap_enabled?(overflow) THEN round_scaled(r1 * b ^ (-alpha), mode)
    ELSE r2
    ENDIF

  overflow((r: nzreal | abs(r) > max_pos), (mode: rounding_mode)):
      [real, exception] =
    CASES mode OF
      to_nearest:
          IF abs(r)
                >= b ^ (E_max + 1)
                     - (1 / 2) * b ^ (E_max + 1 - p)
            THEN (trap_over(r, (sgn(r) * infinity), mode),overflow)
          ELSE (sgn(r) * max_pos, inexact)
          ENDIF,
      to_zero:
          IF abs(r) >= b ^ (E_max + 1)
            THEN (trap_over(r, (sgn(r) * max_pos), mode),overflow)
          ELSE (sgn(r) * max_pos, inexact)
          ENDIF,
      to_pos:
          IF r > max_pos THEN (trap_over(r, infinity, mode),overflow)
          ELSIF r <= -b ^ (E_max + 1)
            THEN (trap_over(r, max_neg, mode),overflow)
          ELSE (max_neg, inexact)
          ENDIF,
      to_neg:
          IF r < max_neg THEN (trap_over(r, -infinity, mode),overflow)
          ELSIF r >= b ^ (E_max + 1)
            THEN (trap_over(r, max_pos, mode),overflow)
          ELSE (max_pos, inexact)
          ENDIF
      ENDCASES

  tiny_flag: bool % = true for tininess detected after rounding
  inaccurate_flag: bool % = true for inaccurate detected using first option

  exact_underflow((r:nzreal|abs(r)<b^E_min),mode:rounding_mode):bool =
       (r*b^alpha=round_scaled(r*b^alpha,mode))
  
  %implicitly already have tininess detected before rounding
  tiny?((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): bool =
    IF tiny_flag THEN abs(round_scaled(r, mode)) < b ^ E_min ELSE TRUE ENDIF

  round_under((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): real
    = b^(E_min - (p - 1))*round(b^(-(E_min - (p - 1)))*r,mode)

  mode: var rounding_mode
 
  round_under_correct: LEMMA
        round_under(min_pos,mode) = min_pos

  fin: var (finite?)

  round_under_value: lemma subnormal?(fin) =>
                 round_under(value(fin),mode) = value(fin)

  r:var nzreal

  round_under_error: LEMMA
        abs(r) < b ^ E_min
          => abs(r - round_under(r, mode)) < b ^ (E_min - (p - 1))

  round_under_near: LEMMA
        abs(r) < b ^ E_min
          => abs(r - round_under(r, to_nearest)) <= b ^ (E_min - (p - 1)) / 2

  round_under_pos: lemma abs(r)<b^E_min => round_under(r,to_pos)>=r

  round_under_neg: lemma abs(r)<b^E_min => round_under(r,to_neg)<=r

  round_under_zero: lemma abs(r)<b^E_min => abs(round_under(r,to_zero))<=abs(r)

  inaccurate?((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): bool =
    IF inaccurate_flag THEN (round_scaled(r,mode)/=round_under(r,mode))
    ELSE (r/=round_under(r,mode))
    ENDIF

  underflow((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)):
      [real, exception] =
    IF tiny?(r, mode)
      THEN IF trap_enabled?(underflow(FALSE))
        THEN (round_scaled(r * b ^ alpha, mode),
              underflow(exact_underflow(r, mode)))
      ELSIF inaccurate?(r, mode) THEN (round_under(r, mode), underflow(TRUE))
      ELSE (round_under(r, mode),
            IF r = round_under(r, mode) THEN no_exceptions
            ELSE inexact
            ENDIF)
      ENDIF
    ELSE (round_under(r, mode), inexact)
    ENDIF
  
  END over_under

$$$over_under.prf
(|over_under| (|over_under?_TCC1| "" (TCC :DEFS !) NIL)
 (|infinity_TCC1| "" (TCC :DEFS !) NIL)
 (|trap_over_TCC1| "" (TCC :DEFS !) NIL)
 (|trap_over_TCC2| "" (SKOSIMP*)
  (("" (REWRITE "zero_times3")
    (("" (LEMMA "expt_nonzero") (("" (INST?) (("" (ASSERT) NIL)))))))))
 (|overflow_TCC1| "" (TCC :DEFS !) NIL) (|overflow_TCC2| "" (TCC :DEFS !) NIL)
 (|overflow_TCC3| "" (TCC) NIL) (|overflow_TCC4| "" (TCC :DEFS !) NIL)
 (|overflow_TCC5| "" (TCC :DEFS !) NIL)
 (|exact_underflow_TCC1| "" (TCC :DEFS !) NIL)
 (|exact_underflow_TCC2| "" (SKOLEM-TYPEPRED)
  (("1" (HIDE -2)
    (("1" (USE "expt_nonzero")
      (("1" (ASSERT) (("1" (PROP) (("1" (REWRITE "zero_times3") NIL)))))
       ("2" (ASSERT) NIL)))))
   ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))
 (|tiny?_TCC1| "" (SUBTYPE-TCC) NIL) (|round_under_TCC1| "" (TCC :DEFS !) NIL)
 (|round_under_TCC2| "" (TCC :DEFS !) NIL)
 (|round_under_correct_TCC1| "" (ASSERT)
  (("" (EXPAND "min_pos")
    (("" (LEMMA "min_fp_correct")
      (("" (REPLACE -1)
        (("" (HIDE -1)
          (("" (LEMMA "expt_pos")
            (("" (INST?)
              (("" (ASSERT)
                (("" (EXPAND "abs")
                  (("" (LEMMA "expt_plus")
                    (("" (INST - "E_min" "1-p" "b")
                      (("" (REPLACE -1)
                        (("" (HIDE -1)
                          (("" (LEMMA "both_sides_times_pos_lt2")
                            (("" (INST - "b^E_min" "b^(1-p)" "1")
                              (("1" (LEMMA "expt_gt1_neg")
                                (("1" (INST - "b" "p-1")
                                  (("1" (GROUND) NIL)))))
                               ("2" (LEMMA "expt_pos")
                                (("2" (INST?)
                                  (("2" (ASSERT)
                                    NIL)))))))))))))))))))))))))))))))))))
 (|round_under_correct| "" (SKOSIMP*)
  (("" (EXPAND "round_under")
    (("" (REWRITE "round_int")
      (("1" (LEMMA "expt_plus")
        (("1" (INST - "(1 + E_min - p)" "(-(1 + E_min - p))" "b")
          (("1" (REWRITE "expt_x0")
            (("1" (REWRITE "associative_mult") (("1" (ASSERT) NIL)))))))))
       ("2" (HIDE 2)
        (("2" (EXPAND "min_pos")
          (("2" (LEMMA "min_fp_correct")
            (("2" (REPLACE -1)
              (("2" (HIDE -1)
                (("2" (REWRITE "expt_plus" :DIR RL)
                  (("2" (REWRITE "expt_x0")
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|round_under_value_TCC1| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (EXPAND "subnormal?") (("1" (EXPAND "zero?") (("1" (GROUND) NIL)))))
     ("2" (LEMMA "value_subnormal") (("2" (INST?) (("2" (ASSERT) NIL)))))))))
 (|round_under_value| "" (SKOSIMP*)
  (("" (EXPAND "round_under")
    (("" (REWRITE "round_int")
      (("1" (LEMMA "expt_plus")
        (("1" (INST - "(1 + E_min - p)" "(-(1 + E_min - p))" "b")
          (("1" (REWRITE "expt_x0")
            (("1" (GROUND)
              (("1" (REWRITE "associative_mult")
                (("1" (ASSERT)
                  (("1" (REWRITE "associative_mult" :DIR RL)
                    (("1" (ASSERT) NIL)))))))))))))))
       ("2" (HIDE 2)
        (("2"
          (CASE "integer?(b ^ (-(1 + E_min - p))
                       * value(fin!1))")
          (("1" (EXPAND "integer?") (("1" (PROPAX) NIL)))
           ("2" (HIDE 2)
            (("2" (EXPAND "subnormal?")
              (("2" (REWRITE "normal_value")
                (("2" (EXPAND "value")
                  (("2" (PROP)
                    (("2" (REPLACE -1)
                      (("2" (ASSERT)
                        (("2"
                          (CASE-REPLACE "b ^ (-(1 + E_min - p))
                     *
                     (Sum(p, value_digit(d(normalize(fin!1))))
                        * (-1) ^ sign(normalize(fin!1))
                        * b ^ E_min) =
 (-1)^sign(normalize(fin!1)) *(Sum(p,scale_value_p(d(normalize(fin!1)))))")
                          (("1" (HIDE -1)
                            (("1" (ASSERT)
                              (("1"
                                (CASE-REPLACE
                                 "scale_value_p(d(normalize(fin!1))) = scale_value(d(normalize(fin!1)),p-1)")
                                (("1" (HIDE -1)
                                  (("1" (LEMMA "scaled_Sum_int")
                                    (("1" (INST?)
                                      (("1"
                                        (CASE
                                         "FORALL (i,j:int): integer?(i*j)")
                                        (("1"
                                          (INST?)
                                          (("1"
                                            (EXPAND "integer?")
                                            (("1" (PROPAX) NIL)))))
                                         ("2"
                                          (HIDE -1 -2 -3 2 3)
                                          (("2"
                                            (EXPAND "integer?")
                                            (("2" (PROPAX) NIL)))))))))))))
                                 ("2" (HIDE -1 -2 2 3)
                                  (("2" (APPLY-EXTENSIONALITY)
                                    (("1" (EXPAND "scale_value_p")
                                      (("1" (PROPAX) NIL)))
                                     ("2" (EXPAND "scale_value")
                                      (("2"
                                        (EXPAND "value_digit")
                                        (("2"
                                          (HIDE 2)
                                          (("2"
                                            (SKOSIMP*)
                                            (("2"
                                              (LIFT-IF)
                                              (("2"
                                                (ASSERT)
                                                (("2"
                                                  (REWRITE
                                                   "associative_mult"
                                                   :DIR
                                                   RL)
                                                  (("2"
                                                    (REWRITE
                                                     "expt_plus"
                                                     :DIR
                                                     RL)
                                                    (("2"
                                                      (GROUND)
                                                      (("1"
                                                        (REWRITE
                                                         "closed_times")
                                                        (("1"
                                                          (REWRITE
                                                           "closed_times")
                                                          (("1"
                                                            (CASE
                                                             "forall (n:nat): integer_pred(b^n)")
                                                            (("1" (INST?) NIL)
                                                             ("2"
                                                              (SKOSIMP*)
                                                              (("2"
                                                                (ASSERT)
                                                                NIL)))))))))
                                                       ("2"
                                                        (REWRITE
                                                         "pos_times_ge")
                                                        (("2"
                                                          (LEMMA "expt_pos")
                                                          (("2"
                                                            (INST?)
                                                            (("2"
                                                              (ASSERT)
                                                              NIL)))))))))))))))))))))))))))))))))))
                           ("2" (HIDE -1 -2 2 3)
                            (("2" (ASSERT)
                              (("2" (LEMMA "scaled_Sum")
                                (("2" (INST?)
                                  (("2" (REPLACE -1 :DIR RL)
                                    (("2" (HIDE -1)
                                      (("2"
                                        (LEMMA "expt_plus")
                                        (("2"
                                          (INST
                                           -
                                           "E_min"
                                           "(-(1 + E_min - p))"
                                           "b")
                                          (("2"
                                            (REPLACE -1)
                                            (("2"
                                              (ASSERT)
                                              NIL)))))))))))))))))))))))))))))))))))))))))))))
 (|round_under_error_TCC1| "" (TCC :DEFS !) NIL)
 (|round_under_error_TCC2| "" (SUBTYPE-TCC) NIL)
 (|round_under_error| "" (SKOSIMP*)
  (("" (EXPAND "round_under")
    ((""
      (CASE-REPLACE "abs(r!1
            - b ^ (1 + E_min - p)
                * round(b ^ (-(1 + E_min - p)) * r!1, mode!1)) =
abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, mode!1))")
      (("1" (HIDE -1 -2)
        (("1" (REWRITE "abs")
          (("1" (LEMMA "expt_pos")
            (("1" (INST?)
              (("1" (ASSERT)
                (("1" (LEMMA "both_sides_times_pos_lt2")
                  (("1" (INST - "b^(1+E_min-p)" "_" "1")
                    (("1" (INST?)
                      (("1" (LEMMA "round1")
                        (("1" (INST?) (("1" (ASSERT) NIL)))))))))))))))))))))
       ("2" (HIDE -1 2)
        (("2" (REWRITE "abs_mult" :DIR RL)
          (("2" (REWRITE "expt_plus" :DIR RL)
            (("2" (REWRITE "expt_x0") (("2" (ASSERT) NIL)))))))))
       ("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))))))
 (|round_under_near| "" (SKOSIMP*)
  (("" (EXPAND "round_under")
    (("" (HIDE -1)
      ((""
        (CASE-REPLACE "abs(r!1
            - b ^ (1 + E_min - p)
                * round(b ^ (-(1 + E_min - p)) * r!1, to_nearest)) =
abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, to_nearest))")
        (("1" (HIDE -1)
          (("1" (EXPAND "abs" + 1)
            (("1" (LEMMA "expt_pos")
              (("1" (INST?)
                (("1" (ASSERT)
                  (("1" (LEMMA "both_sides_times_pos_lt2")
                    (("1" (INST - "b^(1+E_min-p)" "_" "1/2")
                      (("1" (EXPAND "round")
                        (("1" (INST?)
                          (("1" (REWRITE "times_div1")
                            (("1" (LEMMA "round_to_even1")
                              (("1" (INST?)
                                (("1" (ASSERT) NIL)))))))))))))))))
                 ("2" (ASSERT)
                  (("2" (SPLIT)
                    (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))
         ("2" (HIDE 2)
          (("2" (REWRITE "abs_mult" :DIR RL)
            (("2" (REWRITE "expt_plus" :DIR RL)
              (("2" (REWRITE "expt_x0") (("2" (ASSERT) NIL)))))))))
         ("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))))))))
 (|round_under_pos| "" (SKOSIMP*)
  (("" (EXPAND "round_under")
    (("" (HIDE -1)
      (("" (EXPAND "round")
        (("" (LEMMA "both_sides_times_pos_ge2")
          (("" (LEMMA "expt_pos")
            (("" (INST - "(-(1 + E_min - p))" "b")
              (("1"
                (INST - "b ^ (-(1 + E_min - p))"
                 "b ^ (1 + E_min - p) * ceiling(b ^ (-(1 + E_min - p)) * r!1)"
                 "r!1")
                (("1" (REPLACE -2 :DIR RL)
                  (("1" (HIDE -2)
                    (("1" (REWRITE "associative_mult")
                      (("1" (REWRITE "associative_mult" :DIR RL)
                        (("1" (REWRITE "expt_plus" :DIR RL)
                          (("1" (REWRITE "expt_x0")
                            (("1" (ASSERT) NIL)))))))))))))
                 ("2" (ASSERT) NIL) ("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))
               ("2" (ASSERT) NIL)))))))))))))))
 (|round_under_neg| "" (SKOSIMP*)
  (("" (HIDE -1)
    (("" (EXPAND "round_under")
      (("" (EXPAND "round")
        (("" (LEMMA "both_sides_times_pos_le2")
          ((""
            (INST - "b ^ (-(1 + E_min - p))"
             "b ^ (1 + E_min - p) * floor(b ^ (-(1 + E_min - p)) * r!1)"
             "r!1")
            (("1" (REPLACE -1 :DIR RL)
              (("1" (HIDE -1)
                (("1" (REWRITE "associative_mult")
                  (("1" (REWRITE "associative_mult" :DIR RL)
                    (("1" (REWRITE "expt_plus" :DIR RL)
                      (("1" (REWRITE "expt_x0")
                        (("1" (ASSERT) NIL)))))))))))))
             ("2" (ASSERT) NIL)
             ("3" (LEMMA "expt_pos")
              (("3" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))
             ("4" (ASSERT) NIL)))))))))))))
 (|round_under_zero| "" (SKOSIMP*)
  (("" (EXPAND "round_under")
    (("" (REWRITE "abs_mult")
      (("" (EXPAND "round")
        (("" (CASE "forall (r1,r2:real): abs(sgn(r1)*r2) = abs(r2)")
          (("1" (INST?)
            (("1" (REPLACE -1)
              (("1" (HIDE -1)
                (("1"
                  (CASE "forall (r:real): abs(floor(abs(r)))=floor(abs(r))")
                  (("1" (INST?)
                    (("1" (REPLACE -1)
                      (("1" (HIDE -1)
                        (("1" (LEMMA "both_sides_times_pos_le2")
                          (("1"
                            (INST - "abs(b ^ (-(1 + E_min - p)))"
                             "abs(b ^ (1 + E_min - p)) * floor(abs(b ^ (-(1 + E_min - p)) * r!1))"
                             "abs(r!1)")
                            (("1" (REPLACE -1 :DIR RL)
                              (("1" (HIDE -1)
                                (("1" (HIDE -1)
                                  (("1" (REWRITE "abs_mult" :DIR RL)
                                    (("1" (REWRITE "associative_mult")
                                      (("1"
                                        (REWRITE "associative_mult" :DIR RL)
                                        (("1"
                                          (REWRITE "abs_mult" :DIR RL)
                                          (("1"
                                            (REWRITE "expt_plus" :DIR RL)
                                            (("1"
                                              (REWRITE "expt_x0")
                                              (("1"
                                                (EXPAND "abs" + 2)
                                                (("1"
                                                  (ASSERT)
                                                  NIL)))))))))))))))))))))
                             ("2" (HIDE -1 2)
                              (("2" (LEMMA "expt_pos")
                                (("2" (INST?)
                                  (("2" (EXPAND "abs")
                                    (("2" (ASSERT) NIL)))))))))))))))))))
                   ("2" (HIDE -1 2) (("2" (GRIND) NIL)))))))))))
           ("2" (HIDE -1 2) (("2" (TCC) NIL)))))))))))))
 (|underflow_TCC1| "" (TCC :DEFS !) NIL)
 (|underflow_TCC2| "" (SKOSIMP*)
  (("" (REWRITE "zero_times3")
    (("" (LEMMA "expt_pos") (("" (INST?) (("" (ASSERT) NIL))))))))))
$$$fp_round_aux.pvs
fp_round_aux[b,p:above(1)]: THEORY

  BEGIN
  
  importing round,
            enumerated_type_defs

  r: var real
  x: var posreal

  sign_of(r:real): sign_rep = IF r < 0 THEN neg ELSE pos ENDIF

  Exp_of(x:posreal): {i:int| b^i<= x & x < b^(i+1)}

  Exp_of_correct: lemma 
      1 <= x*b^(-Exp_of(x)) & x*b^(-Exp_of(x)) < b

  norm_fp_range: type = {x:posreal | 1 <= x & x < b}

  n1: var norm_fp_range

  z: var nzreal

  E(z):integer = Exp_of(abs(z))

  significand(z):norm_fp_range = abs(z)*b^(-Exp_of(abs(z)))

  real_components: lemma
    z = sgn(z)* b^E(z) * significand(z)    

  abs_real_components: LEMMA
    abs(z) = b^E(z)*significand(z)

  i,j: var integer

  Exp_of_unique: LEMMA
    b^i <= x & x < b^(i+1) & b^j<=x & x<b^(j+1) => i=j

  posreal_exponent: lemma
    x = b^i *n1 => E(x) = i

  real_exponent: lemma
    z = sgn(z)*b^i * n1 => E(z) = i

  scale(x:posreal):{i:int|b^(i+p-1)<=x & x < b^(i+p)} = Exp_of(x)-(p-1)

  scale_correct: lemma b^(p-1)<=x/b^scale(x) & x/b^scale(x)< b^p

  round_scaled(r:nzreal,mode:rounding_mode): real =
    b^(scale(abs(r)))*round( b^(-scale(abs(r)))*r,mode)

  E1: var integer
  px: var posreal
  nnx: var nonneg_real 

  truncate(E1,nnx): [below(p)->below(b)] = 
      (lambda (i:below(p)): mod(floor(b^(i-E1)*nnx),b))

  truncate_shift: LEMMA
    truncate(i,b^j*px) = truncate(i-j,px)

  Exp_of_shift: LEMMA
    Exp_of(b^j*px) = j + Exp_of(px)

  scale_shift: LEMMA
    scale(b^j*px) = j + scale(px)

  END fp_round_aux

$$$fp_round_aux.prf
(|fp_round_aux| (|Exp_of_TCC1| "" (TCC :DEFS !) NIL)
 (|Exp_of_TCC2| "" (TCC :DEFS !) NIL)
 (|Exp_of_TCC3| ""
  (INST + "lambda (px:posreal): choose({i:int|b^i<=px & px<b^(i+1)})")
  (("1" (SKOSIMP*)
    (("1" (REWRITE "nonempty_member")
      (("1" (EXPAND "member")
        (("1" (LEMMA "exp_of_exists")
          (("1" (INST - "b" "px!1") (("1" (ASSERT) NIL)))))))
       ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
       ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))
   ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
   ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
 (|Exp_of_correct_TCC1| "" (TCC :DEFS !) NIL)
 (|Exp_of_correct| "" (SKOSIMP*)
  (("" (TYPEPRED "Exp_of(x!1)")
    (("1" (REWRITE "expt_inverse")
      (("1" (ASSERT)
        (("1" (LEMMA "expt_pos")
          (("1" (INST?)
            (("1" (REWRITE "times_div1")
              (("1" (GROUND)
                (("1" (REWRITE "div_mult_pos_le2") NIL)
                 ("2" (REWRITE "div_mult_pos_lt1")
                  (("2" (REWRITE "expt_plus")
                    (("2" (REWRITE "expt_x1") NIL)))))))))))))))))
     ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
     ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))
 (|significand_TCC1| "" (SUBTYPE-TCC) NIL)
 (|significand_TCC2| "" (SKOSIMP*)
  (("" (ASSERT)
    (("" (USE "pos_times_gt")
      (("" (USE "expt_pos")
        (("" (ASSERT)
          (("" (ASSERT) (("" (REWRITE "Exp_of_correct") NIL)))))))))))))
 (|real_components_TCC1| "" (SUBTYPE-TCC) NIL)
 (|real_components| "" (SKOSIMP*)
  (("" (EXPAND "significand")
    (("" (EXPAND "E")
      (("" (REWRITE "associative_mult" :DIR RL)
        (("" (REWRITE "associative_mult" :DIR RL)
          (("" (REWRITE "associative_mult" :DIR RL)
            (("" (REWRITE "expt_plus" :DIR RL)
              (("" (REWRITE "expt_x0") (("" (GRIND) NIL)))))))))))))))))
 (|abs_real_components| "" (SKOSIMP*)
  (("" (USE "real_components")
    (("" (EXPAND "abs")
      (("" (EXPAND "sgn")
        (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) NIL)))))))))))))
 (|Exp_of_unique_TCC1| "" (SUBTYPE-TCC) NIL)
 (|Exp_of_unique_TCC2| "" (SUBTYPE-TCC) NIL)
 (|Exp_of_unique| "" (SKOSIMP*)
  (("" (CASE "b^i!1 < b^(1+j!1) & b^j!1 < b^(1+i!1)")
    (("1" (HIDE -2 -3 -4 -5)
      (("1" (FLATTEN)
        (("1" (REWRITE "both_sides_expt_gt1_lt")
          (("1" (REWRITE "both_sides_expt_gt1_lt") (("1" (ASSERT) NIL)))))))))
     ("2" (ASSERT) NIL) ("3" (ASSERT) NIL) ("4" (ASSERT) NIL)
     ("5" (ASSERT) NIL) ("6" (ASSERT) NIL)))))
 (|posreal_exponent| "" (SKOSIMP*)
  (("" (EXPAND "E")
    (("" (EXPAND "abs")
      (("" (LEMMA "Exp_of_unique")
        (("" (INST - "Exp_of(x!1)" "i!1" "x!1")
          (("" (ASSERT)
            (("" (HIDE 2)
              (("" (REPLACE -1)
                (("" (HIDE -1)
                  (("" (SPLIT)
                    (("1" (REWRITE "commutative_mult")
                      (("1" (REWRITE "div_mult_pos_le1" :DIR RL) NIL)))
                     ("2" (REWRITE "commutative_mult")
                      (("2" (REWRITE "div_mult_pos_lt2" :DIR RL)
                        (("1" (REWRITE "expt_div")
                          (("1" (REWRITE "expt_x1") (("1" (ASSERT) NIL)))))
                         ("2" (USE "expt_pos")
                          (("2" (ASSERT) NIL)))))))))))))))))))))))))))
 (|real_exponent| "" (SKOSIMP*)
  (("" (LEMMA "posreal_exponent")
    (("" (INST - "i!1" "n1!1" "abs(z!1)")
      (("" (EXPAND "E")
        (("" (EXPAND "sgn")
          (("" (EXPAND "abs")
            (("" (LIFT-IF)
              (("" (LIFT-IF)
                (("" (ASSERT) (("" (GROUND) NIL)))))))))))))))))))
 (|scale_TCC1| "" (TCC :DEFS !) NIL) (|scale_TCC2| "" (TCC :DEFS !) NIL)
 (|scale_TCC3| "" (SKOSIMP*)
  (("" (ASSERT) (("" (TYPEPRED "Exp_of(x!1)") (("" (ASSERT) NIL)))))))
 (|scale_correct_TCC1| "" (TCC :DEFS !) NIL)
 (|scale_correct_TCC2| "" (TCC :DEFS !) NIL)
 (|scale_correct_TCC3| "" (SKOLEM!) (("" (REWRITE "expt_nonzero") NIL)))
 (|scale_correct_TCC4| "" (SUBTYPE-TCC) NIL)
 (|scale_correct| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (REWRITE "div_mult_pos_le2")
      (("1" (EXPAND "scale")
        (("1" (LEMMA "expt_plus")
          (("1" (INST - "p-1" "1+Exp_of(x!1)-p" "b") (("1" (ASSERT) NIL)))))))
       ("2" (LEMMA "expt_pos") (("2" (INST?) (("2" (ASSERT) NIL)))))))
     ("2" (REWRITE "div_mult_pos_lt1")
      (("1" (REWRITE "expt_plus" :DIR RL)
        (("1" (EXPAND "scale") (("1" (ASSERT) NIL)))))
       ("2" (LEMMA "expt_pos") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
 (|round_scaled_TCC1| "" (TCC :DEFS !) NIL)
 (|round_scaled_TCC2| "" (TCC :DEFS !) NIL)
 (|truncate_TCC1| "" (SUBTYPE-TCC) NIL) (|truncate_TCC2| "" (SUBTYPE-TCC) NIL)
 (|truncate_TCC3| "" (SKOSIMP*)
  (("" (REWRITE "mod_pos") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))
 (|truncate_TCC4| "" (SUBTYPE-TCC) NIL)
 (|truncate_TCC5| "" (SKOSIMP*)
  (("" (REWRITE "mod_pos") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))
 (|truncate_shift_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "pos_times_ge") (("" (USE "expt_pos") (("" (ASSERT) NIL)))))))
 (|truncate_shift| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY)
    (("1" (HIDE 2)
      (("1" (EXPAND "truncate")
        (("1" (REWRITE "associative_mult")
          (("1" (REWRITE "expt_plus" :DIR RL) NIL)))))))
     ("2" (HIDE 2)
      (("2" (USE "expt_pos")
        (("2" (REWRITE "pos_times_ge") (("2" (ASSERT) NIL)))))))))))
 (|Exp_of_shift_TCC1| "" (SKOSIMP*)
  (("" (USE "expt_pos")
    (("1" (USE "pos_times_gt")
      (("1" (ASSERT) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL)))
     ("2" (ASSERT) (("2" (ASSERT) NIL)))))))
 (|Exp_of_shift| "" (SKOSIMP*)
  (("" (LEMMA "Exp_of_unique")
    (("" (USE "expt_pos")
      (("1" (INST?)
        (("1" (INST - "b^j!1*px!1")
          (("1" (ASSERT)
            (("1" (HIDE 2)
              (("1" (REWRITE "commutative_mult")
                (("1" (REWRITE "div_mult_pos_le1" :DIR RL)
                  (("1" (REWRITE "div_mult_pos_lt2" :DIR RL)
                    (("1" (REWRITE "expt_div")
                      (("1" (REWRITE "expt_div")
                        (("1" (ASSERT) NIL)))))))))))))))
           ("2" (USE "pos_times_gt")
            (("1" (ASSERT) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL)))
           ("3" (ASSERT) NIL)))
         ("2" (USE "pos_times_gt")
          (("1" (ASSERT) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL)))
         ("3" (ASSERT) NIL)))
       ("2" (ASSERT) NIL)))))))
 (|scale_shift| "" (SKOSIMP*)
  (("" (EXPAND "scale") (("" (REWRITE "Exp_of_shift") NIL))))))
$$$round.pvs
round: THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Defines type:
%   rounding_mode: type = {to_nearest,to_zero,to_pos,to_neg}
%
% Defines functions:
%
%   round: [[real,rounding_mode] -> integer]
%
%   Rounds a real number to the nearest integer in accordance 
%   with the rounding mode (as specified in IEEE-854).
%   The function round can be used in two parts of the IEEE-854
%   floating point standard.
%    1.)  Round floating point to integral value (section 5.5)
%         or for converting a floating point to integer (5.4).
%    2.)  By giving function `round' an appropriately scaled 
%         argument, this function can be used in the process 
%         of converting a real number to a floating point 
%         representation.
%
%   round_to_even:[real -> integer]
%
%   Auxilliary function used in definition of round.  Selects the 
%   integer nearest in value to the real argument.      
%   If the real number is exactly halfway between two integers,
%   this function selects the nearest even integer.
%   Can also be used:
%    --   As an auxilliary function in the definition of
%         the remainder function (section 5.1).  For y/=0,
%         x REM y =def= x - y*n, where n = round_to_even(x/y).
%
%
% Author:
%  Paul S. Miner                | email: p.s.miner@larc.nasa.gov
%  1 South Wright St. / MS 130  |   fax: (804) 864-4234
%  NASA Langley Research Center | phone: (804) 864-6201
%  Hampton, Virginia 23681      |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
%  Requires library `floor'

  BEGIN 

  importing enumerated_type_defs

%  rounding_mode:type = {to_nearest,to_zero,to_pos,to_neg}
  mode: var rounding_mode

  r: VAR real
  
  round_to_even(r): integer =
    IF r - floor(r) < ceiling(r) - r THEN floor(r)
    ELSIF ceiling(r) - r < r - floor(r) THEN ceiling(r)
    ELSIF floor(r) = ceiling(r) THEN floor(r)
    ELSE 2 * floor(ceiling(r) / 2)
    ENDIF
  
  round_to_even0: lemma round_to_even(0)=0

  round_to_even1: LEMMA abs(r - round_to_even(r)) <= 1 / 2
  
  round_to_even2: LEMMA
        abs(r - round_to_even(r)) = 1 / 2 => integer?(round_to_even(r) / 2)
  
  round(r,mode): integer =
    CASES mode of
      to_nearest: round_to_even(r),
      to_zero:    sgn(r) * floor(abs(r)),
      to_pos:     ceiling(r),
      to_neg:     floor(r)
    ENDCASES
    
  round1: LEMMA abs(r-round(r,mode))<1 

  i:var int

  round_int: LEMMA  round(i,mode)=i

  END round

$$$round.prf
(|round| (|round_to_even0| "" (GRIND) NIL)
 (|round_to_even1| "" (SKOSIMP*)
  (("" (EXPAND "abs")
    (("" (LIFT-IF)
      (("" (PROP)
        (("1" (EXPAND "round_to_even")
          (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
         ("2" (EXPAND "round_to_even")
          (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))
 (|round_to_even2| "" (SKOSIMP*)
  (("" (EXPAND "abs")
    (("" (LIFT-IF)
      (("" (PROP)
        (("1" (EXPAND "round_to_even")
          (("1" (LIFT-IF)
            (("1" (GROUND)
              (("1" (EXPAND "integer?") (("1" (PROPAX) NIL)))))))))
         ("2" (EXPAND "round_to_even")
          (("2" (LIFT-IF)
            (("2" (GROUND)
              (("2" (EXPAND "integer?")
                (("2" (PROPAX) NIL)))))))))))))))))
 (|round1| "" (SKOSIMP*)
  (("" (EXPAND "round")
    (("" (LIFT-IF)
      (("" (PROP)
        (("1" (LEMMA "round_to_even1")
          (("1" (INST?) (("1" (ASSERT) NIL)))))
         ("2" (GRIND) NIL) ("3" (GRIND) NIL)
         ("4" (GRIND) NIL)))))))))
 (|round_int| "" (SKOSIMP*)
  (("" (EXPAND "round")
    (("" (LIFT-IF)
      (("" (GROUND)
        (("1" (EXPAND "round_to_even")
          (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
         ("2" (EXPAND "abs")
          (("2" (LIFT-IF)
            (("2" (EXPAND "sgn") (("2" (GROUND) NIL))))))))))))))))
$$$IEEE_854_fp_int.pvs
IEEE_854_fp_int
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  importing IEEE_854_values[b,p,E_max,E_min],
            real_to_fp[b,p,alpha,E_max,E_min],
            round

  fin, fin1: var (finite?)

  mode: var rounding_mode

  fp_to_int(fin,mode):integer = round(value(fin),mode)

  fp_to_int_fp(fin,mode): fp_num = 
       real_to_fp(round(value(fin),mode))

%  large_value: lemma  
%      abs(value(fin)) >= b^p => integer?(value(fin))
%
%  fp_to_int_fp_finite: lemma
%       E_max>p => finite?(real_to_fp(round(value(fin),mode)))

  END IEEE_854_fp_int

$$$IEEE_854_fp_int.prf
(|IEEE_854_fp_int| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL))
$$$arithmetic_ops.pvs
arithmetic_ops
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min],
            real_to_fp[b,p,alpha,E_max,E_min],
            enumerated_type_defs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% fp_op provides a template for defining a floating point operation
%  for the case when both arguments are finites.    

  fin,fin1,fin2: var (finite?)
  op: var fp_ops
  mode: var rounding_mode

  apply(op,fin1,(fin2:{fin| div?(op) => not zero?(fin)})): real =
    cases op of
      add:  value(fin1) + value(fin2),
      sub:  value(fin1) - value(fin2),
      mult: value(fin1) * value(fin2),
      div:  value(fin1) / value(fin2)
    endcases

  signed_zero(op, fin1, fin2, mode): {fin | zero?(fin)} =
    CASES op OF
      add:
          IF zero?(fin1)
                & zero?(fin2) & sign(fin1) = sign(fin2) THEN fin1
          ELSIF to_neg?(mode) THEN neg_zero
          ELSE pos_zero
          ENDIF,
      sub:
          IF zero?(fin1)
                & zero?(fin2) & sign(fin1) /= sign(fin2) THEN fin1
          ELSIF to_neg?(mode) THEN neg_zero
          ELSE pos_zero
          ENDIF,
      mult:
          IF sign(fin1) = sign(fin2) THEN pos_zero
          ELSE neg_zero
          ENDIF,
      div:
          IF sign(fin1) = sign(fin2) THEN pos_zero
          ELSE neg_zero
          ENDIF
      ENDCASES  

  fp_op(op, fin1, (fin2: {fin | div?(op) => NOT zero?(fin)}), mode): fp_num =
    LET r = fp_round(apply(op, fin1, fin2), mode)
      IN IF r = 0 THEN signed_zero(op, fin1, fin2, mode)
        ELSE real_to_fp(r)
        ENDIF

  fp_op_x(op,fin1,(fin2:{fin| div?(op) => not zero?(fin)}),mode): 
    [fp_num, exception]
           = 
    LET rp = fp_round_x(apply(op, fin1, fin2), mode)
      IN IF proj_1(rp) = 0 THEN (signed_zero(op, fin1, fin2, mode),proj_2(rp))
        ELSE real_to_fp_x(rp)
        ENDIF

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  END arithmetic_ops

$$$arithmetic_ops.prf
(|arithmetic_ops| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
 (|apply_TCC1| "" (SKOLEM-TYPEPRED) (("" (TCC) NIL)))
 (|signed_zero_TCC1| "" (SKOSIMP*) NIL)
 (|signed_zero_TCC2| "" (SKOSIMP*) NIL))
$$$comparison1.pvs
comparison1 
  [b,p:above(1),
   E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min]

  num,num1,num2: var {fp:fp_num| finite?(fp) or infinite?(fp)}

% extend value function so that infinities can be compared to finite
% numbers
  n_value(num): real =
    IF infinite?(num) THEN (-1) ^ i_sign(num) * b ^ (E_max + 1)
    ELSE value(num)
    ENDIF
  

% From section 5.7 of IEEE-854:
%   ``Four mutually exclusive relations are possible: "less than,"
%  "equal," "greater than," and "unordered."  The last case arises only
%  when at least one operand is a NaN.'' ...

%  ``The result of a comparison shall be delivered in one of two ways at
%  the implementor's option: either as a condition code identifying one
%  of the four relations listed above, or as a true/false response to a
%  predicate that names the specific comparison desired.''

% fp_compare, below, defines the first option:

  comparison_code: type = {gt, lt, eq, un}

  fp_compare((fp1, fp2: fp_num)): comparison_code =
    IF NaN?(fp1) OR NaN?(fp2) THEN un
    ELSIF n_value(fp1) > n_value(fp2) THEN gt
    ELSIF n_value(fp1) < n_value(fp2) THEN lt
    ELSE eq
    ENDIF

  fp,fp1,fp2: var fp_num

  posinf_ge: LEMMA
        gt?(fp_compare(infinite(pos), num))
          OR eq?(fp_compare(infinite(pos), num))

  NaN_unordered: LEMMA 
      NaN?(fp1) OR NaN?(fp2) => un?(fp_compare(fp1, fp2))

% option 2, minimal set of predicates is {eq, ne, gt, ge, lt, le} also
% should include un.  These predicates are defined below the level
% where invalid will be signalled.

% The follwing predicates are from table 3, page 12 of IEEE-854.  They
% do not include the signalling of the invalid exception.  That test
% may be applied prior to invoking these predicates.

% shall include
  eq?(fp1,fp2) :bool = eq?(fp_compare(fp1,fp2))
  ne?(fp1,fp2) :bool = not eq?(fp_compare(fp1,fp2))
  gt?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2))
  ge?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2)) or eq?(fp_compare(fp1,fp2))
  lt?(fp1,fp2) :bool = lt?(fp_compare(fp1,fp2))
  le?(fp1,fp2) :bool = lt?(fp_compare(fp1,fp2)) or eq?(fp_compare(fp1,fp2))

% should include
  un?(fp1,fp2) :bool = un?(fp_compare(fp1,fp2))

% other
  lg?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2)) or lt?(fp_compare(fp1,fp2))
  leg?(fp1,fp2):bool = not un?(fp_compare(fp1,fp2))
  ug?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2)) or un?(fp_compare(fp1,fp2))
  uge?(fp1,fp2):bool = not lt?(fp_compare(fp1,fp2))
  ul?(fp1,fp2) :bool = lt?(fp_compare(fp1,fp2)) or un?(fp_compare(fp1,fp2))
  ule?(fp1,fp2):bool = not gt?(fp_compare(fp1,fp2))
  ue?(fp1,fp2) :bool = eq?(fp_compare(fp1,fp2)) or un?(fp_compare(fp1,fp2))

  eq_def: lemma  eq?(num1,num2) <=> n_value(num1) = n_value(num2)

  ne_def: lemma  ne?(num1,num2) <=> n_value(num1) /= n_value(num2)

  gt_def: lemma  gt?(num1,num2) <=> n_value(num1) > n_value(num2)

  ge_def: lemma  ge?(num1,num2) <=> n_value(num1) >= n_value(num2)

  lt_def: lemma  lt?(num1,num2) <=> n_value(num1) < n_value(num2)

  le_def: lemma  le?(num1,num2) <=> n_value(num1) <= n_value(num2)

  un_def: lemma  un?(fp1,fp2)   <=> (NaN?(fp1) or NaN?(fp2))

  END comparison1

$$$comparison1.prf
(|comparison1| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
 (|n_value_TCC1| "" (TCC :DEFS !) NIL)
 (|n_value_TCC2| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|fp_compare_TCC1| "" (TCC :DEFS !) NIL)
 (|fp_compare_TCC2| "" (TCC :DEFS !) NIL)
 (|posinf_ge| "" (SKOLEM-TYPEPRED)
  (("" (PROP)
    (("1" (EXPAND "pos")
      (("1" (LEMMA "value_nonzero")
        (("1" (INST?)
          (("1" (HIDE 2)
            (("1" (EXPAND "fp_compare")
              (("1" (ASSERT)
                (("1" (GROUND)
                  (("1" (LIFT-IF)
                    (("1" (EXPAND "n_value")
                      (("1" (REWRITE "expt_x0")
                        (("1" (GROUND)
                          (("1" (CASE "max_pos < b^(1+E_max)")
                            (("1"
                              (EXPAND "abs")
                              (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
                             ("2"
                              (HIDE -1 -2 -3 2)
                              (("2"
                                (LEMMA "max_fp_correct")
                                (("2"
                                  (REPLACE -1)
                                  (("2"
                                    (ASSERT)
                                    (("2"
                                      (LEMMA "expt_pos")
                                      (("2"
                                        (INST-CP - "1+E_max" "b")
                                        (("2"
                                          (INST - "1+E_max-p" "b")
                                          (("2"
                                            (ASSERT)
                                            NIL)))))))))))))))))))))))))
                   ("2" (EXPAND "n_value")
                    (("2" (REWRITE "expt_x0")
                      (("2" (EXPAND "zero?")
                        (("2" (ASSERT)
                          (("2" (LEMMA "expt_pos")
                            (("2"
                              (INST?)
                              (("2"
                                (ASSERT)
                                NIL)))))))))))))))))))))))))))
     ("2" (EXPAND "pos")
      (("2" (EXPAND "fp_compare")
        (("2" (ASSERT)
          (("2" (LIFT-IF)
            (("2" (GROUND)
              (("2" (HIDE -1 1 2 3)
                (("2" (EXPAND "n_value")
                  (("2" (TYPEPRED "i_sign(num!1)")
                    (("2" (GROUND)
                      (("2" (REPLACE -1)
                        (("2" (REWRITE "expt_x0")
                          (("2" (REWRITE "expt_x1")
                            (("2"
                              (LEMMA "expt_pos")
                              (("2"
                                (INST?)
                                (("2"
                                  (REWRITE
                                   "both_sides_times_pos_gt1")
                                  NIL)))))))))))))))))))))))))))))))))
 (|NaN_unordered| "" (SKOSIMP*)
  (("" (EXPAND "fp_compare")
    (("" (ASSERT) (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|eq_def| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "eq?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|ne_def| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "ne?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|gt_def| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "gt?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|ge_def| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "ge?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|lt_def| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "lt?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|le_def| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "le?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|un_def| "" (SKOSIMP*)
  (("" (EXPAND "un?")
    (("" (EXPAND "fp_compare")
      (("" (LIFT-IF) (("" (GROUND) NIL))))))))))
$$$infinity_arithmetic.pvs
infinity_arithmetic
  [b,p:above(1),
   E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min],
            enumerated_type_defs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Special functions for handling arithmetic on infinities
%  These definitions return an undetermined NaN when the Invalid 
%   exception should be raised.
%
%  The definitions come from constraints enumerated in sections
%   6.1, 6.3, and 7.1 of IEEE-854
%

  fp: var fp_num

  num,num1,num2: var {fp| finite?(fp) or infinite?(fp)}

% Addition when at least one operand is an infinity
  fp_add_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num 
     =
    IF infinite?(num1) & infinite?(num2) THEN 
      IF (i_sign(num1) = i_sign(num2)) THEN num1
      ELSE invalid
      ENDIF
    ELSIF infinite?(num1) THEN num1
    ELSE num2
    ENDIF

% Addition when at least one operand is an infinity with exceptions

  fp_add_inf_x(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): 
    [fp_num, exception]
     =
    IF infinite?(num1) & infinite?(num2) THEN 
      IF (i_sign(num1) = i_sign(num2)) THEN (num1,no_exceptions)
      ELSE (invalid,invalid_operation)
      ENDIF
    ELSIF infinite?(num1) THEN (num1,no_exceptions)
    ELSE (num2,no_exceptions)
    ENDIF

% Similarly for subtraction

  fp_sub_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num 
     =
    IF infinite?(num1) & infinite?(num2) THEN 
      IF (i_sign(num1) /= i_sign(num2)) THEN num1
      ELSE invalid
      ENDIF
    ELSIF infinite?(num1) THEN num1
    ELSE toggle_sign(num2)
    ENDIF

% Similarly for subtraction with exceptions

  fp_sub_inf_x(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): 
   [fp_num , exception]
     =
    IF infinite?(num1) & infinite?(num2) THEN 
      IF (i_sign(num1) /= i_sign(num2)) THEN (num1, no_exceptions)
      ELSE (invalid, invalid_operation)
      ENDIF
    ELSIF infinite?(num1) THEN (num1, no_exceptions)
    ELSE (toggle_sign(num2), no_exceptions)
    ENDIF

% Alternate definition for fp_sub_inf
  fp_sub_inf_def: lemma
   forall num1,(num2:{num|infinite?(num1) OR infinite?(num)}):
    fp_sub_inf(num1,num2) = fp_add_inf(num1,toggle_sign(num2));

% xor function defined on sign_rep to determine correct sign for mult/div
  xor(s1,s2:sign_rep): sign_rep = if s1=s2 then 0 else 1 endif

% Determine correct sign for multiplication and division
%  this definition is complicated by a bug in the adt mechanism
%  PVS does not currently allow use of the same accessor for 
%  different constructors. 
  mult_sign(num1,num2):sign_rep =
    if infinite?(num1) then
       if infinite?(num2) then
          xor(i_sign(num1),i_sign(num2))
       else
          xor(i_sign(num1),sign(num2))
       endif
    elsif infinite?(num2) then
          xor(sign(num1),i_sign(num2))
    else
          xor(sign(num1),sign(num2))
    endif
          

% Multiplication of infinity
%  The use of mult_sign may be replaced by xor(sign(num1),sign(num2)) 
%  as soon as the accessor bug is fixed.
  fp_mul_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num 
     =
    If zero?(num1) or zero?(num2) then invalid
    else infinite(mult_sign(num1,num2))
    endif 

% Division with infinities
  fp_div_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num 
     =
    IF infinite?(num1) & infinite?(num2) THEN invalid
    ELSIF infinite?(num1) THEN infinite(mult_sign(num1,num2))
    ELSE finite(mult_sign(num1,num2),E_min,d_zero)
    ENDIF   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  

  END infinity_arithmetic

$$$infinity_arithmetic.prf
(|infinity_arithmetic| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
 (|fp_add_inf_TCC1| "" (TCC :DEFS !) NIL)
 (|fp_add_inf_TCC2| "" (TCC :DEFS !) NIL)
 (|fp_sub_inf_def_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (REWRITE "toggle_infinite")
    (("" (REWRITE "toggle_finite") (("" (GROUND) NIL)))))))
 (|fp_sub_inf_def| "" (SKOSIMP*)
  (("" (REWRITE "fp_sub_inf")
    (("" (REWRITE "fp_add_inf")
      (("1" (REWRITE "toggle_infinite")
        (("1" (LIFT-IF)
          (("1" (LIFT-IF)
            (("1" (GROUND)
              (("1" (EXPAND "toggle_sign") (("1" (ASSERT) NIL)))
               ("2" (EXPAND "toggle_sign")
                (("2" (TYPEPRED "i_sign(num2!1)")
                  (("2" (TYPEPRED "i_sign(num1!1)")
                    (("2" (GROUND) NIL)))))))))))))))
       ("2" (REWRITE "toggle_infinite")
        (("2" (REWRITE "toggle_finite")
          (("2" (TYPEPRED "num2!1") (("2" (GROUND) NIL)))))))))))))
 (XOR_TCC1 "" (TCC :DEFS !) NIL) (XOR_TCC2 "" (TCC :DEFS !) NIL)
 (|mult_sign_TCC1| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|mult_sign_TCC2| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|mult_sign_TCC3| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|mult_sign_TCC4| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
 (|fp_div_inf_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))))
$$$NaN_ops.pvs
NaN_ops
  [b,p:above(1),
   E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min],
            enumerated_type_defs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Placeholders for defining results of operations on NaNs

  fp,fp1,fp2: var fp_num
  nan,nan1,nan2: var (NaN?)

  op: var fp_ops

  signal?(fp):bool = if NaN?(fp) then signal?(status(fp)) else false endif

% mk_quiet takes an fp_num and coerces all NaNs into quiet NaNs.
%  all numeric floating-point arguments are left unchanged
  mk_quiet(fp): fp_num = if NaN?(fp) then NaN(quiet,data(fp)) else fp endif

  mk_quiet_correct: lemma not signal?(fp) => mk_quiet(fp) = fp

  fp_quiet(op,fp1,(fp2| NaN?(fp1) OR NaN?(fp2))):{nan| nan=fp1 or nan=fp2}

  fp_signal(op, fp1,(fp2| NaN?(fp1) OR NaN?(fp2))): fp_num =
    IF trap_enabled?(invalid_operation) THEN invalid
    ELSE fp_quiet(op, mk_quiet(fp1), mk_quiet(fp2))
    ENDIF

  fp_nan(op, fp1, (fp2| NaN?(fp1) OR NaN?(fp2))): fp_num =
    IF signal?(fp1) OR signal?(fp2) THEN fp_signal(op, fp1, fp2)
    ELSE fp_quiet(op, fp1, fp2)
    ENDIF

  NaN_ops_correct: LEMMA
        NOT trap_enabled?(invalid_operation) & (NaN?(fp1) OR NaN?(fp2))
          => quiet?(status(fp_nan(op, fp1, fp2)))

  fp_nan_x(op, fp1, (fp2| NaN?(fp1) OR NaN?(fp2))): [fp_num,exception] =
    IF signal?(fp1) OR signal?(fp2) THEN 
       (fp_signal(op, fp1, fp2),invalid_operation)
    ELSE 
       (fp_quiet(op, fp1, fp2), no_exceptions)
    ENDIF  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  NaN_sqrt(nan): fp_num =
    if signal?(status(nan)) 
        & trap_enabled?(invalid_operation) then
       invalid
    else NaN(quiet,data(nan))
    endif
  

  END NaN_ops

$$$NaN_ops.prf
(|NaN_ops| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
 (|mk_quiet_correct| "" (GRIND)
  (("" (LEMMA "fp_num_NaN_eta") (("" (INST?) (("" (ASSERT) NIL)))))))
 (|fp_quiet_TCC1| ""
  (INST +
   "lambda op,fp1,(fp2|NaN?(fp1) or NaN?(fp2)): if NaN?(fp1) then fp1 else fp2 endif")
  (("1" (SKOLEM-TYPEPRED) (("1" (PROP) NIL))) ("2" (SKOSIMP*) NIL)))
 (|fp_signal_TCC1| "" (SKOLEM-TYPEPRED) (("" (GRIND) NIL)))
 (|NaN_ops_correct_TCC1| "" (TCC :DEFS !) NIL)
 (|NaN_ops_correct_TCC2| "" (TCC :DEFS !) NIL)
 (|NaN_ops_correct| "" (SKOSIMP*)
  (("" (EXPAND "fp_nan")
    (("" (LIFT-IF)
      (("" (EXPAND "fp_signal")
        (("" (ASSERT)
          (("" (SPLIT 2)
            (("1" (FLATTEN)
              (("1" (HIDE -1)
                (("1"
                  (TYPEPRED
                   "fp_quiet(op!1, mk_quiet(fp1!1), mk_quiet(fp2!1))")
                  (("1" (GRIND) NIL) ("2" (GRIND) NIL)))))))
             ("2" (FLATTEN)
              (("2" (TYPEPRED "fp_quiet(op!1, fp1!1, fp2!1)")
                (("1" (EXPAND "signal?") (("1" (GRIND) NIL)))
                 ("2" (PROPAX) NIL))))))))))))))))))
$$$sqrt.pvs
sqrt: THEORY
  BEGIN
  
  e: VAR posreal
  
  x, y: VAR real
  
  epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y
  
  px, py: VAR nonneg_real
  
  times_pos_lt1: LEMMA px * py < 1 => px < 1 OR py < 1
  
  times_pos_le1: LEMMA px * py <= 1 => px <= 1 OR py <= 1
  
  times_pos_gt1: LEMMA px * py > 1 => px > 1 OR py > 1
  
  times_pos_ge1: LEMMA px * py >= 1 => px >= 1 OR py >= 1
  
  ge1_square_ge: LEMMA 1 <= px => px <= px * px

  i: var posnat

  expt_0: lemma 0^i = 0

  ge1_expt_ge: LEMMA 1 <= px => px <= px ^ i
  
  lt1_expt_le: LEMMA px<1 => px^i <= px
  
  square_def: LEMMA x^2 = x*x 

  expt_pos_le: LEMMA px^i<=py^i <=> px<=py
  
  expt_pos_lt: LEMMA px^i<py^i <=> px<py
  
  expt_pos_gt: LEMMA px^i>py^i <=> px>py
  
  expt_pos_ge: LEMMA px^i>=py^i <=> px>=py

  sqrt(px): {py | py^2 = px}
  
  sqrt1: lemma sqrt(px^2)=px

  sqrt_abs: lemma sqrt(x^2) = abs(x)

  END sqrt

$$$sqrt.prf
(|sqrt|
 (|epsilon_delta| "" (SKOSIMP*)
  (("" (INST - "abs(x!1-y!1)/2")
    (("1" (ASSERT) NIL)
     ("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))
 (|times_pos_lt1| "" (SKOSIMP*)
  (("" (LEMMA "ge_times_ge_pos")
    (("" (INST - "1" "1" "px!1" "py!1") (("" (GROUND) NIL)))))))
 (|times_pos_le1| "" (SKOSIMP*)
  (("" (LEMMA "gt_times_gt_pos1")
    (("" (INST - "1" "1" "px!1" "py!1") (("" (GROUND) NIL)))))))
 (|times_pos_gt1| "" (SKOSIMP*)
  (("" (LEMMA "le_times_le_pos")
    (("" (INST - "px!1" "py!1" "1" "1") (("" (ASSERT) NIL)))))))
 (|times_pos_ge1| "" (SKOSIMP*)
  (("" (LEMMA "lt_times_lt_pos1")
    (("" (INST - "px!1" "py!1" "1" "1")
      (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
 (|ge1_square_ge| "" (SKOSIMP*)
  (("" (LEMMA "le_times_le_pos")
    (("" (INST - "1" "px!1" "px!1" "px!1") (("" (ASSERT) NIL)))))))
 (|expt_0| "" (TCC) NIL) (|ge1_expt_ge_TCC1| "" (TCC :DEFS !) NIL)
 (|ge1_expt_ge| "" (INDUCT "i" 1 "above_induction[0]")
  (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)
   ("3" (SKOSIMP*) (("3" (REWRITE "expt_x1") (("3" (ASSERT) NIL)))))
   ("4" (SKOSIMP*)
    (("4" (REWRITE "expt_plus")
      (("4" (REWRITE "expt_x1")
        (("4" (ASSERT)
          (("4" (LEMMA "le_times_le_pos")
            (("4" (INST - "px!1" "1" "px!1" "px!1^ja!1")
              (("4" (ASSERT)
                (("4" (INST?) (("4" (ASSERT) NIL)))))))))))))))))))
 (|lt1_expt_le_TCC1| "" (TCC :DEFS !) NIL)
 (|lt1_expt_le| "" (INDUCT "i" 1 "above_induction[0]")
  (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)
   ("3" (SKOSIMP*) (("3" (REWRITE "expt_x1") (("3" (ASSERT) NIL)))))
   ("4" (SKOSIMP*)
    (("4" (CASE "px!1=0")
      (("1" (REPLACE -1)
        (("1" (REWRITE "expt_0") (("1" (ASSERT) NIL)))))
       ("2" (REWRITE "expt_plus")
        (("2" (REWRITE "expt_x1")
          (("2" (ASSERT)
            (("2" (INST?)
              (("2" (ASSERT)
                (("2" (LEMMA "le_times_le_pos")
                  (("2" (LEMMA "expt_pos")
                    (("2" (INST?)
                      (("2" (INST - "px!1^ja!1" "px!1" "1" "px!1")
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|square_def_TCC1| "" (TCC :DEFS !) NIL)
 (|square_def| "" (GRIND) NIL)
 (|expt_pos_le_TCC1| "" (TCC :DEFS !) NIL)
 (|expt_pos_le| "" (INDUCT "i" 1 "above_induction[0]")
  (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)
   ("3" (SKOSIMP*)
    (("3" (REWRITE "expt_x1")
      (("3" (REWRITE "expt_x1") (("3" (ASSERT) NIL)))))))
   ("4" (SKOSIMP*)
    (("4" (ASSERT)
      (("4" (CASE "px!1 = 0")
        (("1" (REPLACE -1)
          (("1" (REWRITE "expt_0") (("1" (ASSERT) NIL)))))
         ("2" (CASE "py!1=0")
          (("1" (REPLACE -1)
            (("1" (REWRITE "expt_0")
              (("1" (ASSERT)
                (("1" (LEMMA "expt_pos")
                  (("1" (INST?) (("1" (ASSERT) NIL)))))))))))
           ("2" (REWRITE "both_sides_expt_pos_le") NIL)))))))))))
 (|expt_pos_lt| "" (SKOSIMP*)
  (("" (LEMMA "expt_pos_le")
    (("" (INST - "i!1" "py!1" "px!1") (("" (GROUND) NIL)))))))
 (|expt_pos_gt| "" (SKOSIMP*)
  (("" (LEMMA "expt_pos_le")
    (("" (INST?) (("" (INST - "py!1") (("" (GROUND) NIL)))))))))
 (|expt_pos_ge| "" (SKOSIMP*)
  (("" (LEMMA "expt_pos_le")
    (("" (INST - "i!1" "py!1" "px!1") (("" (GROUND) NIL)))))))
 (|sqrt_TCC1| "" (TCC :DEFS !) NIL)
 (|sqrt_TCC2| "" (INST + "lambda px: choose({py|py^2=px})")
  (("" (SKOSIMP*)
    (("" (REWRITE "nonempty_exists")
      (("" (LEMMA "real_complete")
        (("" (INST - "{py|py^2<=px!1}")
          (("1" (PROP)
            (("1" (EXPAND "least_upper_bound?")
              (("1" (SKOSIMP*)
                (("1" (INST + "y!1")
                  (("1" (EXPAND "upper_bound?")
                    (("1" (ASSERT)
                      (("1" (INST-CP - 0)
                        (("1" (ASSERT)
                          (("1"
                            (CASE "forall (e:posreal|e<y!1): abs(y!1^2-px!1)< 4 * y!1 * e")
                            (("1"
                              (REWRITE "epsilon_delta")
                              (("1"
                                (SKOSIMP*)
                                (("1"
                                  (CASE "e!1 < (4* y!1) *y!1")
                                  (("1"
                                    (INST - "e!1/(4*y!1)")
                                    (("1" (ASSERT) NIL)
                                     ("2"
                                      (LEMMA "pos_div_gt")
                                      (("2"
                                        (INST - "4*y!1" "e!1")
                                        (("1"
                                          (ASSERT)
                                          (("1"
                                            (ASSERT)
                                            (("1"
                                              (REWRITE
                                               "div_mult_pos_lt1")
                                              NIL)))))
                                         ("2" (ASSERT) NIL)))))
                                     ("3" (ASSERT) NIL)))
                                   ("2"
                                    (INST - "y!1/4")
                                    (("1" (ASSERT) NIL)
                                     ("2"
                                      (ASSERT)
                                      (("2"
                                        (REWRITE "div_mult_pos_lt1")
                                        (("2"
                                          (CASE "y!1=0")
                                          (("1"
                                            (ASSERT)
                                            (("1"
                                              (REPLACE -1)
                                              (("1"
                                                (REWRITE "expt_0")
                                                (("1"
                                                  (ASSERT)
                                                  (("1"
                                                    (CASE "px!1<1")
                                                    (("1"
                                                      (INST - "px!1")
                                                      (("1"
                                                        (ASSERT)
                                                        NIL)
                                                       ("2"
                                                        (EXPAND
                                                         "extend")
                                                        (("2"
                                                          (REWRITE
                                                           "lt1_expt_le")
                                                          NIL)))))
                                                     ("2"
                                                      (INST - "1")
                                                      (("1"
                                                        (ASSERT)
                                                        NIL)
                                                       ("2"
                                                        (EXPAND
                                                         "extend")
                                                        (("2"
                                                          (REWRITE
                                                           "expt_1i")
                                                          (("2"
                                                            (ASSERT)
                                                            NIL)))))))))))))))))
                                           ("2"
                                            (ASSERT)
                                            NIL)))))))))))))))
                             ("2"
                              (SKOSIMP*)
                              (("2"
                                (CASE-REPLACE
                                 "4*y!1*e!1 = (y!1+e!1)^2 - (y!1-e!1)^2")
                                (("1"
                                  (HIDE -1 2)
                                  (("1"
                                    (CASE
                                     "forall (x,y:real): abs(x)<y iff -y <x & x <y")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (REPLACE -1)
                                        (("1"
                                          (HIDE -1)
                                          (("1"
                                            (PROP)
                                            (("1"
                                              (LEMMA "lt_minus_lt1")
                                              (("1"
                                                (INST
                                                 -
                                                 "px!1"
                                                 "(y!1-e!1)^2"
                                                 "y!1^2"
                                                 "(y!1+e!1)^2")
                                                (("1"
                                                  (GROUND)
                                                  (("1"
                                                    (ASSERT)
                                                    (("1"
                                                      (REWRITE
                                                       "expt_pos_le")
                                                      NIL)))
                                                   ("2"
                                                    (INST
                                                     -
                                                     "e!1+y!1")
                                                    (("1"
                                                      (ASSERT)
                                                      NIL)
                                                     ("2"
                                                      (EXPAND
                                                       "extend")
                                                      (("2"
                                                        (PROPAX)
                                                        NIL)))))))))))
                                             ("2"
                                              (REWRITE
                                               "lt_minus_lt1")
                                              (("1"
                                                (REWRITE
                                                 "expt_pos_le")
                                                NIL)
                                               ("2"
                                                (HIDE 2)
                                                (("2"
                                                  (INST
                                                   -3
                                                   "(y!1-e!1)")
                                                  (("2"
                                                    (ASSERT)
                                                    (("2"
                                                      (SKOLEM-TYPEPRED)
                                                      (("2"
                                                        (EXPAND
                                                         "extend")
                                                        (("2"
                                                          (LEMMA
                                                           "expt_pos_le")
                                                          (("2"
                                                            (INST
                                                             -
                                                             "2"
                                                             "y!2"
                                                             "y!1-e!1")
                                                            (("1"
                                                              (ASSERT)
                                                              (("1"
                                                                (ASSERT)
                                                                NIL)))
                                                             ("2"
                                                              (PROP)
                                                              NIL)))))))))))))))))))))))
                                       ("2" (ASSERT) NIL)))
                                     ("2"
                                      (HIDE -1 -2 -3 2)
                                      (("2" (GRIND) NIL)))))))
                                 ("2"
                                  (HIDE -1 -2 -3 2 3)
                                  (("2"
                                    (REWRITE "square_def")
                                    (("2"
                                      (REWRITE "square_def")
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))
                         ("2" (EXPAND "extend")
                          (("2" (ASSERT)
                            (("2"
                              (REWRITE "expt_0")
                              (("2" (ASSERT) NIL)))))))))))))))))))
             ("2" (INST + "max(px!1,1)")
              (("2" (EXPAND "upper_bound?")
                (("2" (SKOLEM-TYPEPRED)
                  (("2" (EXPAND "extend")
                    (("2" (EXPAND "max")
                      (("2" (LIFT-IF)
                        (("2" (GROUND)
                          (("1" (LEMMA "times_pos_lt1")
                            (("1"
                              (ASSERT)
                              (("1"
                                (REWRITE "square_def")
                                (("1"
                                  (INST?)
                                  (("1" (ASSERT) NIL)))))))))
                           ("2" (LEMMA "ge1_square_ge")
                            (("2"
                              (INST - "px!1")
                              (("2"
                                (ASSERT)
                                (("2"
                                  (LEMMA "expt_pos_le")
                                  (("2"
                                    (INST - "2" "y!1" "px!1")
                                    (("2"
                                      (REWRITE "square_def" :DIR RL)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))
           ("2" (REWRITE "nonempty_exists")
            (("2" (INST + "0")
              (("2" (EXPAND "extend")
                (("2" (REWRITE "expt_0")
                  (("2" (ASSERT) NIL)))))))))))))))))))
 (|sqrt1| "" (SKOSIMP*)
  (("" (TYPEPRED "sqrt(px!1 ^ 2)")
    (("" (LEMMA "expt_pos_ge")
      (("" (INST-CP - "2" "sqrt(px!1 ^ 2)" "px!1")
        (("" (INST - "2" "px!1" "sqrt(px!1 ^ 2)")
          (("" (GROUND) NIL)))))))))))
 (|sqrt_abs_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "square_def")
    (("" (REWRITE "pos_times_ge") (("" (GROUND) NIL)))))))
 (|sqrt_abs| "" (SKOSIMP*)
  (("" (EXPAND "abs")
    (("" (LIFT-IF)
      (("" (GROUND)
        (("1" (CASE-REPLACE "x!1^2 = (-x!1)^2")
          (("1" (REWRITE "sqrt1") NIL)
           ("2" (HIDE -1 2)
            (("2" (REWRITE "square_def")
              (("2" (REWRITE "square_def")
                (("2" (REWRITE "neg_times_neg") NIL)))))))))
         ("2" (REWRITE "sqrt1") NIL))))))))))