Theory "fxp"

Signature

Definitions

streamlength_def

|- !b ib sf. streamlength (b,ib,sf) = b

intbits_def

|- !b ib sf. intbits (b,ib,sf) = ib

signtype_def

|- !b ib st. signtype (b,ib,st) = st

is_signed_def

|- !X. is_signed X = (signtype X = 1)

is_unsigned_def

|- !X. is_unsigned X = (signtype X = 0)

fracbits_def

|- !X.
     fracbits X =
     (if is_unsigned X then
        streamlength X - intbits X
      else
        streamlength X - intbits X - 1)

stream_def

|- !v a. stream (v,a) = v

attrib_def

|- !v a. attrib (v,a) = a

validAttr_def

|- !X.
     validAttr X =
     (streamlength X > 0 /\ streamlength X < 257) /\
     intbits X < streamlength X + 1 /\ signtype X < 2

is_valid_def

|- !a.
     is_valid a =
     validAttr (attrib a) /\ (WORDLEN (stream a) = streamlength (attrib a))

fxp_TY_DEF

|- ?rep. TYPE_DEFINITION is_valid rep

fxp_tybij

|- (!a. fxp (defxp a) = a) /\ !r. is_valid r = (defxp (fxp r) = r)

Stream_def

|- !a. Stream a = stream (defxp a)

Attrib_def

|- !a. Attrib a = attrib (defxp a)

Streamlength_def

|- !a. Streamlength a = streamlength (Attrib a)

Intbits_def

|- !a. Intbits a = intbits (Attrib a)

Fracbits_def

|- !a. Fracbits a = fracbits (Attrib a)

Signtype_def

|- !a. Signtype a = signtype (Attrib a)

Issigned_def

|- !a. Issigned a = is_signed (Attrib a)

Isunsigned_def

|- !a. Isunsigned a = is_unsigned (Attrib a)

Isvalid_def

|- !a. Isvalid a = is_valid (defxp a)

Null_def

|- Null = @a. ~Isvalid a

value_def

|- !a.
     value a =
     (if Isunsigned a then
        & (BNVAL (Stream a)) / 2 pow Fracbits a
      else
        (& (BNVAL (Stream a)) -
         & (BV (MSB (Stream a)) * 2 ** Streamlength a)) / 2 pow Fracbits a)

MAX_def

|- !X.
     MAX X =
     (if is_unsigned X then
        (2 pow streamlength X - 1) / 2 pow fracbits X
      else
        (2 pow (streamlength X - 1) - 1) / 2 pow fracbits X)

MIN_def

|- !X.
     MIN X =
     (if is_unsigned X then
        0
      else
        ~(2 pow (streamlength X - 1)) / 2 pow fracbits X)

topfxp_def

|- !X.
     topfxp X =
     (if is_unsigned X then
        fxp (WORD (REPLICATE (streamlength X) T),X)
      else
        fxp (WCAT (WORD [F],WORD (REPLICATE (streamlength X - 1) T)),X))

bottomfxp_def

|- !X.
     bottomfxp X =
     (if is_unsigned X then
        fxp (WORD (REPLICATE (streamlength X) F),X)
      else
        fxp (WCAT (WORD [T],WORD (REPLICATE (streamlength X - 1) F)),X))

is_fxp_closest_def

|- !v s x a.
     is_fxp_closest v s x a =
     a IN s /\ !b. b IN s ==> abs (v a - x) <= abs (v b - x)

fxp_closest_def

|- !v p s x.
     fxp_closest v p s x =
     @a.
       is_fxp_closest v s x a /\ ((?b. is_fxp_closest v s x b /\ p b) ==> p a)

floor_def

|- !x. floor x = @n. & n <= abs x /\ !i. & i <= abs x ==> i <= n

fraction_def

|- !x. fraction x = x - & (floor x)

BDIG_def

|- !n a. BDIG n a = VB ((a DIV 2 ** n) MOD 2)

BDIGFUN_def

|- !a. BDIGFUN a = (\n. BDIG n a)

BWORD_def

|- !n m. BWORD n m = WORD (GENLIST (BDIGFUN n) m)

TWOEXPONENT_def

|- !x. TWOEXPONENT x = @n. 2 pow n >= abs x /\ !m. 2 pow m >= abs x ==> n <= m

POSITIVE_def

|- !x. POSITIVE x = 2 pow TWOEXPONENT x + x

Wrapp_def

|- !X x.
     Wrapp X x =
     (if x >= 0 then
        fxp
          (WCAT
             (BWORD (floor x) (intbits X),
              BWORD (floor (2 pow fracbits X * fraction x)) (fracbits X)),X)
      else
        fxp
          (WCAT
             (BWORD (floor (POSITIVE x)) (intbits X) WOR
              BWORD (2 ** TWOEXPONENT x) (intbits X),
              BWORD (floor (2 pow fracbits X * fraction (POSITIVE x)))
                (fracbits X)),X))

fxp_roundmode_TY_DEF

|- ?rep. TYPE_DEFINITION (\n. n < 5) rep

fxp_roundmode_BIJ

|- (!a. num2fxp_roundmode (fxp_roundmode2num a) = a) /\
   !r. (\n. n < 5) r = (fxp_roundmode2num (num2fxp_roundmode r) = r)

Round

|- Round = num2fxp_roundmode 0

To_zero

|- To_zero = num2fxp_roundmode 1

To_plus_infinity

|- To_plus_infinity = num2fxp_roundmode 2

Truncate

|- Truncate = num2fxp_roundmode 3

Convergent

|- Convergent = num2fxp_roundmode 4

fxp_roundmode_size_def

|- !x. fxp_roundmode_size x = 0

fxp_roundmode_case

|- !v0 v1 v2 v3 v4 x.
     (case x of
         Round -> v0
      || To_zero -> v1
      || To_plus_infinity -> v2
      || Truncate -> v3
      || Convergent -> v4) =
     (\m.
        (if m < 2 then
           (if m = 0 then v0 else v1)
         else
           (if m < 3 then v2 else (if m = 3 then v3 else v4))))
       (fxp_roundmode2num x)

overflowmode_TY_DEF

|- ?rep. TYPE_DEFINITION (\n. n < 2) rep

overflowmode_BIJ

|- (!a. num2overflowmode (overflowmode2num a) = a) /\
   !r. (\n. n < 2) r = (overflowmode2num (num2overflowmode r) = r)

Wrap

|- Wrap = num2overflowmode 0

Clip

|- Clip = num2overflowmode 1

overflowmode_size_def

|- !x. overflowmode_size x = 0

overflowmode_case

|- !v0 v1 x.
     (case x of Wrap -> v0 || Clip -> v1) =
     (\m. (if m = 0 then v0 else v1)) (overflowmode2num x)

Exception_TY_DEF

|- ?rep. TYPE_DEFINITION (\n. n < 4) rep

Exception_BIJ

|- (!a. num2Exception (Exception2num a) = a) /\
   !r. (\n. n < 4) r = (Exception2num (num2Exception r) = r)

no_except

|- no_except = num2Exception 0

overflow

|- overflow = num2Exception 1

invalid

|- invalid = num2Exception 2

loss_sign

|- loss_sign = num2Exception 3

Exception_size_def

|- !x. Exception_size x = 0

Exception_case

|- !v0 v1 v2 v3 x.
     (case x of
         no_except -> v0
      || overflow -> v1
      || invalid -> v2
      || loss_sign -> v3) =
     (\m.
        (if m < 1 then
           v0
         else
           (if m < 2 then v1 else (if m = 2 then v2 else v3))))
       (Exception2num x)

fxp_round_def

|- (!X x mode.
      fxp_round X Convergent x mode =
      (if x > MAX X /\ (mode = Clip) then
         (topfxp X,overflow)
       else
         (if x < MIN X /\ (mode = Clip) then
            (bottomfxp X,overflow)
          else
            (if x > MAX X /\ (mode = Wrap) then
               (Wrapp X x,overflow)
             else
               (if x < MIN X /\ (mode = Wrap) then
                  (Wrapp X x,overflow)
                else
                  (fxp_closest value (\a. LSB (Stream a) = F)
                     {a | Isvalid a /\ (Attrib a = X)} x,no_except)))))) /\
   (!X x mode.
      fxp_round X To_zero x mode =
      (if x > MAX X /\ (mode = Clip) then
         (topfxp X,overflow)
       else
         (if x < MIN X /\ (mode = Clip) then
            (bottomfxp X,overflow)
          else
            (if x >= MAX X /\ (mode = Wrap) then
               (Wrapp X x,overflow)
             else
               (if x < MIN X /\ (mode = Wrap) then
                  (Wrapp X x,overflow)
                else
                  (fxp_closest value (\a. T)
                     {a |
                      Isvalid a /\ (Attrib a = X) /\ abs (value a) <= abs x}
                     x,no_except)))))) /\
   (!X x mode.
      fxp_round X To_plus_infinity x mode =
      (if x > MAX X /\ (mode = Clip) then
         (topfxp X,overflow)
       else
         (if x < MIN X /\ (mode = Clip) then
            (bottomfxp X,overflow)
          else
            (if x > MAX X /\ (mode = Wrap) then
               (Wrapp X x,overflow)
             else
               (if x < MIN X /\ (mode = Wrap) then
                  (Wrapp X x,overflow)
                else
                  (fxp_closest value (\a. T)
                     {a | Isvalid a /\ (Attrib a = X) /\ value a >= x} x,
                   no_except)))))) /\
   (!X x mode.
      fxp_round X Truncate x mode =
      (if x > MAX X /\ (mode = Clip) then
         (topfxp X,overflow)
       else
         (if x < MIN X /\ (mode = Clip) then
            (bottomfxp X,overflow)
          else
            (if x > MAX X /\ (mode = Wrap) then
               (Wrapp X x,overflow)
             else
               (if x < MIN X /\ (mode = Wrap) then
                  (Wrapp X x,overflow)
                else
                  (fxp_closest value (\a. T)
                     {a | Isvalid a /\ (Attrib a = X) /\ value a <= x} x,
                   no_except)))))) /\
   !X x mode.
     fxp_round X Round x mode =
     (if x > MAX X /\ (mode = Clip) then
        (topfxp X,overflow)
      else
        (if x < MIN X /\ (mode = Clip) then
           (bottomfxp X,overflow)
         else
           (if x > MAX X /\ (mode = Wrap) then
              (Wrapp X x,overflow)
            else
              (if x < MIN X /\ (mode = Wrap) then
                 (Wrapp X x,overflow)
               else
                 (fxp_closest value (\a. value (fxp (Stream a,X)) >= x)
                    {a | Isvalid a /\ (Attrib a = X)} x,no_except)))))

fxpAdd_def

|- !X rnd over a b.
     fxpAdd X rnd over a b =
     (if ~(Isvalid a /\ Isvalid b) then
        (Null,invalid)
      else
        (if value a + value b < 0 /\ is_unsigned X then
           (fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
         else
           fxp_round X rnd (value a + value b) over))

fxpAbs_def

|- !X rnd over a.
     fxpAbs X rnd over a =
     (if ~Isvalid a then
        (Null,invalid)
      else
        fxp_round X rnd (abs (value a)) over)

fxpAShift_def

|- !X rnd over a b.
     fxpAShift X rnd over a b =
     (if ~Isvalid a then
        (Null,invalid)
      else
        (if b < 0 then
           fxp_round X rnd
             (value
                (fxp
                   (WCAT
                      (WORD (REPLICATE (Num (ABS b)) (MSB (Stream a))),
                       WSEG (streamlength (Attrib a) - 1)
                         (streamlength (Attrib a) - Num (ABS b)) (Stream a)),
                    Attrib a))) over
         else
           fxp_round X rnd
             (value
                (fxp
                   (WCAT
                      (WORD (REPLICATE (Num (ABS b)) F),
                       WSEG (streamlength (Attrib a) - SUC (Num (ABS b))) 0
                         (Stream a)),Attrib a))) over))

fxpAnd_def

|- !X a b.
     fxpAnd X a b =
     (if ~(Isvalid a /\ Isvalid b) \/ ~(Attrib a = X) \/ ~(Attrib b = X) then
        (Null,invalid)
      else
        (fxp (Stream a WAND Stream b,X),no_except))

fxpOr_def

|- !X a b.
     fxpOr X a b =
     (if ~(Isvalid a /\ Isvalid b) \/ ~(Attrib a = X) \/ ~(Attrib b = X) then
        (Null,invalid)
      else
        (fxp (Stream a WOR Stream b,X),no_except))

fxpSub_def

|- !X rnd over a b.
     fxpSub X rnd over a b =
     (if ~(Isvalid a /\ Isvalid b) then
        (Null,invalid)
      else
        (if value a - value b < 0 /\ is_unsigned X then
           (fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
         else
           fxp_round X rnd (value a - value b) over))

fxpMul_def

|- !X rnd over a b.
     fxpMul X rnd over a b =
     (if ~(Isvalid a /\ Isvalid b) then
        (Null,invalid)
      else
        (if value a * value b < 0 /\ is_unsigned X then
           (fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
         else
           fxp_round X rnd (value a * value b) over))

fxpDiv_def

|- !X rnd over a b.
     fxpDiv X rnd over a b =
     (if ~(Isvalid a /\ Isvalid b) then
        (Null,invalid)
      else
        (if value b = 0 then
           (fxp (WORD (REPLICATE (streamlength X) F),X),invalid)
         else
           (if value a / value b < 0 /\ is_unsigned X then
              (fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
            else
              fxp_round X rnd (value a / value b) over)))

fxperror_def

|- !X rnd over x.
     fxperror X rnd over x = value (FST (fxp_round X rnd x over)) - x

representable

|- !X x. representable X x = ~(x > MAX X) /\ ~(x < MIN X)

Fxp_round_def

|- !X x. Fxp_round X x = FST (fxp_round X Convergent x Clip)

Fxperror_def

|- !X x. Fxperror X x = fxperror X Convergent Clip x

FxpAdd_def

|- !X a b. FxpAdd X a b = FST (fxpAdd X Convergent Clip a b)

FxpSub_def

|- !X a b. FxpSub X a b = FST (fxpSub X Convergent Clip a b)

FxpMul_def

|- !X a b. FxpMul X a b = FST (fxpMul X Convergent Clip a b)

Theorems

NOTTiIsigned

|- !n m s k.
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ~Isunsigned (fxp (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s))

LASTN1

|- !n k. LASTN n (F::NLIST n VB 2 k) = LASTN n (NLIST n VB 2 k)

DEFXP_FXP_WCAT

|- !w n m s k.
     validAttr (n,m,s) ==>
     (defxp (fxp (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s)) =
      (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s))

DEFXP_FXP_WCATT

|- !w n m s k.
     validAttr (n,m,s) ==>
     (defxp (fxp (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s)) =
      (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s))

ISVALID_WCAT

|- !n m s k.
     validAttr (n,m,s) ==> is_valid (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s)

ISVALID_WCATT

|- !n m s k.
     validAttr (n,m,s) ==> is_valid (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s)

FXP_ERROR_BOUND_LEMMA2_NEG_SIGNED

|- !x n m s.
     0 <= ~x /\
     ~x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?k.
       k < 2 ** (streamlength (n,m,s) - 1) /\
       abs (~(& k / 2 pow fracbits (n,m,s)) - x) <=
       inv (2 pow fracbits (n,m,s))

FXP_ERROR_BOUND_LEMMA2_POS_SIGNED

|- !x n m s.
     0 <= x /\
     x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?k.
       k < 2 ** (streamlength (n,m,s) - 1) /\
       abs (x - & k / 2 pow fracbits (n,m,s)) <= inv (2 pow fracbits (n,m,s))

FXP_ERROR_BOUND_LEMMA1_NEG_SIGNED

|- !x n m s.
     0 <= ~x /\
     ~x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?k.
       k < 2 ** (streamlength (n,m,s) - 1) /\
       & k / 2 pow fracbits (n,m,s) <= ~x /\
       ~x <= & (SUC k) / 2 pow fracbits (n,m,s)

FXP_ERROR_BOUND_LEMMA1_POS_SIGNED

|- !x n m s.
     0 <= x /\
     x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?k.
       k < 2 ** (streamlength (n,m,s) - 1) /\
       & k / 2 pow fracbits (n,m,s) <= x /\
       x <= & (SUC k) / 2 pow fracbits (n,m,s)

FXP_MAIN_ERROR_BOUND_THEOREM_UNSIGNED

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     is_unsigned (n,m,s) ==>
     abs (fxperror (n,m,s) Convergent Clip x) <= inv (2 pow fracbits (n,m,s))

DEFXP_FXP_WORDLEN

|- !w m s.
     validAttr (WORDLEN w,m,s) ==>
     (defxp (fxp (w,WORDLEN w,m,s)) = (w,WORDLEN w,m,s))

ISVALIDWORDLEN

|- !w m s. validAttr (WORDLEN w,m,s) ==> is_valid (w,WORDLEN w,m,s)

FXP_ERROR_BOUND_LEMMA3_UNSIGNED

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     is_unsigned (n,m,s) ==>
     ?w.
       abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
       (WORDLEN w = n)

B4

|- !n m s.
     (2 pow n - 1) / 2 pow fracbits (n,m,s) <=
     2 pow n * inv (2 pow fracbits (n,m,s))

B2

|- !n m s x.
     x - 2 pow n * inv (2 pow fracbits (n,m,s)) <=
     x -
     (2 pow n * inv (2 pow fracbits (n,m,s)) - inv (2 pow fracbits (n,m,s)))

REAL_OF_NUM_SUB

|- !m n. m <= n ==> (& n - & m = & (n - m))

ADD_SUB2

|- !m n. m + n - m = n

TWOEXPGE1

|- !n. 1 <= 2 ** n

TWOEXP

|- !n. 2 ** n - 1 < 2 ** n

iIsigned

|- !n m s k.
     validAttr (n,m,s) /\ is_unsigned (n,m,s) ==>
     Isunsigned (fxp (NBWORD n k,n,m,s))

pwvfracle111

|- !x n m s.
     x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <= 2 pow (streamlength (n,m,s) - 1)

pwvfraclt111

|- !x n m s.
     x < 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x < 2 pow (streamlength (n,m,s) - 1)

pwvfracle21

|- !x n m s.
     & k / 2 pow fracbits (n,m,s) <= x = & k <= 2 pow fracbits (n,m,s) * x

pwvfraclt21

|- !x n m s.
     & k / 2 pow fracbits (n,m,s) < x = & k < 2 pow fracbits (n,m,s) * x

pwvfracle2

|- !x n m s.
     & k / 2 pow fracbits (n,m,s) <= x =
     2 pow fracbits (n,m,s) * (& k / 2 pow fracbits (n,m,s)) <=
     2 pow fracbits (n,m,s) * x

pwvfraclt2

|- !x n m s.
     & k / 2 pow fracbits (n,m,s) < x =
     2 pow fracbits (n,m,s) * (& k / 2 pow fracbits (n,m,s)) <
     2 pow fracbits (n,m,s) * x

pwvfracle1

|- !x n m s.
     x <= (2 pow streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <=
     2 pow fracbits (n,m,s) *
     ((2 pow streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s))

pwvfracltt1

|- !x n m s.
     x < 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <
     2 pow fracbits (n,m,s) *
     (2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s))

num2fxp_roundmode_fxp_roundmode2num

|- !a. num2fxp_roundmode (fxp_roundmode2num a) = a

fxp_roundmode2num_num2fxp_roundmode

|- !r. r < 5 = (fxp_roundmode2num (num2fxp_roundmode r) = r)

num2fxp_roundmode_11

|- !r r'.
     r < 5 ==>
     r' < 5 ==>
     ((num2fxp_roundmode r = num2fxp_roundmode r') = (r = r'))

fxp_roundmode2num_11

|- !a a'. (fxp_roundmode2num a = fxp_roundmode2num a') = (a = a')

num2fxp_roundmode_ONTO

|- !a. ?r. (a = num2fxp_roundmode r) /\ r < 5

fxp_roundmode2num_ONTO

|- !r. r < 5 = ?a. r = fxp_roundmode2num a

num2fxp_roundmode_thm

|- (num2fxp_roundmode 0 = Round) /\ (num2fxp_roundmode 1 = To_zero) /\
   (num2fxp_roundmode 2 = To_plus_infinity) /\
   (num2fxp_roundmode 3 = Truncate) /\ (num2fxp_roundmode 4 = Convergent)

fxp_roundmode2num_thm

|- (fxp_roundmode2num Round = 0) /\ (fxp_roundmode2num To_zero = 1) /\
   (fxp_roundmode2num To_plus_infinity = 2) /\
   (fxp_roundmode2num Truncate = 3) /\ (fxp_roundmode2num Convergent = 4)

fxp_roundmode_EQ_fxp_roundmode

|- !a a'. (a = a') = (fxp_roundmode2num a = fxp_roundmode2num a')

fxp_roundmode_case_def

|- (!v0 v1 v2 v3 v4.
      (case Round of
          Round -> v0
       || To_zero -> v1
       || To_plus_infinity -> v2
       || Truncate -> v3
       || Convergent -> v4) =
      v0) /\
   (!v0 v1 v2 v3 v4.
      (case To_zero of
          Round -> v0
       || To_zero -> v1
       || To_plus_infinity -> v2
       || Truncate -> v3
       || Convergent -> v4) =
      v1) /\
   (!v0 v1 v2 v3 v4.
      (case To_plus_infinity of
          Round -> v0
       || To_zero -> v1
       || To_plus_infinity -> v2
       || Truncate -> v3
       || Convergent -> v4) =
      v2) /\
   (!v0 v1 v2 v3 v4.
      (case Truncate of
          Round -> v0
       || To_zero -> v1
       || To_plus_infinity -> v2
       || Truncate -> v3
       || Convergent -> v4) =
      v3) /\
   !v0 v1 v2 v3 v4.
     (case Convergent of
         Round -> v0
      || To_zero -> v1
      || To_plus_infinity -> v2
      || Truncate -> v3
      || Convergent -> v4) =
     v4

datatype_fxp_roundmode

|- DATATYPE (fxp_roundmode Round To_zero To_plus_infinity Truncate Convergent)

fxp_roundmode_distinct

|- ~(Round = To_zero) /\ ~(Round = To_plus_infinity) /\ ~(Round = Truncate) /\
   ~(Round = Convergent) /\ ~(To_zero = To_plus_infinity) /\
   ~(To_zero = Truncate) /\ ~(To_zero = Convergent) /\
   ~(To_plus_infinity = Truncate) /\ ~(To_plus_infinity = Convergent) /\
   ~(Truncate = Convergent)

fxp_roundmode_case_cong

|- !M M' v0 v1 v2 v3 v4.
     (M = M') /\ ((M' = Round) ==> (v0 = v0')) /\
     ((M' = To_zero) ==> (v1 = v1')) /\
     ((M' = To_plus_infinity) ==> (v2 = v2')) /\
     ((M' = Truncate) ==> (v3 = v3')) /\
     ((M' = Convergent) ==> (v4 = v4')) ==>
     ((case M of
          Round -> v0
       || To_zero -> v1
       || To_plus_infinity -> v2
       || Truncate -> v3
       || Convergent -> v4) =
      case M' of
         Round -> v0'
      || To_zero -> v1'
      || To_plus_infinity -> v2'
      || Truncate -> v3'
      || Convergent -> v4')

fxp_roundmode_nchotomy

|- !a.
     (a = Round) \/ (a = To_zero) \/ (a = To_plus_infinity) \/
     (a = Truncate) \/ (a = Convergent)

fxp_roundmode_Axiom

|- !x0 x1 x2 x3 x4.
     ?f.
       (f Round = x0) /\ (f To_zero = x1) /\ (f To_plus_infinity = x2) /\
       (f Truncate = x3) /\ (f Convergent = x4)

fxp_roundmode_induction

|- !P.
     P Convergent /\ P Round /\ P To_plus_infinity /\ P To_zero /\
     P Truncate ==>
     !a. P a

num2overflowmode_overflowmode2num

|- !a. num2overflowmode (overflowmode2num a) = a

overflowmode2num_num2overflowmode

|- !r. r < 2 = (overflowmode2num (num2overflowmode r) = r)

num2overflowmode_11

|- !r r'.
     r < 2 ==>
     r' < 2 ==>
     ((num2overflowmode r = num2overflowmode r') = (r = r'))

overflowmode2num_11

|- !a a'. (overflowmode2num a = overflowmode2num a') = (a = a')

num2overflowmode_ONTO

|- !a. ?r. (a = num2overflowmode r) /\ r < 2

overflowmode2num_ONTO

|- !r. r < 2 = ?a. r = overflowmode2num a

num2overflowmode_thm

|- (num2overflowmode 0 = Wrap) /\ (num2overflowmode 1 = Clip)

overflowmode2num_thm

|- (overflowmode2num Wrap = 0) /\ (overflowmode2num Clip = 1)

overflowmode_EQ_overflowmode

|- !a a'. (a = a') = (overflowmode2num a = overflowmode2num a')

overflowmode_case_def

|- (!v0 v1. (case Wrap of Wrap -> v0 || Clip -> v1) = v0) /\
   !v0 v1. (case Clip of Wrap -> v0 || Clip -> v1) = v1

datatype_overflowmode

|- DATATYPE (overflowmode Wrap Clip)

overflowmode_distinct

|- ~(Wrap = Clip)

overflowmode_case_cong

|- !M M' v0 v1.
     (M = M') /\ ((M' = Wrap) ==> (v0 = v0')) /\
     ((M' = Clip) ==> (v1 = v1')) ==>
     ((case M of Wrap -> v0 || Clip -> v1) =
      case M' of Wrap -> v0' || Clip -> v1')

overflowmode_nchotomy

|- !a. (a = Wrap) \/ (a = Clip)

overflowmode_Axiom

|- !x0 x1. ?f. (f Wrap = x0) /\ (f Clip = x1)

overflowmode_induction

|- !P. P Clip /\ P Wrap ==> !a. P a

num2Exception_Exception2num

|- !a. num2Exception (Exception2num a) = a

Exception2num_num2Exception

|- !r. r < 4 = (Exception2num (num2Exception r) = r)

num2Exception_11

|- !r r'.
     r < 4 ==> r' < 4 ==> ((num2Exception r = num2Exception r') = (r = r'))

Exception2num_11

|- !a a'. (Exception2num a = Exception2num a') = (a = a')

num2Exception_ONTO

|- !a. ?r. (a = num2Exception r) /\ r < 4

Exception2num_ONTO

|- !r. r < 4 = ?a. r = Exception2num a

num2Exception_thm

|- (num2Exception 0 = no_except) /\ (num2Exception 1 = overflow) /\
   (num2Exception 2 = invalid) /\ (num2Exception 3 = loss_sign)

Exception2num_thm

|- (Exception2num no_except = 0) /\ (Exception2num overflow = 1) /\
   (Exception2num invalid = 2) /\ (Exception2num loss_sign = 3)

Exception_EQ_Exception

|- !a a'. (a = a') = (Exception2num a = Exception2num a')

Exception_case_def

|- (!v0 v1 v2 v3.
      (case no_except of
          no_except -> v0
       || overflow -> v1
       || invalid -> v2
       || loss_sign -> v3) =
      v0) /\
   (!v0 v1 v2 v3.
      (case overflow of
          no_except -> v0
       || overflow -> v1
       || invalid -> v2
       || loss_sign -> v3) =
      v1) /\
   (!v0 v1 v2 v3.
      (case invalid of
          no_except -> v0
       || overflow -> v1
       || invalid -> v2
       || loss_sign -> v3) =
      v2) /\
   !v0 v1 v2 v3.
     (case loss_sign of
         no_except -> v0
      || overflow -> v1
      || invalid -> v2
      || loss_sign -> v3) =
     v3

datatype_Exception

|- DATATYPE (Exception no_except overflow invalid loss_sign)

Exception_distinct

|- ~(no_except = overflow) /\ ~(no_except = invalid) /\
   ~(no_except = loss_sign) /\ ~(overflow = invalid) /\
   ~(overflow = loss_sign) /\ ~(invalid = loss_sign)

Exception_case_cong

|- !M M' v0 v1 v2 v3.
     (M = M') /\ ((M' = no_except) ==> (v0 = v0')) /\
     ((M' = overflow) ==> (v1 = v1')) /\ ((M' = invalid) ==> (v2 = v2')) /\
     ((M' = loss_sign) ==> (v3 = v3')) ==>
     ((case M of
          no_except -> v0
       || overflow -> v1
       || invalid -> v2
       || loss_sign -> v3) =
      case M' of
         no_except -> v0'
      || overflow -> v1'
      || invalid -> v2'
      || loss_sign -> v3')

Exception_nchotomy

|- !a. (a = no_except) \/ (a = overflow) \/ (a = invalid) \/ (a = loss_sign)

Exception_Axiom

|- !x0 x1 x2 x3.
     ?f.
       (f no_except = x0) /\ (f overflow = x1) /\ (f invalid = x2) /\
       (f loss_sign = x3)

Exception_induction

|- !P. P invalid /\ P loss_sign /\ P no_except /\ P overflow ==> !a. P a

STREAM

|- !a. stream a = FST a

ATTRIB

|- !a. attrib a = SND a

STREAMLEN

|- !X. streamlength X = FST X

INTBITS

|- !X. intbits X = FST (SND X)

SIGN

|- !X. signtype X = SND (SND X)

IS_FXP_CLOSEST_EXISTS

|- !v x s. FINITE s ==> ~(s = {}) ==> ?a. is_fxp_closest v s x a

FXP_CLOSEST_IS_EVERYTHING

|- !v p x s.
     FINITE s ==>
     ~(s = {}) ==>
     is_fxp_closest v s x (fxp_closest v p s x) /\
     ((?b. is_fxp_closest v s x b /\ p b) ==> p (fxp_closest v p s x))

FXP_CLOSEST_IN_SET

|- !v p x s. FINITE s ==> ~(s = {}) ==> fxp_closest v p s x IN s

FXP_CLOSEST_IS_FXP_CLOSEST

|- !v p x s.
     FINITE s ==> ~(s = {}) ==> is_fxp_closest v s x (fxp_closest v p s x)

WORDINDUCT

|- !n.
     {w | WORDLEN w = SUC n} =
     IMAGE (\w. WCAT (WORD [T],w)) {w | WORDLEN w = n} UNION
     IMAGE (\w. WCAT (WORD [F],w)) {w | WORDLEN w = n}

WORDBASIS

|- FINITE {w | WORDLEN w = 0} = FINITE {WORD []}

WORDFINITE

|- !x. FINITE {w | WORDLEN w = x}

WORDPAIRIMAGE

|- !n.
     {(w,x) | (WORDLEN w = x) /\ (x = n)} =
     IMAGE (\w. (w,WORDLEN w)) {w | WORDLEN w = n}

FXP_FIRSTCROSS00

|- !x p q r.
     x =
     (\((w,x),y,z). (w,x,y,z))
       ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x)))

FXP_FIRSTCROSS0

|- !x p q r.
     FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
     (WORDLEN (FST x) = FST (SND x)) ==>
     (?x''.
        (FST ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x))),T) =
        (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x'') /\
     FST (SND ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x)))) <
     q /\
     SND (SND ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x)))) < r

FXP_FIRSTCROSS1

|- !x p q r.
     FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
     (WORDLEN (FST x) = FST (SND x)) ==>
     ?x'.
       (x = (\((w,x),y,z). (w,x,y,z)) x') /\
       (?x. (FST x',T) = (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x) /\
       FST (SND x') < q /\ SND (SND x') < r

FXP_FIRSTCROSS2

|- !x p q r.
     (?x'.
        (x = (\((w,x),y,z). (w,x,y,z)) x') /\
        (?x. (FST x',T) = (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x) /\
        FST (SND x') < q /\ SND (SND x') < r) ==>
     FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
     (WORDLEN (FST x) = FST (SND x))

FXP_FIRSTCROSS3

|- !x p q r.
     FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
     (WORDLEN (FST x) = FST (SND x)) =
     ?x'.
       (x = (\((w,x),y,z). (w,x,y,z)) x') /\
       (?x. (FST x',T) = (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x) /\
       FST (SND x') < q /\ SND (SND x') < r

FXP_FIRSTCROSS

|- !p q r.
     {a |
      FST (SND a) < p /\ FST (SND (SND a)) < q /\ SND (SND (SND a)) < r /\
      (WORDLEN (FST a) = FST (SND a))} =
     IMAGE (\((w,x),y,z). (w,x,y,z))
       ({(w,x) | (WORDLEN w = x) /\ x < p} CROSS
        ({y | y < q} CROSS {z | z < r}))

COUNTINDUCT

|- !n. ({x | x < 0} = {}) /\ ({x | x < SUC n} = n INSERT {x | x < n})

FINITECOUNT

|- !n. FINITE {x | x < n}

FINITELESSBASIS

|- {(w,x) | (WORDLEN w = x) /\ x < 0} = {}

FINITELESSINDUCT

|- !n.
     FINITE {(w,x) | (WORDLEN w = x) /\ x < SUC n} =
     FINITE
       ({(w,x) | (WORDLEN w = x) /\ (x = n)} UNION
        {(w,x) | (WORDLEN w = x) /\ x < n})

FINITEPAIRLESS

|- !m. FINITE {(w,x) | (WORDLEN w = x) /\ x < m}

FINITEGENERAL

|- !p q r.
     FINITE
       {a |
        FST (SND a) < p /\ FST (SND (SND a)) < q /\ SND (SND (SND a)) < r /\
        (WORDLEN (FST a) = FST (SND a))}

INSTANCEFINITE

|- FINITE
     {a |
      FST (SND a) < 257 /\ FST (SND (SND a)) < 257 /\ SND (SND (SND a)) < 2 /\
      (WORDLEN (FST a) = FST (SND a))}

ISVALID_SUB

|- {a | is_valid a} SUBSET
   {a |
    FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
    SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))}

INSTANCE

|- {a |
    FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
    SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))} SUBSET
   {a |
    FST (SND a) < 257 /\ FST (SND (SND a)) < 257 /\ SND (SND (SND a)) < 2 /\
    (WORDLEN (FST a) = FST (SND a))}

MATCHFINITE

|- {a |
    FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
    SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))} SUBSET
   {a |
    FST (SND a) < 257 /\ FST (SND (SND a)) < 257 /\ SND (SND (SND a)) < 2 /\
    (WORDLEN (FST a) = FST (SND a))} ==>
   FINITE
     {a |
      FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
      SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))}

MAINFINITE

|- FINITE
     {a |
      FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
      SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))}

MATCHFINITEVALID

|- {a | is_valid a} SUBSET
   {a |
    FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
    SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))} ==>
   FINITE {a | is_valid a}

FINITEVALID

|- FINITE {a | is_valid a}

MATCHFINITEVALIDATTR

|- !n m s.
     {a | is_valid a /\ (attrib a = (n,m,s))} SUBSET {a | is_valid a} ==>
     FINITE {a | is_valid a /\ (attrib a = (n,m,s))}

ISVALID_ATTR_SUB

|- !n m s. {a | is_valid a /\ (attrib a = (n,m,s))} SUBSET {a | is_valid a}

FINITEVALIDATTR

|- !n m s. FINITE {a | is_valid a /\ (attrib a = (n,m,s))}

ISVALID_ATTR_IMAGE

|- !n m s.
     {a | Isvalid a /\ (Attrib a = (n,m,s))} =
     IMAGE fxp {a | is_valid a /\ (attrib a = (n,m,s))}

FINITEFXPVALIDATTR

|- !n m s. FINITE {a | Isvalid a /\ (Attrib a = (n,m,s))}

FINITEFXPVALIDATTRX

|- !X. FINITE {a | Isvalid a /\ (Attrib a = X)}

REPLICATELENGTH

|- !n. LENGTH (REPLICATE n T) = n

ISVALIDREPLICATE

|- !n m s. validAttr (n,m,s) ==> is_valid (WORD (REPLICATE n T),n,m,s)

ISVALIDNBWORD

|- !n m s k. validAttr (n,m,s) ==> is_valid (NBWORD n k,n,m,s)

DEFXP_FXP_NBWORD

|- !n m s k.
     validAttr (n,m,s) ==>
     (defxp (fxp (NBWORD n k,n,m,s)) = (NBWORD n k,n,m,s))

DEFXP_FXP_REPLICATE

|- !n m s.
     validAttr (n,m,s) ==>
     (defxp (fxp (WORD (REPLICATE n T),n,m,s)) = (WORD (REPLICATE n T),n,m,s))

IS_VALID_FXP_CLOSEST

|- !v p x n m s.
     validAttr (n,m,s) ==>
     Isvalid (fxp_closest v p {a | Isvalid a /\ (Attrib a = (n,m,s))} x)

IS_VALID_ROUND_CONV_CLIP

|- !n m s x.
     validAttr (n,m,s) /\ ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) ==>
     Isvalid (FST (fxp_round (n,m,s) Convergent x Clip))

ISVALISPECIAL

|- is_valid (WORD (REPLICATE 2 T),2,1,1)

DEFXP_FXP_SPECIAL

|- defxp (fxp (WORD (REPLICATE 2 T),2,1,1)) = (WORD (REPLICATE 2 T),2,1,1)

IS_VALID_NONEMPTY

|- ~({a | Isvalid a} = {})

IS_VALID_ATTRIB_NONEMPTY

|- !n m s.
     validAttr (n,m,s) ==> ~({a | Isvalid a /\ (Attrib a = (n,m,s))} = {})

REPLICATELENGTHF

|- !n. LENGTH (REPLICATE n F) = n

ISVALIDREPLICATEF

|- !n m s. validAttr (n,m,s) ==> is_valid (WORD (REPLICATE n F),n,m,s)

DEFXP_FXP_REPLICATEF

|- !n m s.
     validAttr (n,m,s) ==>
     (defxp (fxp (WORD (REPLICATE n F),n,m,s)) = (WORD (REPLICATE n F),n,m,s))

FXP_ADD_THM

|- !a b n m s.
     Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
     ~(value a + value b > MAX (n,m,s)) /\
     ~(value a + value b < MIN (n,m,s)) ==>
     Isvalid (FST (fxpAdd (n,m,s) Convergent Clip a b)) /\
     (value (FST (fxpAdd (n,m,s) Convergent Clip a b)) =
      value a + value b +
      fxperror (n,m,s) Convergent Clip (value a + value b))

FXP_SUB_THM

|- !a b n m s.
     Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
     ~(value a - value b > MAX (n,m,s)) /\
     ~(value a - value b < MIN (n,m,s)) ==>
     Isvalid (FST (fxpSub (n,m,s) Convergent Clip a b)) /\
     (value (FST (fxpSub (n,m,s) Convergent Clip a b)) =
      value a - value b +
      fxperror (n,m,s) Convergent Clip (value a - value b))

FXP_MUL_THM

|- !a b n m s.
     Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
     ~(value a * value b > MAX (n,m,s)) /\
     ~(value a * value b < MIN (n,m,s)) ==>
     Isvalid (FST (fxpMul (n,m,s) Convergent Clip a b)) /\
     (value (FST (fxpMul (n,m,s) Convergent Clip a b)) =
      value a * value b +
      fxperror (n,m,s) Convergent Clip (value a * value b))

FXP_DIV_THM

|- !a b n m s.
     Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
     ~(value a / value b > MAX (n,m,s)) /\
     ~(value a / value b < MIN (n,m,s)) /\ ~(value b = 0) ==>
     Isvalid (FST (fxpDiv (n,m,s) Convergent Clip a b)) /\
     (value (FST (fxpDiv (n,m,s) Convergent Clip a b)) =
      value a / value b +
      fxperror (n,m,s) Convergent Clip (value a / value b))

FXP_BOUND_AT_WORST_LEMMA

|- !a x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     Isvalid a /\ (Attrib a = (n,m,s)) ==>
     abs (value (FST (fxp_round (n,m,s) Convergent x Clip)) - x) <=
     abs (value a - x)

FXP_ERROR_AT_WORST_LEMMA

|- !a x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     Isvalid a /\ (Attrib a = (n,m,s)) ==>
     abs (fxperror (n,m,s) Convergent Clip x) <= abs (value a - x)

invfracge0

|- !n m s. 0 <= inv (2 pow fracbits (n,m,s))

invfracgt0

|- !n m s. 0 < inv (2 pow fracbits (n,m,s))

REAL_OF_NUM_GT

|- !m n. & m > & n = m > n

pwvfraclt1

|- !n m s y.
     & y / 2 pow fracbits (n,m,s) < 1 =
     2 pow fracbits (n,m,s) * (& y / 2 pow fracbits (n,m,s)) <
     2 pow fracbits (n,m,s) * 1

pwvfracle11

|- !x n m s.
     x <= (2 pow streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <= 2 pow streamlength (n,m,s) - 1

pwv23le1

|- !x n. & n / 2 pow 23 <= x = 2 pow 23 * (& n / 2 pow 23) <= 2 pow 23 * x

pwv23le11

|- !x n. & n / 2 pow 23 <= x = & n <= 2 pow 23 * x

pwv23lt1

|- !n. & n / 2 pow 23 < 1 = 2 pow 23 * (& n / 2 pow 23) < 2 pow 23 * 1

pwvfraclt11

|- !n m s y. & y / 2 pow fracbits (n,m,s) < 1 = & y < 2 pow fracbits (n,m,s)

pwv23lt11

|- !x. & n / 2 pow 23 < 1 = & n < 2 pow 23

pwvfraclereal

|- !n m s y.
     x < y / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <
     2 pow fracbits (n,m,s) * (y / 2 pow fracbits (n,m,s))

PWFLT_REAL

|- !n m s y.
     x <= y / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <=
     2 pow fracbits (n,m,s) * (y / 2 pow fracbits (n,m,s))

pwvfraclt

|- !n m s y.
     x < & y / 2 pow fracbits (n,m,s) =
     2 pow fracbits (n,m,s) * x <
     2 pow fracbits (n,m,s) * (& y / 2 pow fracbits (n,m,s))

pwv23lt

|- !x. x < & n / 2 pow 23 = 2 pow 23 * x < 2 pow 23 * (& n / 2 pow 23)

pwvexpfraclt

|- !n m s y. y > 2 ** fracbits (n,m,s) = 2 pow fracbits (n,m,s) < & y

pwvexp23lt

|- !n. n > 2 ** 23 = 2 pow 23 < & n

pwvexp23gt

|- !n. n < 2 ** 23 = & n < 2 pow 23

pwvexpfraclt1

|- !n m s x. x < 1 = 2 pow fracbits (n,m,s) * x < 2 pow fracbits (n,m,s) * 1

pwvexp126lt1

|- !x. x < inv (2 pow 126) = 2 pow 126 * x < 2 pow 126 * inv (2 pow 126)

pwvexp126lt11

|- !x. x < inv (2 pow 126) = 2 pow 126 * x < 1

pwvexp23lt1

|- !x. x < 1 = 2 pow 23 * x < 2 pow 23 * 1

pwvexp23lt11

|- !x. x < 1 = 2 pow 23 * x < 2 pow 23

twoone

|- 2 = 1 + 1

opopow

|- !n m s.
     0 < streamlength (n,m,s) ==>
     1 + & (streamlength (n,m,s)) * 1 <= (1 + 1) pow streamlength (n,m,s)

opstream

|- !n m s.
     0 < streamlength (n,m,s) ==> 1 + 0 < 1 + & (streamlength (n,m,s)) * 1

opstream1

|- !n m s.
     0 < streamlength (n,m,s) ==> 1 + 0 < (1 + 1) pow streamlength (n,m,s)

twoexpsl

|- !n m s. validAttr (n,m,s) ==> 1 <= 2 ** streamlength (n,m,s)

otwoexpsl

|- !n m s.
     validAttr (n,m,s) ==>
     (1 + (2 ** streamlength (n,m,s) - 1) = 2 ** streamlength (n,m,s))

otwoexpsl1

|- !n m s.
     validAttr (n,m,s) ==>
     (2 ** streamlength (n,m,s) - 1 + 1 = 2 ** streamlength (n,m,s))

otwoexpsl11

|- !n m s.
     validAttr (n,m,s) ==>
     (2 pow streamlength (n,m,s) - 1 = & (2 ** streamlength (n,m,s) - 1))

s3

|- !n m s.
     (2 pow (streamlength (n,m,s) - 1) - 1) * inv (2 pow fracbits (n,m,s)) <=
     2 pow (streamlength (n,m,s) - 1) * inv (2 pow fracbits (n,m,s))

FXP_ERROR_BOUND_LEMMA1_UNSIGNED

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     is_unsigned (n,m,s) ==>
     ?k.
       k < 2 ** streamlength (n,m,s) /\ & k / 2 pow fracbits (n,m,s) <= x /\
       x < & (SUC k) / 2 pow fracbits (n,m,s)

FXP_ERROR_BOUND_LEMMA2_UNSIGNED

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     is_unsigned (n,m,s) ==>
     ?k.
       k <= 2 ** streamlength (n,m,s) /\
       abs (x - & k / 2 pow fracbits (n,m,s)) <= inv (2 pow fracbits (n,m,s))

REAL_BNVAL_NBWORD

|- !n k. k < 2 ** n ==> (& (BNVAL (NBWORD n k)) = & k)

NOTiIsigned

|- !n m s k.
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ~Isunsigned (fxp (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s))

PWLGSNBW

|- !n k. WORD (NLIST n VB 2 k) IN PWORDLEN n

PWL1

|- WORD [F] IN PWORDLEN 1

BNVAL_WCAT2_SPLIT

|- !n w x.
     w IN PWORDLEN n ==> (BNVAL (WCAT (WORD [x],w)) = BV x * 2 ** n + BNVAL w)

BNVAL_WCATT_NBWORD

|- !n k.
     BNVAL (WCAT (WORD [T],NBWORD (n - 1) k)) =
     BV T * 2 ** (n - 1) + BNVAL (NBWORD (n - 1) k)

BNVAL_WCAT_NBWORD

|- !n k.
     BNVAL (WCAT (WORD [F],NBWORD (n - 1) k)) =
     BV F * 2 ** (n - 1) + BNVAL (NBWORD (n - 1) k)

FXP_ERROR_BOUND_LEMMA3_POS_SIGNED

|- !x n m s.
     0 <= x /\
     x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?w.
       abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
       (WORDLEN w = n)

FXP_ERROR_BOUND_LEMMA3_NEG_SIGNED

|- !x n m s.
     0 <= ~x /\
     ~x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?w.
       abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
       (WORDLEN w = n)

FXP_ERROR_BOUND_LEMMA3_ABS_SIGNED

|- !x n m s.
     abs x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
     ?w.
       abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
       (WORDLEN w = n)

maxmin

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     ~is_unsigned (n,m,s) ==>
     abs x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
     validAttr (n,m,s) /\ ~is_unsigned (n,m,s)

FXP_ERROR_BOUND_LEMMA3_SIGNED

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     ~is_unsigned (n,m,s) ==>
     ?w.
       abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
       (WORDLEN w = n)

FXP_MAIN_ERROR_BOUND_THEOREM_SIGNED

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
     ~is_unsigned (n,m,s) ==>
     abs (fxperror (n,m,s) Convergent Clip x) <= inv (2 pow fracbits (n,m,s))

FXP_MAIN_ERROR_BOUND_THEOREM

|- !x n m s.
     ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) ==>
     abs (fxperror (n,m,s) Convergent Clip x) <= inv (2 pow fracbits (n,m,s))

FXP_ABSOLUTE_ERROR

|- !x X.
     validAttr X /\ representable X x ==>
     ?e. abs e <= inv (2 pow fracbits X) /\ (value (Fxp_round X x) = x + e)

FXP_ADD_ABSOLUTE_THM

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a + value b) ==>
     Isvalid (FxpAdd X a b) /\
     ?e.
       abs e <= inv (2 pow fracbits X) /\
       (value (FxpAdd X a b) = value a + value b + e)

FXP_ADD_ISVALID

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a + value b) ==>
     Isvalid (FxpAdd X a b)

FXP_ADD

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a + value b) ==>
     Isvalid (FxpAdd X a b) /\
     (value (FxpAdd X a b) =
      value a + value b + Fxperror X (value a + value b))

FXP_SUB_ABSOLUTE_THM

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a - value b) ==>
     Isvalid (FxpSub X a b) /\
     ?e.
       abs e <= inv (2 pow fracbits X) /\
       (value (FxpSub X a b) = value a - value b + e)

FXP_SUB_ISVALID

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a - value b) ==>
     Isvalid (FxpSub X a b)

FXP_SUB

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a - value b) ==>
     Isvalid (FxpSub X a b) /\
     (value (FxpSub X a b) =
      value a - value b + Fxperror X (value a - value b))

FXP_MUL_ABSOLUTE_THM

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a * value b) ==>
     Isvalid (FxpMul X a b) /\
     ?e.
       abs e <= inv (2 pow fracbits X) /\
       (value (FxpMul X a b) = value a * value b + e)

FXP_MUL_ISVALID

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a * value b) ==>
     Isvalid (FxpMul X a b)

FXP_MUL

|- !a b X.
     Isvalid a /\ Isvalid b /\ validAttr X /\
     representable X (value a * value b) ==>
     Isvalid (FxpMul X a b) /\
     (value (FxpMul X a b) =
      value a * value b + Fxperror X (value a * value b))