logic add_int : int, int -> int

logic sub_int : int, int -> int

logic mul_int : int, int -> int

logic div_int : int, int -> int

logic mod_int : int, int -> int

logic neg_int : int -> int

logic lt_int : int, int -> prop

logic le_int : int, int -> prop

logic gt_int : int, int -> prop

logic ge_int : int, int -> prop

logic eq_int : int, int -> prop

logic neq_int : int, int -> prop

logic lt_int_bool : int, int -> bool

logic le_int_bool : int, int -> bool

logic gt_int_bool : int, int -> bool

logic ge_int_bool : int, int -> bool

logic eq_int_bool : int, int -> bool

logic neq_int_bool : int, int -> bool

axiom lt_int_bool_axiom:
  (forall x:int. (forall y:int. ((lt_int_bool(x, y) = true) <-> (x < y))))

axiom le_int_bool_axiom:
  (forall x:int. (forall y:int. ((le_int_bool(x, y) = true) <-> (x <= y))))

axiom gt_int_bool_axiom:
  (forall x:int. (forall y:int. ((gt_int_bool(x, y) = true) <-> (x > y))))

axiom ge_int_bool_axiom:
  (forall x:int. (forall y:int. ((ge_int_bool(x, y) = true) <-> (x >= y))))

axiom eq_int_bool_axiom:
  (forall x:int. (forall y:int. ((eq_int_bool(x, y) = true) <-> (x = y))))

axiom neq_int_bool_axiom:
  (forall x:int. (forall y:int. ((neq_int_bool(x, y) = true) <-> (x <> y))))

logic add_real : real, real -> real

logic sub_real : real, real -> real

logic mul_real : real, real -> real

logic div_real : real, real -> real

logic pow_real : real, real -> real

logic neg_real : real -> real

logic abs_real : real -> real

logic sqrt_real : real -> real

logic real_of_int : int -> real

logic int_of_real : real -> int

logic lt_real : real, real -> prop

logic le_real : real, real -> prop

logic gt_real : real, real -> prop

logic ge_real : real, real -> prop

logic eq_real : real, real -> prop

logic neq_real : real, real -> prop

logic eq_bool : bool, bool -> prop

logic neq_bool : bool, bool -> prop

logic eq_unit : unit, unit -> prop

logic neq_unit : unit, unit -> prop

logic ite : bool, 'a1, 'a1 -> 'a1

axiom ite_true: (forall x:'a1. (forall y:'a1. (ite(true, x, y) = x)))

axiom ite_false: (forall x:'a1. (forall y:'a1. (ite(false, x, y) = y)))

type 'a farray

logic array_length : 'a1 farray -> int

logic access : 'a1 farray, int -> 'a1

logic update : 'a1 farray, int, 'a1 -> 'a1 farray

logic sorted_array : int farray, int, int -> prop

axiom sorted_array_def:
  (forall t:int farray.
    (forall i:int.
      (forall j:int.
        (sorted_array(t, i, j) <->
         (forall k:int.
           (((i <= k) and (k < j)) -> (access(t, k) <= access(t, (k + 1)))))))))

logic array_le : int farray, int, int, int -> prop

logic array_ge : int farray, int, int, int -> prop

logic exchange : int farray, int farray, int, int -> prop

axiom exchange_def:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall i:int.
        (forall j:int.
          (exchange(t1, t2, i, j) <->
           ((array_length(t1) = array_length(t2)) and
            ((access(t1, i) = access(t2, j)) and
             ((access(t2, i) = access(t1, j)) and
              (forall k:int.
                (((k <> i) and (k <> j)) -> (access(t1, k) = access(t2, k))))))))))))

logic permut : int farray, int farray -> prop

axiom permut_refl: (forall t:int farray. permut(t, t))

axiom permut_sym:
  (forall t1:int farray.
    (forall t2:int farray. (permut(t1, t2) -> permut(t2, t1))))

axiom permut_trans:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall t3:int farray.
        ((permut(t1, t2) and permut(t2, t3)) -> permut(t1, t3)))))

axiom permut_exchange:
  (forall t:int farray.
    (forall i:int.
      (forall j:int. permut(t, update(update(t, i, access(t, j)), j,
        access(t, i))))))

logic sub_permut : int, int, int farray, int farray -> prop

axiom sub_permut_refl:
  (forall t:int farray.
    (forall g:int. (forall d:int. sub_permut(g, d, t, t))))

axiom sub_permut_sym:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall g:int.
        (forall d:int.
          (sub_permut(g, d, t1, t2) -> sub_permut(g, d, t2, t1))))))

axiom sub_permut_trans:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall t3:int farray.
        (forall g:int.
          (forall d:int.
            (sub_permut(g, d, t1, t2) ->
             (sub_permut(g, d, t2, t3) -> sub_permut(g, d, t1, t3))))))))

axiom sub_permut_exchange_1:
  (forall t:int farray.
    (forall g:int.
      (forall d:int.
        (forall i:int.
          (forall j:int.
            (((g <= i) and ((i <= d) and ((g <= j) and (j <= d)))) ->
             sub_permut(g, d, t, update(update(t, i, access(t, j)), j,
             access(t, i)))))))))

axiom sub_permut_exchange_2:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall g:int.
        (forall d:int.
          (forall i:int.
            (forall j:int.
              (((g <= i) and
                ((i <= d) and
                 ((g <= j) and ((j <= d) and exchange(t1, t2, i, j))))) ->
               sub_permut(g, d, t1, t2))))))))

axiom sub_permut_permut:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall g:int.
        (forall d:int. (sub_permut(g, d, t1, t2) -> permut(t1, t2))))))

axiom array_length_update:
  (forall t:int farray.
    (forall i:int.
      (forall v:int. (array_length(update(t, i, v)) = array_length(t)))))

axiom sub_permut_array_length:
  (forall t1:int farray.
    (forall t2:int farray.
      (forall g:int.
        (forall d:int.
          (sub_permut(g, d, t1, t2) -> (array_length(t1) = array_length(t2)))))))

axiom permut_array_length:
  (forall t1:int farray.
    (forall t2:int farray.
      (permut(t1, t2) -> (array_length(t1) = array_length(t2)))))

type mode

logic nearest_even :  -> mode

logic to_zero :  -> mode

logic up :  -> mode

logic down :  -> mode

logic nearest_away :  -> mode

type single

logic add_single : mode, single, single -> single

logic sub_single : mode, single, single -> single

logic mul_single : mode, single, single -> single

logic div_single : mode, single, single -> single

logic neg_single : mode, single -> single

logic abs_single : mode, single -> single

logic sqrt_single : mode, single -> single

logic s_to_r : single -> real

logic s_to_exact : single -> real

logic s_to_model : single -> real

logic r_to_s : mode, real -> single

logic single_round_error : single -> real

logic single_total_error : single -> real

logic single_set_model : single, real -> single

logic max_single : mode -> real

type double

logic add_double : mode, double, double -> double

logic sub_double : mode, double, double -> double

logic mul_double : mode, double, double -> double

logic div_double : mode, double, double -> double

logic neg_double : mode, double -> double

logic abs_double : mode, double -> double

logic sqrt_double : mode, double -> double

logic d_to_r : double -> real

logic d_to_exact : double -> real

logic d_to_model : double -> real

logic r_to_d : mode, real -> double

logic double_round_error : double -> real

logic double_total_error : double -> real

logic double_set_model : double, real -> double

logic max_double : mode -> real

type quad

logic add_quad : mode, quad, quad -> quad

logic sub_quad : mode, quad, quad -> quad

logic mul_quad : mode, quad, quad -> quad

logic div_quad : mode, quad, quad -> quad

logic neg_quad : mode, quad -> quad

logic abs_quad : mode, quad -> quad

logic sqrt_quad : mode, quad -> quad

logic q_to_r : quad -> real

logic q_to_exact : quad -> real

logic q_to_model : quad -> real

logic r_to_q : mode, real -> quad

logic quad_round_error : quad -> real

logic quad_total_error : quad -> real

logic quad_set_model : quad, real -> quad

logic max_quad : mode -> real

logic double_of_single : single -> double

logic single_of_double : mode, double -> single

logic quad_of_single : single -> quad

logic single_of_quad : mode, quad -> single

logic quad_of_double : double -> quad

logic double_of_quad : mode, quad -> double

logic bw_compl : int -> int

logic bw_and : int, int -> int

logic bw_xor : int, int -> int

logic bw_or : int, int -> int

logic lsl : int, int -> int

logic lsr : int, int -> int

type 'z pointer

type 'z addr

type alloc_table

logic null :  -> 'a1 pointer

logic block_length : alloc_table, 'a1 pointer -> int

logic base_addr : 'a1 pointer -> 'a1 addr

logic offset : 'a1 pointer -> int

logic shift : 'a1 pointer, int -> 'a1 pointer

logic sub_pointer : 'a1 pointer, 'a1 pointer -> int

predicate lt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  ((base_addr(p1) = base_addr(p2)) and (offset(p1) < offset(p2)))

predicate le_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  ((base_addr(p1) = base_addr(p2)) and (offset(p1) <= offset(p2)))

predicate gt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  ((base_addr(p1) = base_addr(p2)) and (offset(p1) > offset(p2)))

predicate ge_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  ((base_addr(p1) = base_addr(p2)) and (offset(p1) >= offset(p2)))

predicate valid(a: alloc_table, p: 'a1 pointer) =
  ((0 <= offset(p)) and (offset(p) < block_length(a, p)))

predicate valid_index(a: alloc_table, p: 'a1 pointer, i: int) =
  ((0 <= (offset(p) + i)) and ((offset(p) + i) < block_length(a, p)))

predicate valid_range(a: alloc_table, p: 'a1 pointer, i: int, j: int) =
  ((0 <= (offset(p) + i)) and
   ((i <= j) and ((offset(p) + j) < block_length(a, p))))

axiom offset_shift:
  (forall p:'a1 pointer.
    (forall i:int [offset(shift(p, i))]. (offset(shift(p,
      i)) = (offset(p) + i))))

axiom shift_zero: (forall p:'a1 pointer [shift(p, 0)]. (shift(p, 0) = p))

axiom shift_shift:
  (forall p:'a1 pointer.
    (forall i:int.
      (forall j:int [shift(shift(p, i), j)]. (shift(shift(p, i),
        j) = shift(p, (i + j))))))

axiom base_addr_shift:
  (forall p:'a1 pointer.
    (forall i:int [base_addr(shift(p, i))]. (base_addr(shift(p,
      i)) = base_addr(p))))

axiom block_length_shift:
  (forall a:alloc_table.
    (forall p:'a1 pointer.
      (forall i:int [block_length(a, shift(p, i))]. (block_length(a, shift(p,
        i)) = block_length(a, p)))))

axiom base_addr_block_length:
  (forall a:alloc_table.
    (forall p1:'a1 pointer.
      (forall p2:'a1 pointer.
        ((base_addr(p1) = base_addr(p2)) -> (block_length(a,
         p1) = block_length(a, p2))))))

axiom pointer_pair_1:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer.
      (((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))) ->
       (p1 = p2))))

axiom pointer_pair_2:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer.
      ((p1 = p2) ->
       ((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))))))

axiom neq_base_addr_neq_shift:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer.
      (forall i:int.
        (forall j:int.
          ((base_addr(p1) <> base_addr(p2)) -> (shift(p1, i) <> shift(p2, j)))))))

axiom neq_offset_neq_shift:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer.
      (forall i:int.
        (forall j:int.
          (((offset(p1) + i) <> (offset(p2) + j)) -> (shift(p1,
           i) <> shift(p2, j)))))))

axiom eq_offset_eq_shift:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer.
      (forall i:int.
        (forall j:int.
          ((base_addr(p1) = base_addr(p2)) ->
           (((offset(p1) + i) = (offset(p2) + j)) -> (shift(p1,
            i) = shift(p2, j))))))))

axiom valid_index_valid_shift:
  (forall a:alloc_table.
    (forall p:'a1 pointer.
      (forall i:int. (valid_index(a, p, i) -> valid(a, shift(p, i))))))

axiom valid_range_valid_shift:
  (forall a:alloc_table.
    (forall p:'a1 pointer.
      (forall i:int.
        (forall j:int.
          (forall k:int.
            (valid_range(a, p, i, j) ->
             (((i <= k) and (k <= j)) -> valid(a, shift(p, k)))))))))

axiom valid_range_valid:
  (forall a:alloc_table.
    (forall p:'a1 pointer.
      (forall i:int.
        (forall j:int.
          (valid_range(a, p, i, j) ->
           (((i <= 0) and (0 <= j)) -> valid(a, p)))))))

axiom valid_range_valid_index:
  (forall a:alloc_table.
    (forall p:'a1 pointer.
      (forall i:int.
        (forall j:int.
          (forall k:int.
            (valid_range(a, p, i, j) ->
             (((i <= k) and (k <= j)) -> valid_index(a, p, k))))))))

axiom sub_pointer_def:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer.
      ((base_addr(p1) = base_addr(p2)) -> (sub_pointer(p1,
       p2) = (offset(p1) - offset(p2))))))

type ('a, 'z) memory

logic acc : ('a1, 'a2) memory, 'a2 pointer -> 'a1

logic upd : ('a1, 'a2) memory, 'a2 pointer, 'a1 -> ('a1, 'a2) memory

axiom acc_upd:
  (forall m:('a1, 'a2) memory.
    (forall p:'a2 pointer.
      (forall a:'a1 [acc(upd(m, p, a), p)]. (acc(upd(m, p, a), p) = a))))

axiom acc_upd_eq:
  (forall m:('a1, 'a2) memory.
    (forall p1:'a2 pointer.
      (forall p2:'a2 pointer.
        (forall a:'a1 [acc(upd(m, p1, a), p2)].
          ((p1 = p2) -> (acc(upd(m, p1, a), p2) = a))))))

axiom acc_upd_neq:
  (forall m:('a1, 'a2) memory.
    (forall p1:'a2 pointer.
      (forall p2:'a2 pointer.
        (forall a:'a1 [acc(upd(m, p1, a), p2)].
          ((p1 <> p2) -> (acc(upd(m, p1, a), p2) = acc(m, p2)))))))

axiom false_not_true: (false <> true)

type 'z pset

logic pset_empty :  -> 'a1 pset

logic pset_singleton : 'a1 pointer -> 'a1 pset

logic pset_star : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset

logic pset_all : 'a1 pset -> 'a1 pset

logic pset_range : 'a1 pset, int, int -> 'a1 pset

logic pset_range_left : 'a1 pset, int -> 'a1 pset

logic pset_range_right : 'a1 pset, int -> 'a1 pset

logic pset_acc_all : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset

logic pset_acc_range : 'a2 pset, ('a1 pointer, 'a2) memory, int,
int -> 'a1 pset

logic pset_acc_range_left : 'a2 pset, ('a1 pointer, 'a2) memory,
int -> 'a1 pset

logic pset_acc_range_right : 'a2 pset, ('a1 pointer, 'a2) memory,
int -> 'a1 pset

logic pset_union : 'a1 pset, 'a1 pset -> 'a1 pset

logic not_in_pset : 'a1 pointer, 'a1 pset -> prop

predicate not_assigns(a: alloc_table, m1: ('a1, 'a2) memory, m2: ('a1,
  'a2) memory, l: 'a2 pset) =
  (forall p:'a2 pointer.
    (valid(a, p) -> (not_in_pset(p, l) -> (acc(m2, p) = acc(m1, p)))))

axiom pset_empty_intro: (forall p:'a1 pointer. not_in_pset(p, pset_empty))

axiom pset_singleton_intro:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
      ((p1 <> p2) -> not_in_pset(p1, pset_singleton(p2)))))

axiom pset_singleton_elim:
  (forall p1:'a1 pointer.
    (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
      (not_in_pset(p1, pset_singleton(p2)) -> (p1 <> p2))))

axiom not_not_in_singleton:
  (forall p:'a1 pointer. (not not_in_pset(p, pset_singleton(p))))

axiom pset_union_intro:
  (forall l1:'a1 pset.
    (forall l2:'a1 pset.
      (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
        ((not_in_pset(p, l1) and not_in_pset(p, l2)) -> not_in_pset(p,
         pset_union(l1, l2))))))

axiom pset_union_elim1:
  (forall l1:'a1 pset.
    (forall l2:'a1 pset.
      (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
        (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l1)))))

axiom pset_union_elim2:
  (forall l1:'a1 pset.
    (forall l2:'a1 pset.
      (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
        (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l2)))))

axiom pset_star_intro:
  (forall l:'a1 pset.
    (forall m:('a2 pointer, 'a1) memory.
      (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
        ((forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l))) ->
         not_in_pset(p, pset_star(l, m))))))

axiom pset_star_elim:
  (forall l:'a1 pset.
    (forall m:('a2 pointer, 'a1) memory.
      (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
        (not_in_pset(p, pset_star(l, m)) ->
         (forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l)))))))

axiom pset_all_intro:
  (forall p:'a1 pointer.
    (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
      ((forall p1:'a1 pointer.
         ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))) ->
       not_in_pset(p, pset_all(l)))))

axiom pset_all_elim:
  (forall p:'a1 pointer.
    (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
      (not_in_pset(p, pset_all(l)) ->
       (forall p1:'a1 pointer.
         ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))))))

axiom pset_range_intro:
  (forall p:'a1 pointer.
    (forall l:'a1 pset.
      (forall a:int.
        (forall b:int [not_in_pset(p, pset_range(l, a, b))].
          ((forall p1:'a1 pointer.
             (not_in_pset(p1, l) or
              (forall i:int.
                (((a <= i) and (i <= b)) -> (p <> shift(p1, i)))))) ->
           not_in_pset(p, pset_range(l, a, b)))))))

axiom pset_range_elim:
  (forall p:'a1 pointer.
    (forall l:'a1 pset.
      (forall a:int.
        (forall b:int [not_in_pset(p, pset_range(l, a, b))].
          (not_in_pset(p, pset_range(l, a, b)) ->
           (forall p1:'a1 pointer.
             ((not not_in_pset(p1, l)) ->
              (forall i:int.
                (((a <= i) and (i <= b)) -> (shift(p1, i) <> p))))))))))

axiom pset_range_left_intro:
  (forall p:'a1 pointer.
    (forall l:'a1 pset.
      (forall a:int [not_in_pset(p, pset_range_left(l, a))].
        ((forall p1:'a1 pointer.
           (not_in_pset(p1, l) or
            (forall i:int. ((i <= a) -> (p <> shift(p1, i)))))) ->
         not_in_pset(p, pset_range_left(l, a))))))

axiom pset_range_left_elim:
  (forall p:'a1 pointer.
    (forall l:'a1 pset.
      (forall a:int [not_in_pset(p, pset_range_left(l, a))].
        (not_in_pset(p, pset_range_left(l, a)) ->
         (forall p1:'a1 pointer.
           ((not not_in_pset(p1, l)) ->
            (forall i:int. ((i <= a) -> (shift(p1, i) <> p)))))))))

axiom pset_range_right_intro:
  (forall p:'a1 pointer.
    (forall l:'a1 pset.
      (forall a:int [not_in_pset(p, pset_range_right(l, a))].
        ((forall p1:'a1 pointer.
           (not_in_pset(p1, l) or
            (forall i:int. ((a <= i) -> (p <> shift(p1, i)))))) ->
         not_in_pset(p, pset_range_right(l, a))))))

axiom pset_range_right_elim:
  (forall p:'a1 pointer.
    (forall l:'a1 pset.
      (forall a:int [not_in_pset(p, pset_range_right(l, a))].
        (not_in_pset(p, pset_range_right(l, a)) ->
         (forall p1:'a1 pointer.
           ((not not_in_pset(p1, l)) ->
            (forall i:int. ((a <= i) -> (shift(p1, i) <> p)))))))))

axiom pset_acc_all_intro:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
        m))].
        ((forall p1:'a2 pointer.
           ((not not_in_pset(p1, l)) ->
            (forall i:int. (p <> acc(m, shift(p1, i)))))) ->
         not_in_pset(p, pset_acc_all(l, m))))))

axiom pset_acc_all_elim:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
        m))].
        (not_in_pset(p, pset_acc_all(l, m)) ->
         (forall p1:'a2 pointer.
           ((not not_in_pset(p1, l)) ->
            (forall i:int. (acc(m, shift(p1, i)) <> p))))))))

axiom pset_acc_range_intro:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory.
        (forall a:int.
          (forall b:int [not_in_pset(p, pset_acc_range(l, m, a, b))].
            ((forall p1:'a2 pointer.
               ((not not_in_pset(p1, l)) ->
                (forall i:int.
                  (((a <= i) and (i <= b)) -> (p <> acc(m, shift(p1, i))))))) ->
             not_in_pset(p, pset_acc_range(l, m, a, b))))))))

axiom pset_acc_range_elim:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory.
        (forall a:int.
          (forall b:int.
            (not_in_pset(p, pset_acc_range(l, m, a, b)) ->
             (forall p1:'a2 pointer.
               ((not not_in_pset(p1, l)) ->
                (forall i:int.
                  (((a <= i) and (i <= b)) -> (acc(m, shift(p1, i)) <> p)))))))))))

axiom pset_acc_range_left_intro:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory.
        (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
          ((forall p1:'a2 pointer.
             ((not not_in_pset(p1, l)) ->
              (forall i:int. ((i <= a) -> (p <> acc(m, shift(p1, i))))))) ->
           not_in_pset(p, pset_acc_range_left(l, m, a)))))))

axiom pset_acc_range_left_elim:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory.
        (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
          (not_in_pset(p, pset_acc_range_left(l, m, a)) ->
           (forall p1:'a2 pointer.
             ((not not_in_pset(p1, l)) ->
              (forall i:int. ((i <= a) -> (acc(m, shift(p1, i)) <> p))))))))))

axiom pset_acc_range_right_intro:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory.
        (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
          ((forall p1:'a2 pointer.
             ((not not_in_pset(p1, l)) ->
              (forall i:int. ((a <= i) -> (p <> acc(m, shift(p1, i))))))) ->
           not_in_pset(p, pset_acc_range_right(l, m, a)))))))

axiom pset_acc_range_right_elim:
  (forall p:'a1 pointer.
    (forall l:'a2 pset.
      (forall m:('a1 pointer, 'a2) memory.
        (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
          (not_in_pset(p, pset_acc_range_right(l, m, a)) ->
           (forall p1:'a2 pointer.
             ((not not_in_pset(p1, l)) ->
              (forall i:int. ((a <= i) -> (acc(m, shift(p1, i)) <> p))))))))))

axiom not_assigns_trans:
  (forall a:alloc_table.
    (forall l:'a1 pset.
      (forall m1:('a2, 'a1) memory.
        (forall m2:('a2, 'a1) memory.
          (forall m3:('a2, 'a1) memory.
            (not_assigns(a, m1, m2, l) ->
             (not_assigns(a, m2, m3, l) -> not_assigns(a, m1, m3, l))))))))

axiom not_assigns_refl:
  (forall a:alloc_table.
    (forall l:'a1 pset.
      (forall m:('a2, 'a1) memory. not_assigns(a, m, m, l))))

predicate valid1(m1: ('a1 pointer, 'a2) memory) =
  (forall p:'a2 pointer.
    (forall a:alloc_table. (valid(a, p) -> valid(a, acc(m1, p)))))

predicate valid1_range(m1: ('a1 pointer, 'a2) memory, size: int) =
  (forall p:'a2 pointer.
    (forall a:alloc_table.
      (valid(a, p) -> valid_range(a, acc(m1, p), 0, (size - 1)))))

axiom valid1_range_valid:
  (forall m1:('a1 pointer, 'a2) memory.
    (forall size:int.
      (forall p:'a2 pointer.
        (forall a:alloc_table.
          (valid1_range(m1, size) -> (valid(a, p) -> valid(a, acc(m1, p))))))))

predicate separation1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
  'a2) memory) =
  (forall p:'a2 pointer.
    (forall a:alloc_table.
      (valid(a, p) -> (base_addr(acc(m1, p)) <> base_addr(acc(m2, p))))))

predicate separation1_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
  'a2) memory, size: int) =
  (forall p:'a2 pointer.
    (forall a:alloc_table.
      (valid(a, p) ->
       (forall i:int.
         (((0 <= i) and (i < size)) -> (base_addr(acc(m1, shift(p,
          i))) <> base_addr(acc(m2, p))))))))

predicate separation1_range(m: ('a1 pointer, 'a2) memory, size: int) =
  (forall p:'a2 pointer.
    (forall a:alloc_table.
      (valid(a, p) ->
       (forall i1:int.
         (forall i2:int.
           (((0 <= i1) and (i1 < size)) ->
            (((0 <= i2) and (i2 < size)) ->
             ((i1 <> i2) -> (base_addr(acc(m, shift(p,
              i1))) <> base_addr(acc(m, shift(p, i2))))))))))))

predicate separation2(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
  'a2) memory) =
  (forall p1:'a2 pointer.
    (forall p2:'a2 pointer.
      (forall a:alloc_table.
        ((p1 <> p2) -> (base_addr(acc(m1, p1)) <> base_addr(acc(m2, p2)))))))

predicate separation2_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
  'a2) memory, size: int) =
  (forall p:'a2 pointer.
    (forall q:'a2 pointer.
      (forall a:alloc_table.
        (forall i:int.
          (((0 <= i) and (i < size)) -> (base_addr(acc(m1, shift(p,
           i))) <> base_addr(acc(m2, q))))))))

logic on_heap : alloc_table, 'a1 pointer -> prop

logic on_stack : alloc_table, 'a1 pointer -> prop

logic fresh : alloc_table, 'a1 pointer -> prop

axiom fresh_not_valid:
  (forall a:alloc_table.
    (forall p:'a1 pointer. (fresh(a, p) -> (not valid(a, p)))))

axiom fresh_not_valid_shift:
  (forall a:alloc_table.
    (forall p:'a1 pointer.
      (fresh(a, p) -> (forall i:int. (not valid(a, shift(p, i)))))))

logic alloc_extends : alloc_table, alloc_table -> prop

axiom alloc_extends_valid:
  (forall a1:alloc_table.
    (forall a2:alloc_table.
      (alloc_extends(a1, a2) ->
       (forall q:'a1 pointer. (valid(a1, q) -> valid(a2, q))))))

axiom alloc_extends_valid_index:
  (forall a1:alloc_table.
    (forall a2:alloc_table.
      (alloc_extends(a1, a2) ->
       (forall q:'a1 pointer.
         (forall i:int. (valid_index(a1, q, i) -> valid_index(a2, q, i)))))))

axiom alloc_extends_valid_range:
  (forall a1:alloc_table.
    (forall a2:alloc_table.
      (alloc_extends(a1, a2) ->
       (forall q:'a1 pointer.
         (forall i:int.
           (forall j:int.
             (valid_range(a1, q, i, j) -> valid_range(a2, q, i, j))))))))

axiom alloc_extends_refl: (forall a:alloc_table. alloc_extends(a, a))

axiom alloc_extends_trans:
  (forall a1:alloc_table.
    (forall a2:alloc_table.
      (forall a3:alloc_table.
        (alloc_extends(a1, a2) ->
         (alloc_extends(a2, a3) -> alloc_extends(a1, a3))))))

logic free_stack : alloc_table, alloc_table, alloc_table -> prop

axiom free_stack_heap:
  (forall a1:alloc_table.
    (forall a2:alloc_table.
      (forall a3:alloc_table.
        (free_stack(a1, a2, a3) ->
         (forall p:'a1 pointer.
           (valid(a2, p) -> (on_heap(a2, p) -> valid(a3, p))))))))

axiom free_stack_stack:
  (forall a1:alloc_table.
    (forall a2:alloc_table.
      (forall a3:alloc_table.
        (free_stack(a1, a2, a3) ->
         (forall p:'a1 pointer.
           (valid(a1, p) -> (on_stack(a1, p) -> valid(a3, p))))))))

type t_0

type t_1

type t_2

type t_3

type t_4

type t_5

type t_6

type t_7

type t_8

goal index2_impl_po_1:
  forall t:'a1 pointer.
  forall n:int.
  forall alloc:alloc_table.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  (0 <= 0)

goal index2_impl_po_2:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  forall k:int.
  ((0 <= k) and (k < 0)) ->
  (acc(intM_t_8, shift(t, k)) <> v)

goal index2_impl_po_3:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result)

goal index2_impl_po_4:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_8, result)) ->
  (result0 = v) ->
  ((0 <= i) and (i < n)) ->
  (acc(intM_t_8, shift(t, i)) = v)

goal index2_impl_po_5:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_8, result)) ->
  (result0 <> v) ->
  forall i0:int.
  (i0 = (i + 1)) ->
  (0 <= i0)

goal index2_impl_po_6:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_8, result)) ->
  (result0 <> v) ->
  forall i0:int.
  (i0 = (i + 1)) ->
  forall k:int.
  ((0 <= k) and (k < i0)) ->
  (acc(intM_t_8, shift(t, k)) <> v)

goal index2_impl_po_7:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_8, result)) ->
  (result0 <> v) ->
  forall i0:int.
  (i0 = (i + 1)) ->
  ((0 <= (n - i)) and ((n - i0) < (n - i)))

goal index2_impl_po_8:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_8:(int,
  'a1) memory.
  (("File \"search.c\", line 22, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 27, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_8, shift(t, k)) <> v))))) ->
  (i >= n) ->
  ((0 <= n) and (n < n)) ->
  (acc(intM_t_8, shift(t, n)) = v)

goal index_impl_po_1:
  forall t:'a1 pointer.
  forall n:int.
  forall alloc:alloc_table.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  (0 <= 0)

goal index_impl_po_2:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  forall k:int.
  ((0 <= k) and (k < 0)) ->
  (acc(intM_t_7, shift(t, k)) <> v)

goal index_impl_po_3:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result)

goal index_impl_po_4:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_7, result)) ->
  (result0 = v) ->
  ((0 <= i) and (i < n)) ->
  (acc(intM_t_7, shift(t, i)) = v)

goal index_impl_po_5:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_7, result)) ->
  (result0 = v) ->
  (i = n) ->
  forall i0:int.
  ((0 <= i0) and (i0 < n)) ->
  (acc(intM_t_7, shift(t, i0)) <> v)

goal index_impl_po_6:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_7, result)) ->
  (result0 <> v) ->
  forall i0:int.
  (i0 = (i + 1)) ->
  (0 <= i0)

goal index_impl_po_7:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_7, result)) ->
  (result0 <> v) ->
  forall i0:int.
  (i0 = (i + 1)) ->
  forall k:int.
  ((0 <= k) and (k < i0)) ->
  (acc(intM_t_7, shift(t, k)) <> v)

goal index_impl_po_8:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i < n) ->
  forall result:'a1 pointer.
  (result = shift(t, i)) ->
  valid(alloc, result) ->
  forall result0:int.
  (result0 = acc(intM_t_7, result)) ->
  (result0 <> v) ->
  forall i0:int.
  (i0 = (i + 1)) ->
  ((0 <= (n - i)) and ((n - i0) < (n - i)))

goal index_impl_po_9:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i >= n) ->
  ((0 <= i) and (i < n)) ->
  (acc(intM_t_7, shift(t, i)) = v)

goal index_impl_po_10:
  forall t:'a1 pointer.
  forall n:int.
  forall v:int.
  forall alloc:alloc_table.
  forall intM_t_7:(int,
  'a1) memory.
  (("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
   (n - 1))) and valid_range(alloc, t, 0, 3)) ->
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= 0) and
   (forall k:int.
     (((0 <= k) and (k < 0)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  forall i:int.
  ("File \"search.c\", line 11, characters 17-65":
  ((0 <= i) and
   (forall k:int.
     (((0 <= k) and (k < i)) -> (acc(intM_t_7, shift(t, k)) <> v))))) ->
  (i >= n) ->
  (i = n) ->
  forall i0:int.
  ((0 <= i0) and (i0 < n)) ->
  (acc(intM_t_7, shift(t, i0)) <> v)

goal test_impl_po_1:
  forall alloc:alloc_table.
  forall t:t_6 pointer.
  valid_range(alloc, t, 0, 3) ->
  ("File \"search.c\", line 4, characters 14-35": valid_range(alloc, t, 0,
  (4 - 1)))