$$$top.pvs
top: THEORY
BEGIN

  IMPORTING div_top, bv_top

END top



$$$exp2_table.pvs
exp2_table: THEORY
  BEGIN

  IMPORTING exp2

  exp2_0: LEMMA exp2(0) = 1

  exp2_1: LEMMA exp2(1) = 2

  exp2_2: LEMMA exp2(2) = 4

  exp2_3: LEMMA exp2(3) = 8

  exp2_4: LEMMA exp2(4) = 16

  exp2_8: LEMMA exp2(8) = 256

  exp2_16: LEMMA exp2(16) = 65536

  END exp2_table



$$$exp2_table.prf
(|exp2_table| (|exp2_0| ""
                        (EXPAND "exp2")
                        (("" (PROPAX) NIL)))
              (|exp2_1| ""
                        (EXPAND "exp2")
                        (("" (EXPAND "exp2")
                             (("" (PROPAX) NIL)))))
              (|exp2_2| ""
                        (EXPAND "exp2")
                        (("" (EXPAND "exp2")
                             (("" (EXPAND "exp2")
                                  (("" (PROPAX) NIL)))))))
              (|exp2_3| ""
                        (EXPAND "exp2")
                        (("" (EXPAND "exp2")
                             (("" (EXPAND "exp2")
                                  (("" (EXPAND "exp2")
                                       (("" (PROPAX) NIL)))))))))
              (|exp2_4| ""
                        (LEMMA "exp2_sum")
                        (("" (INST -1 "2" "2")
                             (("" (LEMMA "exp2_2")
                                  (("" (ASSERT) NIL)))))))
              (|exp2_8| ""
                        (LEMMA "exp2_sum")
                        (("" (INST -1 "4" "4")
                             (("" (LEMMA "exp2_4")
                                  (("" (ASSERT) NIL)))))))
              (|exp2_16| ""
                         (LEMMA "exp2_sum")
                         (("" (INST -1 "8" "8")
                              (("" (LEMMA "exp2_8")
                                   (("" (ASSERT) NIL))))))))

$$$bv_rules.pvs

bv_rules [N: posnat]: THEORY

  BEGIN
  IMPORTING exp2_table, bv_arith_nat, mod_lems

  i, i1, i2: VAR int
  n, k, n1, n2: VAR nat
  m: VAR posnat
  bv: VAR bvec[N]

  % some rules for exp2
  exp2_3: LEMMA exp2(3) = 8
  exp2_16: LEMMA exp2(16) = 65536

  % some rules about mod arithmetic

  mod_mod_lemma: LEMMA mod(mod(i, m), m) = mod(i, m)

  % The following rule characterizes the property that incrementing
  % modulo m wraps around the zero point.  

  mod_wrap_around: LEMMA n < m & (k <= m & k >= m-n) =>
                              mod(n+k, m) = n - (m-k)

  % some properties about bit-vector arithmetic

  word0: bvec[16] = (LAMBDA (i: below(16)): 0)
  word0_nat: LEMMA bv2nat[16](word0) = 0

  IMPORTING bv_nat

  % The following rules normalize expressions involving multiple bit-vector
  % increments and decrements into a cannonical form in which there is a
  % single increment/decrement.

  bv_minus_def: LEMMA bv - i = bv + (-i)
  bv_plus_assoc: LEMMA bv + i1 + i2 = bv + (i1+i2)

  bv_minus_0: LEMMA n=0 => bv + (-n) = bv
  bv_plus_0: LEMMA n=0 => bv + n = bv


  bv2nat_minus: LEMMA i<0 & (-i) <= bv2nat(bv) =>
                    bv2nat(bv + i) = bv2nat(bv) + i

  % The following rules convert the bv2nat of a "bv+n" expression
  % into an expression of bv2nat of bv.

  bv2nat_plus: LEMMA n < (exp2(N) - bv2nat(bv)) =>
                    bv2nat(bv + n) = bv2nat(bv) + n

  % The following rule states the equivalent of the mod-wrap-around,
  % stated above, for bit-vector incrementing.

  bv2nat_plus2: LEMMA n < exp2(N) & bv2nat(bv)+n >= exp2(N) =>
                    bv2nat(bv +  n) = bv2nat(bv) - (exp2(N) - n)


  % The following rules convert (under certain conditions) an
  % equality/disequality checks on bit-vector inc/dec expressions into
  % equality/disequality on integers

  bv_equal_lemma0: LEMMA (bv = bv + i) = (bv + 0 = bv + i)

  bv_equal_lemma1: LEMMA
    0 <= n & n < exp2(N) & 0 <= k & k < exp2(N)
        IMPLIES (bv + n = bv + k) = (n = k)

  bv_equal_lemma2: LEMMA
    0 <= -i1 & -i1 < exp2(N) & 0 <= -i2 & -i2 < exp2(N)
        IMPLIES (bv + i1 = bv + i2) = (i1 = i2)

  bv_equal_lemma3: LEMMA
    0 <= n & n < exp2(N) & 0 < -i1 & -i1 < exp2(N)
      IMPLIES (bv + n = bv + i1) = ((n-i1) = exp2(N))

  END bv_rules

$$$bv_rules.prf
(|bv_rules| (|exp2_3| ""
                      (LEMMA "exp2_table.exp2_3")
                      (("" (PROPAX) NIL)))
            (|exp2_16| ""
                       (LEMMA "exp2_table.exp2_16")
                       (("" (PROPAX) NIL)))
            (|mod_mod_lemma| ""
                             (SKOSIMP*)
                             (("" (LEMMA "mod_of_mod")
                                  (("" (INST -1 "0" "i!1" "m!1")
                                       (("" (ASSERT) NIL)))))))
            (|mod_wrap_around| ""
                               (SKOSIMP*)
                               (("" (LEMMA "mod_wrap_around")
                                    (("" (INST?)
                                         (("" (ASSERT) NIL)))))))
            (|word0_TCC1| "" (TCC) NIL)
            (|word0_nat| ""
                         (LEMMA "bv2nat_bvec0[16]")
                         (("" (EXPAND "word0")
                              (("" (EXPAND "bvec0")
                                   (("" (PROPAX) NIL)))))))
            (|bv_minus_def| ""
                            (SKOSIMP*)
                            (("" (EXPAND "-" 1 1)
                                 (("" (PROPAX) NIL)))))
            (|bv_plus_assoc| ""
                             (SKOSIMP*)
                             (("" (EXPAND "+")
                                  ((""
                                     (CASE
                                       "mod(bv2nat[N](nat2bv[N](mod(bv2nat(bv!1) + i1!1, exp2(N)))) + i2!1,
                 exp2(N))
            = mod(bv2nat[N](bv!1) + i1!1 + i2!1, exp2(N))")
                                     (("1" (ASSERT) NIL)
                                       ("2" (HIDE 2)
                                            (("2"
                                               (CASE
                                                 "bv2nat[N](nat2bv[N](mod(bv2nat(bv!1) + i1!1, exp2(N)))) =
               mod(bv2nat(bv!1) + i1!1, exp2(N))")
                                               (("1" (REPLACE -1)
                                                     (("1" (HIDE -1)
                                                           (("1"
                                                              (LEMMA
                                                                "mod_of_mod")
                                                              (("1"
                                                                 (INST -1
                                                                      "i2!1"
                                                                      "bv2nat(bv!1) + i1!1"
                                                                      "exp2(N)")
                                                                 (("1"
                                                                    (ASSERT)
                                                                    NIL)))))))))
                                                 ("2" (HIDE 2)
                                                      (("2"
                                                         (LEMMA "bv2nat_inv[N]")
                                                         (("2"
                                                            (INST -1
                                                                  "mod(bv2nat(bv!1) + i1!1, exp2(N))")
                                                            (("2" (ASSERT)
                                                                  (("2"
                                                                     (HIDE 2)
                                                                     (("2"
                                                                      (REWRITE
                                                                      "mod_pos")
                                                                      NIL)))))))))))))))
                                       ("3" (ASSERT)
                                            (("3" (REWRITE "mod_pos")
                                                  NIL)))))))))
            (|bv_minus_0| ""
                          (SKOSIMP*)
                          (("" (REPLACE -1)
                               (("" (HIDE -1)
                                    (("" (EXPAND "+")
                                         (("" (LEMMA "mod_lt_nat")
                                              (("" (INST?)
                                                   (("" (ASSERT)
                                                        (("" (REPLACE -1)
                                                             (("" (HIDE -1)
                                                                  ((""
                                                                     (LEMMA
                                                                      "nat2bv_inv[N]")
                                                                     ((""
                                                                      (INST?)
                                                                      NIL)))))))))))))))))))))
            (|bv_plus_0| ""
                         (SKOSIMP*)
                         (("" (EXPAND "+")
                              (("" (REPLACE -1)
                                   (("" (HIDE -1)
                                        (("" (REWRITE "mod_lt_nat")
                                             (("" (REWRITE "nat2bv_inv[N]")
                                                  NIL)))))))))))
            (|bv2nat_minus| ""
                            (SKOSIMP*)
                            (("" (EXPAND "+")
                                 (("" (LEMMA "bv2nat_inv[N]")
                                      (("" (INST?)
                                           (("1" (REPLACE -1)
                                                 (("1" (HIDE -1)
                                                       (("1"
                                                          (REWRITE "mod_lt_nat")
                                                          NIL)))))
                                             ("2" (HIDE 2)
                                                  (("2" (REWRITE "mod_pos")
                                                        NIL)))))))))))
            (|bv2nat_plus| ""
                           (SKOSIMP*)
                           (("" (REWRITE "bv_plus[N]")
                                (("" (REWRITE "mod_lt_nat")
                                     NIL)))))
            (|bv2nat_plus2| ""
                            (SKOSIMP*)
                            (("" (EXPAND "+")
                                 (("" (LEMMA "bv2nat_inv[N]")
                                      (("" (INST?)
                                           (("1" (REPLACE -1)
                                                 (("1" (HIDE -1)
                                                       (("1"
                                                          (LEMMA
                                                            "mod_wrap_around")
                                                          (("1"
                                                             (INST -1
                                                                   "bv2nat(bv!1)"
                                                                   "exp2(N)"
                                                                   "n!1")
                                                             (("1" (SPLIT -1)
                                                                   (("1"
                                                                      (ASSERT)
                                                                      NIL)
                                                                     ("2"
                                                                      (PROPAX)
                                                                      NIL)
                                                                     ("3"
                                                                      (ASSERT)
                                                                      NIL)
                                                                     ("4"
                                                                      (ASSERT)
                                                                      NIL)))))))))))
                                             ("2" (ASSERT)
                                                  (("2" (HIDE 2)
                                                        (("2"
                                                           (REWRITE "mod_pos")
                                                           NIL)))))))))))))
            (|bv_equal_lemma0| ""
                               (SKOSIMP*)
                               (("" (EXPAND "+")
                                    (("" (LEMMA "mod_lt_nat")
                                         ((""
                                            (INST -1
                                                  "exp2(N)"
                                                  "bv2nat(bv!1)")
                                            (("" (ASSERT)
                                                 (("" (REPLACE -1)
                                                      (("" (HIDE -1)
                                                           ((""
                                                              (LEMMA
                                                                "nat2bv_inv[N]")
                                                              (("" (INST?)
                                                                   ((""
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))))))
            (|bv_equal_lemma1| ""
                               (SKOSIMP*)
                               (("" (IFF 1)
                                    (("" (SPLIT 1)
                                         (("1" (FLATTEN)
                                               (("1" (EXPAND "+")
                                                     (("1"
                                                        (LEMMA "nat2bv_bij[N]")
                                                        (("1"
                                                           (EXPAND "bijective?")
                                                           (("1" (FLATTEN)
                                                                 (("1"
                                                                    (HIDE -2)
                                                                    (("1"
                                                                      (EXPAND
                                                                      "injective?")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "mod(bv2nat(bv!1) + n!1, exp2(N))"
                                                                      "mod(bv2nat(bv!1) + k!1, exp2(N))")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      (("1"
                                                                      (HIDE
                                                                      -2)
                                                                      (("1"
                                                                      (LEMMA
                                                                      "mod_inj1")
                                                                      (("1"
                                                                      (INST?)
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))))
                                                                      ("2"
                                                                      (ASSERT)
                                                                      (("2"
                                                                      (HIDE
                                                                      2)
                                                                      (("2"
                                                                      (REWRITE
                                                                      "mod_pos")
                                                                      NIL)))))
                                                                      ("3"
                                                                      (REWRITE
                                                                      "mod_pos")
                                                                      NIL)))))))))))))))))
                                           ("2" (FLATTEN)
                                                (("2" (ASSERT) NIL)))))))))
            (|bv_equal_lemma2| ""
                               (SKOSIMP*)
                               (("" (IFF 1)
                                    (("" (SPLIT 1)
                                         (("1" (FLATTEN)
                                               (("1" (EXPAND "+")
                                                     (("1"
                                                        (LEMMA "nat2bv_bij[N]")
                                                        (("1"
                                                           (EXPAND "bijective?")
                                                           (("1" (FLATTEN)
                                                                 (("1"
                                                                    (HIDE -2)
                                                                    (("1"
                                                                      (EXPAND
                                                                      "injective?")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "mod(bv2nat(bv!1) + i1!1, exp2(N))"
                                                                      "mod(bv2nat(bv!1) + i2!1, exp2(N))")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      (("1"
                                                                      (HIDE
                                                                      -2)
                                                                      (("1"
                                                                      (LEMMA
                                                                      "mod_inj2")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "-i2!1"
                                                                      "exp2(N)"
                                                                      "-i1!1"
                                                                      "bv2nat(bv!1)")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))))
                                                                      ("2"
                                                                      (ASSERT)
                                                                      (("2"
                                                                      (HIDE
                                                                      -1
                                                                      -2
                                                                      -3
                                                                      -4
                                                                      -5
                                                                      2)
                                                                      (("2"
                                                                      (REWRITE
                                                                      "mod_pos")
                                                                      NIL)))))
                                                                      ("3"
                                                                      (HIDE
                                                                      -1
                                                                      -2
                                                                      -3
                                                                      -4
                                                                      -5
                                                                      2)
                                                                      (("3"
                                                                      (REWRITE
                                                                      "mod_pos")
                                                                      NIL)))))))))))))))))))
                                           ("2" (FLATTEN)
                                                (("2" (ASSERT) NIL)))))))))
            (|bv_equal_lemma3| ""
                               (SKOSIMP*)
                               (("" (EXPAND "+")
                                    (("" (LEMMA "nat2bv_bij[N]")
                                         (("" (EXPAND "bijective?")
                                              (("" (FLATTEN)
                                                   (("" (HIDE -2)
                                                        ((""
                                                           (EXPAND "injective?")
                                                           ((""
                                                              (INST -1
                                                                    "mod(bv2nat(bv!1) + n!1, exp2(N))"
                                                                    "mod(bv2nat(bv!1) + i1!1, exp2(N))")
                                                              (("1" (IFF 1)
                                                                    (("1"
                                                                      (SPLIT 1)
                                                                      (("1"
                                                                      (FLATTEN)
                                                                      (("1"
                                                                      (ASSERT)
                                                                      (("1"
                                                                      (HIDE
                                                                      -1)
                                                                      (("1"
                                                                      (LEMMA
                                                                      "mod_wrap_inj")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "n!1"
                                                                      "-i1!1"
                                                                      "exp2(N)"
                                                                      "bv2nat(bv!1)")
                                                                      (("1"
                                                                      (CASE
                                                                      "n!1=0")
                                                                      (("1"
                                                                      (REPLACE
                                                                      -1)
                                                                      (("1"
                                                                      (HIDE
                                                                      -1)
                                                                      (("1"
                                                                      (HIDE
                                                                      -1)
                                                                      (("1"
                                                                      (REWRITE
                                                                      "mod_lt_nat")
                                                                      (("1"
                                                                      (LEMMA
                                                                      "mod_lt")
                                                                      (("1"
                                                                      (INST?)
                                                                      (("1"
                                                                      (EXPAND
                                                                      "abs")
                                                                      (("1"
                                                                      (EXPAND
                                                                      "sgn")
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))))))
                                                                      ("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))
                                                                      ("2"
                                                                      (FLATTEN)
                                                                      (("2"
                                                                      (ASSERT)
                                                                      (("2"
                                                                      (CASE-REPLACE
                                                                      "i1!1 =  n!1 - exp2(N)")
                                                                      (("1"
                                                                      (HIDE
                                                                      -1
                                                                      -2)
                                                                      (("1"
                                                                      (LEMMA
                                                                      "mod_sum")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "bv2nat(bv!1) + n!1 - exp2(N)"
                                                                      "exp2(N)"
                                                                      "1")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))
                                                                      ("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))
                                                                ("2" (ASSERT)
                                                                     (("2"
                                                                      (HIDE
                                                                      -1
                                                                      -2
                                                                      -3
                                                                      -4
                                                                      2)
                                                                      (("2"
                                                                      (REWRITE
                                                                      "mod_pos")
                                                                      NIL)))))
                                                                ("3"
                                                                  (HIDE -1
                                                                      -2
                                                                      -3
                                                                      -4
                                                                      2)
                                                                  (("3"
                                                                     (REWRITE
                                                                      "mod_pos")
                                                                     NIL))))))))))))))))))))
$$$bv_select.pvs
bv_select[n:posnat, l:posnat ]: THEORY
%------------------------------------------------------------------------
% The bit vector binary ops restricted theory defines functions that 
% take two bit vectors as their primary inputs where the second bit
% must be smaller or the same size as the first bit vector. The theory
% is instantiated with the sizes of the two bit vectors.
%------------------------------------------------------------------------
BEGIN

  ASSUMING
    leq: ASSUMPTION l <= n
  ENDASSUMING

  IMPORTING bv_arithmetic

  ii: VAR below(n)

  %------------------------------------------------------------------------
  % Bv_select selects bits s+l-1 to s of a bit vector.
  %------------------------------------------------------------------------
    
  bv_select(bvn: bvec[n], s: upto(n-l)): bvec[l] = bvn^(s+l-1,s)

  %------------------------------------------------------------------------
  % Bv_assign replaces bits s+l-1 to s of a bit vector.
  %------------------------------------------------------------------------
    
  bv_assign(bvn: bvec[n], s: upto(n-l), bvl: bvec[l]): bvec[n] =
        (LAMBDA ii: IF ii >= s AND ii <= s+l-1 
                    THEN bvl(ii-s) ELSE bvn(ii) ENDIF)

% === Some Lemmas =========================================================

  i,j: VAR below(n)
  bvn: VAR bvec[n]
  s : VAR upto(n-l)

  select_2step:  LEMMA i >= j IMPLIES bvn^(i,j) = (bvn^(i, 0))^(i,j)

  bv_select_lem: LEMMA bv2nat(bv_select(bvn,s)) 
                       = div(mod(bv2nat(bvn),exp2(s+l)), exp2(s))

  bv_assign_lem: LEMMA bv_assign(bvn,s,bv_select(bvn,s)) = bvn 

  caret_i_lem  : LEMMA bvn^ii = bv2nat[1](bvn^(ii,ii))

END bv_select

$$$bv_select.prf
(|bv_select| (|bv_select_TCC1| "" (SUBTYPE-TCC) NIL)
 (|bv_select_TCC2| "" (SUBTYPE-TCC) NIL)
 (|bv_assign_TCC1| "" (SUBTYPE-TCC) NIL)
 (|s_TCC1| "" (USE "leq") (("" (ASSERT) NIL)))
 (|select_2step_TCC1| "" (SUBTYPE-TCC) NIL)
 (|select_2step_TCC2| "" (SUBTYPE-TCC) NIL)
 (|select_2step_TCC3| "" (SUBTYPE-TCC) NIL)
 (|select_2step_TCC4| "" (SUBTYPE-TCC) NIL)
 (|select_2step_TCC5| "" (SUBTYPE-TCC) NIL)
 (|select_2step| "" (SKOSIMP) (("" (EXPAND "^") (("" (PROPAX) NIL)))))
 (|bv_select_lem| "" (SKOSIMP*)
  (("" (EXPAND "bv_select")
    (("" (LEMMA "select_2step")
      (("" (INST?)
        (("1" (ASSERT)
          (("1" (REPLACE -1)
            (("1" (HIDE -1)
              (("1" (LEMMA "bv_shift[s!1+l]")
                (("1" (INST?)
                  (("1" (REPLACE -1)
                    (("1" (HIDE -1)
                      (("1" (LEMMA "bv_bottom[n]")
                        (("1" (INST?)
                          (("1" (REPLACE -1)
                            (("1" (ASSERT) NIL)))))))))))))))))))))
         ("2" (ASSERT) NIL) ("3" (ASSERT) NIL)))))))))
 (|bv_assign_lem| "" (SKOLEM 1 ("bvn!1" "s!1"))
  (("" (EXPAND "bv_select")
    (("" (EXPAND "bv_assign")
      (("" (APPLY-EXTENSIONALITY 1)
        (("1" (HIDE 2)
          (("1" (LIFT-IF 1)
            (("1" (SPLIT 1)
              (("1" (FLATTEN)
                (("1" (EXPAND "^") (("1" (PROPAX) NIL)))))
               ("2" (FLATTEN) (("2" (PROPAX) NIL)))))))))
         ("2" (HIDE 2)
          (("2" (SKOLEM 1 ("jj!1"))
            (("2" (FLATTEN) (("2" (ASSERT) NIL)))))))
         ("3" (HIDE 2) (("3" (SKOSIMP) (("3" (ASSERT) NIL)))))
         ("4" (HIDE 2) (("4" (SKOSIMP) (("4" (ASSERT) NIL)))))))))))))
 (|caret_i_lem_TCC1| "" (SUBTYPE-TCC) NIL)
 (|caret_i_lem| "" (GRIND) NIL))

$$$bv_bitwise_lems.pvs
bv_bitwise_lems [N: nat] : THEORY
BEGIN

  IMPORTING bv_bitwise, bv_extractors[N]

  bv, bv1, bv2: VAR bvec[N]
  sel_pair: TYPE = [i1: below(N), upto(i1)]
  sp: VAR sel_pair

  bv_OR     : LEMMA (bv1 OR bv2)^sp = (bv1^sp OR bv2^sp)

  bv_AND    : LEMMA (bv1 AND bv2)^sp = (bv1^sp AND bv2^sp)

  bv_IFF    : LEMMA (bv1 IFF bv2)^sp = (bv1^sp IFF bv2^sp)

  bv_XOR    : LEMMA XOR(bv1,bv2)^sp = XOR(bv1^sp,bv2^sp)

  bv_NOT    : LEMMA (NOT bv)^sp = NOT(bv^sp)

END bv_bitwise_lems

$$$bv_bitwise_lems.prf
(|bv_bitwise_lems| (|bv_OR_TCC1| "" (GRIND) NIL)
                   (|bv_OR| ""
                            (SKOLEM 1
                                    ("bv1!1" "bv2!1" "sp!1"))
                            (("" (EXPAND "^")
                                 (("" (EXPAND "OR")
                                      (("" (PROPAX) NIL)))))))
                   (|bv_AND| ""
                             (SKOLEM 1
                                     ("bv1!1" "bv2!1" "sp!1"))
                             (("" (EXPAND "AND")
                                  (("" (EXPAND "^")
                                       (("" (PROPAX) NIL)))))))
                   (|bv_IFF| ""
                             (SKOLEM 1
                                     ("bv1!1" "bv2!1" "sp!1"))
                             (("" (EXPAND "IFF")
                                  (("" (EXPAND "^")
                                       (("" (PROPAX) NIL)))))))
                   (|bv_XOR| ""
                             (SKOSIMP*)
                             (("" (EXPAND "XOR")
                                  (("" (EXPAND "^")
                                       (("" (PROPAX) NIL)))))))
                   (|bv_NOT| ""
                             (SKOLEM 1
                                     ("bvn!1" "sp!1"))
                             (("" (EXPAND "NOT")
                                  (("" (EXPAND "^")
                                       (("" (PROPAX) NIL))))))))
$$$bv_arith_nat.pvs
bv_arith_nat[N: nat]: THEORY
%------------------------------------------------------------------------
% Defines functions over bit vectors interpreted as natural numbers.
%
%    Introduces:
%
%         > :  bv1 > bv2
%         >=:  bv1 >= bv2
%         < :  bv1 < bv2
%         <=:  bv1 <= bv1
%         + :  bv1 + i
%         - :  bv1 - i
%         + :  bv1 + bv2
%         * :  bv1 * bv2
%         carryout: [bvec, bvec -> bvec[1]] 
%   
%------------------------------------------------------------------------

  BEGIN

  IMPORTING bv_nat[N], mod

  % ----------------------------------------------------------------------
  % Definition of inequalities over the bit vectors.
  % ----------------------------------------------------------------------

  < (bv1: bvec, bv2: bvec): bool = bv2nat(bv1) <  bv2nat(bv2) ;
  <=(bv1: bvec, bv2: bvec): bool = bv2nat(bv1) <= bv2nat(bv2) ;

  > (bv1: bvec, bv2: bvec): bool = bv2nat(bv1) >  bv2nat(bv2) ;
  >=(bv1: bvec, bv2: bvec): bool = bv2nat(bv1) >= bv2nat(bv2) ;

  % ----------------------------------------------------------------------
  % Increments a bit vector by a integer modulo 2**N.
  % ----------------------------------------------------------------------

  +(bv: bvec, i: int): bvec = nat2bv(mod(bv2nat(bv) + i, exp2(N))) ;

  % ----------------------------------------------------------------------
  % Decrements a bit vector by a integer modulo 2**N.
  % ----------------------------------------------------------------------

  -(bv: bvec,i: int): bvec = bv + (-i) ;

  % ----------------------------------------------------------------------
  % Addition of two bit vectors interpreted as natural numbers.
  % ----------------------------------------------------------------------

  +(bv1: bvec, bv2: bvec): bvec = 
       IF bv2nat(bv1) + bv2nat(bv2) < exp2(N)
       THEN nat2bv(bv2nat(bv1) + bv2nat(bv2))
       ELSE nat2bv(bv2nat(bv1) + bv2nat(bv2) - exp2(N)) 
       ENDIF ;

% ========= Properties of these functions ================================

  i            : VAR int
  n            : VAR below(N)
  bv, bv1, bv2 : VAR bvec

  bv_smallest  : LEMMA (FORALL bv: bv >= bvec0)
  bv_greatest  : LEMMA (FORALL bv: bv <= bvec1)

  bv_plus      : LEMMA bv2nat(bv + i) = mod(bv2nat(bv) + i, exp2(N))

  bv_plus1     : LEMMA bv2nat(bv + 1) = IF bv2nat(bv) = (exp2(N)-1) THEN 0
                                        ELSE bv2nat(bv) + 1 ENDIF 

  bv_minus     : LEMMA bv2nat(bv - i) = mod(bv2nat(bv) - i, exp2(N))

  bv_minus1    : LEMMA bv2nat(bv - 1) = IF bv2nat(bv) = 0 THEN exp2(N)-1
                                        ELSE bv2nat(bv) - 1 ENDIF

  bv_minus_plus: LEMMA (bv-1)+1 = bv
  bv_plus_minus: LEMMA (bv+1)-1 = bv 

  bv_add       : LEMMA bv2nat(bv1 + bv2) =
			  IF bv2nat(bv1) + bv2nat(bv2) < exp2(N)
			  THEN bv2nat(bv1) + bv2nat(bv2)
			  ELSE bv2nat(bv1) + bv2nat(bv2) - exp2(N) ENDIF 

  bv_addcomm   : THEOREM bv1 + bv2 = bv2 + bv1

% ================== Additional functions ================================

  IMPORTING bv_nat

  % ----------------------------------------------------------------------
  % The operator * denotes unsigned multiplication two n-bit bvecs.
  % ----------------------------------------------------------------------

  *(bv1: bvec[N], bv2: bvec[N]): bvec[2*N] 
       = nat2bv[2*N](bv2nat(bv1) * bv2nat(bv2)) ;


  m1,  m2      : VAR nat   
  mult_lem     : LEMMA m1 < exp2(N) AND m2 < exp2(N)
                         IMPLIES m1 * m2 < exp2(2 * N)

  bv_mult      : LEMMA bv2nat(bv1 * bv2) = bv2nat(bv1) * bv2nat(bv2) 

  % ----------------------------------------------------------------------
  % Function carryout returns a bvec[1].  The value of the bit is 1 iff the
  % addition of two bit vectors yields a carry out of the msb position.
  % ----------------------------------------------------------------------
 
  carryout(bv1: bvec, bv2: bvec, Cin: bvec[1]): bvec[1] =
      (LAMBDA (bb: below(1)):
           bool2bit(bv2nat(bv1) + bv2nat(bv2) + bv2nat(Cin) >= exp2(N))) ;

END bv_arith_nat

$$$bv_arith_nat.prf
(|bv_arith_nat| (|plus_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|bv_smallest| "" (EXPAND ">=")
  (("" (SKOLEM 1 ("bv!1"))
    (("" (ASSERT) (("" (LEMMA "bv2nat_bvec0") (("" (ASSERT) NIL)))))))))
 (|bv_greatest| "" (EXPAND "<=")
  (("" (LEMMA "bv2nat_bvec1")
    (("" (SKOLEM 1 ("bv!1")) (("" (ASSERT) NIL)))))))
 (|bv_plus| "" (SKOLEM!)
  (("" (EXPAND "+" 1 1) (("" (LEMMA "bv2nat_inv") (("" (INST?) NIL)))))))
 (|bv_plus1| "" (SKOLEM!)
  (("" (REWRITE "bv_plus")
    (("" (EXPAND "mod")
      (("" (LIFT-IF)
        (("" (GROUND)
          (("" (REWRITE "floor_small")
            (("1" (LIFT-IF)
              (("1" (ASSERT)
                (("1" (PROP)
                  (("1" (ASSERT) (("1" (REWRITE "pos_div_ge") NIL)))))))))
             ("2" (EXPAND "abs") (("2" (ASSERT) NIL)))))))))))))))
 (|bv_minus| "" (EXPAND "-")
  (("" (SKOSIMP*) (("" (REWRITE "bv_plus") (("" (ASSERT) NIL)))))))
 (|bv_minus1| "" (SKOSIMP*)
  (("" (REWRITE "bv_minus")
    (("" (LIFT-IF)
      (("" (GROUND)
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (CASE "N=0")
              (("1" (REPLACE -1)
                (("1" (EXPAND "exp2")
                  (("1" (EXPAND "mod") (("1" (ASSERT) NIL)))))))
               ("2" (REWRITE "mod_lt")
                (("1" (EXPAND "sgn") (("1" (PROPAX) NIL)))
                 ("2" (EXPAND "abs")
                  (("2" (HIDE 3)
                    (("2" (EXPAND "exp2") (("2" (ASSERT) NIL)))))))))))))))
         ("2" (REWRITE "mod_lt_nat") NIL)))))))))
 (|bv_minus_plus| "" (SKOSIMP *)
  (("" (LEMMA "bv2nat_inj")
    (("" (EXPAND "injective?")
      (("" (INST?)
        (("" (ASSERT)
          (("" (HIDE 2)
            (("" (LEMMA "bv_minus1")
              (("" (INST?)
                (("" (LEMMA "bv_plus1")
                  (("" (INST?)
                    (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))))))))))))))
 (|bv_plus_minus| "" (SKOLEM!)
  (("" (LEMMA "bv2nat_inj")
    (("" (EXPAND "injective?")
      (("" (INST?)
        (("" (ASSERT)
          (("" (HIDE 2)
            (("" (LEMMA "bv_plus1")
              (("" (INST?)
                (("" (LEMMA "bv_minus1")
                  (("" (INST?)
                    (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))))))))))))))
 (|bv_add| "" (SKOLEM!)
  (("" (EXPAND "+")
    (("" (LEMMA "bv2nat_inv")
      (("" (LIFT-IF)
        (("" (GROUND) (("1" (INST?) NIL) ("2" (INST?) NIL)))))))))))
 (|bv_addcomm| "" (SKOSIMP*) (("" (EXPAND "+") (("" (PROPAX) NIL)))))
 (|times_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "exp2_sum")
    (("" (INST -1 "N" "N")
      (("" (REPLACE -1)
        (("" (HIDE -1)
          (("" (TYPEPRED "bv2nat[N](bv1!1)")
            (("" (TYPEPRED "bv2nat[N](bv2!1)")
              (("" (LEMMA "lt_times_lt_pos1")
                (("" (INST?)
                  (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)
                   ("3" (ASSERT) NIL)))))))))))))))))))
 (|mult_lem| "" (SKOSIMP*)
  (("" (LEMMA "exp2_sum")
    (("" (INST - "N" "N")
      (("" (REPLACE -1)
        (("" (CASE "forall (l,m,n:nat): l l*m bvec] 
%         - : [bvec, bvec -> bvec]
%         overflow    : [bvec, bvec -> bool]  
%         underflow   : [bvec, bvec -> bool]  
%   
%------------------------------------------------------------------------

  BEGIN

  IMPORTING bv_int[N], bv_arith_shift[N]

  bv, bv1, bv2 : VAR bvec

  % ----------------------------------------------------------------------
  % 2's complement negation of a bit vector
  % ----------------------------------------------------------------------
    
  -(bv: bvec): bvec = int2bv( IF bv2int(bv) = minint THEN bv2int(bv)
                              ELSE -(bv2int(bv)) ENDIF ) ;

  % ----------------------------------------------------------------------
  % 2's complement subtraction of two bit vectors
  % ----------------------------------------------------------------------
    
  -(bv1, bv2): bvec = (bv1 + (-bv2))

  % ----------------------------------------------------------------------
  % Define conditions for 2's complement overflow 
  % ----------------------------------------------------------------------
    
  overflow(bv1,bv2): bool = (bv2int(bv1) + bv2int(bv2)) > maxint
                             OR (bv2int(bv1) + bv2int(bv2)) < minint 

% === Properties of these additional functions ================================

  % ----------------------------------------------------------------------
  % If the result is in the range of 2s complement integers, addition of
  % two bit vectors is the same as for a natural number interpretation
  % ----------------------------------------------------------------------
   
  intaddlem  : THEOREM in_rng_2s_comp(bv2int(bv1) + bv2int(bv2))
                         IMPLIES bv2int(bv1 + bv2) = bv2int(bv1) + bv2int(bv2)  
    
  unaryminus : LEMMA bv2int(-bv) = IF bv2int(bv) = minint THEN bv2int(bv)
                                   ELSE -(bv2int(bv)) ENDIF 

  minus1lem  : LEMMA bv2int(bv1) > minint AND bv2int(bv) = 1 
                       IMPLIES bv2int(bv1 - bv) = bv2int(bv1) - 1

  IMPORTING bv_bitwise[N]
 
  n          : VAR upto(N)
   
  compl_max  : THEOREM bv2nat_rec(n, bv) + bv2nat_rec(n, NOT bv) 
                          = exp2(n) - 1
    
  % ----------------------------------------------------------------------
  % The 2s complement of a number is its 1s complement + 1
  % ----------------------------------------------------------------------

  twos_compl  : THEOREM -bv2int(bv) = bv2int(NOT bv) + 1;

END bv_arithmetic

$$$bv_arithmetic.prf
(|bv_arithmetic|
 (|difference_TCC1| "" (SKOLEM 1 ("bv!1"))
  (("" (FLATTEN)
    (("" (TYPEPRED "bv2int(bv!1)")
      (("" (ASSERT)
        (("" (EXPAND "minint")
          (("" (EXPAND "maxint") (("" (ASSERT) NIL)))))))))))))
 (|intaddlem| "" (SKOSIMP*)
  (("" (AUTO-REWRITE "bv2int_lem")
    (("" (EXPAND "in_rng_2s_comp")
      (("" (EXPAND "maxint")
        (("" (EXPAND "minint")
          (("" (ASSERT)
            (("" (EXPAND "+")
              (("" (LIFT-IF)
                (("" (LEMMA "bv2nat_top_bit")
                  (("" (INST -1 "bv1!1")
                    (("" (LEMMA "bv2nat_top_bit")
                      (("" (INST -1 "bv2!1")
                        (("" (SPLIT -1)
                          (("1" (SPLIT -2)
                            (("1"
                              (FLATTEN)
                              (("1"
                                (SPLIT 1)
                                (("1"
                                  (FLATTEN)
                                  (("1"
                                    (LEMMA "bv2nat_inv")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (LEMMA "bv2nat_top_bit")
                                        (("1"
                                          (INST
                                           -1
                                           "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1))")
                                          (("1"
                                            (SPLIT -1)
                                            (("1"
                                              (FLATTEN)
                                              (("1" (ASSERT) NIL)))
                                             ("2"
                                              (FLATTEN)
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))
                                 ("2"
                                  (FLATTEN)
                                  (("2"
                                    (EXPAND "exp2" 1)
                                    (("2" (ASSERT) NIL)))))))))
                             ("2"
                              (FLATTEN)
                              (("2"
                                (SPLIT 2)
                                (("1"
                                  (FLATTEN)
                                  (("1"
                                    (LEMMA "bv2nat_inv")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (LEMMA "bv2nat_top_bit")
                                        (("1"
                                          (INST
                                           -1
                                           "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1))")
                                          (("1"
                                            (SPLIT -1)
                                            (("1"
                                              (FLATTEN)
                                              (("1" (ASSERT) NIL)))
                                             ("2"
                                              (FLATTEN)
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))
                                 ("2"
                                  (FLATTEN)
                                  (("2"
                                    (LEMMA "bv2nat_inv")
                                    (("2"
                                      (INST?)
                                      (("1"
                                        (LEMMA "bv2nat_top_bit")
                                        (("1"
                                          (INST
                                           -1
                                           "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1) - exp2(N))")
                                          (("1"
                                            (SPLIT -1)
                                            (("1"
                                              (FLATTEN)
                                              (("1"
                                                (EXPAND "exp2" -1 1)
                                                (("1"
                                                  (EXPAND "exp2" 1)
                                                  (("1"
                                                    (ASSERT)
                                                    NIL)))))))
                                             ("2"
                                              (FLATTEN)
                                              (("2" (ASSERT) NIL)))))
                                           ("2" (ASSERT) NIL)))))
                                       ("2" (ASSERT) NIL)))))))))))))
                           ("2" (FLATTEN)
                            (("2"
                              (SPLIT -2)
                              (("1"
                                (FLATTEN)
                                (("1"
                                  (SPLIT 2)
                                  (("1"
                                    (FLATTEN)
                                    (("1"
                                      (LEMMA "bv2nat_inv")
                                      (("1"
                                        (INST?)
                                        (("1"
                                          (LEMMA "bv2nat_top_bit")
                                          (("1"
                                            (INST
                                             -1
                                             "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1))")
                                            (("1"
                                              (SPLIT -1)
                                              (("1"
                                                (FLATTEN)
                                                (("1" (ASSERT) NIL)))
                                               ("2"
                                                (FLATTEN)
                                                (("2"
                                                  (ASSERT)
                                                  NIL)))))))))))))))
                                   ("2"
                                    (FLATTEN)
                                    (("2"
                                      (LEMMA "bv2nat_inv")
                                      (("2"
                                        (INST?)
                                        (("1"
                                          (LEMMA "bv2nat_top_bit")
                                          (("1"
                                            (INST
                                             -1
                                             "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1) - exp2(N))")
                                            (("1"
                                              (SPLIT -1)
                                              (("1" (ASSERT) NIL)
                                               ("2"
                                                (FLATTEN)
                                                (("2"
                                                  (REPLACE -2)
                                                  (("2"
                                                    (HIDE -1 -2)
                                                    (("2"
                                                      (REPLACE -2)
                                                      (("2"
                                                        (REPLACE -3)
                                                        (("2"
                                                          (HIDE
                                                           -2
                                                           -3)
                                                          (("2"
                                                            (ASSERT)
                                                            NIL)))))))))))))))
                                             ("2"
                                              (HIDE -1)
                                              (("2"
                                                (REPLACE -2)
                                                (("2"
                                                  (REPLACE -3)
                                                  (("2"
                                                    (HIDE -2 -3)
                                                    (("2"
                                                      (ASSERT)
                                                      NIL)))))))))))))
                                         ("2"
                                          (REPLACE -2)
                                          (("2"
                                            (REPLACE -3)
                                            (("2"
                                              (HIDE -2 -3)
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))))
                               ("2"
                                (FLATTEN)
                                (("2"
                                  (LEMMA "bv2nat_inv")
                                  (("2"
                                    (SPLIT 3)
                                    (("1"
                                      (FLATTEN)
                                      (("1"
                                        (EXPAND "exp2" -1)
                                        (("1" (ASSERT) NIL)))))
                                     ("2"
                                      (FLATTEN)
                                      (("2"
                                        (INST?)
                                        (("1"
                                          (LEMMA "bv2nat_top_bit")
                                          (("1"
                                            (INST
                                             -1
                                             "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1) - exp2(N))")
                                            (("1"
                                              (CASE
                                               "exp2(N) = 2*exp2(N-1)")
                                              (("1" (ASSERT) NIL)
                                               ("2"
                                                (HIDE
                                                 -1
                                                 -2
                                                 -3
                                                 -4
                                                 -5
                                                 -6
                                                 2
                                                 3
                                                 4
                                                 5)
                                                (("2"
                                                  (EXPAND "exp2" 1 1)
                                                  (("2"
                                                    (PROPAX)
                                                    NIL)))))))
                                             ("2" (ASSERT) NIL)))))
                                         ("2"
                                          (ASSERT)
                                          NIL)))))))))))))))))))))))))))))))))))))))))
 (|unaryminus| "" (SKOLEM 1 ("bv!1"))
  (("" (EXPAND "-" 1 1)
    (("" (CASE " bv2int(bv!1) = minint")
      (("1" (ASSERT)
        (("1" (LEMMA "bv2int_inv") (("1" (INST?) NIL)))))
       ("2" (ASSERT)
        (("2" (LEMMA "bv2int_inv")
          (("2" (INST?)
            (("2" (ASSERT)
              (("2" (TYPEPRED "bv2int(bv!1)")
                (("2" (EXPAND "minint")
                  (("2" (EXPAND "maxint")
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|minus1lem| "" (SKOLEM 1 ("bv!1" "bv1!1"))
  (("" (FLATTEN)
    (("" (EXPAND "-" 1 1)
      (("" (LEMMA "unaryminus")
        (("" (INST?)
          (("" (EXPAND "minint")
            (("" (ASSERT)
              (("" (ASSERT)
                (("" (LEMMA "intaddlem")
                  (("" (INST?)
                    (("" (EXPAND "in_rng_2s_comp")
                      (("" (REPLACE -3)
                        (("" (EXPAND "minint")
                          (("" (ASSERT)
                            NIL)))))))))))))))))))))))))))
 (|compl_max| "" (INDUCT "n")
  (("1" (TCC) NIL)
   ("2" (SKOSIMP*)
    (("2" (ASSERT)
      (("2" (EXPAND "bv2nat_rec" +)
        (("2" (INST - "bv!1")
          (("2" (HIDE -1) (("2" (TCC) NIL)))))))))))))
 (|twos_compl| "" (SKOSIMP*)
  (("" (LEMMA "compl_max")
    (("" (AUTO-REWRITE "bv2int_lem")
      (("" (DO-REWRITE)
        (("" (EXPAND "bv2nat")
          (("" (INST?)
            (("" (EXPAND "NOT")
              (("" (EXPAND "NOT")
                (("" (ASSERT)
                  (("" (LIFT-IF)
                    (("" (GROUND) NIL))))))))))))))))))))))
$$$bv_extend.pvs
bv_extend [N: posnat] : THEORY
% -----------------------------------------------------------------------  
%    Introduces:
%	zero_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%	sign_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%	zero_extend_lsend: [k: above(N) -> [bvec[N] -> bvec[l]]]
%	lsb_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%   
% -----------------------------------------------------------------------  

BEGIN

  IMPORTING bv_extractors, bv_concat
    
  bv: VAR bvec[N]
  k: VAR above(N)
  
  %------------------------------------------------------------------------
  % zero_extend returns a function that extends a bit vector to length k 
  % such that its interpretation as a natural number remains unchanged.
  % That is, it fills 0's at the most significant positions.
  %------------------------------------------------------------------------

  zero_extend(k: above(N)): [bvec[N] -> bvec[k]] =
       (LAMBDA bv: bvec0[k-N] o bv)

  %------------------------------------------------------------------------
  % sign_extend returns a function that extends a bit vector to length k
  % by repeating the most significant bit of the given bit vector.
  % The set above(N) contains nat numbers greater than n.
  %------------------------------------------------------------------------

  sign_extend(k: above(N)): [bvec[N] -> bvec[k]] =
       (LAMBDA bv:  IF bv(N-1) = 1 THEN bvec1[k-N] o bv
                    ELSE bvec0[k-N] o bv ENDIF)

  %------------------------------------------------------------------------
  % zero_extend_lsend returns a function that extends a bit vector to
  % length k by padding 0's at the least significant end of bvec.
  % That is, the bv2nat interpretation of the argument increases by 2**(k-N)
  %------------------------------------------------------------------------
    
  zero_extend_lsend(k: above(N)): [bvec[N] -> bvec[k]] =
        (LAMBDA bv:  bv o bvec0[k-N])
  
  %------------------------------------------------------------------------
  % lsb_extend returns a function that extends a bit vector to
  % length k by repeating the lsb of the bit vector at its
  % least significant end.
  %------------------------------------------------------------------------
    
  lsb_extend(k: above(N)): [bvec[N] -> bvec[k]] =
       (LAMBDA bv:  IF bv^0 = 0 THEN bv o bvec0[k-N]
                    ELSE bv o bvec1[k-N] ENDIF)


% ======= Useful theorems =================================================

  IMPORTING bv_bitwise, bv_arithmetic

  zero_extend_lem  : THEOREM bv2nat[k](zero_extend(k)(bv)) = bv2nat(bv)

  sign_to_zero     : THEOREM sign_extend(k)(bv) =
			       IF bv(N-1) = 1 THEN NOT(zero_extend(k)(NOT(bv)))
			       ELSE zero_extend(k)(bv)
			       ENDIF

  sign_extend_lem  : THEOREM bv2int[k](sign_extend(k)(bv)) = bv2int(bv)

  zero_extend_lsend: THEOREM bv2nat(zero_extend_lsend(k)(bv)) 
                               = bv2nat(bv) * exp2(k-N)

END bv_extend

$$$bv_extend.prf
(|bv_extend| (|zero_extend_TCC1| "" (GRIND) NIL)
 (|zero_extend_TCC2| "" (TCC :DEFS !) NIL)
 (|sign_extend_TCC1| "" (GROUND) NIL)
 (|sign_extend_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|sign_extend_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|lsb_extend_TCC1| "" (GROUND) NIL)
 (|lsb_extend_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|lsb_extend_TCC3| "" (AUTO-REWRITE "bv_extractors.^" "bit.islow")
  (("" (GROUND) NIL)))
 (|zero_extend_lem| "" (SKOSIMP*)
  (("" (EXPAND "zero_extend")
    (("" (REWRITE "bvconcat2nat[k!1-N,N]")
      (("" (LEMMA "bv2nat_bvec0[k!1-N]") (("" (ASSERT) NIL)))))))))
 (|sign_to_zero_TCC1| "" (SUBTYPE-TCC) NIL)
 (|sign_to_zero| "" (SKOLEM 1 ("bv!1" "k!1"))
  (("" (EXPAND "sign_extend")
    (("" (EXPAND "zero_extend")
      (("" (LIFT-IF 1)
        (("" (SPLIT 1)
          (("1" (FLATTEN)
            (("1" (EXPAND "NOT")
              (("1" (EXPAND "NOT")
                (("1" (EXPAND "o ")
                  (("1" (EXPAND "bvec1")
                    (("1" (EXPAND "bvec0")
                      (("1" (APPLY-EXTENSIONALITY 1)
                        (("1" (HIDE 2)
                          (("1" (LIFT-IF 1)
                            (("1" (SPLIT 1)
                              (("1" (FLATTEN)
                                (("1" (ASSERT)
                                  (("1" (LIFT-IF 1) (("1" (ASSERT) NIL)))))))
                               ("2" (FLATTEN)
                                (("2" (PROPAX) NIL)))))))))))))))))))))))
           ("2" (FLATTEN) (("2" (PROPAX) NIL)))))))))))))
 (|sign_extend_lem_TCC1| "" (SKOSIMP*)
  (("" (TYPEPRED "k!1") (("" (ASSERT) NIL)))))
 (|sign_extend_lem| "" (SKOSIMP*)
  (("" (REWRITE "sign_to_zero")
    (("" (LIFT-IF)
      (("" (SPLIT 1)
        (("1" (FLATTEN)
          (("1" (LEMMA "twos_compl[k!1]")
            (("1" (INST -1 "NOT (zero_extend(k!1)(NOT bv!1))")
              (("1" (ASSERT)
                (("1"
                  (CASE "bv2int(NOT (zero_extend(k!1)(NOT bv!1)))
        = -bv2int(zero_extend(k!1)(NOT bv!1)) - 1")
                  (("1" (HIDE -2)
                    (("1" (REPLACE -1)
                      (("1" (HIDE -1)
                        (("1"
                          (CASE "bv2nat(zero_extend(k!1)(NOT bv!1)) =
             bv2nat(NOT bv!1)")
                          (("1" (LEMMA "bv2int_lem[k!1]")
                            (("1" (INST?)
                              (("1" (REPLACE -1 1)
                                (("1" (HIDE -1)
                                  (("1" (REPLACE -1)
                                    (("1" (HIDE -1)
                                      (("1"
                                        (CASE
                                         "zero_extend(k!1)(NOT bv!1)(k!1 - 1) = 0")
                                        (("1"
                                          (REPLACE -1)
                                          (("1"
                                            (HIDE -1)
                                            (("1"
                                              (LEMMA "twos_compl[N]")
                                              (("1"
                                                (INST?)
                                                (("1"
                                                  (LEMMA "bv2int_lem[N]")
                                                  (("1"
                                                    (INST?)
                                                    (("1"
                                                      (REPLACE -1)
                                                      (("1"
                                                        (HIDE -1)
                                                        (("1"
                                                          (LEMMA
                                                           "bv2int_lem[N]")
                                                          (("1"
                                                            (INST
                                                             -1
                                                             "NOT bv!1")
                                                            (("1"
                                                              (REPLACE -1)
                                                              (("1"
                                                                (HIDE -1)
                                                                (("1"
                                                                  (REPLACE -2)
                                                                  (("1"
                                                                    (CASE
                                                                     "(NOT bv!1)(N - 1) = 0")
                                                                    (("1"
                                                                      (ASSERT)
                                                                      NIL)
                                                                     ("2"
                                                                      (HIDE
                                                                       -1
                                                                       2)
                                                                      (("2"
                                                                        (EXPAND
                                                                         "NOT")
                                                                        (("2"
                                                                          (EXPAND
                                                                           "NOT")
                                                                          (("2"
                                                                            (PROPAX)
                                                                            NIL)))))))))))))))))))))))))))))))))))
                                         ("2"
                                          (ASSERT)
                                          (("2"
                                            (HIDE -1 -2 2)
                                            (("2"
                                              (EXPAND "zero_extend")
                                              (("2"
                                                (EXPAND "NOT")
                                                (("2"
                                                  (EXPAND "NOT")
                                                  (("2"
                                                    (EXPAND "o ")
                                                    (("2"
                                                      (EXPAND "bvec0")
                                                      (("2"
                                                        (PROPAX)
                                                        NIL)))))))))))))))))))))))))))))
                           ("2" (TYPEPRED "k!1")
                            (("2" (ASSERT)
                              (("2" (LEMMA "zero_extend_lem")
                                (("2" (INST?) NIL)))))))))))))))
                   ("2" (HIDE 2)
                    (("2"
                      (CASE "(NOT NOT (zero_extend(k!1)(NOT bv!1))) =
             zero_extend(k!1)(NOT bv!1)")
                      (("1" (REPLACE -1 -2)
                        (("1" (HIDE -1) (("1" (ASSERT) NIL)))))
                       ("2" (HIDE -1 -2 2)
                        (("2" (EXPAND "NOT")
                          (("2" (APPLY-EXTENSIONALITY 1)
                            (("2" (HIDE 2)
                              (("2" (EXPAND "NOT")
                                (("2" (ASSERT)
                                  (("2" (LIFT-IF 1)
                                    (("2" (LIFT-IF)
                                      (("2"
                                        (SPLIT 1)
                                        (("1" (FLATTEN) (("1" (ASSERT) NIL)))
                                         ("2"
                                          (FLATTEN)
                                          (("2"
                                            (SPLIT 2)
                                            (("1"
                                              (FLATTEN)
                                              (("1" (ASSERT) NIL)))
                                             ("2"
                                              (FLATTEN)
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))))))))))))))))))))))))))
         ("2" (TYPEPRED "k!1")
          (("2" (ASSERT)
            (("2" (TYPEPRED "k!1")
              (("2" (FLATTEN)
                (("2" (LEMMA "zero_extend_lem")
                  (("2" (INST?)
                    (("2" (LEMMA "bv2int_lem[k!1]")
                      (("2" (INST?)
                        (("2" (REPLACE -1)
                          (("2" (HIDE -1)
                            (("2" (LEMMA "bv2int_lem[N]")
                              (("2" (INST?)
                                (("2" (REPLACE -1)
                                  (("2" (HIDE -1)
                                    (("2" (REPLACE -1)
                                      (("2"
                                        (HIDE -1)
                                        (("2"
                                          (EXPAND "zero_extend")
                                          (("2"
                                            (EXPAND "o ")
                                            (("2"
                                              (EXPAND "bvec0")
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))))))))))))))))))))))))))))))))))))
 (|zero_extend_lsend| "" (SKOSIMP*)
  (("" (EXPAND "zero_extend_lsend")
    (("" (LEMMA "bvconcat2nat[N, k!1 - N]")
      (("" (INST?)
        (("" (REPLACE -1)
          (("" (HIDE -1)
            (("" (ASSERT)
              (("" (LEMMA "bv2nat_bvec0[k!1-N]")
                (("" (PROPAX) NIL))))))))))))))))))
$$$bv_manipulations.pvs
bv_manipulations[n, m: posnat] : THEORY

BEGIN

  IMPORTING bv_concat, bv_extractors

  i: VAR below(n)
  bvn: VAR bvec[n]
  bvm: VAR bvec[m]

  caret_bvec0	   : LEMMA (FORALL (i: below(n)),(j: upto(i)): 
			      bvec0[n]^(i,j) = bvec0[i-j+1])
 
  caret_bvec1	   : LEMMA (FORALL (i: below(n)),(j: upto(i)): 
			      bvec1[n]^(i,j) = bvec1[i-j+1])
 
  caret_concat_bot : THEOREM (FORALL (i: below(n)), (j: upto(i)):
			 i < m IMPLIES (bvn o bvm)^(i,j) = bvm^(i,j))
 
  caret_concat_top : THEOREM (FORALL (i: below(n)), (j: upto(i)):
			      i >= m AND j >= m 
				IMPLIES (bvn o bvm)^(i,j) = bvn^(i-m, j-m))
 
  caret_concat_all : THEOREM (FORALL (i: below(n)), (j: upto(i)):
			       i >= m AND j < m 
				 IMPLIES (bvn o bvm)^(i,j) =
					  bvn^(i-m,0) o bvm^(m-1,j) )
 
  concat_bottom	   : THEOREM (bvn o bvm)^((m-1), 0) = bvm
 
  concat_top	   : THEOREM (bvn o bvm)^((n+m-1), m) = bvn

END bv_manipulations

$$$bv_manipulations.prf
(|bv_manipulations|
 (|caret_bvec0_TCC1| "" (AUTO-REWRITE-THEORY "integers")
  (("" (ASSERT) NIL)))
 (|caret_bvec0_TCC2| "" (TCC :DEFS !) NIL)
 (|caret_bvec0_TCC3| "" (AUTO-REWRITE-THEORY "integers")
  (("" (ASSERT) NIL)))
 (|caret_bvec0| "" (SKOLEM 1 ("i!1" "j!1"))
  (("" (EXPAND "^") (("" (EXPAND "bvec0") (("" (PROPAX) NIL)))))))
 (|caret_bvec1| "" (SKOLEM 1 ("i!1" "j!1"))
  (("" (EXPAND "^") (("" (EXPAND "bvec1") (("" (PROPAX) NIL)))))))
 (|caret_concat_bot_TCC1| "" (GROUND)
  (("" (SKOLEM 1 ("i!1"))
    (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|caret_concat_bot| "" (SKOSIMP*)
  (("" (EXPAND "^")
    (("" (APPLY-EXTENSIONALITY 1)
      (("" (HIDE 2) (("" (EXPAND "o") (("" (PROPAX) NIL)))))))))))
 (|caret_concat_top_TCC1| "" (GRIND) NIL)
 (|caret_concat_top_TCC2| "" (GROUND)
  (("" (SKOLEM 1 ("i!2" "j!1"))
    (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|caret_concat_top_TCC3| "" (SKOLEM 1 ("i!2" "j!1"))
  (("" (FLATTEN) (("" (ASSERT) NIL)))))
 (|caret_concat_top| "" (SKOSIMP*)
  (("" (EXPAND "^")
    (("" (APPLY-EXTENSIONALITY 1)
      (("" (HIDE 2) (("" (EXPAND "o ") (("" (PROPAX) NIL)))))))))))
 (|caret_concat_all_TCC1| "" (GRIND) NIL)
 (|caret_concat_all_TCC2| "" (GRIND) NIL)
 (|caret_concat_all_TCC3| "" (GROUND)
  (("" (SKOLEM 1 ("i!2" "j!1"))
    (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|caret_concat_all_TCC4| "" (GROUND)
  (("" (SKOLEM 1 ("i!2" "j!1"))
    (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|caret_concat_all_TCC5| "" (GROUND)
  (("" (SKOLEM 1 ("i!2" "j!1"))
    (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|caret_concat_all_TCC6| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|caret_concat_all_TCC7| "" (GRIND) NIL)
 (|caret_concat_all| "" (SKOSIMP*)
  (("" (EXPAND "o ")
    (("" (EXPAND "^")
      (("" (CASE "i!1 - j!1 + 1 = i!1 + 1 - j!1")
        (("1" (APPLY-EXTENSIONALITY 1)
          (("1" (HIDE 2) (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
           ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))
           ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
           ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL)))))))
         ("2" (HIDE 2) (("2" (ASSERT) NIL)))))))))))
 (|concat_bottom_TCC1| "" (ASSERT) (("" (ASSERT) (("" (ASSERT) NIL)))))
 (|concat_bottom_TCC2| "" (ASSERT) NIL)
 (|concat_bottom| "" (SKOLEM 1 ("bvm!1" "bvn!1"))
  (("" (EXPAND "o ")
    (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) NIL)))))))
 (|concat_top_TCC1| "" (ASSERT) NIL)
 (|concat_top_TCC2| "" (ASSERT) NIL)
 (|concat_top| "" (SKOLEM 1 ("bvm!1" "bvn!1"))
  (("" (EXPAND "o ")
    (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) NIL))))))))

$$$bv_rotate.pvs
bv_rotate [N: posnat ] : THEORY
%-----------------------------------------------------------------------  
%  Defines rotate operations.
%  Introduces:
%      rotate_right(k: upto(N), bv: bvec[N]): bvec[N] 
%      rotate_left(k: upto(N), bv: bvec[N]): bvec[N] 
%      rot_r1(bv: bvec[N]): bvec[N] 
%      rot_l1(bv: bvec[N]): bvec[N] 
%-----------------------------------------------------------------------  

BEGIN

  IMPORTING bv_concat, bv_extractors

  rotate_right(k: upto(N), bv: bvec[N]): bvec[N] = 
     IF (k = 0) OR (k = N) THEN bv 
     ELSE bv^(k-1,0) o bv^(N-1, k) ENDIF

  rotate_left(k: upto(N), bv: bvec[N]): bvec[N] =
     IF (k=0) OR (k = N) THEN bv 
     ELSE bv^(N-k-1, 0) o bv^(N-1,N-k) ENDIF

  rot_r1(bv: bvec[N]): bvec[N] = rotate_right(1,bv)

  rot_l1(bv: bvec[N]): bvec[N] = rotate_left(1,bv)

  i:  VAR below(N)
  k:  VAR upto(N)
  bv: VAR bvec[N]

  rotate_right_0   : LEMMA rotate_right(0,bv)= bv

  rotate_right_lem : LEMMA rotate_right(k,bv)^i =
                             IF i+k < N THEN bv^(i+k) ELSE bv^(i+k-N) ENDIF

  rotate_left_0    : LEMMA rotate_left(0,bv)= bv

  rotate_left_lem  : LEMMA rotate_left(k,bv)^i = 
                             IF i-k >= 0 THEN bv^(i-k) ELSE bv^(N+i-k) ENDIF

  iterate_rot_r1   : LEMMA iterate(rot_r1,k)(bv) = rotate_right(k,bv)

  iterate_rot_l1   : LEMMA iterate(rot_l1,k)(bv) = rotate_left(k,bv)

END bv_rotate

$$$bv_rotate.prf
(|bv_rotate|
 (|rotate_right_TCC1| "" (AUTO-REWRITE-THEORY "integers")
  (("" (ASSERT) NIL)))
 (|rotate_right_TCC2| "" (TCC :DEFS !) NIL)
 (|rotate_right_TCC3| "" (TCC :DEFS !) NIL)
 (|rotate_right_TCC4| "" (TCC :DEFS !) NIL)
 (|rotate_right_TCC5| "" (TCC :DEFS !) NIL)
 (|rotate_left_TCC1| "" (TCC :DEFS !) NIL)
 (|rotate_left_TCC2| "" (GRIND) NIL)
 (|rotate_left_TCC3| "" (TCC :DEFS !) NIL)
 (|rot_r1_TCC1| "" (TCC :DEFS !) NIL)
 (|rotate_right_0_TCC1| "" (TCC :DEFS !) NIL)
 (|rotate_right_0| "" (SKOSIMP*)
  (("" (EXPAND "rotate_right") (("" (PROPAX) NIL)))))
 (|rotate_right_lem_TCC1| "" (TCC :DEFS !) NIL)
 (|rotate_right_lem| "" (SKOSIMP*)
  (("" (EXPAND "rotate_right")
    (("" (EXPAND "^")
      (("" (EXPAND "o")
        (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL)))))))))))))
 (|rotate_left_0| "" (TCC :DEFS !) NIL)
 (|rotate_left_lem_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|rotate_left_lem_TCC2| "" (TCC :DEFS !) NIL)
 (|rotate_left_lem| "" (GRIND) NIL)
 (|iterate_rot_r1| "" (INDUCT "k" 1 "upto_induction[N]")
  (("1" (SKOSIMP*)
    (("1" (EXPAND "iterate")
      (("1" (EXPAND "rotate_right") (("1" (PROPAX) NIL)))))))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "iterate" +)
      (("2" (INST -2 "bv!1")
        (("2" (REPLACE -2)
          (("2" (HIDE -2)
            (("2" (EXPAND "rotate_right")
              (("2" (EXPAND "rot_r1")
                (("2" (EXPAND "rotate_right")
                  (("2" (EXPAND "^")
                    (("2" (LIFT-IF)
                      (("2" (ASSERT)
                        (("2" (EXPAND "o")
                          (("2" (LIFT-IF)
                            (("2"
                              (PROP)
                              (("1" (ASSERT) NIL)
                               ("2" (APPLY-EXTENSIONALITY 2) NIL)
                               ("3"
                                (REPLACE -1)
                                (("3"
                                  (HIDE -1)
                                  (("3" (ASSERT) NIL)))))
                               ("4"
                                (ASSERT)
                                (("4"
                                  (APPLY-EXTENSIONALITY 2)
                                  (("1"
                                    (HIDE 3)
                                    (("1"
                                      (LIFT-IF)
                                      (("1" (GROUND) NIL)))))
                                   ("2"
                                    (HIDE 2 3 4)
                                    (("2"
                                      (SKOSIMP*)
                                      (("2" (ASSERT) NIL)))))
                                   ("3"
                                    (HIDE 2 3 4)
                                    (("3"
                                      (SKOSIMP*)
                                      (("3" (ASSERT) NIL)))))
                                   ("4"
                                    (HIDE 2 3 4)
                                    (("4"
                                      (SKOSIMP*)
                                      (("4" (ASSERT) NIL)))))
                                   ("5"
                                    (HIDE 2 3 4)
                                    (("5"
                                      (SKOSIMP*)
                                      (("5"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|iterate_rot_l1| "" (INDUCT "k" 1 "upto_induction[N]")
  (("1" (SKOSIMP*)
    (("1" (EXPAND "iterate")
      (("1" (EXPAND "rotate_left") (("1" (PROPAX) NIL)))))))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "iterate" 1)
      (("2" (EXPAND "rotate_left" 1)
        (("2" (INST -2 "bv!1")
          (("2" (REPLACE -2)
            (("2" (HIDE -2)
              (("2" (EXPAND "rotate_left")
                (("2" (EXPAND "rot_l1")
                  (("2" (EXPAND "rotate_left")
                    (("2" (EXPAND "^")
                      (("2" (LIFT-IF)
                        (("2" (ASSERT)
                          (("2" (EXPAND "o")
                            (("2"
                              (LIFT-IF)
                              (("2"
                                (PROP)
                                (("1" (ASSERT) NIL)
                                 ("2" (APPLY-EXTENSIONALITY 2) NIL)
                                 ("3"
                                  (REPLACE -1)
                                  (("3"
                                    (HIDE -1)
                                    (("3" (ASSERT) NIL)))))
                                 ("4"
                                  (ASSERT)
                                  (("4"
                                    (APPLY-EXTENSIONALITY 2)
                                    (("1"
                                      (HIDE 3)
                                      (("1"
                                        (LIFT-IF)
                                        (("1" (GROUND) NIL)))))
                                     ("2"
                                      (HIDE 2 3 4)
                                      (("2"
                                        (SKOSIMP*)
                                        (("2" (ASSERT) NIL)))))
                                     ("3"
                                      (HIDE 2 3 4)
                                      (("3"
                                        (SKOSIMP*)
                                        (("3" (ASSERT) NIL)))))
                                     ("4"
                                      (HIDE 2 3 4)
                                      (("4"
                                        (SKOSIMP*)
                                        (("4" (ASSERT) NIL)))))
                                     ("5"
                                      (HIDE 2 3 4)
                                      (("5"
                                        (SKOSIMP*)
                                        (("5" (ASSERT) NIL)))))
                                     ("6"
                                      (HIDE 2 3 4)
                                      (("6"
                                        (SKOSIMP*)
                                        (("6"
                                          (ASSERT)
                                          NIL))))))))))))))))))))))))))))))))))))))))))
$$$bv_shift.pvs
bv_shift [N: nat ] : THEORY
%-----------------------------------------------------------------------  
%  Defines shift operations.
%  Introduces:
%     left_shift(i: nat, bv: bvec[N]): bvec[N]
%     right_shift(i: nat, bv: bvec[N]): bvec[N] 
%     left_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N]
%     right_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N]
%-----------------------------------------------------------------------  

BEGIN

  IMPORTING bv_concat, bv_extractors

  %------------------------------------------------------------------------
  % right_shift (left_shift) shifts a bit vector by a given number of
  % positions to the right (left) filling 0's to the shifted bits
  %------------------------------------------------------------------------

  right_shift(i: nat, bv: bvec[N]): bvec[N] =
    IF i = 0 THEN bv
    ELSIF i < N THEN bvec0[i] o bv^(N-1, i) 
    ELSE bvec0[N] ENDIF
    
  left_shift(i: nat, bv: bvec[N]): bvec[N] =
    IF i = 0 THEN bv
    ELSIF i < N THEN bv^(N-i-1, 0) o bvec0[i]
    ELSE bvec0[N] ENDIF

  %------------------------------------------------------------------------    
  % left_shift_with (right_shift_with) shifts a bit vector by a given
  % number of positions to the left (right) replacing the shifted bits
  % by the bit vector given as the second argument.
  %------------------------------------------------------------------------

  left_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N] =
     IF k = N THEN bvk
     ELSE bv^(N-k-1, 0) o bvk ENDIF

  right_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N] =
     IF k = N THEN bvk
     ELSE bvk o bv^(N-1, k) ENDIF

END bv_shift

$$$bv_shift.prf
(|bv_shift| (|right_shift_TCC1| "" (GRIND) NIL)
 (|right_shift_TCC2| "" (GROUND)
  (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|right_shift_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|left_shift_TCC1| "" (GROUND)
  (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|left_shift_TCC2| "" (GRIND) NIL)
 (|left_shift_with_TCC1| "" (GROUND)
  (("" (SKOLEM!)
    (("" (FLATTEN) (("" (REPLACE -1) (("" (ASSERT) NIL)))))))))
 (|left_shift_with_TCC2| "" (GROUND) NIL)
 (|left_shift_with_TCC3| "" (GROUND)
  (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|left_shift_with_TCC4| "" (GRIND) NIL)
 (|right_shift_with_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|right_shift_with_TCC2| "" (GROUND)
  (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))))

$$$sums.pvs
sums: THEORY
%------------------------------------------------------------------------------
% The summations theory introduces and defines properties of the sigma 
% function that sums an arbitrary function F: [nat -> nat] over a range
% from low to high
%
%  		          high
%		          ----
%  sigma(low, high, F) =  \     F(j)
%		          /
%		          ----
%		         j = low
%
%------------------------------------------------------------------------------

BEGIN

  low, high, rng, l, h, n, m, x: VAR nat

  F, G: VAR function[nat -> nat]

  sigma(low, high, F): RECURSIVE nat
      = IF low > high THEN 0
        ELSIF high = low THEN F(low) 
        ELSE  F(high) + sigma(low, high-1, F)
        ENDIF
   MEASURE (LAMBDA low, high, F: high)

%  sigma_rec(high, F): RECURSIVE nat
%      = IF high = 0 THEN F(0)
%        ELSE F(high) + sigma_rec(high-1, F)
%        ENDIF
%   MEASURE high
%
%  sigma(low, high, F): nat
%      = IF low > high THEN 0
%        ELSE sigma_rec(high - low, (LAMBDA n: F(n + low)))
%        ENDIF

  sigma_mult:  THEOREM sigma(low, high, (LAMBDA n -> nat : x * F(n)))
                         = x * sigma(low, high, F)

  sigma_split: THEOREM m >= low AND high > m 
          IMPLIES sigma(low, high, F) = sigma(low, m, F) + sigma(m+1, high, F)

  sigma_shift: THEOREM sigma(low+m,high+m,F) = sigma(low,high, (LAMBDA n: F(n+m)))

  restrict(F, low, high): function[nat -> nat] = 
     (LAMBDA n: IF n < low OR n > high THEN 0 ELSE F(n) ENDIF )

  sigma_restrict_eq: THEOREM restrict(F,low,high) = restrict(G,low,high) 
                        IMPLIES sigma(low,high,F) = sigma(low,high,G) 

END sums

$$$sums.prf
(|sums| (|sigma_TCC1| "" (TCC) NIL)
        (|sigma_TCC2| "" (TCC) NIL)
        (|sigma_mult| ""
                      (INDUCT "high")
                      (("1" (SKOSIMP*)
                            (("1" (EXPAND "sigma")
                                  (("1" (LIFT-IF)
                                        (("1" (GROUND) NIL)))))))
                        ("2" (SKOSIMP*)
                             (("2" (EXPAND "sigma" 1)
                                   (("2" (ASSERT)
                                         (("2" (INST?)
                                               (("2" (REPLACE -1)
                                                     (("2" (HIDE -1)
                                                           (("2" (LIFT-IF)
                                                                 (("2"
                                                                    (GROUND)
                                                                    NIL)))))))))))))))))
        (|sigma_split| ""
                       (INDUCT "high")
                       (("1" (SKOSIMP*)
                             (("1" (EXPAND "sigma")
                                   (("1" (LIFT-IF)
                                         (("1" (GROUND) NIL)))))))
                         ("2" (SKOSIMP*)
                              (("2" (EXPAND "sigma" 1 1)
                                    (("2" (EXPAND "sigma" 1 2)
                                          (("2" (ASSERT)
                                                (("2" (CASE "j!1=m!1")
                                                      (("1" (REPLACE -1)
                                                            (("1" (HIDE -1)
                                                                  (("1"
                                                                     (ASSERT)
                                                                     NIL)))))
                                                        ("2"
                                                          (INST -1
                                                                "F!1"
                                                                "low!1"
                                                                "m!1")
                                                          (("2" (ASSERT)
                                                                NIL)))))))))))))))
        (|sigma_shift| ""
                       (INDUCT "high")
                       (("1" (SKOSIMP*)
                             (("1" (EXPAND "sigma")
                                   (("1" (LIFT-IF)
                                         (("1" (GROUND) NIL)))))))
                         ("2" (SKOSIMP*)
                              (("2" (EXPAND "sigma" 1)
                                    (("2" (LIFT-IF)
                                          (("2" (LIFT-IF)
                                                (("2" (ASSERT)
                                                      (("2" (INST?)
                                                            (("2" (GROUND)
                                                                  NIL)))))))))))))))
        (|sigma_restrict_eq| ""
                             (INDUCT "high")
                             (("1" (SKOSIMP*)
                                   (("1" (EXPAND "sigma")
                                         (("1" (EXPAND "restrict")
                                               (("1" (LIFT-IF)
                                                     (("1" (GROUND)
                                                           (("1"
                                                              (CASE
                                                                "(LAMBDA (n: nat): IF n > 0 THEN 0 ELSE F!1(n) ENDIF)(low!1)
        = (LAMBDA (n: nat): IF n > 0 THEN 0 ELSE G!1(n) ENDIF)(low!1)")
                                                              (("1" (HIDE -2)
                                                                    (("1"
                                                                      (BETA -1)
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (GROUND)
                                                                      NIL)))))))
                                                                ("2"
                                                                  (HIDE 2 3)
                                                                  (("2"
                                                                     (REPLACE
                                                                      -1)
                                                                     (("2"
                                                                      (PROPAX)
                                                                      NIL)))))))))))))))))
                               ("2" (SKOSIMP*)
                                    (("2" (EXPAND "sigma" 1)
                                          (("2" (LIFT-IF)
                                                (("2" (GROUND)
                                                      (("1" (REPLACE -1)
                                                            (("1" (HIDE -1)
                                                                  (("1"
                                                                     (HIDE -1)
                                                                     (("1"
                                                                      (EXPAND
                                                                      "restrict")
                                                                      (("1"
                                                                      (CASE
                                                                      "  (LAMBDA (n: nat): IF n < low!1 OR n > low!1 THEN 0 ELSE F!1(n) ENDIF)(low!1)
        = (LAMBDA (n: nat): IF n < low!1 OR n > low!1 THEN 0 ELSE G!1(n) ENDIF)(low!1)")
                                                                      (("1"
                                                                      (HIDE
                                                                      -2)
                                                                      (("1"
                                                                      (BETA
                                                                      -1)
                                                                      (("1"
                                                                      (GROUND)
                                                                      NIL)))))
                                                                      ("2"
                                                                      (HIDE
                                                                      2
                                                                      3)
                                                                      (("2"
                                                                      (REPLACE
                                                                      -1)
                                                                      (("2"
                                                                      (PROPAX)
                                                                      NIL)))))))))))))))
                                                        ("2"
                                                          (INST -1
                                                                "F!1"
                                                                "G!1"
                                                                "low!1")
                                                          (("2" (SPLIT -1)
                                                                (("1" (ASSERT)
                                                                      (("1"
                                                                      (HIDE
                                                                      -1)
                                                                      (("1"
                                                                      (EXPAND
                                                                      "restrict")
                                                                      (("1"
                                                                      (CASE
                                                                      "  (LAMBDA (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE F!1(n) ENDIF)(j!1+1)
        =
        (LAMBDA
         (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE G!1(n) ENDIF)(j!1+1)")
                                                                      (("1"
                                                                      (BETA
                                                                      -1)
                                                                      (("1"
                                                                      (HIDE
                                                                      -2)
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (GROUND)
                                                                      NIL)))))))
                                                                      ("2"
                                                                      (REPLACE
                                                                      -1)
                                                                      (("2"
                                                                      (HIDE
                                                                      -1
                                                                      2
                                                                      3
                                                                      4)
                                                                      (("2"
                                                                      (BETA
                                                                      1)
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (GROUND)
                                                                      NIL)))))))))))))))))
                                                                  ("2"
                                                                    (HIDE 3)
                                                                    (("2"
                                                                      (EXPAND
                                                                      "restrict")
                                                                      (("2"
                                                                      (HIDE
                                                                      3)
                                                                      (("2"
                                                                      (APPLY-EXTENSIONALITY
                                                                      1)
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (GROUND)
                                                                      (("2"
                                                                      (CASE
                                                                      " (LAMBDA (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE F!1(n) ENDIF)(x!1)
        =
        (LAMBDA
         (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE G!1(n) ENDIF)(x!1)")
                                                                      (("1"
                                                                      (HIDE
                                                                      -2)
                                                                      (("1"
                                                                      (BETA
                                                                      -1)
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (GROUND)
                                                                      NIL)))))))
                                                                      ("2"
                                                                      (REPLACE
                                                                      -1)
                                                                      (("2"
                                                                      (BETA
                                                                      1)
                                                                      (("2"
                                                                      (ASSERT)
                                                                      NIL))))))))))))))))))))))))))))))))))
$$$bv_sum.pvs
bv_sum[N: nat]: THEORY
%------------------------------------------------------------------------------
% The bv_sum theory defines bv2nat as a summation over the bits in bv:
%
%		       N-1
%		      ----
%   bv2nat_rec(bv) =  \      exp2(n) * bv(n)  
%		      /
%		      ----
%		      n = 0
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING bv_nat, sums

  bv: VAR bvec[N]

  nn: VAR nat
  n, ii: VAR below(N)

  F: VAR function[below(N) -> nat]
  extend(F): function[nat -> nat] = 
     (LAMBDA nn: IF nn < N THEN F(nn) ELSE 0 ENDIF)

  bv2nat_rec_as_sum: LEMMA bv2nat_rec(n+1,bv) = 
     sigma(0,n, extend((LAMBDA ii: exp2(ii) * bv(ii))))

  bv2nat_as_sum: THEOREM bv2nat(bv) = IF N = 0 THEN 0
         ELSE sigma(0,N-1, extend((LAMBDA ii: exp2(ii) * bv(ii)))) ENDIF

END bv_sum

$$$bv_sum.prf
(|bv_sum| (|bv2nat_rec_as_sum_TCC1| "" (TCC :DEFS !) NIL)
 (|bv2nat_rec_as_sum| ""
  (AUTO-REWRITE :NAMES ("bv2nat_rec" "sigma" "extend"))
  (("" (INDUCT "n" 1 NIL)
    (("1" (SKOSIMP*) (("1" (ASSERT) NIL)))
     ("2" (SKOSIMP*)
      (("2" (ASSERT)
        (("2" (LIFT-IF)
          (("2"
            (APPLY (THEN* (ASSERT) (BDDSIMP) (SKOSIMP*)
                    (IF (LET* ((VAR '"n")
                               (FNUM '1)
                               (REWRITES
                                '("bv2nat_rec" "sigma" "extend"))
                               (NAME 'NIL)
                               (DEFS 'NIL)
                               (IF-MATCH 'BEST)
                               (THEORIES 'NIL))
                          IF-MATCH)
                        (INST? :IF-MATCH BEST)
                        (SKIP))
                    (LIFT-IF))
                   "Applying assert, propositional simplification, instantiation,
skolemization, and if-lifting")
            NIL)))))))))))
 (|bv2nat_as_sum_TCC1| "" (TCC) NIL)
 (|bv2nat_as_sum| "" (SKOSIMP*)
  (("" (LIFT-IF)
    (("" (EXPAND "bv2nat")
      (("" (GROUND)
        (("1" (EXPAND "bv2nat_rec") (("1" (PROPAX) NIL)))
         ("2" (LEMMA "bv2nat_rec_as_sum")
          (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))
$$$bv_concat_lems.pvs
bv_concat_lems: THEORY

BEGIN

  IMPORTING bv_concat

  null_bv: bvec[0]  %% zero-length bit-vector

% ===== (bvec,o,1) is a monoid ===========================================

  concat_identity_r  : LEMMA (FORALL (n: nat), (bvn:bvec[n]):
                                 bvn o null_bv = bvn)

  concat_identity_l  : LEMMA (FORALL (n: nat), (bvn:bvec[n]):
                                 null_bv o bvn = bvn)

  concat_associative : LEMMA (FORALL (m,n,p: nat), (bvm:bvec[m]),
                                     (bvn:bvec[n]),  (bvp:bvec[p]):
                             (bvm o bvn) o bvp = bvm o (bvn o bvp))

END bv_concat_lems

$$$bv_concat_lems.prf
(|bv_concat_lems|
  (|concat_identity_r| ""
                       (SKOSIMP*)
                       (("" (APPLY-EXTENSIONALITY 1)
                            (("" (HIDE 2)
                                 (("" (EXPAND "o ")
                                      (("" (PROPAX) NIL)))))))))
  (|concat_identity_l| ""
                       (SKOSIMP*)
                       (("" (APPLY-EXTENSIONALITY 1)
                            (("" (HIDE 2)
                                 (("" (EXPAND "o ")
                                      (("" (PROPAX) NIL)))))))))
  (|concat_associative| ""
                        (SKOSIMP*)
                        (("" (APPLY-EXTENSIONALITY 1)
                             (("" (HIDE 2)
                                  (("" (EXPAND "o ")
                                       (("" (LIFT-IF)
                                            (("" (GROUND) NIL))))))))))))
$$$bv_concat_nat.pvs
bv_concat_nat [n:nat, m:nat ]: THEORY
BEGIN

  IMPORTING bv_concat_lems, bv_sum

  bvn: VAR bvec[n]
  bvm: VAR bvec[m]
  nm: VAR below(n+m) 

  bvconcat2nat: THEOREM bv2nat[n+m](bvn o bvm) 
                               = bv2nat[n](bvn) * exp2(m) + bv2nat[m](bvm)


END bv_concat_nat

$$$bv_concat_nat.prf
(|bv_concat_nat| (|bvconcat2nat_TCC1| "" (SAME-NAME-TCC) NIL)
 (|bvconcat2nat| "" (SKOSIMP*)
  (("" (CASE "m = 0")
    (("1" (REPLACE -1)
      (("1" (EXPAND "bv2nat" 1 3)
        (("1" (EXPAND "bv2nat_rec")
          (("1" (REWRITE "bvconcat_bot0")
            (("1" (EXPAND "exp2")
              (("1" (REPLACE -1)
                (("1" (ASSERT)
                  (("1" (SAME-NAME "bv2nat[n + m]" "bv2nat[n]")
                    (("1" (ASSERT) NIL)))))))))))))))))
     ("2" (CASE "n = 0")
      (("1" (EXPAND "bv2nat" + 2)
        (("1" (SAME-NAME "bv2nat[n + m]" "bv2nat[m]")
          (("1" (REPLACE -1)
            (("1" (EXPAND "bv2nat_rec")
              (("1" (ASSERT)
                (("1" (REWRITE "bvconcat_top0") NIL)))))))
           ("2" (PROPAX) NIL)))))
       ("2" (REWRITE "bv2nat_as_sum[n+m]")
        (("2" (LEMMA "sigma_split")
          (("2"
            (INST -1 "extend((LAMBDA (ii: below(n + m)):
                      exp2(ii) * (bvn!1 o bvm!1)(ii)))"
             "n+m-1" "0" "m-1")
            (("1" (ASSERT)
              (("1" (REPLACE -1)
                (("1" (HIDE -1)
                  (("1"
                    (CASE "sigma(0, m - 1,
            extend((LAMBDA (ii: below(n + m)):
                      exp2(ii) * (bvn!1 o bvm!1)(ii)))) = bv2nat[m](bvm!1)")
                    (("1" (REPLACE -1)
                      (("1" (HIDE -1)
                        (("1" (ASSERT)
                          (("1" (LEMMA "sigma_shift")
                            (("1"
                              (EXPAND "extend")
                              (("1"
                                (EXPAND "o ")
                                (("1"
                                  (INST
                                   -1
                                   " (LAMBDA (nn: nat):
			  IF nn < n + m THEN exp2(nn)
			      * IF nn < m THEN bvm!1(nn)
				ELSE bvn!1(nn - m)
				ENDIF
			  ELSE 0
			  ENDIF)"
                                   "n-1"
                                   "0"
                                   "m")
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (REPLACE -1)
                                      (("1"
                                        (HIDE -1)
                                        (("1"
                                          (REWRITE
                                           "bv2nat_as_sum[n]")
                                          (("1"
                                            (LEMMA "sigma_mult")
                                            (("1"
                                              (INST
                                               -1
                                               "extend((LAMBDA (ii: below(n)): exp2(ii) * bvn!1(ii)))"
                                               "n-1"
                                               "0"
                                               "exp2(m)")
                                              (("1"
                                                (REPLACE -1 + RL)
                                                (("1"
                                                  (HIDE -1)
                                                  (("1"
                                                    (EXPAND "extend")
                                                    (("1"
                                                      (REWRITE
                                                       "sigma_restrict_eq")
                                                      (("1"
                                                        (HIDE 2 3 4)
                                                        (("1"
                                                          (EXPAND
                                                           "restrict")
                                                          (("1"
                                                            (APPLY-EXTENSIONALITY
                                                             1)
                                                            (("1"
                                                              (HIDE
                                                               2)
                                                              (("1"
                                                                (LIFT-IF)
                                                                (("1"
                                                                  (LEMMA
                                                                   "exp2_sum")
                                                                  (("1"
                                                                    (INST?)
                                                                    (("1"
                                                                      (GROUND)
                                                                      NIL)))))))))
                                                             ("2"
                                                              (HIDE
                                                               2)
                                                              (("2"
                                                                (SKOSIMP*)
                                                                (("2"
                                                                  (ASSERT)
                                                                  NIL)))))))))))
                                                       ("2"
                                                        (HIDE 2)
                                                        (("2"
                                                          (SKOSIMP*)
                                                          (("2"
                                                            (ASSERT)
                                                            NIL)))))))))))))))))))))))))
                                   ("2"
                                    (SKOSIMP*)
                                    (("2"
                                      (ASSERT)
                                      NIL)))))))))))))))))
                     ("2" (ASSERT)
                      (("2" (HIDE 4)
                        (("2" (REWRITE "bv2nat_as_sum[m]")
                          (("2" (REWRITE "sigma_restrict_eq")
                            (("2"
                              (HIDE 2)
                              (("2"
                                (EXPAND "extend")
                                (("2"
                                  (EXPAND "restrict")
                                  (("2"
                                    (APPLY-EXTENSIONALITY 1)
                                    (("1"
                                      (HIDE 2)
                                      (("1"
                                        (LIFT-IF)
                                        (("1"
                                          (GROUND)
                                          (("1"
                                            (EXPAND "o ")
                                            (("1"
                                              (PROPAX)
                                              NIL)))))))))
                                     ("2"
                                      (HIDE 2)
                                      (("2"
                                        (SKOSIMP*)
                                        (("2" (ASSERT) NIL)))))
                                     ("3"
                                      (HIDE 2)
                                      (("3"
                                        (SKOSIMP*)
                                        (("3"
                                          (ASSERT)
                                          NIL)))))))))))))))))))))))))))))
             ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))))))))))
$$$bv_int.pvs
bv_int[N: posnat]: THEORY
%------------------------------------------------------------------------------
% This theory introduces the functions bv2int and int2bv that convert 
% between bit vectors and natural numbers.  These are based upon
% twos-complement interpretation.
%
%    Introduces:
%         bv2int : [bvec -> rng_2s_comp] 
%         int2bv : [rng_2s_comp  -> bvec]
%------------------------------------------------------------------------------
BEGIN

  IMPORTING bv_nat[N]

  n: VAR upto(N)
  bv, bv1, bv2: VAR bvec

% === Range of bv2int =========================================================

  minint: int = -exp2(N-1)
  maxint: int =  exp2(N-1) - 1

  in_rng_2s_comp(i: int): bool = (minint <= i AND i <= maxint)
  rng_2s_comp: TYPE = {i: int | minint <= i AND i <= maxint}

% === Preliminary results needed for proofs of TCCs ===========================

  bv2nat_top_bit: THEOREM IF bv2nat(bv) < exp2(N-1) THEN bv(N-1) = 0 
                                                    ELSE bv(N-1) = 1 ENDIF

% ===  Interpretation of a bit vector as an integer ===========================

  bv2int(bv: bvec): rng_2s_comp = IF bv2nat(bv) < exp2(N-1) THEN bv2nat(bv)
                                  ELSE bv2nat(bv) - exp2(N) ENDIF

  int2bv(iv: rng_2s_comp):bvec = inverse(bv2int)(iv) ;

% === Properties of bv2int and int2bv =========================================

  iv: VAR rng_2s_comp

  % ----------------------------------------------------------------------
  % bv2int_inj is injective, i.e.,
  %   (FORALL (x, y: bvec[N]): (bv2int(x) = bv2int(y) => (x = y)))
  % ----------------------------------------------------------------------
    
  bv2int_inj:  THEOREM injective?(bv2int)

  % ----------------------------------------------------------------------
  % bv2int is surjective, i.e.,
  %   (FORALL (y: rng_2s_comp): (EXISTS (x: bvec[N]): bv2int(x) = y))
  % ----------------------------------------------------------------------
    
  bv2int_surj: THEOREM surjective?(bv2int)

  % ----------------------------------------------------------------------
  % b2int and int2bv are bijective (injective and surjective)
  % ----------------------------------------------------------------------

  bv2int_bij : THEOREM bijective?(bv2int)
  bv2int_inv : THEOREM bv2int(int2bv(iv))=iv;


  bv2int_lem : THEOREM bv2int(bv) = bv2nat(bv) - exp2(N) * bv(N - 1)

END bv_int

$$$bv_int.prf
(|bv_int| (|minint_TCC1| "" (ASSERT) NIL)
 (|bv2nat_top_bit_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|bv2nat_top_bit_TCC2| "" (AUTO-REWRITE-EXPLICIT)
  (("" (GROUND)
    (("" (SKOLEM 1 ("bv!1"))
      (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))))
 (|bv2nat_top_bit| "" (SKOSIMP*)
  (("" (EXPAND "bv2nat")
    (("" (EXPAND "bv2nat_rec")
      (("" (LIFT-IF)
        (("" (ASSERT)
          (("" (ASSERT)
            (("" (LEMMA "bv_lem")
              (("" (INST?)
                (("" (GROUND)
                  (("" (REPLACE -1)
                    (("" (ASSERT)
                      (("" (REWRITE "bv2nat_rec_bound")
                        NIL)))))))))))))))))))))))
 (|bv2int_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "minint")
    (("" (EXPAND "maxint") (("" (ASSERT) NIL)))))))
 (|bv2int_TCC2| "" (SKOSIMP*)
  (("" (EXPAND "minint")
    (("" (EXPAND "maxint")
      (("" (ASSERT)
        (("" (EXPAND "exp2" 2 2) (("" (ASSERT) NIL)))))))))))
 (|bv2int_inj| "" (EXPAND "injective?")
  (("" (SKOSIMP *)
    (("" (LEMMA "bv2nat_inj")
      (("" (EXPAND "injective?")
        (("" (INST?)
          (("" (EXPAND "bv2int")
            (("" (LIFT-IF)
              (("" (SPLIT -2)
                (("1" (LIFT-IF)
                  (("1" (SPLIT -1)
                    (("1" (FLATTEN) (("1" (ASSERT) NIL)))
                     ("2" (FLATTEN) (("2" (ASSERT) NIL)))))))
                 ("2" (FLATTEN)
                  (("2" (LIFT-IF -1)
                    (("2" (SPLIT -1)
                      (("1" (FLATTEN) (("1" (ASSERT) NIL)))
                       ("2" (FLATTEN)
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|bv2int_surj| "" (EXPAND "surjective?")
  (("" (SKOSIMP *)
    ((""
      (CASE "(FORALL (m: {i:int | i >= minint AND i < 0}):
                                (EXISTS bv: bv2int(bv) = m))")
      (("1"
        (CASE "(FORALL (m: {i:int | i >= 0 AND i <= maxint}):
                                (EXISTS bv: bv2int(bv) = m))")
        (("1" (CASE "y!1 >= 0")
          (("1" (INST -2 "y!1") NIL)
           ("2" (INST -2 "y!1") (("2" (ASSERT) NIL)))))
         ("2" (HIDE -1 2)
          (("2" (SKOSIMP *)
            (("2" (EXPAND "bv2int")
              (("2" (TYPEPRED "m!1")
                (("2" (LEMMA "bv2nat_surj")
                  (("2" (EXPAND "surjective?")
                    (("2" (INST -1 "m!1")
                      (("1" (SKOLEM -1 ("bv!1"))
                        (("1" (INST 1 "bv!1")
                          (("1" (EXPAND "maxint")
                            (("1" (ASSERT) NIL)))))))
                       ("2" (EXPAND "maxint")
                        (("2" (EXPAND "exp2" 1)
                          (("2" (HIDE 2)
                            (("2"
                              (LIFT-IF 1)
                              (("2"
                                (SPLIT 1)
                                (("1" (ASSERT) NIL)
                                 ("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))
       ("2" (HIDE 2)
        (("2" (SKOSIMP *)
          (("2" (EXPAND "bv2int")
            (("2" (TYPEPRED "m!1")
              (("2" (LEMMA "bv2nat_surj")
                (("2" (EXPAND "surjective?")
                  (("2" (INST -1 "m!1 + exp2(N)")
                    (("1" (SKOLEM -1 ("bv!1"))
                      (("1" (INST 1 "bv!1")
                        (("1" (EXPAND "minint")
                          (("1" (ASSERT)
                            (("1"
                              (LIFT-IF 1)
                              (("1"
                                (SPLIT 1)
                                (("1"
                                  (FLATTEN)
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (EXPAND "exp2" -2)
                                      (("1" (ASSERT) NIL)))))))
                                 ("2"
                                  (FLATTEN)
                                  (("2" (ASSERT) NIL)))))))))))))))
                     ("2" (EXPAND "minint")
                      (("2" (EXPAND "exp2" 1)
                        (("2" (HIDE 2)
                          (("2" (LIFT-IF 1)
                            (("2"
                              (SPLIT 1)
                              (("1" (ASSERT) NIL)
                               ("2"
                                (ASSERT)
                                NIL)))))))))))))))))))))))))))))))
 (|bv2int_bij| "" (EXPAND "bijective?")
  (("" (LEMMA "bv2int_inj")
    (("" (LEMMA "bv2int_surj") (("" (ASSERT) NIL)))))))
 (|bv2int_inv| "" (SKOLEM!)
  (("" (EXPAND "int2bv")
    (("" (LEMMA "surj_right" ("f" "bv2int"))
      (("" (EXPAND "right_inverse?")
        (("" (REWRITE "bv2int_surj")
          (("" (ASSERT) (("" (INST?) NIL)))))))))))))
 (|bv2int_lem_TCC1| "" (TCC) NIL)
 (|bv2int_lem| "" (SKOLEM 1 ("bv!1"))
  (("" (EXPAND "bv2int")
    (("" (LIFT-IF)
      (("" (LEMMA "bv2nat_top_bit")
        (("" (INST -1 "bv!1")
          (("" (SPLIT 1)
            (("1" (FLATTEN) (("1" (ASSERT) NIL)))
             ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))))
$$$bv_extractors.pvs
bv_extractors[N: nat]: THEORY
%-----------------------------------------------------------------------
% An extractor operation decomposes a bvec into smaller
% bit vectors.  In the following, we define a number of
% extractors for bvec. 
%
%    Introduces:
%       bv^(i,j) creates bv[i-j+1] from bits i through j
%    
%   
%-----------------------------------------------------------------------  
BEGIN

  IMPORTING bv

  %-----------------------------------------------------------------------  
  % The following operator (^) extracts a contiguous fragment of
  % a bit vector between two given positions.
  %-----------------------------------------------------------------------  

   ^(bv: bvec[N], sp:[i1: below(N), upto(i1)]): bvec[proj_1(sp)-proj_2(sp)+1] =
       (LAMBDA  (ii: below(proj_1(sp) - proj_2(sp) + 1)):
		  bv(ii + proj_2(sp))) ;

% === Useful Lemmas and Theorems =========================================

  bv: VAR bvec[N]

  caret_all: LEMMA N > 0 IMPLIES bv^(N-1, 0) = bv

END bv_extractors

$$$bv_extractors.prf
(|bv_extractors| (|caret_TCC1| "" (GRIND) NIL)
 (|caret_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|caret_TCC3| "" (GRIND) NIL) (|caret_TCC4| "" (SUBTYPE-TCC) NIL)
 (|caret_all_TCC1| "" (FLATTEN) (("" (ASSERT) NIL)))
 (|caret_all_TCC2| "" (GROUND) NIL)
 (|caret_all| "" (SKOSIMP*)
  (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) NIL))))))
$$$bv_fract.pvs
bv_fract [N: above(1)]: THEORY
%------------------------------------------------------------------------------
% Defines an interpretation of bit vectors as 2's complement fractions.
%
%   Introduces:
%        bv2fract: function [bvec[N] -> bv2fract_range]
%------------------------------------------------------------------------------
BEGIN

  IMPORTING bv, exp2
  
  %----------------------------------------------------------------------------
  % Using a 2's complement representation, a bit vector of size N can 
  % represent any fraction of the form i/exp2(N-1) as a rational number, 
  % where i ranges over all integers representable by a bit vector of size N.
  % The predicate bv2fract_range characterizes this set of rationals.
  %--------------------------------------------------------------------------- 

  fract_numerator_range: TYPE = {i: int| i >= -exp2(N-1) & i < exp2(N-1)}

  bv2fract_range(r: rational): bool =
     (EXISTS (i: fract_numerator_range): (r = i/exp2(N-1)) )

  bv2fract_range: TYPE = (bv2fract_range) CONTAINING 0

  bv2fract: [bvec[N] -> bv2fract_range]

  %---------------------------------------------------------------------------
  % The following min and max definitions ignore 0 and -1, instead
  % naming their nearest fractional representations.
  %---------------------------------------------------------------------------

  min_pos_fract: bv2fract_range = 1/exp2(N-1)
  max_pos_fract: bv2fract_range = 1 - 1/exp2(N-1)

  min_neg_fract: bv2fract_range = -1/exp2(N-1)
  max_neg_fract: bv2fract_range = -1 + 1/exp2(N-1)

END bv_fract






$$$bv_fract.prf
(|bv_fract| (|fract_numerator_range_TCC1| "" (GROUND) NIL)
 (|bv2fract_range_TCC1| "" (TCC) NIL)
 (|bv2fract_TCC1| "" (ASSERT) NIL)
 (|min_pos_fract_TCC1| "" (ASSERT)
  (("" (EXPAND "bv2fract_range")
    (("" (INST 1 "1")
      (("" (ASSERT) (("" (EXPAND "exp2") (("" (ASSERT) NIL)))))))))))
 (|max_pos_fract_TCC1| "" (EXPAND "bv2fract_range")
  (("" (INST 1 "exp2(N-1) - 1")
    (("1" (ASSERT) NIL)
     ("2" (AUTO-REWRITE-THEORY "integers") (("2" (ASSERT) NIL)))
     ("3" (ASSERT) NIL)))))
 (|min_neg_fract_TCC1| "" (EXPAND "bv2fract_range")
  (("" (INST 1 "-1")
    (("" (ASSERT)
      (("" (AUTO-REWRITE-THEORY "integers")
        (("" (ASSERT) NIL)))))))))
 (|max_neg_fract_TCC1| "" (EXPAND "bv2fract_range")
  (("" (AUTO-REWRITE-THEORY "integers")
    (("" (INST 1 "1 - exp2(N-1)")
      (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))))
$$$bv_concat.pvs
bv_concat [n:nat, m:nat ]: THEORY
%------------------------------------------------------------------------
% This theory defines the concatenation operator o for bitvectors:
%
%   o: [bvec[n], bvec[m] -> bvec[n+m]] 
%
% The bit vector binary ops theory defines functions that take 
% two bit vectors as their primary inputs.  The theory is 
% instantiated with the sizes of the input bit vectors.
%------------------------------------------------------------------------

BEGIN

  IMPORTING bv

  o(bvn: bvec[n], bvm: bvec[m]): bvec[n+m] =
       (LAMBDA (nm: below(n+m)): IF nm < m THEN bvm(nm)
                                 ELSE bvn(nm - m)
                                 ENDIF)

  bvn: VAR bvec[n]
  bvm: VAR bvec[m]

  bvconcat_bot0: THEOREM m = 0 IMPLIES bvn o bvm = bvn 

  bvconcat_top0: THEOREM n = 0 IMPLIES bvn o bvm = bvm

%------------------------------------------------------------------------
% See bv_concat_lems for proof that (bvec,o,null_bv) is a monoid
% See bv_concat_nat  for lemma giving bv2nat(bvn o bvm)
%------------------------------------------------------------------------

END bv_concat

$$$bv_concat.prf
(|bv_concat| (|oh_TCC1| "" (TCC) NIL) (|oh_TCC2| "" (SUBTYPE-TCC) NIL)
 (|bvconcat_bot0_TCC1| "" (SUBTYPE-TCC) NIL)
 (|bvconcat_bot0| "" (SKOSIMP*)
  (("" (EXPAND "o ")
    (("" (APPLY-EXTENSIONALITY 1)
      (("" (REPLACE -1) (("" (ASSERT) NIL)))))))))
 (|bvconcat_top0_TCC1| "" (SUBTYPE-TCC) NIL)
 (|bvconcat_top0| "" (SKOSIMP*)
  (("" (EXPAND "o ")
    (("" (APPLY-EXTENSIONALITY 1)
      (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))

$$$exp2.pvs
exp2: THEORY
BEGIN

  n,m, x1, x2: VAR nat
  
  exp2(n: nat): RECURSIVE posnat = IF n = 0 THEN 1 ELSE 2 * exp2(n - 1) ENDIF
    MEASURE n

% === Properties of exp2 ===================================================

  exp2_def	 : LEMMA exp2(n) = 2^n
 
  exp2pos	 : LEMMA exp2(n)>0
 
  exp2_n	 : LEMMA exp2(n+1) = 2*exp2(n)
 
  exp2_sum	 : LEMMA exp2(n + m) = exp2(n) * exp2(m)
 
  exp2_minus	 : LEMMA (FORALL n,(k:upto(n)): exp2(n-k)=exp2(n)/exp2(k))
 
  exp2_strictpos : LEMMA n > 0 IMPLIES exp2(n) > 1
 
  exp2_lt	 : LEMMA n < m IMPLIES exp2(n) < exp2(m)

  exp_prop       : LEMMA x1 < exp2(n) AND  x2 < exp2(m) 
                           IMPLIES x1 * exp2(m) + x2 < exp2(n + m)

END exp2



$$$exp2.prf
(|exp2|
 (|exp2_TCC1| "" (SKOLEM 1 ("n!1"))
  (("" (FLATTEN) (("" (ASSERT) NIL)))))
 (|exp2_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|exp2_def| "" (INDUCT-AND-REWRITE "n" 1 "^" "expt" "exp2") NIL)
 (|exp2pos| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|exp2_n| "" (SKOSIMP*)
  (("" (REWRITE "exp2_def")
    (("" (REWRITE "expt_plus")
      (("" (REWRITE "expt_x1") (("" (REWRITE "exp2_def") NIL)))))))))
 (|exp2_sum| "" (SKOSIMP*)
  (("" (REWRITE "exp2_def")
    (("" (REWRITE "expt_plus")
      (("" (REWRITE "exp2_def")
        (("" (REWRITE "exp2_def") (("" (ASSERT) NIL)))))))))))
 (|exp2_minus_TCC1| "" (SUBTYPE-TCC) NIL)
 (|exp2_minus| "" (SKOSIMP*)
  (("" (REWRITE "exp2_def")
    (("" (REWRITE "exp2_def")
      (("" (REWRITE "exp2_def")
        (("" (REWRITE "minus_add")
          (("" (ASSERT)
            (("" (TYPEPRED "k!1")
              (("" (CASE "k!1=0")
                (("1" (ASSERT)
                  (("1" (REPLACE -1)
                    (("1" (HIDE -1)
                      (("1" (LEMMA "expt_x0")
                        (("1" (INST -1 "2")
                          (("1" (ASSERT) NIL)))))))))))
                 ("2" (ASSERT)
                  (("2" (REWRITE "expt_plus")
                    (("2" (EXPAND "^")
                      (("2" (ASSERT) NIL)))))))))))))))))))))))
 (|exp2_strictpos| "" (INDUCT "n")
  (("1" (EXPAND "exp2") (("1" (PROPAX) NIL)))
   ("2" (SKOLEM 1 ("j!1"))
    (("2" (FLATTEN)
      (("2" (LEMMA "exp2_n" ("n" "j!1"))
        (("2" (TYPEPRED "j!1")
          (("2" (CASE "j!1 = 0")
            (("1" (ASSERT)
              (("1" (ASSERT)
                (("1" (EXPAND "exp2") (("1" (ASSERT) NIL)))))))
             ("2" (ASSERT) NIL)))))))))))))
 (|exp2_lt| "" (INDUCT "m" 1)
  (("1" (SKOLEM 1 ("j!1")) (("1" (FLATTEN) (("1" (ASSERT) NIL)))))
   ("2" (SKOLEM 1 ("j!1"))
    (("2" (FLATTEN)
      (("2" (SKOLEM 1 ("n!1"))
        (("2" (FLATTEN)
          (("2" (INST -1 "n!1")
            (("2" (EXPAND "exp2" 1 2)
              (("2" (CASE "n!1 = j!1")
                (("1" (REPLACE -1 * RL) (("1" (ASSERT) NIL)))
                 ("2" (ASSERT) NIL)))))))))))))))))
 (|exp_prop| "" (SKOSIMP*)
  (("" (REWRITE "exp2_sum")
    (("" (LEMMA "both_sides_times_pos_le1")
      (("" (INST -1 "exp2(m!1)" "x1!1" "exp2(n!1)-1")
        (("" (ASSERT) NIL))))))))))
$$$bv_nat.pvs
bv_nat[N: nat]: THEORY
% -----------------------------------------------------------------------
% This theory introduces the functions bv2nat and nat2bv that convert 
% between bit vectors and natural numbers.
%
%    Introduces:
%         bv2nat: function[bvec -> below(exp2(N))] 
%         nat2bv: function[below(exp2(N)) -> bvec]
% -----------------------------------------------------------------------

BEGIN

   IMPORTING bv[N], exp2

% === Interpretation of a bit vector as a natural number ================

  % ----------------------------------------------------------------------
  % bv2nat_rec is an auxilliary function used only to define bv2nat.
  % It interprets the lower portion of a bit vector as a natural number.
  % ----------------------------------------------------------------------

  bv2nat_rec(n: upto(N), bv:bvec): RECURSIVE nat =
      IF n = 0 THEN 0
      ELSE exp2(n-1) * bv(n-1) + bv2nat_rec(n - 1, bv)
      ENDIF
    MEASURE n

  bv_lem: LEMMA (FORALL (n: below(N)),(bv: bvec): bv(n) = 0 OR bv(n) = 1)

  bv2nat_rec_bound: LEMMA 
      (FORALL (n: upto(N)),(bv: bvec): bv2nat_rec(n, bv) < exp2(n))

  bv2nat(bv:bvec): below(exp2(N)) = bv2nat_rec(N, bv)

  nat2bv(val:below(exp2(N))): bvec = inverse(bv2nat)(val)


% === Properties of bv2nat and nat2bv ===================================

  n           : VAR upto(N)
  val         : VAR below(exp2(N))
  bv, bv1, bv2: VAR bvec

  uniqueness: LEMMA N /= 0 IMPLIES bvec0 /= bvec1

  % ----------------------------------------------------------------------
  % bv2nat_rec is injective over the lower n bits.
  % ----------------------------------------------------------------------

  bv2nat_inj_rec: LEMMA
      bv2nat_rec(n, bv1) = bv2nat_rec(n, bv2)
        <=>  (FORALL (m: below(N)): (m < n) => bv1(m) = bv2(m))

  % ----------------------------------------------------------------------
  % bv2nat_rec is surjective over the lower n bits.
  % ----------------------------------------------------------------------

  bv2nat_surj_rec: LEMMA 
      FORALL (y:below(exp2(n))): EXISTS bv:bv2nat_rec(n, bv) = y

  % ----------------------------------------------------------------------
  % bv2nat is injective, i.e. 
  %   (FORALL (x, y: bvec): (bv2nat(x) = bv2nat(y) => (x = y)))
  % ----------------------------------------------------------------------

  bv2nat_inj : THEOREM injective?(bv2nat)

  % ----------------------------------------------------------------------
  % bv2nat is surjective, i.e.
  %    (FORALL (y: below(exp2(N))): (EXISTS (x: bvec): bv2nat(x) = y))
  % ----------------------------------------------------------------------

  bv2nat_surj      : THEOREM surjective?(bv2nat)

  % ----------------------------------------------------------------------
  % bv2nat is bijective (injective and surjective)
  % ----------------------------------------------------------------------

  bv2nat_bij       : THEOREM bijective?(bv2nat)    
  bv2nat_inv       : THEOREM bv2nat(nat2bv(val)) = val


% === Useful lemmas =====================================================
      
  nat2bv_bij       : THEOREM bijective?(nat2bv)

  nat2bv_inv       : THEOREM nat2bv(bv2nat(bv)) = bv

  bv2nat_rec_bvec0 : LEMMA bv2nat_rec(n, bvec0) = 0
 
  bv2nat_bvec0     : LEMMA bv2nat(bvec0) = 0

  bv2nat_rec_bvec1 : LEMMA bv2nat_rec(n, bvec1) = exp2(n)-1

  bv2nat_bvec1     : LEMMA bv2nat(bvec1) = exp2(N)-1




END bv_nat

$$$bv_nat.prf
(|bv_nat|
 (|bv2nat_rec_TCC1| "" (GROUND)
  (("" (SKOLEM 1 ("n!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))
 (|bv2nat_rec_TCC2| "" (GROUND) (("" (TCC) NIL)))
 (|bv2nat_rec_TCC3| "" (TCC) NIL) (|bv2nat_rec_TCC4| "" (TCC) NIL)
 (|bv_lem| "" (SKOSIMP) (("" (ASSERT) NIL)))
 (|bv2nat_rec_bound| "" (INDUCT-AND-REWRITE "n" 1 "bv2nat_rec" "exp2")
  (("" (LEMMA "bv_lem") (("" (INST - "jt!1" "bv!1") (("" (GROUND) NIL)))))))
 (|bv2nat_TCC1| "" (GROUND) NIL)
 (|bv2nat_TCC2| "" (SKOSIMP*) (("" (REWRITE "bv2nat_rec_bound") NIL)))
 (|uniqueness| "" (CASE "bvec0(0)=bvec1(0)")
  (("1" (TCC) NIL) ("2" (PROP) (("2" (REPLACE -1) (("2" (PROPAX) NIL)))))
   ("3" (ASSERT) NIL)))
 (|bv2nat_inj_rec| "" (INDUCT "n")
  (("1" (TCC) NIL)
   ("2" (SKOSIMP*)
    (("2" (ASSERT)
      (("2" (EXPAND "bv2nat_rec" +)
        (("2" (INST - "bv1!1" "bv2!1")
          (("2" (BDDSIMP)
            (("1" (SKOSIMP*)
              (("1" (INST?)
                (("1" (ASSERT)
                  (("1" (ASSERT)
                    (("1" (REWRITE "both_sides_times2") NIL)))))))))
             ("2" (ASSERT) (("2" (INST -4 "jt!1") (("2" (ASSERT) NIL)))))
             ("3" (LEMMA "bv2nat_rec_bound")
              (("3" (INST-CP - "jt!1" "bv1!1")
                (("3" (INST - "jt!1" "bv2!1")
                  (("3" (LEMMA "bv_lem")
                    (("3" (INST-CP - "jt!1" "bv1!1")
                      (("3" (INST - "jt!1" "bv2!1")
                        (("3" (GROUND) NIL)))))))))))))
             ("4" (SKOSIMP*) (("4" (INST?) (("4" (ASSERT) NIL)))))))))))))))))
 (|bv2nat_surj_rec| "" (INDUCT "n" 1 "upto_induction[N]")
  (("1" (SKOSIMP*)
    (("1" (TYPEPRED "y!1") (("1" (TCC) (("1" (INST + "bvec0") NIL)))))))
   ("2" (SKOSIMP*)
    (("2" (TYPEPRED "y!1")
      (("2" (EXPAND "exp2")
        (("2" (EXPAND "bv2nat_rec" +)
          (("2"
            (CASE "forall bv,(b:bit),(n:below(N)),(m:{n1:below(N)|n<=n1}):
bv2nat_rec(n,bv)=bv2nat_rec(n,bv with [(m):=b])")
            (("1" (CASE "y!1 bit]
%       ^(bv, (i: below(N))): bit
% -----------------------------------------------------------------------
BEGIN

  IMPORTING bit

  bvec : TYPE = [below(N) -> bit]

  bvec1: bvec = (LAMBDA (n: below(N)) : 1)
  bvec0: bvec = (LAMBDA (n: below(N)) : 0)


  fill(b: bit): bvec = (LAMBDA (n: below(N)): b) 

  fill_lem:  LEMMA fill(0) = bvec0 AND fill(1) = bvec1 

  unspecified_bool : bool
  unspecified_bit  : bit
  unspecified_bvec : bvec

  %-----------------------------------------------------------------------    
  % The implementation of the bitvector can be hidden through use of
  % the ^ function below.
  %-----------------------------------------------------------------------  
    
  ^(bv: bvec, (i: below(N))): bit = bv(i)

END bv

$$$bv.prf
(|bv| (|bvec1_TCC1| "" (TCC) NIL) (|bvec0_TCC1| "" (TCC) NIL)
 (|fill_lem_TCC1| "" (SUBTYPE-TCC) NIL)
 (|fill_lem_TCC2| "" (SUBTYPE-TCC) NIL)
 (|fill_lem| "" (EXPAND "fill")
  (("" (EXPAND "bvec0")
    (("" (EXPAND "bvec1") (("" (PROPAX) NIL)))))))
 (|unspecified_bit_TCC1| "" (INST 1 "0") NIL))
$$$bv_top.pvs
bv_top[N: nat]: THEORY
%------------------------------------------------------------------------
%  Top of bit-vectors theory.
%  --------------------------
%      Authors:  Paul Miner
%                Ricky W. Butler
%                Mandayam Srivas
%                Steve Miller
%                Dave Greve
%       
%      Index:
%      ------
%        bv		  -- basic definition of bitvector type "bvec"
%        bv_nat		  -- interpretes bvec as a natural number
%        bv_int		  -- interpretes bvec as an integer
%        bv_arithmetic	  -- defines basic operators (i.e. + - >) over
%			     bitvectors
%        bv_extractors	  -- defines extractor operator ^ that
%        bv_concat	  -- defines concatenation operator o
%			     creates smaller bitvectors from larger
%           bv_concat_lems:    establishes that concat is a monoid
%           bv_concat_nat:     formula for bv2nat of concat
%        bv_manipulations -- lemmas concerning ^ and o
%        bv_bitwise	  -- defines bit-wise logical operations on bitvectors
%          bv_bitwise_lems:    lemmas about bit-wise logical operations 
%        bv_shift	  -- defines shift operations
%        bv_extend        -- zero and sign extend operations
%        bv_fract	  -- defines fractional interpretation of a bitvector
%        bv_select	  -- defines operators bv_select and bv_assign
%        bv_rules	  -- rewrite-oriented bv lemmas
%
%
%                               bv
%                               |
%       ------------------------------------------------------------
%       |        |                 |               |               |
%  bv_bitwise  bv_nat          bv_concat       bv_fract      bv_extractors
%  |   |         |                 |                               |
%  |   |    --------        -------------------------------        |        
%  |   |    |      |        |             |               |        |
%  |   |  bv_int   |   bv_concat_nat  bv_concat_lems      |        |      
%  |   |    |      |        |                             |        |          
%  |   |    |      |        |      ==========================================
%  |   |    | bv_arith_nat  |      ||        ||           ||               ||
%  |   |    |      |        |   bv_shift  bv_rotate  bv_manipulations  bv_extend
%  |   |    |      |        |    /
%  |   |    |      |        |   /
%  |   |    |      |        |  /
%  |   |    |      |        | |
%  |   |    |     bv_arith_shift
%  |   |    |      |
%  |   bv_arithmetic
%  |  
% bv_bitwise_lems 
%----------------------------------------------------------------------------
  
 BEGIN

  IMPORTING bv, bv_bitwise, bv_nat, bv_concat, bv_fract, bv_extractors, 
            bv_int, bv_concat_nat, bv_concat_lems,
            bv_shift, bv_rotate, bv_manipulations,  bv_extend, 
            bv_arithmetic, 
            bv_bitwise_lems, 
            bv_select, bv_rules

END bv_top

$$$div_nt_alt.pvs
div_nt_alt: THEORY

BEGIN

  IMPORTING div_nt

  n: VAR nat
  m: VAR posnat
  natdiv(n,m): RECURSIVE nat =
    (IF n>=m THEN 1+natdiv(n-m, m) ELSE 0 ENDIF)
    MEASURE (LAMBDA n,m: n)

  i,k: VAR int
  j: VAR nonzero_integer

  is_multiple(i,j): bool = (EXISTS k: i = k*j)
 
  rdiv(i,j): integer = IF sgn(i) = sgn(j) THEN
                          natdiv(abs(i),abs(j))
                       ELSIF is_multiple(i,j) THEN
                          -natdiv(abs(i),abs(j))
                       ELSE
                          -natdiv(abs(i),abs(j))-1
                       ENDIF

  floor_is_natdiv: LEMMA natdiv(n,m) = floor(n/m)

  rdiv_lem: LEMMA div(i,j) = rdiv(i,j)

END div_nt_alt



$$$div_nt_alt.prf
(|div_nt_alt| (|natdiv_TCC1| "" (TCC :DEFS !) NIL)
 (|natdiv_TCC2| "" (TCC :DEFS !) NIL)
 (|floor_is_natdiv| "" (INDUCT "n" 1 "NAT_induction")
  (("" (SKOSIMP*)
    (("" (CASE "j!1 < m!1")
      (("1" (REWRITE "floor_small")
        (("1" (HIDE -2)
          (("1" (EXPAND "natdiv")
            (("1" (ASSERT) (("1" (REWRITE "pos_div_ge") NIL)))))))
         ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))
       ("2" (EXPAND "natdiv" 2)
        (("2" (ASSERT)
          (("2" (INST -1 "j!1-m!1")
            (("2" (ASSERT)
              (("2" (INST?)
                (("2" (REPLACE -1)
                  (("2" (HIDE -1)
                    (("2" (LEMMA "floor_plus_int")
                      (("2" (INST -1 "-1" "j!1/m!1")
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|rdiv_lem| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "rdiv")
      (("" (LIFT-IF)
        (("" (LEMMA "floor_is_natdiv")
          (("" (INST -1 "abs(j!1)" "abs(i!1)")
            (("" (REPLACE -1)
              (("" (HIDE -1)
                (("" (LEMMA "floor_neg")
                  (("" (INST?)
                    ((""
                      (CASE-REPLACE
                       "integer_pred(i!1/j!1) IFF is_multiple(i!1,j!1)")
                      (("1" (HIDE -1)
                        (("1" (EXPAND "sgn")
                          (("1" (EXPAND "abs")
                            (("1" (LIFT-IF)
                              (("1" (LIFT-IF)
                                (("1" (LIFT-IF)
                                  (("1" (ASSERT)
                                    (("1" (GROUND)
                                      (("1"
                                        (EXPAND "is_multiple")
                                        (("1"
                                          (INST 1 "i!1/j!1")
                                          (("1" (ASSERT) NIL)))))
                                       ("2"
                                        (EXPAND "is_multiple")
                                        (("2"
                                          (INST 1 "i!1/j!1")
                                          (("2" (ASSERT) NIL)))))
                                       ("3"
                                        (EXPAND "integer?")
                                        (("3"
                                          (EXPAND "is_multiple")
                                          (("3" (PROPAX) NIL)))))
                                       ("4"
                                        (EXPAND "is_multiple")
                                        (("4" (PROPAX) NIL)))))))))))))))))))
                       ("2" (HIDE -1 2)
                        (("2" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (EXPAND "is_multiple")
                              (("1" (INST 1 "i!1/j!1")
                                (("1" (ASSERT) NIL)))))))
                           ("2" (FLATTEN)
                            (("2" (EXPAND "is_multiple")
                              (("2" (SKOSIMP*)
                                (("2" (REPLACE -1)
                                  (("2" (HIDE -1)
                                    (("2" (ASSERT)
                                      NIL))))))))))))))))))))))))))))))))))))))
$$$div_alt.pvs
div_alt: THEORY

BEGIN

  IMPORTING div

  n: VAR nat
  m: VAR posnat
  natdiv(n,m): RECURSIVE nat =
    (IF n>=m THEN 1+natdiv(n-m, m) ELSE 0 ENDIF)
    MEASURE (LAMBDA n,m: n)

  i: VAR int
  j: VAR nonzero_integer

  rdiv(i,j): integer = sgn(i)*sgn(j)*natdiv(abs(i),abs(j))

  natdiv_is_floor: LEMMA natdiv(n,m) = floor(n/m)

  rdiv_lem: LEMMA div(i,j) = rdiv(i,j)

END div_alt



$$$div_alt.prf
(|div_alt| (|natdiv_TCC1| "" (TCC :DEFS !) NIL)
           (|natdiv_TCC2| "" (TCC :DEFS !) NIL)
           (|natdiv_is_floor| ""
                              (INDUCT "n" 1 "NAT_induction")
                              (("" (SKOSIMP*)
                                   (("" (CASE "j!1 < m!1")
                                        (("1" (REWRITE "floor_small")
                                              (("1" (HIDE -2)
                                                    (("1" (EXPAND "natdiv")
                                                          (("1" (ASSERT)
                                                                (("1"
                                                                   (REWRITE
                                                                     "pos_div_ge")
                                                                   NIL)))))))
                                                ("2" (EXPAND "abs")
                                                     (("2" (PROPAX)
                                                           NIL)))))
                                          ("2" (EXPAND "natdiv" 2)
                                               (("2" (ASSERT)
                                                     (("2" (INST -1
                                                                 "j!1-m!1")
                                                           (("2" (ASSERT)
                                                                 (("2" (INST?)
                                                                      (("2"
                                                                      (REPLACE
                                                                      -1)
                                                                      (("2"
                                                                      (HIDE
                                                                      -1)
                                                                      (("2"
                                                                      (LEMMA
                                                                      "floor_plus_int")
                                                                      (("2"
                                                                      (INST
                                                                      -1
                                                                      "-1"
                                                                      "j!1/m!1")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)
                                                                      ("2"
                                                                      (AUTO-REWRITE-THEORY
                                                                      "integers")
                                                                      (("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))))))))))))))
           (|rdiv_lem| ""
                       (SKOSIMP*)
                       (("" (EXPAND "div")
                            (("" (EXPAND "rdiv")
                                 (("" (REWRITE "natdiv_is_floor")
                                      (("" (ASSERT) NIL))))))))))
$$$mod_lems.pvs
mod_lems: THEORY
%------------------------------------------------------------------------
% Develops lemmas about mod
%
% This version of "mod" is based upon the Ada Reference Manual's
% definition.  These depend upon the use of a division theory that truncates
% toward zero on a negative argument.  
%
% AUTHOR
% ------
% 
%   Ricky W. Butler   		   email: r.w.butler@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%------------------------------------------------------------------------

  BEGIN
 
  IMPORTING mod
 
  i,j,k: VAR int
  m: VAR posnat
  n,a,b,c,x: VAR nat   

% The following rule characterizes the property that incrementing
% modulo m wraps around the zero point. 

  mod_wrap_around: LEMMA n < m & (c <= m & c >= m-n) =>
                              mod(n+c, m) = n - (m-c)

  mod_wrap2:       LEMMA c < m IMPLIES mod(m+c, m) = c

% Injection-like properties for mod for limited ranges

  mod_inj1:        LEMMA x < m AND n < m AND c < m AND
                       mod(x + n, m) = mod(x + c, m) IMPLIES n = c

  mod_inj2:        LEMMA x < m AND n < m AND c < m AND
                        mod(x - n, m) = mod(x - c, m) IMPLIES n = c

  mod_wrap_inj:    LEMMA
      x < m AND a < m AND b < m AND a > 0
        IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m)

  kk, vv: VAR nat
  mod_neg_limited: LEMMA 0 <= kk AND  kk < m AND vv < m AND
                      vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk


END mod_lems

$$$mod_lems.prf
(|mod_lems|
  (|mod_wrap_around| ""
                     (SKOSIMP*)
                     (("" (EXPAND "mod")
                          (("" (LEMMA "floor_val")
                               (("" (INST?)
                                    (("" (INST -1 "1")
                                         (("" (GROUND) NIL)))))))))))
  (|mod_wrap2| ""
               (SKOSIMP*)
               (("" (EXPAND "mod")
                    (("" (CASE "(m!1 + c!1) / m!1 = 1 + c!1/m!1")
                         (("1" (LEMMA "floor_plus_int")
                               (("1" (INST -1 "1" "c!1/m!1")
                                     (("1" (LEMMA "floor_small")
                                           (("1" (INST?)
                                                 (("1" (EXPAND "abs")
                                                       (("1" (ASSERT)
                                                             NIL)))))))))))
                           ("2" (ASSERT) NIL)))))))
  (|mod_inj1| ""
              (SKOSIMP*)
              (("" (EXPAND "mod")
                   (("" (LEMMA "floor_val")
                        ((""
                           (CASE
                             "floor((x!1 + n!1) / m!1) = 0 OR floor((x!1 + n!1) / m!1) = 1")
                           (("1"
                              (CASE
                                "floor((x!1 + c!1) / m!1) = 0 OR floor((x!1 + c!1) / m!1) = 1")
                              (("1" (GROUND) NIL)
                                ("2" (CASE "x!1 + c!1 < m!1")
                                     (("1" (FLATTEN)
                                           (("1" (INST?)
                                                 (("1" (ASSERT) NIL)))))
                                       ("2" (FLATTEN)
                                            (("2"
                                               (INST -2
                                                     "x!1+c!1"
                                                     "m!1"
                                                     "1")
                                               (("2" (ASSERT) NIL)))))))))
                             ("2" (CASE "x!1 + n!1 < m!1")
                                  (("1" (INST?)
                                        (("1" (FLATTEN)
                                              (("1" (ASSERT) NIL)))))
                                    ("2" (FLATTEN)
                                         (("2" (INST -1
                                                     "x!1+n!1"
                                                     "m!1"
                                                     "1")
                                               (("2" (ASSERT) NIL)))))))))))))))
  (|mod_inj2| ""
              (SKOSIMP*)
              (("" (EXPAND "mod")
                   (("" (REWRITE "floor_small")
                        (("1" (REWRITE "floor_small")
                              (("1" (TCC-BDD) NIL) ("2" (TCC-BDD) NIL)))
                          ("2" (TCC-BDD) NIL)))))))
  (|mod_wrap_inj| ""
                  (SKOSIMP*)
                  (("" (IFF 1)
                       (("" (SPLIT 1)
                            (("1" (FLATTEN)
                                  (("1" (CASE "abs(x!1-b!1) < abs(m!1)")
                                        (("1" (LEMMA "mod_lt")
                                              (("1" (INST -1
                                                          "x!1-b!1"
                                                          "m!1")
                                                    (("1" (ASSERT)
                                                          (("1"
                                                             (LEMMA "mod_lt")
                                                             (("1"
                                                                (INST -1
                                                                      "x!1+a!1"
                                                                      "m!1")
                                                                (("1"
                                                                   (LEMMA
                                                                     "mod_wrap_around")
                                                                   (("1"
                                                                      (INST?)
                                                                      (("1"
                                                                      (EXPAND
                                                                      "sgn")
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (ASSERT)
                                                                      (("1"
                                                                      (EXPAND
                                                                      "abs")
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (GROUND)
                                                                      NIL)))))))))))))))))))))))))
                                          ("2" (HIDE -1 2)
                                               (("2" (EXPAND "abs")
                                                     (("2" (LIFT-IF)
                                                           (("2" (GROUND)
                                                                 NIL)))))))))))
                              ("2" (FLATTEN)
                                   (("2" (CASE-REPLACE "a!1 = m!1-b!1")
                                         (("1" (LEMMA "mod_sum")
                                               (("1"
                                                  (INST -1
                                                        "x!1-b!1"
                                                        "m!1"
                                                        "1")
                                                  (("1" (ASSERT) NIL)))))
                                           ("2" (ASSERT) NIL)))))))))))
  (|mod_neg_limited| ""
                     (SKOSIMP*)
                     (("" (LEMMA "mod_lt")
                          (("" (INST?)
                               (("" (EXPAND "abs")
                                    (("" (ASSERT)
                                         (("" (EXPAND "sgn")
                                              (("" (PROPAX) NIL))))))))))))))
$$$mod_div_lems.pvs
mod_div_lems: THEORY
%------------------------------------------------------------------------
%
%
%------------------------------------------------------------------------

BEGIN
 
  IMPORTING floor_div_props, rem, mod

  i: VAR int
  j: VAR nonzero_integer

  mod_rem: LEMMA mod(i,j)= IF sgn(i) = sgn(j) OR integer?(i/j) THEN
                              rem(i,j)
                           ELSE j + rem(i,j)
                           ENDIF

END mod_div_lems

$$$mod_div_lems.prf
(|mod_div_lems|
  (|rem_rng| ""
             (SKOSIMP*)
             (("" (EXPAND "rem")
                  (("" (REWRITE "div_def")
                       (("" (LIFT-IF)
                            (("" (SPLIT 3)
                                 (("1" (FLATTEN)
                                       (("1" (CASE "i!1 = 0")
                                             (("1" (ASSERT)
                                                   (("1" NIL NIL)))
                                               ("2" (HIDE 2 4)
                                                    (("2" (EXPAND "sgn")
                                                          (("2"
                                                             (LEMMA
                                                               "pos_div_ge")
                                                             (("2" (INST?)
                                                                   (("2"
                                                                      (LEMMA
                                                                      "div_eq_zero")
                                                                      (("2"
                                                                      (INST?)
                                                                      (("2"
                                                                      (GROUND)
                                                                      (("2"
                                                                      NIL
                                                                      NIL)))))))))))))))))))
                                   ("2" (FLATTEN)
                                        (("2" (SPLIT 2)
                                              (("1" (FLATTEN)
                                                    (("1" (PROPAX)
                                                          (("1" NIL NIL)))))
                                                ("2" (FLATTEN)
                                                     (("2"
                                                        (LEMMA "pos_div_ge")
                                                        (("2" (INST?)
                                                              (("2" (FLATTEN)
                                                                    (("2"
                                                                      (HIDE -2)
                                                                      (("2"
                                                                      (HIDE
                                                                      1
                                                                      5)
                                                                      (("2"
                                                                      (EXPAND
                                                                      "sgn")
                                                                      (("2"
                                                                      (EXPAND
                                                                      "abs")
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (GROUND)
                                                                      (("2"
                                                                      NIL
                                                                      NIL)))))))))))))))))))))))))))))))))))))
  (|mod_rem| ""
             (SKOSIMP*)
             (("" (EXPAND "rem")
                  (("" (EXPAND "div")
                       (("" (EXPAND "mod")
                            (("" (EXPAND "sgn")
                                 (("" (LIFT-IF)
                                      (("" (LIFT-IF)
                                           (("" (ASSERT)
                                                (("" (LIFT-IF)
                                                     (("" (EXPAND "abs")
                                                          ((""
                                                             (LEMMA "floor_neg")
                                                             (("" (INST?)
                                                                  ((""
                                                                     (LIFT-IF)
                                                                     ((""
                                                                      (GROUND)
                                                                      NIL))))))))))))))))))))))))))))
$$$div_nt.pvs
div_nt: THEORY

%------------------------------------------------------------------------
% Defines natural and integer division  (Number Theory Style)
%
% There is no universally agreed semantics for integer division for a
% negative argument.  For a negative argument, division can be defined
% with truncation towards or away from zero.  The definition in this
% theory truncates away from zero (i.e. div(-7,3) = -3).  This is is the
% approach used in most number theory books.  This approach has the
% advantage that div(i,m) = the greatest integer less than i/m.  The
% alternate approach (i.e. truncation towards zero: div(-7,3) = -2) is
% simpler to compute because div(-i,m) = -div(i,m) under that
% definition.  It is the method defined in tha Ada reference manual.
%   
%% AUTHOR
% ------
% 
%   Ricky W. Butler   		   email: r.w.butler@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%------------------------------------------------------------------------


  BEGIN

  IMPORTING floor_div_props

  negint: TYPE = {i: int | i < 0} CONTAINING -1

  i,k: VAR int
  n: VAR nat
  m: VAR posnat
  j: VAR nonzero_integer
  x: VAR real

  div(i,j): integer = floor(i/j)

  JUDGEMENT div HAS_TYPE [nat,posnat -> nat]
  JUDGEMENT div HAS_TYPE [negint,posnat -> negint]
  JUDGEMENT div HAS_TYPE [negint,negint -> nonneg_int]
  JUDGEMENT div HAS_TYPE [posnat,negint -> negint]

  div_nat:        LEMMA div(n,m) = IF n>=m THEN 1 + div(n-m, m) ELSE 0 ENDIF

  div_neg_d:	  LEMMA div(i,-j) = IF integer?(i/j) THEN
				      -div(i,j)
				    ELSE
				      -div(i,j)-1
				    ENDIF 
		       
  div_neg:	  LEMMA div(-i,j) = IF integer?(i/j) THEN
			              -div(i,j)
				    ELSE
				      -div(i,j)-1
				    ENDIF
 

  div_def:      THEOREM div(i,m) =
                           IF i >= m THEN 1 + div(i-m, m) 
                           ELSIF i >= 0 THEN 0
                           ELSIF integer?(i/m) THEN -div(-i,m) 
                           ELSE
                             -1 - div(-i,m)           
                           ENDIF   

 
  div_sgn:        LEMMA div(i,-j) = div(-i,j) 

  div_value:      LEMMA i >= k*j AND i < (k+1)*j IMPLIES 
                          div(i,j) = k

% ================== div for special values =============================

  div_zero:	  LEMMA div(0,j) = 0
  
  div_one:	  LEMMA abs(j) > 1 IMPLIES div(1,j) = 
                           IF j >= 0 THEN 0 ELSE -1 ENDIF
   
  div_eq_arg:	  LEMMA div(j,j) = 1
  
  div_by_one:	  LEMMA div(i,1) = i

  div_eq_0:	  LEMMA div(i,j) = 0 IMPLIES i = 0 OR
                    (sgn(i) = sgn(j) AND abs(i) < abs(j))
  
  div_lt:	  LEMMA abs(i) < abs(j) IMPLIES 
                          div(i,j) = IF i = 0 OR sgn(i) = sgn(j) THEN 0 
                                     ELSE -1
                                     ENDIF

  div_parity:	  LEMMA sgn(i) = sgn(j) IMPLIES div(i,j) >= 0
		    
  div_parity_neg: LEMMA sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0

  div_smaller:    LEMMA m * div(n,m) <= n 

  div_abs:        LEMMA abs(div(i,j)) =
                          IF integer?(i/j) OR sgn(i) = sgn(j) THEN
                             div(abs(i),abs(j))
                          ELSE div(abs(i),abs(j)) + 1
                          ENDIF
 
  div_max:        LEMMA abs(j) * abs(div(i,j)) <= abs(i) + abs(j)

% ================== div over addition =================================

  div_multiple:      LEMMA div(k*j,j) = k   

  div_sum:           LEMMA div(i+k*j,j) = div(i,j) + k

  END div_nt



$$$div_nt.prf
(|div_nt| (|negint_TCC1| "" (TCC) NIL)
          (|div_TCC1| ""
                      (SKOSIMP*)
                      (("" (ASSERT)
                           (("" (EXPAND "div")
                                (("" (LEMMA "pos_div_ge")
                                     (("" (INST -1 "x2!1" "x1!1")
                                          (("" (GROUND) NIL)))))))))))
          (|div_TCC2| ""
                      (SKOSIMP*)
                      (("" (EXPAND "div")
                           (("" (LEMMA "pos_div_ge")
                                (("" (INST -1 "x2!1" "x1!1")
                                     (("" (GROUND) NIL)))))))))
          (|div_TCC3| ""
                      (SKOSIMP*)
                      (("" (ASSERT) NIL)))
          (|div_TCC4| ""
                      (SKOSIMP*)
                      (("" (EXPAND "div")
                           (("" (LEMMA "pos_div_ge")
                                (("" (INST?)
                                     (("" (FLATTEN)
                                          (("" (GROUND) NIL)))))))))))
          (|div_TCC5| ""
                      (SKOSIMP*)
                      (("" (EXPAND "div")
                           (("" (LEMMA "pos_div_ge")
                                (("" (INST -1 "x2!1" "x1!1")
                                     (("" (GROUND) NIL)))))))))
          (|div_nat| ""
                     (SKOSIMP*)
                     (("" (LIFT-IF)
                          (("" (EXPAND "div")
                               (("" (SPLIT 1)
                                    (("1" (FLATTEN)
                                          (("1"
                                             (CASE
                                               "(n!1 - m!1) / m!1 = n!1/m!1 - 1")
                                             (("1" (LEMMA "floor_plus_int")
                                                   (("1"
                                                      (INST -1
                                                            "-1"
                                                            "n!1/m!1")
                                                      (("1" (GROUND)
                                                            NIL)))))
                                               ("2" (ASSERT) NIL)))))
                                      ("2" (FLATTEN)
                                           (("2" (LEMMA "floor_small")
                                                 (("2" (INST?)
                                                       (("2" (EXPAND "abs")
                                                             (("2" (ASSERT)
                                                                   (("2"
                                                                      (REPLACE
                                                                      -1)
                                                                      (("2"
                                                                      (HIDE
                                                                      -1)
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (LEMMA
                                                                      "pos_div_ge")
                                                                      (("2"
                                                                      (INST?)
                                                                      (("2"
                                                                      (GROUND)
                                                                      NIL)))))))))))))))))))))))))))))
          (|div_neg_d| ""
                       (SKOSIMP*)
                       (("" (EXPAND "div")
                            (("" (LIFT-IF)
                                 (("" (LEMMA "floor_neg")
                                      (("" (INST -1 "i!1/j!1")
                                           (("" (LIFT-IF)
                                                (("" (GROUND) NIL)))))))))))))
          (|div_neg| ""
                     (SKOSIMP*)
                     (("" (EXPAND "div")
                          (("" (LIFT-IF)
                               (("" (LEMMA "floor_neg")
                                    (("" (INST -1 "i!1/j!1")
                                         (("" (LIFT-IF)
                                              (("" (GROUND) NIL)))))))))))))
          (|div_def_TCC1| "" (TCC) NIL)
          (|div_def| ""
                     (SKOSIMP*)
                     (("" (LIFT-IF)
                          (("" (SPLIT 1)
                               (("1" (FLATTEN)
                                     (("1" (LEMMA "div_nat")
                                           (("1" (INST?)
                                                 (("1" (LIFT-IF)
                                                       (("1" (ASSERT)
                                                             NIL)))
                                                   ("2" (ASSERT) NIL)))))))
                                 ("2" (FLATTEN)
                                      (("2" (SPLIT 2)
                                            (("1" (FLATTEN)
                                                  (("1" (LEMMA "div_nat")
                                                        (("1" (INST?)
                                                              (("1" (LIFT-IF)
                                                                    (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))))
                                              ("2" (FLATTEN)
                                                   (("2" (SPLIT 2)
                                                         (("1" (FLATTEN)
                                                               (("1"
                                                                  (LEMMA
                                                                    "div_neg")
                                                                  (("1"
                                                                     (INST?)
                                                                     (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))))
                                                           ("2" (FLATTEN)
                                                                (("2"
                                                                   (LEMMA
                                                                     "div_neg")
                                                                   (("2"
                                                                      (INST?)
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))))))))))
          (|div_sgn| ""
                     (SKOSIMP*)
                     (("" (EXPAND "div")
                          (("" (ASSERT) NIL)))))
          (|div_value| ""
                       (SKOSIMP*)
                       (("" (EXPAND "div")
                            (("" (LEMMA "floor_val")
                                 (("" (INST?)
                                      (("" (ASSERT) NIL)))))))))
          (|div_zero| ""
                      (SKOSIMP*)
                      (("" (EXPAND "div")
                           (("" (ASSERT) NIL)))))
          (|div_one| ""
                     (SKOSIMP*)
                     (("" (EXPAND "div")
                          (("" (LEMMA "floor_small")
                               (("" (INST -1 "1" "j!1")
                                    (("" (EXPAND "abs" -1 1)
                                         (("" (ASSERT)
                                              (("" (LEMMA "pos_div_ge")
                                                   (("" (INST -1
                                                              "j!1"
                                                              "1")
                                                        (("" (FLATTEN)
                                                             (("" (ASSERT)
                                                                  ((""
                                                                     (LIFT-IF)
                                                                     ((""
                                                                      (LEMMA
                                                                      "div_eq_zero")
                                                                      ((""
                                                                      (INST
                                                                      -1
                                                                      "j!1"
                                                                      "1")
                                                                      ((""
                                                                      (GROUND)
                                                                      NIL)))))))))))))))))))))))))))
          (|div_eq_arg| ""
                        (SKOSIMP*)
                        (("" (EXPAND "div")
                             (("" (ASSERT) NIL)))))
          (|div_by_one_TCC1| "" (ASSERT) NIL)
          (|div_by_one| ""
                        (SKOSIMP*)
                        (("" (EXPAND "div")
                             (("" (ASSERT) NIL)))))
          (|div_eq_0| ""
                      (SKOSIMP*)
                      (("" (EXPAND "div")
                           (("" (LEMMA "floor_eq_0")
                                (("" (INST -1 "i!1/j!1")
                                     (("" (SPLIT -1)
                                          (("1" (FLATTEN)
                                                (("1" (LEMMA "pos_div_ge")
                                                      (("1" (INST?)
                                                            (("1"
                                                               (LEMMA
                                                                 "div_eq_zero")
                                                               (("1" (INST?)
                                                                     (("1"
                                                                      (FLATTEN)
                                                                      (("1"
                                                                      (EXPAND
                                                                      "sgn")
                                                                      (("1"
                                                                      (EXPAND
                                                                      "abs")
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (ASSERT)
                                                                      (("1"
                                                                      (GROUND)
                                                                      (("1"
                                                                      (HIDE
                                                                      1
                                                                      3)
                                                                      (("1"
                                                                      (LEMMA
                                                                      "both_sides_times_pos_lt1")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "-j!1"
                                                                      "1"
                                                                      "i!1/j!1")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))))
                                                                      ("2"
                                                                      (LEMMA
                                                                      "both_sides_times_pos_lt1")
                                                                      (("2"
                                                                      (INST
                                                                      -1
                                                                      "j!1"
                                                                      "1"
                                                                      "i!1/j!1")
                                                                      (("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))))))))))))))))
                                            ("2" (PROPAX) NIL)))))))))))
          (|div_lt| ""
                    (SKOSIMP*)
                    (("" (EXPAND "div")
                         (("" (LEMMA "floor_small")
                              (("" (INST?)
                                   (("" (ASSERT)
                                        ((""
                                           (CASE
                                             "(i!1 = 0 OR sgn(i!1) = sgn(j!1)) = (i!1 / j!1 >= 0)")
                                           (("1" (LIFT-IF)
                                                 (("1" (EXPAND "sgn")
                                                       (("1" (LIFT-IF)
                                                             (("1" (LIFT-IF)
                                                                   (("1"
                                                                      (GROUND)
                                                                      NIL)))))))))
                                             ("2" (HIDE -1 -2 2)
                                                  (("2" (IFF 1)
                                                        (("2" (SPLIT 1)
                                                              (("1" (FLATTEN)
                                                                    (("1"
                                                                      (EXPAND
                                                                      "sgn")
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (LIFT-IF)
                                                                      (("1"
                                                                      (GROUND)
                                                                      (("1"
                                                                      (LEMMA
                                                                      "pos_div_ge")
                                                                      (("1"
                                                                      (INST
                                                                      -1
                                                                      "j!1"
                                                                      "i!1")
                                                                      (("1"
                                                                      (ASSERT)
                                                                      NIL)))))
                                                                      ("2"
                                                                      (LEMMA
                                                                      "pos_div_ge")
                                                                      (("2"
                                                                      (INST
                                                                      -1
                                                                      "-j!1"
                                                                      "-i!1")
                                                                      (("2"
                                                                      (GROUND)
                                                                      NIL)))))))))))))))
                                                                ("2" (FLATTEN)
                                                                     (("2"
                                                                      (EXPAND
                                                                      "sgn")
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (LIFT-IF)
                                                                      (("2"
                                                                      (LEMMA
                                                                      "pos_div_ge")
                                                                      (("2"
                                                                      (INST
                                                                      -1
                                                                      "j!1"
                                                                      "i!1")
                                                                      (("2"
                                                                      (LEMMA
                                                                      "div_eq_zero")
                                                                      (("2"
                                                                      (INST?)
                                                                      (("2"
                                                                      (GROUND)
                                                                      NIL)))))))))))))))))))))))))))))))))))
          (|div_parity| ""
                        (SKOSIMP*)
                        (("" (EXPAND "div")
                             (("" (EXPAND "sgn")
                                  (("" (LIFT-IF)
                                       (("" (LEMMA "pos_div_ge")
                                            (("" (INST?)
                                                 (("" (FLATTEN)
                                                      (("" (LIFT-IF)
                                                           (("" (GROUND)
                                                                NIL)))))))))))))))))
          (|div_parity_neg| ""
                            (SKOSIMP*)
                            (("" (EXPAND "div")
                                 (("" (EXPAND "sgn")
                                      (("" (LIFT-IF)
                                           (("" (LEMMA "pos_div_ge")
                                                (("" (INST?)
                                                     (("" (FLATTEN)
                                                          (("" (LIFT-IF)
                                                               (("" (GROUND)
                                                                    NIL)))))))))))))))))
          (|div_smaller| ""
                         (SKOSIMP*)
                         (("" (EXPAND "div")
                              (("" (ASSERT)
                                   (("" (TYPEPRED "floor(n!1 / m!1)")
                                        ((""
                                           (LEMMA "both_sides_times_pos_lt1")
                                           ((""
                                              (INST -1
                                                    "m!1"
                                                    "floor(n!1 / m!1)"
                                                    "n!1 / m!1")
                                              (("" (FLATTEN)
                                                   (("" (GROUND) NIL)))))))))))))))
          (|div_abs| ""
                     (SKOSIMP*)
                     (("" (EXPAND "div")
                          (("" (EXPAND "abs")
                               (("" (LIFT-IF)
                                    (("" (LIFT-IF)
                                         (("" (LIFT-IF)
                                              (("" (LEMMA "floor_neg")
                                                   (("" (INST?)
                                                        (("" (LIFT-IF)
                                                             ((""
                                                                (EXPAND "sgn")
                                                                (("" (LIFT-IF)
                                                                     ((""
                                                                      (ASSERT)
                                                                      ((""
                                                                      (LEMMA
                                                                      "pos_div_ge")
                                                                      ((""
                                                                      (INST?)
                                                                      ((""
                                                                      (GROUND)
                                                                      NIL)))))))))))))))))))))))))))))
          (|div_max| ""
                     (SKOSIMP*)
                     (("" (LEMMA "div_smaller")
                          (("" (INST -1
                                     "abs(j!1)"
                                     "abs(i!1)")
                               (("" (LEMMA "div_abs")
                                    (("" (INST?)
                                         (("" (REPLACE -1)
                                              (("" (HIDE -1)
                                                   (("" (LIFT-IF)
                                                        (("" (GROUND)
                                                             NIL)))))))))))))))))
          (|div_multiple| ""
                          (SKOSIMP*)
                          (("" (EXPAND "div")
                               (("" (ASSERT) NIL)))))
          (|div_sum| ""
                     (SKOSIMP*)
                     (("" (EXPAND "div")
                          (("" (LEMMA "floor_plus_int")
                               (("" (INST -1
                                          "k!1*j!1/j!1"
                                          "i!1/j!1")
                                    (("" (ASSERT) NIL))))))))))
$$$rem.pvs
rem: THEORY
%------------------------------------------------------------------------
% Defines remainder (rem)   (Ada Style)
%
% This version of "rem" is based upon the Ada Reference Manual's
% definition.  These depend upon the use of a division theory that truncates
% toward zero on a negative argument.  
%
% AUTHORS
% -------
%   Ricky W. Butler   		   email: r.w.butler@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
% 
%------------------------------------------------------------------------

  BEGIN
 
  IMPORTING div
 
  i,k,cc: VAR int
  m: VAR posnat
  n,a,b,c: VAR nat   

  j: VAR nonzero_integer

% ======================= define rem(i,m) ========================

  ml1: LEMMA n -  m * div(n,m) < m
  ml3: LEMMA abs(i -  m * div(i,m)) < m

  rem(i,j): {k| abs(k) < abs(j)} =  i - j*div(i,j)

  rem_neg:        LEMMA rem(-i,j) = -rem(i,j)

  rem_neg_d:      LEMMA rem(i,-j) = rem(i,j)

  rem_even:       LEMMA integer?(i/j) IMPLIES rem(i,j) = 0

  rem_eq_arg:     LEMMA rem(j,j) = 0

  rem_zero:       LEMMA rem(0,j) = 0

  rem_lt:         LEMMA abs(i) < abs(j) IMPLIES 
                        rem(i,j) = i 

  rem_it_is:      LEMMA a = b + m*c AND b < m IMPLIES
                        b = rem(a,m)

  rem_eq_0:       LEMMA rem(i,j) = 0 IMPLIES integer?(i/j)

  rem_one:        LEMMA rem(1,j) = IF abs(j) = 1 THEN 0
                                   ELSE 1
                                   ENDIF
 
  JUDGEMENT rem HAS_TYPE [nat, m:posnat -> below(m)]

  END rem

$$$rem.prf
(|rem|
 (|ml1| "" (SKOLEM!)
  (("" (EXPAND "div")
    (("" (EXPAND "sgn")
      (("" (EXPAND "abs")
        (("" (ASSERT)
          (("" (LEMMA "both_sides_times_pos_lt1")
            (("" (INST - "m!1" "n!1/m!1" "floor(n!1/m!1)+1")
              (("" (FLATTEN) (("" (GROUND) NIL)))))))))))))))))
 (|ml3| "" (SKOSIMP*)
  (("" (CASE "i!1 >= 0")
    (("1" (EXPAND "abs")
      (("1" (LIFT-IF)
        (("1" (SPLIT 1)
          (("1" (FLATTEN)
            (("1" (LEMMA "div_smaller")
              (("1" (INST?) (("1" (ASSERT) NIL)))))))
           ("2" (FLATTEN) (("2" (LEMMA "ml1") (("2" (INST?) NIL)))))))))))
     ("2" (EXPAND "abs")
      (("2" (LIFT-IF)
        (("2" (LEMMA "div_neg")
          (("2" (INST?)
            (("2" (SPLIT 2)
              (("1" (FLATTEN)
                (("1" (LEMMA "ml1")
                  (("1" (INST -1 "m!1" "-i!1")
                    (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
               ("2" (FLATTEN)
                (("2" (LEMMA "div_smaller")
                  (("2" (INST -1 "m!1" "-i!1")
                    (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))))))))))
 (|rem_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "ml3")
    (("" (CASE "j!1 >= 0")
      (("1" (INST?)
        (("1" (EXPAND "abs" 1 2) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL)))
       ("2" (INST -1 "i!1" "-j!1")
        (("1" (LEMMA "div_neg_d")
          (("1" (INST?)
            (("1" (REPLACE -1)
              (("1" (EXPAND "abs" 2 2) (("1" (ASSERT) NIL)))))))))
         ("2" (ASSERT) NIL)))))))))
 (|rem_neg| "" (SKOSIMP*)
  (("" (EXPAND "rem") (("" (REWRITE "div_neg") (("" (ASSERT) NIL)))))))
 (|rem_neg_d| "" (SKOSIMP*)
  (("" (EXPAND "rem") (("" (REWRITE "div_neg_d") (("" (ASSERT) NIL)))))))
 (|rem_even| "" (SKOSIMP*)
  (("" (EXPAND "rem") (("" (REWRITE "div_even") NIL)))))
 (|rem_eq_arg| "" (SKOLEM!)
  (("" (EXPAND "rem") (("" (REWRITE "div_eq_arg") (("" (ASSERT) NIL)))))))
 (|rem_zero| "" (SKOSIMP*)
  (("" (EXPAND "rem") (("" (REWRITE "div_zero") (("" (ASSERT) NIL)))))))
 (|rem_lt| "" (SKOSIMP*)
  (("" (EXPAND "rem") (("" (REWRITE "div_lt") (("" (ASSERT) NIL)))))))
 (|rem_it_is| "" (SKOSIMP*)
  (("" (EXPAND "rem")
    (("" (CASE "div(a!1,m!1) = c!1")
      (("1" (ASSERT) NIL)
       ("2" (HIDE 2)
        (("2" (EXPAND "div")
          (("2" (EXPAND "sgn")
            (("2" (EXPAND "abs")
              (("2" (REPLACE -1)
                (("2" (HIDE -1)
                  (("2" (LEMMA "floor_plus_int")
                    (("2" (CASE "(b!1 + m!1 * c!1) / m!1 = b!1 / m!1 + c!1")
                      (("1" (REPLACE -1)
                        (("1" (HIDE -1)
                          (("1" (INST -1 "c!1" "b!1/m!1")
                            (("1" (REPLACE -1)
                              (("1" (HIDE -1)
                                (("1" (LEMMA "floor_small")
                                  (("1" (INST?)
                                    (("1" (EXPAND "abs")
                                      (("1" (ASSERT) NIL)))))))))))))))))
                       ("2" (HIDE -1 -2 2)
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|rem_eq_0| "" (SKOSIMP)
  (("" (REWRITE "is_multiple")
    (("" (EXPAND "rem")
      (("" (INST + "div(i!1, j!1)") (("" (ASSERT) NIL)))))))))
 (|rem_one| "" (SKOSIMP*)
  (("" (LIFT-IF)
    (("" (SPLIT 1)
      (("1" (FLATTEN)
        (("1" (EXPAND "abs")
          (("1" (LIFT-IF)
            (("1" (SPLIT -1)
              (("1" (FLATTEN)
                (("1" (LEMMA "rem_eq_arg")
                  (("1" (INST -1 "1")
                    (("1" (LEMMA "rem_neg_d")
                      (("1" (INST -1 "1" "1") (("1" (ASSERT) NIL)))))))))))
               ("2" (FLATTEN)
                (("2" (LEMMA "rem_eq_arg")
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))
       ("2" (FLATTEN)
        (("2" (LEMMA "rem_lt")
          (("2" (INST?)
            (("2" (EXPAND "abs")
              (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))))))
 (|rem_TCC2| "" (INDUCT "x1" :NAME "NAT_induction")
  (("" (SKOSIMP)
    (("" (SKOSIMP)
      (("" (SPLIT)
        (("1" (EXPAND "rem" +)
          (("1" (LEMMA "div_nat")
            (("1" (INST -1 "x2!1" "j!1")
              (("1" (LIFT-IF)
                (("1" (PROP)
                  (("1" (ASSERT) NIL)
                   ("2" (INST -2 "j!1-x2!1")
                    (("1" (ASSERT)
                      (("1" (INST -2 "x2!1")
                        (("1" (FLATTEN)
                          (("1" (EXPAND "rem" -2) (("1" (ASSERT) NIL)))))))))
                     ("2" (ASSERT) NIL)))))))))))))
         ("2" (TYPEPRED "rem(j!1, x2!1)")
          (("2" (EXPAND "abs") (("2" (ASSERT) NIL))))))))))))))
$$$div.pvs
div: THEORY

%------------------------------------------------------------------------
% Defines natural and integer division  (Ada Style)
%
% There is no universally agreed semantics for integer division for a
% negative argument.  For a negative argument, division can be defined
% with truncation towards or away from zero.  The definition in this
% theory truncates toward zero (i.e. div(-7,3) = -2).  This is 
% simpler to compute because div(-i,m) = -div(i,m) and is the
% method defined in tha Ada reference manual. The alternate method
% (i.e. truncation away from zero: div(-7,3) = -3) is the approach
% used in most number theory books.  This approach has the
% advantage that div(i,m) = the greatest integer less than i/m.
%
% AUTHOR
% ------
% 
%   Ricky W. Butler   		   email: r.w.butler@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%------------------------------------------------------------------------


  BEGIN

  IMPORTING floor_div_props


  i,k: VAR int
  n: VAR nat
  m: VAR posnat
  j: VAR nonzero_integer
  x: VAR real

  div(i,j): integer = sgn(i)*sgn(j)*floor(abs(i)/abs(j))

  div_nat:     LEMMA div(n,m) = IF n < m THEN 0 ELSE 1 + div(n-m,m) ENDIF

  div_def:     LEMMA div(i,j) = IF i/j >= 0 THEN floor(i/j)
				ELSIF integer?(i/j) THEN
				   floor(i/j)
				ELSE 
				   floor(i/j) + 1
				ENDIF    

  div_value:    LEMMA IF sgn(i) = sgn(j) THEN
                         i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k 
                      ELSE
                         i > (k-1)*j AND i <= k*j IMPLIES div(i,j) = k
                      ENDIF 


  div_neg:	LEMMA div(-i,j) = -div(i,j)

  div_neg_d:	LEMMA div(i,-j) = -div(i,j)
 
% ================== div for special values =============================

  div_zero:	  LEMMA div(0,j) = 0
  
  div_one:	  LEMMA abs(j) > 1 IMPLIES div(1,j) = 0
  
  div_minus1:	  LEMMA abs(j) > 1 IMPLIES div(-1, j) = 0
  
  div_eq_arg:	  LEMMA div(j,j) = 1
  
  div_by_one:	  LEMMA div(i,1) = i
  
  div_eq_0:	  LEMMA div(i,j) = 0 IMPLIES abs(i) < abs(j)
  
  div_lt:	  LEMMA abs(i) < abs(j) IMPLIES div(i,j) = 0

  div_lt_nat:	  LEMMA n < m IMPLIES div(n,m) = 0

  div_is_0:       LEMMA div(i,j) = 0 IFF abs(i) < abs(j)
  
  div_parity:	  LEMMA (sgn(i) = sgn(j) AND abs(i) >= abs(j)) IMPLIES
			  div(i,j) > 0
		    
  div_parity_neg: LEMMA (sgn(i) /= sgn(j) AND abs(i) >= abs(j)) IMPLIES
                          div(i,j) < 0

  div_ge_0:       LEMMA (sgn(i) = sgn(j) IMPLIES div(i,j) >= 0) AND
                          (div(i,j) >= 0 IMPLIES 
                             abs(i) < abs(j) OR sgn(i) = sgn(j))

  div_le_0:       LEMMA (sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0) AND
			  (div(i,j) <= 0 IMPLIES 
                             abs(i) < abs(j) OR sgn(i) /= sgn(j))

  div_smaller:    LEMMA m * div(n,m) <= n 
 
  div_abs:        LEMMA abs(div(i,j)) = div(abs(i),abs(j))

  div_max:        LEMMA abs(j)*abs(div(i,j)) <= abs(i)

% ================== div over addition =================================

  div_multiple:	  LEMMA div(k*j,j) = k   
  
  div_even:	  LEMMA integer?(i/j) IMPLIES i - j*div(i,j) = 0
  
  div_sum:	  LEMMA IF integer?(i/j) OR sgn(i+k*j) = sgn(i) THEN
			   div(i+k*j,j) = div(i,j) + k
			ELSE 
			   div(i+k*j,j) = div(i,j) + k + sgn(i)*sgn(j)
			ENDIF

  b: VAR nat
  div_sum_nat:	  LEMMA div(n+b*m,m) = div(n,m) + b

  nonposint: TYPE = {i: int | i <= 0} CONTAINING -1
  negint: TYPE = {i: int | i < 0} CONTAINING -1

  JUDGEMENT div HAS_TYPE [nat,posnat -> nat]
  JUDGEMENT div HAS_TYPE [nonposint,posnat -> nonposint]
  JUDGEMENT div HAS_TYPE [nonposint,negint -> nat]
  JUDGEMENT div HAS_TYPE [posnat,negint -> nonposint]

  END div



$$$div.prf
(|div|
 (|div_nat| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "sgn")
      (("" (LIFT-IF)
        (("" (EXPAND "abs")
          (("" (SPLIT 1)
            (("1" (FLATTEN)
              (("1" (LEMMA "floor_small")
                (("1" (INST?) (("1" (EXPAND "abs") (("1" (ASSERT) NIL)))))))))
             ("2" (FLATTEN)
              (("2" (LEMMA "floor_plus_int")
                (("2" (INST -1 "-1" "n!1/ m!1")
                  (("2" (ASSERT) NIL)))))))))))))))))))
 (|div_def| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "abs")
      (("" (EXPAND "sgn")
        (("" (LEMMA "floor_neg")
          (("" (INST -1 "i!1/j!1")
            (("" (LEMMA "div_eq_zero")
              (("" (INST?)
                (("" (LEMMA "pos_div_lt")
                  (("" (INST?)
                    (("" (ASSERT)
                      (("" (APPLY (REPEAT (LIFT-IF)))
                        (("" (ASSERT)
                          (("" (EXPAND "integer?")
                            (("" (GROUND) NIL)))))))))))))))))))))))))))))
 (|div_value| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "sgn")
      (("" (EXPAND "abs")
        (("" (LIFT-IF)
          (("" (LIFT-IF)
            (("" (LIFT-IF)
              (("" (LIFT-IF)
                (("" (ASSERT)
                  (("" (GROUND)
                    (("1" (TYPEPRED "floor(-i!1 / j!1)")
                      (("1" (LEMMA "both_sides_div_pos_lt1")
                        (("1" (INST -1 "j!1" "-i!1" "-k!1*j!1 + j!1")
                          (("1" (ASSERT)
                            (("1" (LEMMA "both_sides_div_pos_le1")
                              (("1" (INST -1 "j!1" "-k!1*j!1" "-i!1")
                                (("1" (ASSERT)
                                  (("1"
                                    (CASE "(-k!1 * j!1 + j!1) / j!1 = -k!1 + 1")
                                    (("1" (REPLACE -1)
                                      (("1"
                                        (HIDE -1)
                                        (("1"
                                          (NAME "X" "-i!1/j!1")
                                          (("1"
                                            (REPLACE -1)
                                            (("1"
                                              (HIDE -1)
                                              (("1"
                                                (HIDE -7 -8)
                                                (("1"
                                                  (CASE
                                                   "-k!1 * j!1 / j!1 = -k!1")
                                                  (("1"
                                                    (REPLACE -1)
                                                    (("1"
                                                      (HIDE -1)
                                                      (("1" (ASSERT) NIL)))))
                                                   ("2"
                                                    (ASSERT)
                                                    NIL)))))))))))))))
                                     ("2" (ASSERT) NIL)))))))))))))))))
                     ("2" (TYPEPRED "floor(i!1 / j!1)")
                      (("2" (LEMMA "both_sides_div_pos_lt1")
                        (("2" (INST -1 "j!1" "i!1" "k!1 * j!1 + j!1")
                          (("2" (ASSERT)
                            (("2" (CASE "(k!1 * j!1 + j!1) / j!1 = k!1 + 1")
                              (("1" (REPLACE -1)
                                (("1" (HIDE -1)
                                  (("1" (LEMMA "both_sides_div_pos_le1")
                                    (("1" (INST -1 "j!1" "k!1 * j!1" "i!1")
                                      (("1"
                                        (ASSERT)
                                        (("1"
                                          (CASE "k!1 * j!1 / j!1 = k!1")
                                          (("1"
                                            (REPLACE -1)
                                            (("1"
                                              (HIDE -1)
                                              (("1"
                                                (NAME "X" "i!1/j!1")
                                                (("1"
                                                  (REPLACE -1)
                                                  (("1"
                                                    (HIDE -1)
                                                    (("1"
                                                      (HIDE -6 -7)
                                                      (("1"
                                                        (ASSERT)
                                                        NIL)))))))))))))
                                           ("2" (ASSERT) NIL)))))))))))))
                               ("2" (ASSERT)
                                NIL)))))))))))))))))))))))))))))))
 (|div_neg| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "abs")
      (("" (EXPAND "sgn")
        (("" (LIFT-IF)
          (("" (LIFT-IF)
            (("" (LIFT-IF)
              (("" (LIFT-IF)
                (("" (LIFT-IF)
                  (("" (LIFT-IF)
                    (("" (ASSERT)
                      (("" (LEMMA "floor_neg")
                        (("" (INST -1 "i!1/j!1")
                          (("" (LIFT-IF)
                            (("" (GROUND) NIL)))))))))))))))))))))))))))))
 (|div_neg_d| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "abs")
      (("" (EXPAND "sgn")
        (("" (LIFT-IF)
          (("" (LIFT-IF)
            (("" (LIFT-IF)
              (("" (LIFT-IF)
                (("" (LIFT-IF)
                  (("" (LIFT-IF) (("" (ASSERT) NIL)))))))))))))))))))))
 (|div_zero| "" (SKOSIMP*) (("" (REWRITE "div_def") (("" (ASSERT) NIL)))))
 (|div_one| "" (SKOSIMP*)
  (("" (LEMMA "div_nat")
    (("" (INST -1 "abs(j!1)" "1")
      (("" (CASE "j!1 >= 0")
        (("1" (EXPAND "abs") (("1" (ASSERT) (("1" (ASSERT) NIL)))))
         ("2" (EXPAND "abs")
          (("2" (ASSERT)
            (("2" (ASSERT)
              (("2" (LEMMA "div_neg_d")
                (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))
 (|div_minus1| "" (SKOSIMP*)
  (("" (LEMMA "div_neg")
    (("" (INST?)
      (("" (LEMMA "div_one") (("" (INST?) (("" (ASSERT) NIL)))))))))))
 (|div_eq_arg| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "sgn")
      (("" (EXPAND "abs")
        (("" (LIFT-IF) (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))))
 (|div_by_one| "" (ASSERT)
  (("" (SKOSIMP*)
    (("" (EXPAND "div")
      (("" (EXPAND "sgn")
        (("" (EXPAND "abs")
          (("" (LIFT-IF)
            (("" (LIFT-IF)
              (("" (LEMMA "floor_neg")
                (("" (INST -1 "i!1")
                  (("" (EXPAND "integer?")
                    (("" (ASSERT) NIL)))))))))))))))))))))
 (|div_eq_0| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (LEMMA "floor_eq_0")
      (("" (INST -1 "abs(i!1) / abs(j!1)")
        (("" (CASE "abs(j!1) /= 0")
          (("1" (SPLIT -2)
            (("1" (FLATTEN)
              (("1" (LEMMA "floor_eq_0")
                (("1" (INST?)
                  (("1" (EXPAND "sgn")
                    (("1" (LIFT-IF)
                      (("1" (LIFT-IF)
                        (("1" (LEMMA "both_sides_times_pos_lt1")
                          (("1" (INST -1 "abs(j!1)" "abs(i!1)/abs(j!1)" "1")
                            (("1" (GROUND) NIL)))))))))))))))))
             ("2" (EXPAND "sgn")
              (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))
           ("2" (HIDE -1 -2 2)
            (("2" (EXPAND "abs")
              (("2" (LIFT-IF) (("2" (ASSERT) NIL)))))))))))))))))
 (|div_lt| "" (SKOSIMP*)
  (("" (CASE "i!1 = 0")
    (("1" (REPLACE -1)
      (("1" (HIDE -1) (("1" (LEMMA "div_zero") (("1" (INST?) NIL)))))))
     ("2" (EXPAND "div")
      (("2" (LEMMA "floor_small")
        (("2" (INST?)
          (("2" (SPLIT -1)
            (("1" (REPLACE -1)
              (("1" (HIDE -1)
                (("1" (LIFT-IF)
                  (("1" (LEMMA "pos_div_ge")
                    (("1" (INST?)
                      (("1" (FLATTEN)
                        (("1" (EXPAND "sgn")
                          (("1" (LIFT-IF) (("1" (ASSERT) NIL)))))))))))))))))
             ("2" (HIDE 2 3)
              (("2" (EXPAND "abs")
                (("2" (LIFT-IF)
                  (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))))))))))
 (|div_lt_nat| "" (SKOSIMP*)
  (("" (LEMMA "div_lt")
    (("" (INST?) (("" (EXPAND "abs") (("" (ASSERT) NIL)))))))))
 (|div_is_0| "" (SKOSIMP*)
  (("" (LEMMA "div_eq_0")
    (("" (INST?)
      (("" (LEMMA "div_lt") (("" (INST?) (("" (GROUND) NIL)))))))))))
 (|div_parity| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (LEMMA "both_sides_div_pos_le1")
      (("" (INST -1 "abs(j!1)" "abs(j!1)" "abs(i!1)")
        (("" (ASSERT)
          (("" (EXPAND "sgn")
            (("" (HIDE -3)
              (("" (LIFT-IF)
                (("" (LIFT-IF) (("" (ASSERT) NIL)))))))))))))))))))
 (|div_parity_neg| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (LEMMA "both_sides_div_pos_le1")
      (("" (INST -1 "abs(j!1)" "abs(j!1)" "abs(i!1)")
        (("" (ASSERT)
          (("" (EXPAND "sgn")
            (("" (LIFT-IF)
              (("" (LIFT-IF)
                (("" (ASSERT) (("" (GROUND) NIL)))))))))))))))))))
 (|div_ge_0| "" (SKOSIMP*)
  (("" (LEMMA "div_parity")
    (("" (INST?)
      (("" (LEMMA "div_is_0")
        (("" (INST?)
          (("" (LEMMA "div_parity_neg")
            (("" (INST?) (("" (GROUND) NIL)))))))))))))))
 (|div_le_0| "" (SKOSIMP*)
  (("" (LEMMA "div_parity")
    (("" (INST?)
      (("" (LEMMA "div_is_0")
        (("" (INST?)
          (("" (LEMMA "div_parity_neg")
            (("" (INST?) (("" (GROUND) NIL)))))))))))))))
 (|div_smaller| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "sgn")
      (("" (EXPAND "abs")
        (("" (ASSERT)
          (("" (TYPEPRED "floor(n!1 / m!1)")
            (("" (LEMMA "both_sides_times_pos_le1")
              (("" (INST -1 "m!1" "floor(n!1 / m!1)" "n!1/m!1")
                (("" (FLATTEN) (("" (ASSERT) NIL)))))))))))))))))))
 (|div_abs| "" (EXPAND "div") (("" (GRIND) NIL)))
 (|div_max| "" (SKOSIMP*)
  (("" (LEMMA "div_smaller")
    (("" (LEMMA "div_abs")
      (("" (INST?)
        (("" (REPLACE -1) (("" (HIDE -1) (("" (INST?) NIL)))))))))))))
 (|div_multiple| "" (SKOSIMP*)
  (("" (REWRITE "div_def")
    (("" (LEMMA "floor_int")
      (("" (EXPAND "integer?") (("" (INST?) (("" (ASSERT) NIL)))))))))))
 (|div_even| "" (SKOSIMP*)
  (("" (EXPAND "integer?")
    (("" (LEMMA "div_multiple")
      (("" (CASE "(EXISTS k: j!1*k = i!1)")
        (("1" (SKOSIMP*) (("1" (INST -2 "j!1" "k!1") (("1" (ASSERT) NIL)))))
         ("2" (INST 1 "i!1/j!1") (("2" (ASSERT) NIL)))))))))))
 (|div_sum| "" (SKOSIMP*)
  (("" (EXPAND "div")
    (("" (EXPAND "abs")
      (("" (LIFT-IF)
        (("" (EXPAND "sgn")
          (("" (LIFT-IF)
            (("" (ASSERT)
              (("" (LIFT-IF)
                (("" (LIFT-IF)
                  (("" (LEMMA "floor_plus_int")
                    (("" (INST -1 "k!1" "i!1/j!1")
                      (("" (LEMMA "floor_neg")
                        (("" (INST -1 "i!1/j!1")
                          (("" (LEMMA "floor_plus_int")
                            (("" (INST -1 "-k!1" "-i!1/j!1")
                              (("" (LIFT-IF)
                                (("" (GROUND)
                                  NIL)))))))))))))))))))))))))))))))))
 (|div_sum_nat| "" (SKOSIMP*)
  (("" (LEMMA "div_sum")
    (("" (INST?)
      (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))
 (|nonposint_TCC1| "" (TCC :DEFS !) NIL) (|negint_TCC1| "" (TCC) NIL)
 (|div_TCC1| "" (GRIND) NIL) (|div_TCC2| "" (GRIND) NIL)
 (|div_TCC3| "" (GRIND) NIL) (|div_TCC4| "" (GRIND) NIL)
 (|div_TCC5| "" (GRIND) NIL))

$$$floor_div_props.pvs
floor_div_props: THEORY
BEGIN

  IMPORTING floor_ceil

  i,k: VAR int
  j: VAR nonzero_integer
  x: VAR real

  sgn(x): int = IF x >= 0 THEN 1 ELSE -1 ENDIF

  floor_val:   LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k 

  floor_small: LEMMA  abs(i) < abs(j) IMPLIES
                         floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF

  floor_eq_0:  LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1

  is_multiple: LEMMA integer?(i/j) = (EXISTS k: i = k*j)
	
END floor_div_props




$$$floor_div_props.prf
(|floor_div_props|
 (|floor_val| "" (SKOSIMP*)
  (("" (CASE "j!1 >= 0")
    (("1" (LEMMA "both_sides_div_pos_lt1")
      (("1" (INST -1 "j!1" "i!1" "(k!1 + 1) * j!1")
        (("1" (LEMMA "both_sides_div_pos_ge1")
          (("1" (INST -1 "j!1" "i!1" "k!1 * j!1")
            (("1" (FLATTEN)
              (("1" (HIDE -1 -3)
                (("1" (ASSERT)
                  (("1"
                    (CASE "floor(i!1 / j!1) > k!1 - 1 AND floor(i!1 / j!1) < k!1 + 1")
                    (("1" (FLATTEN)
                      (("1" (ASSERT)
                        (("1" (ASSERT) (("1" (ASSERT :FLUSH? T) NIL)))))))
                     ("2" (ASSERT) NIL)))))))))
             ("2" (ASSERT) NIL)))))
         ("2" (ASSERT) NIL)))))
     ("2" (LEMMA "both_sides_div_neg_lt1")
      (("2" (INST -1 "j!1" "(k!1 + 1) * j!1" "i!1")
        (("1" (FLATTEN)
          (("1" (HIDE -1)
            (("1" (LEMMA "both_sides_div_neg_ge1")
              (("1" (INST -1 "j!1" "k!1 * j!1" "i!1")
                (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL)))))
                 ("2" (ASSERT) NIL)))))))))
         ("2" (ASSERT) NIL)))))))))
 (|floor_small| "" (SKOSIMP*)
  (("" (LEMMA "pos_div_ge")
    (("" (INST?)
      (("" (LIFT-IF)
        (("" (EXPAND "abs")
          (("" (LIFT-IF)
            (("" (GROUND)
              (("1" (LEMMA "floor_val")
                (("1" (INST -1 "-i!1" "-j!1" "0") (("1" (ASSERT) NIL)))))
               ("2" (LEMMA "floor_val") (("2" (INST?) (("2" (ASSERT) NIL)))))
               ("3" (LEMMA "floor_val")
                (("3" (INST -1 "-i!1" "-j!1" "-1") (("3" (ASSERT) NIL)))))
               ("4" (LEMMA "floor_val")
                (("4" (INST -1 "i!1" "j!1" "-1")
                  (("4" (ASSERT) NIL)))))))))))))))))))
 (|floor_eq_0| "" (TCC) NIL)
 (|is_multiple| "" (SKOSIMP*)
  (("" (IFF 1)
    (("" (EXPAND "integer?")
      (("" (SPLIT 1)
        (("1" (FLATTEN) (("1" (INST 1 "i!1/j!1") (("1" (ASSERT) NIL)))))
         ("2" (FLATTEN) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))))))
$$$mod.pvs
mod: THEORY
%------------------------------------------------------------------------
%
%  mod function as defined in `Concrete Mathematics'
%  The Ada definition of mod is consistent with this definition
%
% 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 floor_div_props

  i,k,cc: VAR int
  m: VAR posnat
  n,a,b,c: VAR nat   

  j: VAR nonzero_integer

  ml3: LEMMA abs(i -  m * floor(i/m)) < m
  ml4: LEMMA abs(i +  m * floor(-i/m)) < m

  mod(i,j): {k| abs(k) < abs(j)} = i-j*floor(i/j)

  mod_even:       LEMMA integer?(i/j) IMPLIES mod(i,j) = 0

  mod_neg:        LEMMA mod(-i,j) = IF integer?(i/j) THEN 0
		                    ELSE j - mod(i,j)
                                    ENDIF

  mod_neg_d:      LEMMA mod(i,-j) = IF integer?(i/j) THEN 0
		                    ELSE mod(i,j) - j 
                                    ENDIF

  mod_eq_arg:     LEMMA mod(j,j) = 0
  
  mod_lt:         LEMMA abs(i) < abs(j) IMPLIES mod(i,j) = 
	                          IF sgn(i) = sgn(j) OR i = 0 THEN i
                          ELSE i + j
                          ENDIF

  mod_lt_nat:     LEMMA n < m IMPLIES mod(n,m) = n

  mod_sum_pos:    LEMMA mod(i+k*m,m) = mod(i,m)

  mod_sum:        LEMMA mod(i+k*j,j) = mod(i,j)

  mod_it_is:      LEMMA a = b + m*c AND b < m IMPLIES
                        b = mod(a,m)

  mod_Ada:        LEMMA (EXISTS k: i = k*j + mod(i,j))

  mod_zero:       LEMMA mod(0,j) = 0

  mod_one:        LEMMA mod(1,j) = IF abs(j) = 1 THEN 0
                                   ELSIF j > 0 THEN 1
                                   ELSE j + 1
                                   ENDIF

  mod_of_mod:     LEMMA mod(i + mod(k,m), m) = mod(i+k, m)

  mod_pos:        LEMMA mod(i,m) >= 0 AND mod(i,m) < m

  JUDGEMENT mod HAS_TYPE [int, m:posnat -> below(m)]

END mod

$$$mod.prf
(|mod|
 (|ml3| "" (SKOSIMP*)
  (("" (EXPAND "abs")
    (("" (LIFT-IF)
      (("" (GROUND)
        (("1" (LEMMA "both_sides_times_pos_lt1")
          (("1" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1 / m!1")
            (("1" (FLATTEN) (("1" (ASSERT) NIL)))))))
         ("2" (TYPEPRED "floor(i!1 / m!1)")
          (("2" (LEMMA "both_sides_times_pos_lt1")
            (("2" (INST -1 "m!1" "i!1 / m!1" " 1 + floor(i!1 / m!1)")
              (("2" (FLATTEN)
                (("2" (HIDE -1) (("2" (ASSERT) NIL)))))))))))))))))))
 (|ml4| "" (SKOSIMP*)
  (("" (EXPAND "abs")
    (("" (LIFT-IF)
      (("" (GROUND)
        (("1" (TYPEPRED "floor(-i!1 / m!1)")
          (("1" (LEMMA "both_sides_times_pos_lt1")
            (("1" (INST -1 "m!1" "-i!1 / m!1" "1 + floor(-i!1 / m!1)")
              (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL)))))))))))
         ("2" (LEMMA "both_sides_times_pos_lt1")
          (("2" (INST -1 "m!1" "floor(-i!1 / m!1)" "-i!1 / m!1")
            (("2" (FLATTEN)
              (("2" (HIDE -1) (("2" (ASSERT) NIL)))))))))))))))))
 (|mod_TCC1| "" (SKOSIMP*)
  (("" (CASE "j!1 >= 0")
    (("1" (LEMMA "ml3")
      (("1" (INST?)
        (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
         ("2" (ASSERT) NIL)))))
     ("2" (LEMMA "ml4")
      (("2" (INST -1 "i!1" "-j!1")
        (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
         ("2" (ASSERT) NIL)))))))))
 (|mod_even| "" (SKOSIMP*)
  (("" (EXPAND "integer?")
    (("" (EXPAND "mod") (("" (REWRITE "floor_int") (("" (ASSERT) NIL)))))))))
 (|mod_neg| "" (AUTO-REWRITE-THEORY "integers")
  (("" (SKOSIMP*)
    (("" (LIFT-IF)
      (("" (EXPAND "mod")
        (("" (CASE "-i!1/j!1 = -(i!1/j!1)")
          (("1" (REPLACE -1)
            (("1" (HIDE -1)
              (("1" (GROUND)
                (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL)))
                 ("2" (REWRITE "floor_neg")
                  (("2" (LIFT-IF)
                    (("2" (GROUND)
                      (("2" (CASE "integer_pred(--(i!1/j!1))")
                        (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))))
           ("2" (ASSERT) NIL)))))))))))
 (|mod_neg_d| "" (AUTO-REWRITE-THEORY "integers")
  (("" (SKOSIMP*)
    (("" (LIFT-IF)
      (("" (EXPAND "mod")
        (("" (CASE "i!1/-j!1=-(i!1/j!1)")
          (("1" (REPLACE -1)
            (("1" (HIDE -1)
              (("1" (REWRITE "floor_neg")
                (("1" (LIFT-IF)
                  (("1" (GROUND)
                    (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL)))
                     ("2" (ASSERT)
                      (("2" (CASE "integer_pred(--(i!1/j!1))")
                        (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))))
           ("2" (ASSERT) NIL)))))))))))
 (|mod_eq_arg| "" (TCC) NIL)
 (|mod_lt| "" (SKOSIMP*)
  (("" (LIFT-IF)
    (("" (EXPAND "mod")
      (("" (EXPAND "abs")
        (("" (EXPAND "sgn")
          (("" (LIFT-IF)
            (("" (LIFT-IF)
              (("" (GROUND)
                (("1" (REWRITE "floor_small")
                  (("1" (LIFT-IF)
                    (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL)))))
                   ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))
                 ("2" (REWRITE "floor_small")
                  (("1" (LIFT-IF)
                    (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL)))))
                   ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))
                 ("3" (REWRITE "floor_small")
                  (("1" (LIFT-IF)
                    (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL)))))
                   ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))
                 ("4" (REWRITE "floor_small")
                  (("1" (LIFT-IF)
                    (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL)))))
                   ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))))))))))))))))))
 (|mod_lt_nat| "" (SKOSIMP*)
  (("" (REWRITE "mod_lt")
    (("1" (EXPAND "sgn") (("1" (PROPAX) NIL)))
     ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))))
 (|mod_sum_pos| "" (SKOSIMP*)
  (("" (EXPAND "mod")
    (("" (LEMMA "floor_plus_int")
      (("" (INST - "k!1*m!1/m!1" "i!1/m!1")
        (("" (REPLACE -1) (("" (ASSERT) NIL)))))))))))
 (|mod_sum| "" (SKOSIMP*)
  (("" (EXPAND "mod")
    (("" (LEMMA "floor_plus_int")
      (("" (INST - "k!1*j!1/j!1" "i!1/j!1")
        (("" (REPLACE -1) (("" (ASSERT) NIL)))))))))))
 (|mod_it_is| "" (SKOSIMP*)
  (("" (REPLACE -1)
    (("" (HIDE -1)
      (("" (LEMMA "mod_sum")
        (("" (INST - "b!1" "m!1" "c!1")
          (("" (REPLACE -1)
            (("" (HIDE -1)
              (("" (REWRITE "mod_lt")
                (("1" (LIFT-IF) (("1" (EXPAND "sgn") (("1" (PROPAX) NIL)))))
                 ("2" (EXPAND "abs") (("2" (PROPAX) NIL)))))))))))))))))))
 (|mod_Ada| "" (SKOLEM!)
  (("" (EXPAND "mod") (("" (INST + "floor(i!1/j!1)") (("" (ASSERT) NIL)))))))
 (|mod_zero| "" (TCC) NIL)
 (|mod_one| "" (GRIND)
  (("1" (REWRITE "floor_small")
    (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL)))))))
   ("2" (LEMMA "div_cancel3")
    (("2" (INST -1 "j!1" "1" "0")
      (("2" (ASSERT)
        (("2" (REWRITE "floor_small")
          (("2" (LIFT-IF)
            (("2" (GROUND) (("2" (REWRITE "pos_div_ge") NIL)))))))))))))))
 (|mod_of_mod| "" (SKOSIMP*)
  (("" (REWRITE "mod")
    (("" (LEMMA "mod_sum")
      (("" (INST - "i!1+k!1" "m!1" "-floor(k!1/m!1)")
        (("" (ASSERT) NIL)))))))))
 (|mod_pos| "" (SKOSIMP*)
  (("" (TYPEPRED "mod(i!1,m!1)")
    (("" (TCC)
      (("" (LEMMA "both_sides_times_pos_le1")
        (("" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1/m!1")
          (("" (ASSERT) NIL)))))))))))
 (|mod_TCC2| "" (SKOSIMP) (("" (REWRITE "mod_pos") NIL))))
$$$div_top.pvs
div_top: THEORY
%------------------------------------------------------------------------
% Defines "div" and "mod" in two different manners.
%    (1) according to the Ada Reference Manual
%    (2) according to standard number theory text.
%
% The Ada theory truncates toward zero on a negative argument while
% the number theory truncates away from zero on a negative argument.  
% 
%  div                 -- Ada Reference Manual division theory
%  div_nt              -- Number theory division theory
%  div_alt             -- Ada div defined recursively
%  div_nt_alt          -- Number theory div defined recursively
%  mod                 -- mod theory
%  rem                 -- Ada Reference Manual rem theory
%  mod_lems            -- Additional lemmas about mod
%
% AUTHOR
% ------
% 
%   Ricky W. Butler   		   email: r.w.butler@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%
%
%   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 mod, div, rem, div_nt, mod_div_lems, mod_lems,
            div_alt, div_nt_alt

  END div_top