(* This file was originally generated by why.
   It can be modified; only the generated parts will be overwritten. *)

Require Export Why.
Require Export WhyReal.

(*Why logic*) Definition bw_compl : Z -> Z.
Admitted.

(*Why logic*) Definition bw_and : Z -> Z -> Z.
Admitted.

(*Why logic*) Definition bw_xor : Z -> Z -> Z.
Admitted.

(*Why logic*) Definition bw_or : Z -> Z -> Z.
Admitted.

(*Why logic*) Definition lsl : Z -> Z -> Z.
Admitted.

(*Why logic*) Definition lsr : Z -> Z -> Z.
Admitted.

(*Why type*) Definition pointer: Set ->Set.
Admitted.

(*Why type*) Definition addr: Set ->Set.
Admitted.

(*Why type*) Definition alloc_table: Set.
Admitted.


(*Why logic*) Definition block_length :
  forall (A1:Set), alloc_table -> (pointer A1) -> Z.
Admitted.
Implicit Arguments block_length.

(*Why logic*) Definition base_addr :
  forall (A1:Set), (pointer A1) -> (addr A1).
Admitted.
Implicit Arguments base_addr.

(*Why logic*) Definition offset : forall (A1:Set), (pointer A1) -> Z.
Admitted.
Implicit Arguments offset.

(*Why logic*) Definition shift :
  forall (A1:Set), (pointer A1) -> Z -> (pointer A1).
Admitted.
Implicit Arguments shift.

(*Why logic*) Definition sub_pointer :
  forall (A1:Set), (pointer A1) -> (pointer A1) -> Z.
Admitted.
Implicit Arguments sub_pointer.

(*Why predicate*) Definition lt_pointer (A703:Set) (p1:(pointer A703)) (p2:(pointer A703))
  := (base_addr p1) = (base_addr p2) /\ (offset p1) < (offset p2).
Implicit Arguments lt_pointer.

(*Why predicate*) Definition le_pointer (A704:Set) (p1:(pointer A704)) (p2:(pointer A704))
  := (base_addr p1) = (base_addr p2) /\ (offset p1) <= (offset p2).
Implicit Arguments le_pointer.

(*Why predicate*) Definition gt_pointer (A705:Set) (p1:(pointer A705)) (p2:(pointer A705))
  := (base_addr p1) = (base_addr p2) /\ (offset p1) > (offset p2).
Implicit Arguments gt_pointer.

(*Why predicate*) Definition ge_pointer (A706:Set) (p1:(pointer A706)) (p2:(pointer A706))
  := (base_addr p1) = (base_addr p2) /\ (offset p1) >= (offset p2).
Implicit Arguments ge_pointer.

(*Why predicate*) Definition valid (A707:Set) (a:alloc_table) (p:(pointer A707))
  := 0 <= (offset p) /\ (offset p) < (block_length a p).
Implicit Arguments valid.

(*Why predicate*) Definition valid_index (A708:Set) (a:alloc_table) (p:(pointer A708)) (i:Z)
  := 0 <= ((offset p) + i) /\ ((offset p) + i) < (block_length a p).
Implicit Arguments valid_index.

(*Why predicate*) Definition valid_range (A709:Set) (a:alloc_table) (p:(pointer A709)) (i:Z) (j:Z)
  := 0 <= ((offset p) + i) /\ ((offset p) + j) < (block_length a p).
Implicit Arguments valid_range.

(*Why axiom*) Lemma offset_shift :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (i:Z), (offset (shift p i)) = ((offset p) + i))).
Admitted.

(*Why axiom*) Lemma shift_zero :
  forall (A1:Set), (forall (p:(pointer A1)), (shift p 0) = p).
Admitted.

(*Why axiom*) Lemma shift_shift :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (i:Z), (forall (j:Z), (shift (shift p i) j) = (shift p (i + j))))).
Admitted.

(*Why axiom*) Lemma base_addr_shift :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (i:Z), (base_addr (shift p i)) = (base_addr p))).
Admitted.

(*Why axiom*) Lemma block_length_shift :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)),
    (forall (i:Z), (block_length a (shift p i)) = (block_length a p)))).
Admitted.

(*Why axiom*) Lemma base_addr_block_length :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p1:(pointer A1)),
    (forall (p2:(pointer A1)),
     ((base_addr p1) = (base_addr p2) -> (block_length a p1) =
      (block_length a p2))))).
Admitted.

(*Why axiom*) Lemma pointer_pair_1 :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    ((base_addr p1) = (base_addr p2) /\ (offset p1) = (offset p2) -> p1 = p2))).
Admitted.

(*Why axiom*) Lemma pointer_pair_2 :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    (p1 = p2 -> (base_addr p1) = (base_addr p2) /\ (offset p1) = (offset p2)))).
Admitted.

(*Why axiom*) Lemma neq_base_addr_neq_shift :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    (forall (i:Z),
     (forall (j:Z),
      (~((base_addr p1) = (base_addr p2)) -> ~((shift p1 i) = (shift p2 j))))))).
Admitted.

(*Why axiom*) Lemma neq_offset_neq_shift :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    (forall (i:Z),
     (forall (j:Z),
      (((offset p1) + i) <> ((offset p2) + j) ->
       ~((shift p1 i) = (shift p2 j))))))).
Admitted.

(*Why axiom*) Lemma eq_offset_eq_shift :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    (forall (i:Z),
     (forall (j:Z),
      ((base_addr p1) = (base_addr p2) ->
       (((offset p1) + i) = ((offset p2) + j) -> (shift p1 i) = (shift p2 j))))))).
Admitted.

(*Why axiom*) Lemma valid_index_valid_shift :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)),
    (forall (i:Z), ((valid_index a p i) -> (valid a (shift p i)))))).
Admitted.

(*Why axiom*) Lemma valid_range_valid_shift :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)),
    (forall (i:Z),
     (forall (j:Z),
      (forall (k:Z),
       ((valid_range a p i j) -> (i <= k /\ k <= j -> (valid a (shift p k))))))))).
Admitted.

(*Why axiom*) Lemma valid_range_valid :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)),
    (forall (i:Z),
     (forall (j:Z),
      ((valid_range a p i j) -> (i <= 0 /\ 0 <= j -> (valid a p))))))).
Admitted.

(*Why axiom*) Lemma valid_range_valid_index :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)),
    (forall (i:Z),
     (forall (j:Z),
      (forall (k:Z),
       ((valid_range a p i j) -> (i <= k /\ k <= j -> (valid_index a p k)))))))).
Admitted.

(*Why axiom*) Lemma sub_pointer_def :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    ((base_addr p1) = (base_addr p2) -> (sub_pointer p1 p2) =
     ((offset p1) - (offset p2))))).
Admitted.

(*Why type*) Definition memory: Set -> Set ->Set.
Admitted.

(*Why logic*) Definition acc :
  forall (A1:Set), forall (A2:Set), (memory A1 A2) -> (pointer A2) -> A1.
Admitted.
Implicit Arguments acc.

(*Why logic*) Definition upd :
  forall (A1:Set), forall (A2:Set), (memory A1 A2) -> (pointer A2)
  -> A1 -> (memory A1 A2).
Admitted.
Implicit Arguments upd.

(*Why axiom*) Lemma acc_upd :
  forall (A1:Set), forall (A2:Set),
  (forall (m:(memory A1 A2)),
   (forall (p:(pointer A2)), (forall (a:A1), (acc (upd m p a) p) = a))).
Admitted.

(*Why axiom*) Lemma acc_upd_neq :
  forall (A1:Set), forall (A2:Set),
  (forall (m:(memory A1 A2)),
   (forall (p1:(pointer A2)),
    (forall (p2:(pointer A2)),
     (forall (a:A1), (~(p1 = p2) -> (acc (upd m p1 a) p2) = (acc m p2)))))).
Admitted.

(*Why axiom*) Lemma false_not_true : ~(false = true).
Admitted.

(*Why type*) Definition pset: Set ->Set.
Admitted.

(*Why logic*) Definition pset_empty : forall (A1:Set), (pset A1).
Admitted.
Set Contextual Implicit.
Implicit Arguments pset_empty.
Unset Contextual Implicit.

(*Why logic*) Definition pset_singleton :
  forall (A1:Set), (pointer A1) -> (pset A1).
Admitted.
Implicit Arguments pset_singleton.

(*Why logic*) Definition pset_star :
  forall (A1:Set), forall (A2:Set), (pset A2)
  -> (memory (pointer A1) A2) -> (pset A1).
Admitted.
Implicit Arguments pset_star.

(*Why logic*) Definition pset_all : forall (A1:Set), (pset A1) -> (pset A1).
Admitted.
Implicit Arguments pset_all.

(*Why logic*) Definition pset_range :
  forall (A1:Set), (pset A1) -> Z -> Z -> (pset A1).
Admitted.
Implicit Arguments pset_range.

(*Why logic*) Definition pset_range_left :
  forall (A1:Set), (pset A1) -> Z -> (pset A1).
Admitted.
Implicit Arguments pset_range_left.

(*Why logic*) Definition pset_range_right :
  forall (A1:Set), (pset A1) -> Z -> (pset A1).
Admitted.
Implicit Arguments pset_range_right.

(*Why logic*) Definition pset_acc_all :
  forall (A1:Set), forall (A2:Set), (pset A2)
  -> (memory (pointer A1) A2) -> (pset A1).
Admitted.
Implicit Arguments pset_acc_all.

(*Why logic*) Definition pset_acc_range :
  forall (A1:Set), forall (A2:Set), (pset A2) -> (memory (pointer A1) A2)
  -> Z -> Z -> (pset A1).
Admitted.
Implicit Arguments pset_acc_range.

(*Why logic*) Definition pset_acc_range_left :
  forall (A1:Set), forall (A2:Set), (pset A2) -> (memory (pointer A1) A2)
  -> Z -> (pset A1).
Admitted.
Implicit Arguments pset_acc_range_left.

(*Why logic*) Definition pset_acc_range_right :
  forall (A1:Set), forall (A2:Set), (pset A2) -> (memory (pointer A1) A2)
  -> Z -> (pset A1).
Admitted.
Implicit Arguments pset_acc_range_right.

(*Why logic*) Definition pset_union :
  forall (A1:Set), (pset A1) -> (pset A1) -> (pset A1).
Admitted.
Implicit Arguments pset_union.

(*Why logic*) Definition not_in_pset :
  forall (A1:Set), (pointer A1) -> (pset A1) -> Prop.
Admitted.
Implicit Arguments not_in_pset.

(*Why predicate*) Definition not_assigns (A753:Set) (A752:Set) (a:alloc_table) (m1:(memory A752 A753)) (m2:(memory A752 A753)) (l:(pset A753))
  := (forall (p:(pointer A753)),
      ((valid a p) -> ((not_in_pset p l) -> (acc m2 p) = (acc m1 p)))).
Implicit Arguments not_assigns.

(*Why axiom*) Lemma pset_empty_intro :
  forall (A1:Set),
  (forall (p:(pointer A1)), (not_in_pset p (@pset_empty A1))).
Admitted.

(*Why axiom*) Lemma pset_singleton_intro :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    (~(p1 = p2) -> (not_in_pset p1 (pset_singleton p2))))).
Admitted.

(*Why axiom*) Lemma pset_singleton_elim :
  forall (A1:Set),
  (forall (p1:(pointer A1)),
   (forall (p2:(pointer A1)),
    ((not_in_pset p1 (pset_singleton p2)) -> ~(p1 = p2)))).
Admitted.

(*Why axiom*) Lemma not_not_in_singleton :
  forall (A1:Set),
  (forall (p:(pointer A1)), ~(not_in_pset p (pset_singleton p))).
Admitted.

(*Why axiom*) Lemma pset_union_intro :
  forall (A1:Set),
  (forall (l1:(pset A1)),
   (forall (l2:(pset A1)),
    (forall (p:(pointer A1)),
     ((not_in_pset p l1) /\ (not_in_pset p l2) ->
      (not_in_pset p (pset_union l1 l2)))))).
Admitted.

(*Why axiom*) Lemma pset_union_elim1 :
  forall (A1:Set),
  (forall (l1:(pset A1)),
   (forall (l2:(pset A1)),
    (forall (p:(pointer A1)),
     ((not_in_pset p (pset_union l1 l2)) -> (not_in_pset p l1))))).
Admitted.

(*Why axiom*) Lemma pset_union_elim2 :
  forall (A1:Set),
  (forall (l1:(pset A1)),
   (forall (l2:(pset A1)),
    (forall (p:(pointer A1)),
     ((not_in_pset p (pset_union l1 l2)) -> (not_in_pset p l2))))).
Admitted.

(*Why axiom*) Lemma pset_star_intro :
  forall (A1:Set), forall (A2:Set),
  (forall (l:(pset A1)),
   (forall (m:(memory (pointer A2) A1)),
    (forall (p:(pointer A2)),
     ((forall (p1:(pointer A1)), (p = (acc m p1) -> (not_in_pset p1 l))) ->
      (not_in_pset p (pset_star l m)))))).
Admitted.

(*Why axiom*) Lemma pset_star_elim :
  forall (A1:Set), forall (A2:Set),
  (forall (l:(pset A1)),
   (forall (m:(memory (pointer A2) A1)),
    (forall (p:(pointer A2)),
     ((not_in_pset p (pset_star l m)) ->
      (forall (p1:(pointer A1)), (p = (acc m p1) -> (not_in_pset p1 l))))))).
Admitted.

(*Why axiom*) Lemma pset_all_intro :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    ((forall (p1:(pointer A1)),
      (~(not_in_pset p1 l) -> ~((base_addr p) = (base_addr p1)))) ->
     (not_in_pset p (pset_all l))))).
Admitted.

(*Why axiom*) Lemma pset_all_elim :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    ((not_in_pset p (pset_all l)) ->
     (forall (p1:(pointer A1)),
      (~(not_in_pset p1 l) -> ~((base_addr p) = (base_addr p1))))))).
Admitted.

(*Why axiom*) Lemma pset_range_intro :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    (forall (a:Z),
     (forall (b:Z),
      ((forall (p1:(pointer A1)), (not_in_pset p1 l) \/
        (forall (i:Z), (a <= i /\ i <= b -> ~(p = (shift p1 i))))) ->
       (not_in_pset p (pset_range l a b))))))).
Admitted.

(*Why axiom*) Lemma pset_range_elim :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    (forall (a:Z),
     (forall (b:Z),
      ((not_in_pset p (pset_range l a b)) ->
       (forall (p1:(pointer A1)),
        (~(not_in_pset p1 l) ->
         (forall (i:Z), (a <= i /\ i <= b -> ~((shift p1 i) = p)))))))))).
Admitted.

(*Why axiom*) Lemma pset_range_left_intro :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    (forall (a:Z),
     ((forall (p1:(pointer A1)), (not_in_pset p1 l) \/
       (forall (i:Z), (i <= a -> ~(p = (shift p1 i))))) ->
      (not_in_pset p (pset_range_left l a)))))).
Admitted.

(*Why axiom*) Lemma pset_range_left_elim :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    (forall (a:Z),
     ((not_in_pset p (pset_range_left l a)) ->
      (forall (p1:(pointer A1)),
       (~(not_in_pset p1 l) ->
        (forall (i:Z), (i <= a -> ~((shift p1 i) = p))))))))).
Admitted.

(*Why axiom*) Lemma pset_range_right_intro :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    (forall (a:Z),
     ((forall (p1:(pointer A1)), (not_in_pset p1 l) \/
       (forall (i:Z), (a <= i -> ~(p = (shift p1 i))))) ->
      (not_in_pset p (pset_range_right l a)))))).
Admitted.

(*Why axiom*) Lemma pset_range_right_elim :
  forall (A1:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A1)),
    (forall (a:Z),
     ((not_in_pset p (pset_range_right l a)) ->
      (forall (p1:(pointer A1)),
       (~(not_in_pset p1 l) ->
        (forall (i:Z), (a <= i -> ~((shift p1 i) = p))))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_all_intro :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     ((forall (p1:(pointer A2)),
       (~(not_in_pset p1 l) -> (forall (i:Z), ~(p = (acc m (shift p1 i)))))) ->
      (not_in_pset p (pset_acc_all l m)))))).
Admitted.

(*Why axiom*) Lemma pset_acc_all_elim :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     ((not_in_pset p (pset_acc_all l m)) ->
      (forall (p1:(pointer A2)),
       (~(not_in_pset p1 l) -> (forall (i:Z), ~((acc m (shift p1 i)) = p)))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_range_intro :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     (forall (a:Z),
      (forall (b:Z),
       ((forall (p1:(pointer A2)),
         (~(not_in_pset p1 l) ->
          (forall (i:Z), (a <= i /\ i <= b -> ~(p = (acc m (shift p1 i))))))) ->
        (not_in_pset p (pset_acc_range l m a b)))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_range_elim :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     (forall (a:Z),
      (forall (b:Z),
       ((not_in_pset p (pset_acc_range l m a b)) ->
        (forall (p1:(pointer A2)),
         (~(not_in_pset p1 l) ->
          (forall (i:Z), (a <= i /\ i <= b -> ~((acc m (shift p1 i)) = p))))))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_range_left_intro :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     (forall (a:Z),
      ((forall (p1:(pointer A2)),
        (~(not_in_pset p1 l) ->
         (forall (i:Z), (i <= a -> ~(p = (acc m (shift p1 i))))))) ->
       (not_in_pset p (pset_acc_range_left l m a))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_range_left_elim :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     (forall (a:Z),
      ((not_in_pset p (pset_acc_range_left l m a)) ->
       (forall (p1:(pointer A2)),
        (~(not_in_pset p1 l) ->
         (forall (i:Z), (i <= a -> ~((acc m (shift p1 i)) = p)))))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_range_right_intro :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     (forall (a:Z),
      ((forall (p1:(pointer A2)),
        (~(not_in_pset p1 l) ->
         (forall (i:Z), (a <= i -> ~(p = (acc m (shift p1 i))))))) ->
       (not_in_pset p (pset_acc_range_right l m a))))))).
Admitted.

(*Why axiom*) Lemma pset_acc_range_right_elim :
  forall (A1:Set), forall (A2:Set),
  (forall (p:(pointer A1)),
   (forall (l:(pset A2)),
    (forall (m:(memory (pointer A1) A2)),
     (forall (a:Z),
      ((not_in_pset p (pset_acc_range_right l m a)) ->
       (forall (p1:(pointer A2)),
        (~(not_in_pset p1 l) ->
         (forall (i:Z), (a <= i -> ~((acc m (shift p1 i)) = p)))))))))).
Admitted.

(*Why axiom*) Lemma not_assigns_trans :
  forall (A1:Set), forall (A2:Set),
  (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)))))))).
Admitted.

(*Why axiom*) Lemma not_assigns_refl :
  forall (A1:Set), forall (A2:Set),
  (forall (a:alloc_table),
   (forall (l:(pset A1)), (forall (m:(memory A2 A1)), (not_assigns a m m l)))).
Admitted.

(*Why predicate*) Definition valid_acc (A794:Set) (A793:Set) (m1:(memory (pointer A793) A794))
  := (forall (p:(pointer A794)),
      (forall (a:alloc_table), ((valid a p) -> (valid a (acc m1 p))))).
Implicit Arguments valid_acc.

(*Why predicate*) Definition valid_acc_range (A796:Set) (A795:Set) (m1:(memory (pointer A795) A796)) (size:Z)
  := (forall (p:(pointer A796)),
      (forall (a:alloc_table),
       ((valid a p) -> (valid_range a (acc m1 p) 0 (size - 1))))).
Implicit Arguments valid_acc_range.

(*Why axiom*) Lemma valid_acc_range_valid :
  forall (A1:Set), forall (A2:Set),
  (forall (m1:(memory (pointer A1) A2)),
   (forall (size:Z),
    (forall (p:(pointer A2)),
     (forall (a:alloc_table),
      ((valid_acc_range m1 size) -> ((valid a p) -> (valid a (acc m1 p)))))))).
Admitted.

(*Why predicate*) Definition separation1 (A800:Set) (A799:Set) (m1:(memory (pointer A799) A800)) (m2:(memory (pointer A799) A800))
  := (forall (p:(pointer A800)),
      (forall (a:alloc_table),
       ((valid a p) -> ~((base_addr (acc m1 p)) = (base_addr (acc m2 p)))))).
Implicit Arguments separation1.

(*Why predicate*) Definition separation1_range1 (A802:Set) (A801:Set) (m1:(memory (pointer A801) A802)) (m2:(memory (pointer A801) A802)) (size:Z)
  := (forall (p:(pointer A802)),
      (forall (a:alloc_table),
       ((valid a p) ->
        (forall (i1:Z),
         (forall (i2:Z),
          (0 <= i1 /\ i1 < size ->
           (0 <= i2 /\ i2 < size ->
            ~((base_addr (acc m1 (shift p i1))) =
            (base_addr (acc m2 (shift p i2))))))))))).
Implicit Arguments separation1_range1.

(*Why predicate*) Definition separation1_range (A804:Set) (A803:Set) (m:(memory (pointer A803) A804)) (size:Z)
  := (forall (p:(pointer A804)),
      (forall (a:alloc_table),
       ((valid a p) ->
        (forall (i1:Z),
         (0 <= i1 /\ i1 < size ->
          ~((base_addr (acc m (shift p i1))) = (base_addr (acc m p)))))))).
Implicit Arguments separation1_range.

(*Why predicate*) Definition separation2 (A806:Set) (A805:Set) (m1:(memory (pointer A805) A806)) (m2:(memory (pointer A805) A806))
  := (forall (p1:(pointer A806)),
      (forall (p2:(pointer A806)),
       (~(p1 = p2) -> ~((base_addr (acc m1 p1)) = (base_addr (acc m2 p2)))))).
Implicit Arguments separation2.

(*Why predicate*) Definition separation2_range1 (A808:Set) (A807:Set) (m1:(memory (pointer A807) A808)) (m2:(memory (pointer A807) A808)) (size:Z)
  := (forall (p:(pointer A808)),
      (forall (q:(pointer A808)),
       (forall (a:alloc_table),
        (forall (i:Z),
         (0 <= i /\ i < size ->
          ~((base_addr (acc m1 (shift p i))) = (base_addr (acc m2 q)))))))).
Implicit Arguments separation2_range1.

(*Why logic*) Definition on_heap :
  forall (A1:Set), alloc_table -> (pointer A1) -> Prop.
Admitted.
Implicit Arguments on_heap.

(*Why logic*) Definition on_stack :
  forall (A1:Set), alloc_table -> (pointer A1) -> Prop.
Admitted.
Implicit Arguments on_stack.

(*Why logic*) Definition fresh :
  forall (A1:Set), alloc_table -> (pointer A1) -> Prop.
Admitted.
Implicit Arguments fresh.

(*Why axiom*) Lemma fresh_not_valid :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)), ((fresh a p) -> ~(valid a p)))).
Admitted.

(*Why axiom*) Lemma fresh_not_valid_shift :
  forall (A1:Set),
  (forall (a:alloc_table),
   (forall (p:(pointer A1)),
    ((fresh a p) -> (forall (i:Z), ~(valid a (shift p i)))))).
Admitted.

(*Why logic*) Definition alloc_extends : alloc_table -> alloc_table -> Prop.
Admitted.

(*Why axiom*) Lemma alloc_extends_valid :
  forall (A1:Set),
  (forall (a1:alloc_table),
   (forall (a2:alloc_table),
    ((alloc_extends a1 a2) ->
     (forall (q:(pointer A1)), ((valid a1 q) -> (valid a2 q)))))).
Admitted.

(*Why axiom*) Lemma alloc_extends_valid_index :
  forall (A1:Set),
  (forall (a1:alloc_table),
   (forall (a2:alloc_table),
    ((alloc_extends a1 a2) ->
     (forall (q:(pointer A1)),
      (forall (i:Z), ((valid_index a1 q i) -> (valid_index a2 q i))))))).
Admitted.

(*Why axiom*) Lemma alloc_extends_valid_range :
  forall (A1:Set),
  (forall (a1:alloc_table),
   (forall (a2:alloc_table),
    ((alloc_extends a1 a2) ->
     (forall (q:(pointer A1)),
      (forall (i:Z),
       (forall (j:Z), ((valid_range a1 q i j) -> (valid_range a2 q i j)))))))).
Admitted.

(*Why axiom*) Lemma alloc_extends_refl :
  (forall (a:alloc_table), (alloc_extends a a)).
Admitted.

(*Why axiom*) Lemma 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)))))).
Admitted.

(*Why logic*) Definition free_stack :
  alloc_table -> alloc_table -> alloc_table -> Prop.
Admitted.

(*Why axiom*) Lemma free_stack_heap :
  forall (A1:Set),
  (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)))))))).
Admitted.

(*Why axiom*) Lemma free_stack_stack :
  forall (A1:Set),
  (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)))))))).
Admitted.

(*Why logic*) Definition null : forall (A1:Set), (pointer A1).
Admitted.
Set Contextual Implicit.
Implicit Arguments null.
Unset Contextual Implicit.

(*Why axiom*) Lemma null_not_valid :
  forall (A1:Set), (forall (a:alloc_table), ~(valid a (@null A1))).
Admitted.