theory Why2
use array.Array as A
  use unit_inf.Unit
  use int.Int
  use int.ComputerDivision
  use real.Real
  use bool_inf.Bool
  predicate eq_unit Unit.unit Unit.unit

  predicate neq_unit Unit.unit Unit.unit

  predicate eq_bool Bool.bool Bool.bool

  predicate neq_bool Bool.bool Bool.bool

  predicate lt_int int int

  predicate le_int int int

  predicate gt_int int int

  predicate ge_int int int

  predicate eq_int int int

  predicate neq_int int int

  function add_int int int : int

  function sub_int int int : int

  function mul_int int int : int

  function div_int int int : int

  function mod_int int int : int

  function neg_int int : int

  predicate zwf_zero (a : int) (b : int) = ((Int.(<=) 0 b) /\ (Int.(<) a b))

  function bw_compl int : int

  function bw_and int int : int

  function bw_xor int int : int

  function bw_or int int : int

  function lsl int int : int

  function lsr int int : int

  type pointer 'z

  type addr 'z

  type alloc_table

  function block_length alloc_table (pointer 'a1) : int

  function base_addr (pointer 'a1) : (addr 'a1)

  function offset (pointer 'a1) : int

  function shift (pointer 'a1) int : (pointer 'a1)

  function sub_pointer (pointer 'a1) (pointer 'a1) : int

  predicate lt_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) =
    (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\
     (Int.(<) (offset p1 : int) (offset p2 : int)))

  predicate le_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) =
    (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\
     (Int.(<=) (offset p1 : int) (offset p2 : int)))

  predicate gt_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) =
    (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\
     (Int.(>) (offset p1 : int) (offset p2 : int)))

  predicate ge_pointer (p1 : (pointer 'a1)) (p2 : (pointer 'a1)) =
    (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\
     (Int.(>=) (offset p1 : int) (offset p2 : int)))

  predicate valid (a : alloc_table) (p : (pointer 'a1)) =
    ((Int.(<=) 0 (offset p : int)) /\
     (Int.(<) (offset p : int) (block_length a p : int)))

  predicate valid_index (a : alloc_table) (p : (pointer 'a1)) (i : int) =
    ((Int.(<=) 0 (Int.(+) (offset p : int) i : int)) /\
     (Int.(<) (Int.(+) (offset p : int) i : int) (block_length a p : int)))

  predicate valid_range (a : alloc_table) (p : (pointer 'a1)) (i : int) (j : int) =
    ((Int.(<=) 0 (Int.(+) (offset p : int) i : int)) /\
     (Int.(<) (Int.(+) (offset p : int) j : int) (block_length a p : int)))

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

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

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

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

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

  axiom Base_addr_block_length:
    (forall a:alloc_table.
      (forall p1:(pointer 'a1).
        (forall p2:(pointer 'a1).
          (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) ->
           ((block_length a p1 : int) = (block_length a p2 : int))))))

  axiom Pointer_pair_1:
    (forall p1:(pointer 'a1).
      (forall p2:(pointer 'a1).
        ((((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\
          ((offset p1 : int) = (offset p2 : int))) ->
         (p1 = p2))))

  axiom Pointer_pair_2:
    (forall p1:(pointer 'a1).
      (forall p2:(pointer 'a1).
        ((p1 = p2) ->
         (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) /\
          ((offset p1 : int) = (offset p2 : int))))))

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

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

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

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

  axiom Valid_range_valid_shift:
    (forall a:alloc_table.
      (forall p:(pointer 'a1).
        (forall i:int.
          (forall j:int.
            (forall k:int.
              ((valid_range a p i j) ->
               (((Int.(<=) i k) /\ (Int.(<=) k j)) ->
                (valid a (shift p k : (pointer 'a1))))))))))

  axiom Valid_range_valid:
    (forall a:alloc_table.
      (forall p:(pointer 'a1).
        (forall i:int.
          (forall j:int.
            ((valid_range a p i j) ->
             (((Int.(<=) i 0) /\ (Int.(<=) 0 j)) -> (valid a p)))))))

  axiom Valid_range_valid_index:
    (forall a:alloc_table.
      (forall p:(pointer 'a1).
        (forall i:int.
          (forall j:int.
            (forall k:int.
              ((valid_range a p i j) ->
               (((Int.(<=) i k) /\ (Int.(<=) k j)) -> (valid_index a p k))))))))

  axiom Sub_pointer_def:
    (forall p1:(pointer 'a1).
      (forall p2:(pointer 'a1).
        (((base_addr p1 : (addr 'a1)) = (base_addr p2 : (addr 'a1))) ->
         ((sub_pointer p1 p2 : int) = (Int.(-) (offset p1 : int) (offset p2 : int) : int)))))

  type memory 'a 'z = A.t (pointer 'z) 'a

  function acc (m:memory 'a1 'a2) (k:pointer 'a2) : 'a1 = A.get m k

  function upd (m:memory 'a1 'a2) (k:pointer 'a2) (v:'a1) : (memory 'a1 'a2) = A.set m k v





  type pset 'z

  function pset_empty  : (pset 'a1)

  function pset_singleton (pointer 'a1) : (pset 'a1)

  function pset_star (pset 'a2) (memory (pointer 'a1) 'a2) : (pset 'a1)

  function pset_all (pset 'a1) : (pset 'a1)

  function pset_range (pset 'a1) int int : (pset 'a1)

  function pset_range_left (pset 'a1) int : (pset 'a1)

  function pset_range_right (pset 'a1) int : (pset 'a1)

  function pset_acc_all (pset 'a2) (memory (pointer 'a1) 'a2) : (pset 'a1)

  function pset_acc_range (pset 'a2) (memory (pointer 'a1) 'a2) int int : (pset 'a1)

  function pset_acc_range_left (pset 'a2) (memory (pointer 'a1) 'a2) int : (pset 'a1)

  function pset_acc_range_right (pset 'a2) (memory (pointer 'a1) 'a2) int : (pset 'a1)

  function pset_union (pset 'a1) (pset 'a1) : (pset 'a1)

  predicate not_in_pset (pointer 'a1) (pset 'a1)

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

  axiom Pset_empty_intro:
    (forall p:(pointer 'a1). (not_in_pset p (pset_empty : (pset 'a1))))

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

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

  axiom Not_not_in_singleton:
    (forall p:(pointer 'a1).
      (not (not_in_pset p (pset_singleton p : (pset 'a1)))))

  axiom Pset_union_intro:
    (forall l1:(pset 'a1).
      (forall l2:(pset 'a1).
        (forall p:(pointer 'a1) [(not_in_pset p (pset_union l1 l2 : (pset 'a1)))].
          (((not_in_pset p l1) /\ (not_in_pset p l2)) ->
           (not_in_pset p (pset_union l1 l2 : (pset 'a1)))))))

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

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

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

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

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

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

  axiom Pset_range_intro:
    (forall p:(pointer 'a1).
      (forall l:(pset 'a1).
        (forall a:int.
          (forall b:int [(not_in_pset p (pset_range l a b : (pset 'a1)))].
            ((forall p1:(pointer 'a1).
               ((not_in_pset p1 l) \/
                (forall i:int.
                  (((Int.(<=) a i) /\ (Int.(<=) i b)) ->
                   (p <> (shift p1 i : (pointer 'a1))))))) ->
             (not_in_pset p (pset_range l a b : (pset 'a1))))))))

  axiom Pset_range_elim:
    (forall p:(pointer 'a1).
      (forall l:(pset 'a1).
        (forall a:int.
          (forall b:int [(not_in_pset p (pset_range l a b : (pset 'a1)))].
            ((not_in_pset p (pset_range l a b : (pset 'a1))) ->
             (forall p1:(pointer 'a1).
               ((not (not_in_pset p1 l)) ->
                (forall i:int.
                  (((Int.(<=) a i) /\ (Int.(<=) i b)) ->
                   ((shift p1 i : (pointer 'a1)) <> p))))))))))

  axiom Pset_range_left_intro:
    (forall p:(pointer 'a1).
      (forall l:(pset 'a1).
        (forall a:int [(not_in_pset p (pset_range_left l a : (pset 'a1)))].
          ((forall p1:(pointer 'a1).
             ((not_in_pset p1 l) \/
              (forall i:int.
                ((Int.(<=) i a) -> (p <> (shift p1 i : (pointer 'a1))))))) ->
           (not_in_pset p (pset_range_left l a : (pset 'a1)))))))

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

  axiom Pset_range_right_intro:
    (forall p:(pointer 'a1).
      (forall l:(pset 'a1).
        (forall a:int [(not_in_pset p (pset_range_right l a : (pset 'a1)))].
          ((forall p1:(pointer 'a1).
             ((not_in_pset p1 l) \/
              (forall i:int.
                ((Int.(<=) a i) -> (p <> (shift p1 i : (pointer 'a1))))))) ->
           (not_in_pset p (pset_range_right l a : (pset 'a1)))))))

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

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

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

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

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

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

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

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

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

  axiom Not_assigns_trans:
    (forall a:alloc_table.
      (forall l:(pset 'a1).
        (forall m1:(memory 'a2 'a1).
          (forall m2:(memory 'a2 'a1).
            (forall m3:(memory 'a2 'a1).
              ((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:(pset 'a1).
        (forall m:(memory 'a2 'a1). (not_assigns a m m l))))

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

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

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

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

  predicate separation1_range1 (m1 : (memory (pointer 'a1) 'a2)) (m2 : (memory (pointer 'a1) 'a2)) (size : int) =
    (forall p:(pointer 'a2).
      (forall a:alloc_table.
        ((valid a p) ->
         (forall i1:int.
           (forall i2:int.
             (((Int.(<=) 0 i1) /\ (Int.(<) i1 size)) ->
              (((Int.(<=) 0 i2) /\ (Int.(<) i2 size)) ->
               ((base_addr (acc m1 (shift p i1 : (pointer 'a2)) : (pointer 'a1)) : (addr 'a1)) <> (base_addr (acc m2 (shift p i2 : (pointer 'a2)) : (pointer 'a1)) : (addr 'a1))))))))))

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

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

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

  predicate on_heap alloc_table (pointer 'a1)

  predicate on_stack alloc_table (pointer 'a1)

  predicate fresh alloc_table (pointer 'a1)

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

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

  predicate alloc_extends alloc_table alloc_table

  axiom Alloc_extends_valid:
    (forall a1:alloc_table.
      (forall a2:alloc_table.
        ((alloc_extends a1 a2) ->
         (forall q:(pointer 'a1). ((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:(pointer 'a1).
           (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:(pointer 'a1).
           (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 a2) ->
           ((alloc_extends a2 a3) -> (alloc_extends a1 a3))))))

  predicate free_stack alloc_table alloc_table alloc_table

  axiom Free_stack_heap:
    (forall a1:alloc_table.
      (forall a2:alloc_table.
        (forall a3:alloc_table.
          ((free_stack a1 a2 a3) ->
           (forall p:(pointer 'a1).
             ((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:(pointer 'a1).
             ((valid a1 p) -> ((on_stack a1 p) -> (valid a3 p))))))))

  function null  : (pointer 'a1)

  axiom Null_not_valid:
    (forall a:alloc_table. (not (valid a (null : (pointer 'a1)))))

  type t_0

  type t_1

  type t_2

  axiom Mean_1:
    ("CADUCEUS_1"
    (forall x:int.
      (forall y:int.
        ((Int.(<=) x y) ->
         ((Int.(<=) x (ComputerDivision.div (Int.(+) x y : int) 2 : int)) /\
          (Int.(<=) (ComputerDivision.div (Int.(+) x y : int) 2 : int) y))))))

  goal Binary_search1_impl_po_1:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall alloc:alloc_table.
          (("CADUCEUS_2"
           ((Int.(>=) n 0) /\ (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
           ("CADUCEUS_3" (Int.(<=) (Int.(-) n 1 : int) (Int.(-) n 1 : int)))))))

  goal Binary_search1_impl_po_2:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall alloc:alloc_table.
          (("CADUCEUS_2"
           ((Int.(>=) n 0) /\ (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
           (forall l:int.
             (forall u:int.
               (("CADUCEUS_3"
                ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                ((Int.(<=) l u) ->
                 ((2 <> 0) ->
                  (forall result:int.
                    ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                     (forall result0:(pointer 'a1).
                       ((result0 = (shift t result : (pointer 'a1))) ->
                        (valid alloc result0))))))))))))))

  goal Binary_search1_impl_po_3:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(<) result1 v) ->
                                 (forall l0:int.
                                   ((l0 = (Int.(+) result 1 : int)) ->
                                    ("CADUCEUS_3" (Int.(<=) 0 l0)))))))))))))))))))))))

  goal Binary_search1_impl_po_4:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(<) result1 v) ->
                                 (forall l0:int.
                                   ((l0 = (Int.(+) result 1 : int)) ->
                                    (Int.(<=) 0 ("CADUCEUS_4"
                                                (Int.(-) u l : int))))))))))))))))))))))))

  goal Binary_search1_impl_po_5:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(<) result1 v) ->
                                 (forall l0:int.
                                   ((l0 = (Int.(+) result 1 : int)) ->
                                    (Int.(<) ("CADUCEUS_4"
                                             (Int.(-) u l0 : int)) ("CADUCEUS_4"
                                                                   (Int.(-) u l : int))))))))))))))))))))))))

  goal Binary_search1_impl_po_6:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(>=) result1 v) ->
                                 (forall result2:(pointer 'a1).
                                   ((result2 = (shift t result : (pointer 'a1))) ->
                                    (valid alloc result2))))))))))))))))))))))

  goal Binary_search1_impl_po_7:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(>=) result1 v) ->
                                 (forall result2:(pointer 'a1).
                                   ((result2 = (shift t result : (pointer 'a1))) ->
                                    ((valid alloc result2) ->
                                     (forall result3:int.
                                       ((result3 = (acc intM_t_2 result2 : int)) ->
                                        ((Int.(>) result3 v) ->
                                         (forall u0:int.
                                           ((u0 = (Int.(-) result 1 : int)) ->
                                            ("CADUCEUS_3"
                                            (Int.(<=) u0 (Int.(-) n 1 : int))))))))))))))))))))))))))))))

  goal Binary_search1_impl_po_8:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(>=) result1 v) ->
                                 (forall result2:(pointer 'a1).
                                   ((result2 = (shift t result : (pointer 'a1))) ->
                                    ((valid alloc result2) ->
                                     (forall result3:int.
                                       ((result3 = (acc intM_t_2 result2 : int)) ->
                                        ((Int.(>) result3 v) ->
                                         (forall u0:int.
                                           ((u0 = (Int.(-) result 1 : int)) ->
                                            (Int.(<=) 0 ("CADUCEUS_4"
                                                        (Int.(-) u l : int))))))))))))))))))))))))))))))

  goal Binary_search1_impl_po_9:
    (forall t:(pointer 'a1).
      (forall n:int.
        (forall v:int.
          (forall alloc:alloc_table.
            (forall intM_t_2:(memory int 'a1).
              (("CADUCEUS_2"
               ((Int.(>=) n 0) /\
                (valid_range alloc t 0 (Int.(-) n 1 : int)))) ->
               (forall l:int.
                 (forall u:int.
                   (("CADUCEUS_3"
                    ((Int.(<=) 0 l) /\ (Int.(<=) u (Int.(-) n 1 : int)))) ->
                    ((Int.(<=) l u) ->
                     ((2 <> 0) ->
                      (forall result:int.
                        ((result = (ComputerDivision.div (Int.(+) l u : int) 2 : int)) ->
                         (forall result0:(pointer 'a1).
                           ((result0 = (shift t result : (pointer 'a1))) ->
                            ((valid alloc result0) ->
                             (forall result1:int.
                               ((result1 = (acc intM_t_2 result0 : int)) ->
                                ((Int.(>=) result1 v) ->
                                 (forall result2:(pointer 'a1).
                                   ((result2 = (shift t result : (pointer 'a1))) ->
                                    ((valid alloc result2) ->
                                     (forall result3:int.
                                       ((result3 = (acc intM_t_2 result2 : int)) ->
                                        ((Int.(>) result3 v) ->
                                         (forall u0:int.
                                           ((u0 = (Int.(-) result 1 : int)) ->
                                            (Int.(<) ("CADUCEUS_4"
                                                     (Int.(-) u0 l : int))
                                            ("CADUCEUS_4"
                                            (Int.(-) u l : int))))))))))))))))))))))))))))))


end