(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2012                                               *)
(*    CEA (Commissariat a l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

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

(*Why logic*) Definition bool_and : bool -> bool -> bool.
Admitted.

(*Why logic*) Definition bool_or : bool -> bool -> bool.
Admitted.

(*Why logic*) Definition bool_xor : bool -> bool -> bool.
Admitted.

(*Why logic*) Definition bool_not : bool -> bool.
Admitted.

(*Why axiom*) Lemma bool_and_def :
  (forall (a:bool),
   (forall (b:bool), ((bool_and a b) = true <-> a = true /\ b = true))).
Admitted.

(*Why axiom*) Lemma bool_or_def :
  (forall (a:bool),
   (forall (b:bool), ((bool_or a b) = true <-> a = true \/ b = true))).
Admitted.

(*Why axiom*) Lemma bool_xor_def :
  (forall (a:bool), (forall (b:bool), ((bool_xor a b) = true <-> ~(a = b)))).
Admitted.

(*Why axiom*) Lemma bool_not_def :
  (forall (a:bool), ((bool_not a) = true <-> a = false)).
Admitted.

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

(*Why axiom*) Lemma ite_true :
  forall (A1:Set),
  (forall (x:A1), (forall (y:A1), (if_then_else true x y) = x)).
Admitted.

(*Why axiom*) Lemma ite_false :
  forall (A1:Set),
  (forall (x:A1), (forall (y:A1), (if_then_else false x y) = y)).
Admitted.

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

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

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

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

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

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

(*Why axiom*) Lemma lt_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((lt_int_bool x y) = true <-> x < y))).
Admitted.

(*Why axiom*) Lemma le_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((le_int_bool x y) = true <-> x <= y))).
Admitted.

(*Why axiom*) Lemma gt_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((gt_int_bool x y) = true <-> x > y))).
Admitted.

(*Why axiom*) Lemma ge_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((ge_int_bool x y) = true <-> x >= y))).
Admitted.

(*Why axiom*) Lemma eq_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((eq_int_bool x y) = true <-> x = y))).
Admitted.

(*Why axiom*) Lemma neq_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((neq_int_bool x y) = true <-> x <> y))).
Admitted.

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

(*Why axiom*) Lemma abs_int_pos :
  (forall (x:Z), (x >= 0 -> (abs_int x) = x)).
Admitted.

(*Why axiom*) Lemma abs_int_neg :
  (forall (x:Z), (x <= 0 -> (abs_int x) = (Zopp x))).
Admitted.

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

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

(*Why axiom*) Lemma int_max_is_ge :
  (forall (x:Z), (forall (y:Z), (int_max x y) >= x /\ (int_max x y) >= y)).
Admitted.

(*Why axiom*) Lemma int_max_is_some :
  (forall (x:Z), (forall (y:Z), (int_max x y) = x \/ (int_max x y) = y)).
Admitted.

(*Why axiom*) Lemma int_min_is_le :
  (forall (x:Z), (forall (y:Z), (int_min x y) <= x /\ (int_min x y) <= y)).
Admitted.

(*Why axiom*) Lemma int_min_is_some :
  (forall (x:Z), (forall (y:Z), (int_min x y) = x \/ (int_min x y) = y)).
Admitted.

(*Why logic*) Definition lt_real : R -> R -> Prop.
Admitted.

(*Why logic*) Definition le_real : R -> R -> Prop.
Admitted.

(*Why logic*) Definition gt_real : R -> R -> Prop.
Admitted.

(*Why logic*) Definition ge_real : R -> R -> Prop.
Admitted.

(*Why logic*) Definition eq_real : R -> R -> Prop.
Admitted.

(*Why logic*) Definition neq_real : R -> R -> Prop.
Admitted.

(*Why logic*) Definition add_real : R -> R -> R.
Admitted.

(*Why logic*) Definition sub_real : R -> R -> R.
Admitted.

(*Why logic*) Definition mul_real : R -> R -> R.
Admitted.

(*Why logic*) Definition div_real : R -> R -> R.
Admitted.

(*Why logic*) Definition neg_real : R -> R.
Admitted.

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

(*Why axiom*) Lemma real_of_int_zero : (eq (IZR 0) (0)%R).
Admitted.

(*Why axiom*) Lemma real_of_int_one : (eq (IZR 1) (1)%R).
Admitted.

(*Why axiom*) Lemma real_of_int_add :
  (forall (x:Z), (forall (y:Z), (eq (IZR (x + y)) (Rplus (IZR x) (IZR y))))).
Admitted.

(*Why axiom*) Lemma real_of_int_sub :
  (forall (x:Z), (forall (y:Z), (eq (IZR (x - y)) (Rminus (IZR x) (IZR y))))).
Admitted.

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

(*Why axiom*) Lemma truncate_down_pos :
  (forall (x:R),
   ((Rge x (0)%R) -> (Rle (IZR (truncate_real_to_int x)) x) /\
    (Rlt x (IZR ((truncate_real_to_int x) + 1))))).
Admitted.

(*Why axiom*) Lemma truncate_up_neg :
  (forall (x:R),
   ((Rle x (0)%R) -> (Rlt (IZR ((truncate_real_to_int x) - 1)) x) /\
    (Rle x (IZR (truncate_real_to_int x))))).
Admitted.

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

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

(*Why logic*) Definition lt_real_bool : R -> R -> bool.
Admitted.

(*Why logic*) Definition le_real_bool : R -> R -> bool.
Admitted.

(*Why logic*) Definition gt_real_bool : R -> R -> bool.
Admitted.

(*Why logic*) Definition ge_real_bool : R -> R -> bool.
Admitted.

(*Why logic*) Definition eq_real_bool : R -> R -> bool.
Admitted.

(*Why logic*) Definition neq_real_bool : R -> R -> bool.
Admitted.

(*Why axiom*) Lemma lt_real_bool_axiom :
  (forall (x:R), (forall (y:R), ((lt_real_bool x y) = true <-> (Rlt x y)))).
Admitted.

(*Why axiom*) Lemma le_real_bool_axiom :
  (forall (x:R), (forall (y:R), ((le_real_bool x y) = true <-> (Rle x y)))).
Admitted.

(*Why axiom*) Lemma gt_real_bool_axiom :
  (forall (x:R), (forall (y:R), ((gt_real_bool x y) = true <-> (Rgt x y)))).
Admitted.

(*Why axiom*) Lemma ge_real_bool_axiom :
  (forall (x:R), (forall (y:R), ((ge_real_bool x y) = true <-> (Rge x y)))).
Admitted.

(*Why axiom*) Lemma eq_real_bool_axiom :
  (forall (x:R), (forall (y:R), ((eq_real_bool x y) = true <-> (eq x y)))).
Admitted.

(*Why axiom*) Lemma neq_real_bool_axiom :
  (forall (x:R), (forall (y:R), ((neq_real_bool x y) = true <-> ~(eq x y)))).
Admitted.

(*Why logic*) Definition real_max : R -> R -> R.
Admitted.

(*Why logic*) Definition real_min : R -> R -> R.
Admitted.

(*Why axiom*) Lemma real_max_is_ge :
  (forall (x:R),
   (forall (y:R), (Rge (real_max x y) x) /\ (Rge (real_max x y) y))).
Admitted.

(*Why axiom*) Lemma real_max_is_some :
  (forall (x:R),
   (forall (y:R), (eq (real_max x y) x) \/ (eq (real_max x y) y))).
Admitted.

(*Why axiom*) Lemma real_min_is_le :
  (forall (x:R),
   (forall (y:R), (Rle (real_min x y) x) /\ (Rle (real_min x y) y))).
Admitted.

(*Why axiom*) Lemma real_min_is_some :
  (forall (x:R),
   (forall (y:R), (eq (real_min x y) x) \/ (eq (real_min x y) y))).
Admitted.

(*Why function*) Definition sqr_real  (x:R) := (Rmult x x).

(*Why logic*) Definition sqrt_real : R -> R.
Admitted.

(*Why axiom*) Lemma sqrt_pos :
  (forall (x:R), ((Rge x (0)%R) -> (Rge (sqrt x) (0)%R))).
Admitted.

(*Why axiom*) Lemma sqrt_sqr :
  (forall (x:R), ((Rge x (0)%R) -> (eq (sqr_real (sqrt x)) x))).
Admitted.

(*Why axiom*) Lemma sqr_sqrt :
  (forall (x:R), ((Rge x (0)%R) -> (eq (sqrt (Rmult x x)) x))).
Admitted.

(*Why logic*) Definition pow_real : R -> R -> R.
Admitted.

(*Why logic*) Definition abs_real : R -> R.
Admitted.

(*Why axiom*) Lemma abs_real_pos :
  (forall (x:R), ((Rge x (0)%R) -> (eq (Rabs x) x))).
Admitted.

(*Why axiom*) Lemma abs_real_neg :
  (forall (x:R), ((Rle x (0)%R) -> (eq (Rabs x) (Ropp x)))).
Admitted.

(*Why logic*) Definition exp : R -> R.
Admitted.

(*Why logic*) Definition log : R -> R.
Admitted.

(*Why logic*) Definition log10 : R -> R.
Admitted.

(*Why axiom*) Lemma log_exp : (forall (x:R), (eq (log (exp x)) x)).
Admitted.

(*Why axiom*) Lemma exp_log :
  (forall (x:R), ((Rgt x (0)%R) -> (eq (exp (log x)) x))).
Admitted.

(*Why logic*) Definition cos : R -> R.
Admitted.

(*Why logic*) Definition sin : R -> R.
Admitted.

(*Why logic*) Definition tan : R -> R.
Admitted.

(*Why logic*) Definition pi : R.
Admitted.

(*Why logic*) Definition cosh : R -> R.
Admitted.

(*Why logic*) Definition sinh : R -> R.
Admitted.

(*Why logic*) Definition tanh : R -> R.
Admitted.

(*Why logic*) Definition acos : R -> R.
Admitted.

(*Why logic*) Definition asin : R -> R.
Admitted.

(*Why logic*) Definition atan : R -> R.
Admitted.

(*Why logic*) Definition atan2 : R -> R -> R.
Admitted.

(*Why logic*) Definition hypot : R -> R -> R.
Admitted.

(*Why axiom*) Lemma prod_pos :
  (forall (x:R),
   (forall (y:R),
    (((Rgt x (0)%R) /\ (Rgt y (0)%R) -> (Rgt (Rmult x y) (0)%R))) /\
    (((Rlt x (0)%R) /\ (Rlt y (0)%R) -> (Rgt (Rmult x y) (0)%R))))).
Admitted.

(*Why axiom*) Lemma abs_minus :
  (forall (x:R), (eq (Rabs (Ropp x)) (Rabs x))).
Admitted.

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

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

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

(*Why axiom*) Lemma access_update :
  forall (A1:Set),
  (forall (a:(array A1)),
   (forall (i:Z), (forall (v:A1), (access (update a i v) i) = v))).
Admitted.

(*Why axiom*) Lemma access_update_neq :
  forall (A1:Set),
  (forall (a:(array A1)),
   (forall (i:Z),
    (forall (j:Z),
     (forall (v:A1), (i <> j -> (access (update a i v) j) = (access a j)))))).
Admitted.

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

(*Why predicate*) Definition sorted_array  (t:(array Z)) (i:Z) (j:Z)
  := (forall (k1:Z),
      (forall (k2:Z),
       ((i <= k1 /\ k1 <= k2) /\ k2 <= j -> (access t k1) <= (access t k2)))).

(*Why predicate*) Definition exchange (A226:Set) (a1:(array A226)) (a2:(array A226)) (i:Z) (j:Z)
  := (array_length a1) = (array_length a2) /\
     (access a1 i) = (access a2 j) /\ (access a2 i) = (access a1 j) /\
     (forall (k:Z), (k <> i /\ k <> j -> (access a1 k) = (access a2 k))).
Implicit Arguments exchange.

(*Why logic*) Definition permut :
  forall (A1:Set), (array A1) -> (array A1) -> Z -> Z -> Prop.
Admitted.
Implicit Arguments permut.

(*Why axiom*) Lemma permut_refl :
  forall (A1:Set),
  (forall (t:(array A1)), (forall (l:Z), (forall (u:Z), (permut t t l u)))).
Admitted.

(*Why axiom*) Lemma permut_sym :
  forall (A1:Set),
  (forall (t1:(array A1)),
   (forall (t2:(array A1)),
    (forall (l:Z), (forall (u:Z), ((permut t1 t2 l u) -> (permut t2 t1 l u)))))).
Admitted.

(*Why axiom*) Lemma permut_trans :
  forall (A1:Set),
  (forall (t1:(array A1)),
   (forall (t2:(array A1)),
    (forall (t3:(array A1)),
     (forall (l:Z),
      (forall (u:Z),
       ((permut t1 t2 l u) -> ((permut t2 t3 l u) -> (permut t1 t3 l u)))))))).
Admitted.

(*Why axiom*) Lemma permut_exchange :
  forall (A1:Set),
  (forall (a1:(array A1)),
   (forall (a2:(array A1)),
    (forall (l:Z),
     (forall (u:Z),
      (forall (i:Z),
       (forall (j:Z),
        (l <= i /\ i <= u ->
         (l <= j /\ j <= u -> ((exchange a1 a2 i j) -> (permut a1 a2 l u)))))))))).
Admitted.

(*Why axiom*) Lemma exchange_upd :
  forall (A1:Set),
  (forall (a:(array A1)),
   (forall (i:Z),
    (forall (j:Z),
     (exchange a (update (update a i (access a j)) j (access a i)) i j)))).
Admitted.

(*Why axiom*) Lemma permut_weakening :
  forall (A1:Set),
  (forall (a1:(array A1)),
   (forall (a2:(array A1)),
    (forall (l1:Z),
     (forall (r1:Z),
      (forall (l2:Z),
       (forall (r2:Z),
        ((l1 <= l2 /\ l2 <= r2) /\ r2 <= r1 ->
         ((permut a1 a2 l2 r2) -> (permut a1 a2 l1 r1))))))))).
Admitted.

(*Why axiom*) Lemma permut_eq :
  forall (A1:Set),
  (forall (a1:(array A1)),
   (forall (a2:(array A1)),
    (forall (l:Z),
     (forall (u:Z),
      (l <= u ->
       ((permut a1 a2 l u) ->
        (forall (i:Z), (i < l \/ u < i -> (access a2 i) = (access a1 i))))))))).
Admitted.

(*Why predicate*) Definition permutation (A235:Set) (a1:(array A235)) (a2:(array A235))
  := (permut a1 a2 0 ((array_length a1) - 1)).
Implicit Arguments permutation.

(*Why axiom*) Lemma array_length_update :
  forall (A1:Set),
  (forall (a:(array A1)),
   (forall (i:Z),
    (forall (v:A1), (array_length (update a i v)) = (array_length a)))).
Admitted.

(*Why axiom*) Lemma permut_array_length :
  forall (A1:Set),
  (forall (a1:(array A1)),
   (forall (a2:(array A1)),
    (forall (l:Z),
     (forall (u:Z),
      ((permut a1 a2 l u) -> (array_length a1) = (array_length a2)))))).
Admitted.

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

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

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

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

(*Why axiom*) Lemma math_div_mod :
  (forall (x:Z),
   (forall (y:Z), (y <> 0 -> x = (y * (math_div x y) + (math_mod x y))))).
Admitted.

(*Why axiom*) Lemma math_mod_bound :
  (forall (x:Z),
   (forall (y:Z),
    (y <> 0 -> 0 <= (math_mod x y) /\ (math_mod x y) < (abs_int y)))).
Admitted.

(*Why axiom*) Lemma computer_div_mod :
  (forall (x:Z),
   (forall (y:Z),
    (y <> 0 -> x = (y * (computer_div x y) + (computer_mod x y))))).
Admitted.

(*Why axiom*) Lemma computer_div_bound :
  (forall (x:Z),
   (forall (y:Z),
    (x >= 0 /\ y > 0 -> 0 <= (computer_div x y) /\ (computer_div x y) <= x))).
Admitted.

(*Why axiom*) Lemma computer_mod_bound :
  (forall (x:Z),
   (forall (y:Z), (y <> 0 -> (abs_int (computer_mod x y)) < (abs_int y)))).
Admitted.

(*Why axiom*) Lemma computer_mod_sign_pos :
  (forall (x:Z),
   (forall (y:Z), (x >= 0 /\ y <> 0 -> (computer_mod x y) >= 0))).
Admitted.

(*Why axiom*) Lemma computer_mod_sign_neg :
  (forall (x:Z),
   (forall (y:Z), (x <= 0 /\ y <> 0 -> (computer_mod x y) <= 0))).
Admitted.

(*Why axiom*) Lemma computer_rounds_toward_zero :
  (forall (x:Z),
   (forall (y:Z),
    (y <> 0 -> (abs_int ((computer_div x y) * y)) <= (abs_int x)))).
Admitted.

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

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

(*Why axiom*) Lemma positive_computer_div_div :
  (forall (x:Z),
   (forall (y:Z), (x > 0 -> (y > 0 -> (computer_div x y) = (math_div x y))))).
Admitted.

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

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

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

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

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

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

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

(*Why logic*) Definition subset :
  forall (A1:Set), (set A1) -> (set A1) -> Prop.
Admitted.
Implicit Arguments subset.

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

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

(*Why logic*) Definition integers_set : (set Z).
Admitted.

(*Why logic*) Definition equiv :
  forall (A1:Set), (set A1) -> (set A1) -> Prop.
Admitted.
Implicit Arguments equiv.

(*Why logic*) Definition member : forall (A1:Set), A1 -> (set A1) -> Prop.
Admitted.
Implicit Arguments member.

(*Why axiom*) Lemma singleton_def :
  forall (A1:Set), (forall (x:A1), (member x (singleton x))).
Admitted.

(*Why axiom*) Lemma singleton_eq :
  forall (A1:Set),
  (forall (x:A1), (forall (y:A1), ((member x (singleton y)) <-> x = y))).
Admitted.

(*Why axiom*) Lemma union_member :
  forall (A1:Set),
  (forall (x:A1),
   (forall (s1:(set A1)),
    (forall (s2:(set A1)),
     ((member x (union s1 s2)) <-> (member x s1) \/ (member x s2))))).
Admitted.

(*Why axiom*) Lemma union_of_empty :
  forall (A1:Set), (forall (x:(set A1)), (union x (@empty A1)) = x).
Admitted.

(*Why axiom*) Lemma inter_of_empty :
  forall (A1:Set), (forall (x:(set A1)), (inter x (@empty A1)) = (@empty A1)).
Admitted.

(*Why axiom*) Lemma union_comm :
  forall (A1:Set),
  (forall (x:(set A1)), (forall (y:(set A1)), (union x y) = (union y x))).
Admitted.

(*Why axiom*) Lemma inter_comm :
  forall (A1:Set),
  (forall (x:(set A1)), (forall (y:(set A1)), (inter x y) = (inter y x))).
Admitted.

(*Why axiom*) Lemma inter_member :
  forall (A1:Set),
  (forall (x:A1),
   (forall (s1:(set A1)),
    (forall (s2:(set A1)),
     ((member x (inter s1 s2)) <-> (member x s1) /\ (member x s2))))).
Admitted.

(*Why axiom*) Lemma plus_int_member_1 :
  (forall (sa:(set Z)),
   (forall (sb:(set Z)),
    (forall (a:Z),
     (forall (b:Z),
      ((member a sa) -> ((member b sb) -> (member (a + b) (plus_int sa sb)))))))).
Admitted.

(*Why axiom*) Lemma plus_int_member_2 :
  (forall (sa:(set Z)),
   (forall (sb:(set Z)),
    (forall (c:Z),
     ((member c (plus_int sa sb)) ->
      (exists a:Z,
       (exists b:Z, (member a sa) /\ (member b sb) /\ c = (a + b))))))).
Admitted.

(*Why axiom*) Lemma subset_empty :
  forall (A1:Set), (forall (sa:(set A1)), (subset (@empty A1) sa)).
Admitted.

(*Why axiom*) Lemma subset_sym :
  forall (A1:Set), (forall (sa:(set A1)), (subset sa sa)).
Admitted.

(*Why axiom*) Lemma subset_trans :
  forall (A1:Set),
  (forall (sa:(set A1)),
   (forall (sb:(set A1)),
    (forall (sc:(set A1)),
     ((subset sa sb) -> ((subset sb sc) -> (subset sa sc)))))).
Admitted.

(*Why axiom*) Lemma subset_def :
  forall (A1:Set),
  (forall (sa:(set A1)),
   (forall (sb:(set A1)),
    ((forall (a:A1), ((member a sa) -> (member a sb))) <-> (subset sa sb)))).
Admitted.

(*Why axiom*) Lemma range_def :
  (forall (i:Z),
   (forall (j:Z),
    (forall (k:Z), (i <= k /\ k <= j <-> (member k (range i j)))))).
Admitted.

(*Why axiom*) Lemma range_def1 :
  (forall (i:Z),
   (forall (j:Z),
    (forall (k:Z), (i <= k /\ k <= j -> (member k (range i j)))))).
Admitted.

(*Why axiom*) Lemma range_def2 :
  (forall (i:Z),
   (forall (j:Z),
    (forall (k:Z), ((member k (range i j)) -> i <= k /\ k <= j)))).
Admitted.

(*Why axiom*) Lemma range_inf_def :
  (forall (i:Z), (forall (k:Z), (i <= k <-> (member k (range_inf i))))).
Admitted.

(*Why axiom*) Lemma range_sup_def :
  (forall (j:Z), (forall (k:Z), (k <= j <-> (member k (range_sup j))))).
Admitted.

(*Why axiom*) Lemma integers_set_def :
  (forall (k:Z), (k >= 0 <-> (member k integers_set))).
Admitted.

(*Why axiom*) Lemma equiv_def :
  forall (A1:Set),
  (forall (s1:(set A1)),
   (forall (s2:(set A1)),
    ((forall (a:A1), ((member a s1) -> (member a s2))) /\
     (forall (b:A1), ((member b s2) -> (member b s1))) <-> (equiv s1 s2)))).
Admitted.

(*Why axiom*) Lemma equiv_refl :
  forall (A1:Set), (forall (s:(set A1)), (equiv s s)).
Admitted.

(*Why axiom*) Lemma equiv_sym :
  forall (A1:Set),
  (forall (s1:(set A1)),
   (forall (s2:(set A1)), ((equiv s1 s2) -> (equiv s2 s1)))).
Admitted.

(*Why axiom*) Lemma equiv_trans :
  forall (A1:Set),
  (forall (s1:(set A1)),
   (forall (s2:(set A1)),
    (forall (s3:(set A1)),
     ((equiv s1 s2) -> ((equiv s2 s3) -> (equiv s1 s3)))))).
Admitted.

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

(*Why predicate*) Definition is_uint8  (x:Z) := 0 <= x /\ x < 256.

(*Why axiom*) Lemma as_uint8_def : (forall (x:Z), (is_uint8 (as_uint8 x))).
Admitted.

(*Why axiom*) Lemma as_uint8_involve :
  (forall (x:Z), (as_uint8 (as_uint8 x)) = (as_uint8 x)).
Admitted.

(*Why axiom*) Lemma is_as_uint8 :
  (forall (x:Z), ((is_uint8 x) -> (as_uint8 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_sint8  (x:Z) := (-128) <= x /\ x < 128.

(*Why axiom*) Lemma as_sint8_def : (forall (x:Z), (is_sint8 (as_sint8 x))).
Admitted.

(*Why axiom*) Lemma as_sint8_involve :
  (forall (x:Z), (as_sint8 (as_sint8 x)) = (as_sint8 x)).
Admitted.

(*Why axiom*) Lemma is_as_sint8 :
  (forall (x:Z), ((is_sint8 x) -> (as_sint8 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_uint16  (x:Z) := 0 <= x /\ x < 65536.

(*Why axiom*) Lemma as_uint16_def :
  (forall (x:Z), (is_uint16 (as_uint16 x))).
Admitted.

(*Why axiom*) Lemma as_uint16_involve :
  (forall (x:Z), (as_uint16 (as_uint16 x)) = (as_uint16 x)).
Admitted.

(*Why axiom*) Lemma is_as_uint16 :
  (forall (x:Z), ((is_uint16 x) -> (as_uint16 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_sint16  (x:Z) := (-32768) <= x /\ x < 32768.

(*Why axiom*) Lemma as_sint16_def :
  (forall (x:Z), (is_sint16 (as_sint16 x))).
Admitted.

(*Why axiom*) Lemma as_sint16_involve :
  (forall (x:Z), (as_sint16 (as_sint16 x)) = (as_sint16 x)).
Admitted.

(*Why axiom*) Lemma is_as_sint16 :
  (forall (x:Z), ((is_sint16 x) -> (as_sint16 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_uint32  (x:Z) := 0 <= x /\ x < 4294967296.

(*Why axiom*) Lemma as_uint32_def :
  (forall (x:Z), (is_uint32 (as_uint32 x))).
Admitted.

(*Why axiom*) Lemma as_uint32_involve :
  (forall (x:Z), (as_uint32 (as_uint32 x)) = (as_uint32 x)).
Admitted.

(*Why axiom*) Lemma is_as_uint32 :
  (forall (x:Z), ((is_uint32 x) -> (as_uint32 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_sint32  (x:Z)
  := (-2147483648) <= x /\ x < 2147483648.

(*Why axiom*) Lemma as_sint32_def :
  (forall (x:Z), (is_sint32 (as_sint32 x))).
Admitted.

(*Why axiom*) Lemma as_sint32_involve :
  (forall (x:Z), (as_sint32 (as_sint32 x)) = (as_sint32 x)).
Admitted.

(*Why axiom*) Lemma is_as_sint32 :
  (forall (x:Z), ((is_sint32 x) -> (as_sint32 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_uint64  (x:Z)
  := 0 <= x /\ x < 18446744073709551616.

(*Why axiom*) Lemma as_uint64_def :
  (forall (x:Z), (is_uint64 (as_uint64 x))).
Admitted.

(*Why axiom*) Lemma as_uint64_involve :
  (forall (x:Z), (as_uint64 (as_uint64 x)) = (as_uint64 x)).
Admitted.

(*Why axiom*) Lemma is_as_uint64 :
  (forall (x:Z), ((is_uint64 x) -> (as_uint64 x) = x)).
Admitted.

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

(*Why predicate*) Definition is_sint64  (x:Z)
  := (-9223372036854775808) <= x /\ x < 9223372036854775808.

(*Why axiom*) Lemma as_sint64_def :
  (forall (x:Z), (is_sint64 (as_sint64 x))).
Admitted.

(*Why axiom*) Lemma as_sint64_involve :
  (forall (x:Z), (as_sint64 (as_sint64 x)) = (as_sint64 x)).
Admitted.

(*Why axiom*) Lemma is_as_sint64 :
  (forall (x:Z), ((is_sint64 x) -> (as_sint64 x) = x)).
Admitted.

(*Why logic*) Definition as_float16 : R -> R.
Admitted.

(*Why logic*) Definition is_float16 : R -> Prop.
Admitted.

(*Why axiom*) Lemma as_float16_def :
  (forall (x:R), (is_float16 (as_float16 x))).
Admitted.

(*Why axiom*) Lemma as_float16_involve :
  (forall (x:R), (eq (as_float16 (as_float16 x)) (as_float16 x))).
Admitted.

(*Why axiom*) Lemma is_as_float16 :
  (forall (x:R), ((is_float16 x) -> (eq (as_float16 x) x))).
Admitted.

(*Why logic*) Definition as_float32 : R -> R.
Admitted.

(*Why logic*) Definition is_float32 : R -> Prop.
Admitted.

(*Why axiom*) Lemma as_float32_def :
  (forall (x:R), (is_float32 (as_float32 x))).
Admitted.

(*Why axiom*) Lemma as_float32_involve :
  (forall (x:R), (eq (as_float32 (as_float32 x)) (as_float32 x))).
Admitted.

(*Why axiom*) Lemma is_as_float32 :
  (forall (x:R), ((is_float32 x) -> (eq (as_float32 x) x))).
Admitted.

(*Why logic*) Definition as_float64 : R -> R.
Admitted.

(*Why logic*) Definition is_float64 : R -> Prop.
Admitted.

(*Why axiom*) Lemma as_float64_def :
  (forall (x:R), (is_float64 (as_float64 x))).
Admitted.

(*Why axiom*) Lemma as_float64_involve :
  (forall (x:R), (eq (as_float64 (as_float64 x)) (as_float64 x))).
Admitted.

(*Why axiom*) Lemma is_as_float64 :
  (forall (x:R), ((is_float64 x) -> (eq (as_float64 x) x))).
Admitted.

(*Why logic*) Definition as_float128 : R -> R.
Admitted.

(*Why logic*) Definition is_float128 : R -> Prop.
Admitted.

(*Why axiom*) Lemma as_float128_def :
  (forall (x:R), (is_float128 (as_float128 x))).
Admitted.

(*Why axiom*) Lemma as_float128_involve :
  (forall (x:R), (eq (as_float128 (as_float128 x)) (as_float128 x))).
Admitted.

(*Why axiom*) Lemma is_as_float128 :
  (forall (x:R), ((is_float128 x) -> (eq (as_float128 x) x))).
Admitted.

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

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

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

(*Why axiom*) Lemma intofdata_dataofint :
  (forall (x:Z), (int_of_data (data_of_int x)) = x).
Admitted.

(*Why logic*) Definition data_of_real : R -> data.
Admitted.

(*Why logic*) Definition real_of_data : data -> R.
Admitted.

(*Why axiom*) Lemma realofdata_dataofreal :
  (forall (x:R), (eq (real_of_data (data_of_real x)) x)).
Admitted.

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

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

(*Why axiom*) Lemma is_uint8_of_data :
  (forall (d:data), (is_uint8 (uint8_of_data d))).
Admitted.

(*Why axiom*) Lemma uint8ofdata_dataofuint8 :
  (forall (x:Z), ((is_uint8 x) -> (uint8_of_data (data_of_uint8 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_sint8_of_data :
  (forall (d:data), (is_sint8 (sint8_of_data d))).
Admitted.

(*Why axiom*) Lemma sint8ofdata_dataofsint8 :
  (forall (x:Z), ((is_sint8 x) -> (sint8_of_data (data_of_sint8 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_uint16_of_data :
  (forall (d:data), (is_uint16 (uint16_of_data d))).
Admitted.

(*Why axiom*) Lemma uint16ofdata_dataofuint16 :
  (forall (x:Z), ((is_uint16 x) -> (uint16_of_data (data_of_uint16 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_sint16_of_data :
  (forall (d:data), (is_sint16 (sint16_of_data d))).
Admitted.

(*Why axiom*) Lemma sint16ofdata_dataofsint16 :
  (forall (x:Z), ((is_sint16 x) -> (sint16_of_data (data_of_sint16 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_uint32_of_data :
  (forall (d:data), (is_uint32 (uint32_of_data d))).
Admitted.

(*Why axiom*) Lemma uint32ofdata_dataofuint32 :
  (forall (x:Z), ((is_uint32 x) -> (uint32_of_data (data_of_uint32 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_sint32_of_data :
  (forall (d:data), (is_sint32 (sint32_of_data d))).
Admitted.

(*Why axiom*) Lemma sint32ofdata_dataofsint32 :
  (forall (x:Z), ((is_sint32 x) -> (sint32_of_data (data_of_sint32 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_uint64_of_data :
  (forall (d:data), (is_uint64 (uint64_of_data d))).
Admitted.

(*Why axiom*) Lemma uint64ofdata_dataofuint64 :
  (forall (x:Z), ((is_uint64 x) -> (uint64_of_data (data_of_uint64 x)) = x)).
Admitted.

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

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

(*Why axiom*) Lemma is_sint64_of_data :
  (forall (d:data), (is_sint64 (sint64_of_data d))).
Admitted.

(*Why axiom*) Lemma sint64ofdata_dataofsint64 :
  (forall (x:Z), ((is_sint64 x) -> (sint64_of_data (data_of_sint64 x)) = x)).
Admitted.

(*Why logic*) Definition data_of_float16 : R -> data.
Admitted.

(*Why logic*) Definition float16_of_data : data -> R.
Admitted.

(*Why axiom*) Lemma is_float16_of_data :
  (forall (d:data), (is_float16 (float16_of_data d))).
Admitted.

(*Why axiom*) Lemma float16ofdata_dataoffloat16 :
  (forall (x:R),
   ((is_float16 x) -> (eq (float16_of_data (data_of_float16 x)) x))).
Admitted.

(*Why logic*) Definition data_of_float32 : R -> data.
Admitted.

(*Why logic*) Definition float32_of_data : data -> R.
Admitted.

(*Why axiom*) Lemma is_float32_of_data :
  (forall (d:data), (is_float32 (float32_of_data d))).
Admitted.

(*Why axiom*) Lemma float32ofdata_dataoffloat32 :
  (forall (x:R),
   ((is_float32 x) -> (eq (float32_of_data (data_of_float32 x)) x))).
Admitted.

(*Why logic*) Definition data_of_float64 : R -> data.
Admitted.

(*Why logic*) Definition float64_of_data : data -> R.
Admitted.

(*Why axiom*) Lemma is_float64_of_data :
  (forall (d:data), (is_float64 (float64_of_data d))).
Admitted.

(*Why axiom*) Lemma float64ofdata_dataoffloat64 :
  (forall (x:R),
   ((is_float64 x) -> (eq (float64_of_data (data_of_float64 x)) x))).
Admitted.

(*Why logic*) Definition data_of_float128 : R -> data.
Admitted.

(*Why logic*) Definition float128_of_data : data -> R.
Admitted.

(*Why axiom*) Lemma is_float128_of_data :
  (forall (d:data), (is_float128 (float128_of_data d))).
Admitted.

(*Why axiom*) Lemma float128ofdata_dataoffloat128 :
  (forall (x:R),
   ((is_float128 x) -> (eq (float128_of_data (data_of_float128 x)) x))).
Admitted.

(*Why logic*) Definition set_range_index :
  forall (A1:Set), (array A1) -> (set Z) -> Z -> (array A1).
Admitted.
Implicit Arguments set_range_index.

(*Why axiom*) Lemma set_range_def :
  forall (A1:Set),
  (forall (t:(array A1)),
   (forall (rg:(set Z)),
    (forall (k:Z),
     (forall (i:Z),
      (~(member i rg) -> (access (set_range_index t rg k) i) = (access t i)))))).
Admitted.

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

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

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

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

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

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

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

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

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

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

(*Why axiom*) Lemma addr_def :
  (forall (a:Z),
   (forall (b:Z),
    (forall (d:Z), ((addr b d) = a -> (base a) = b /\ (offset a) = d)))).
Admitted.

(*Why axiom*) Lemma addr_id : (forall (p:Z), (addr (base p) (offset p)) = p).
Admitted.

(*Why axiom*) Lemma addr_id2 :
  (forall (p:Z),
   (forall (q:Z), ((base p) = (base q) -> ((offset p) = (offset q) -> p = q)))).
Admitted.

(*Why axiom*) Lemma addr_id3 :
  (forall (p:Z),
   (forall (q:Z), ((base p) = (base q) -> ((offset p) = (offset q) -> p = q)))).
Admitted.

(*Why axiom*) Lemma addr_id4 :
  (forall (p:Z),
   (forall (q:Z), ((base p) = (base q) -> ((offset p) = (offset q) -> p = q)))).
Admitted.

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

(*Why axiom*) Lemma minus_addr_def :
  (forall (a:Z),
   (forall (b:Z),
    ((base a) = (base b) -> (minus_addr a b) = ((offset a) - (offset b))))).
Admitted.

(*Why predicate*) Definition addr_lt  (a:Z) (b:Z)
  := (base a) = (base b) /\ (offset a) < (offset b).

(*Why function*) Definition addr_lt_bool  (a:Z) (b:Z)
  := (bool_and
      (eq_int_bool (base a) (base b)) (lt_int_bool (offset a) (offset b))).

(*Why predicate*) Definition addr_le  (a:Z) (b:Z)
  := (base a) = (base b) /\ (offset a) <= (offset b).

(*Why function*) Definition addr_le_bool  (a:Z) (b:Z)
  := (bool_and
      (eq_int_bool (base a) (base b)) (le_int_bool (offset a) (offset b))).

(*Why function*) Definition addr_eq_bool  (a:Z) (b:Z)
  := (bool_and
      (eq_int_bool (base a) (base b)) (eq_int_bool (offset a) (offset b))).

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

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

(*Why axiom*) Lemma addrofdata_dataofaddr :
  (forall (p:Z), (addr_of_data (data_of_addr p)) = p).
Admitted.

(*Why predicate*) Definition valid  (ta:(array Z)) (p:Z) (n:Z)
  := (n > 0 -> 0 <= (offset p) /\ ((offset p) + n) <= (access ta (base p))).

(*Why logic*) Definition global : (array Z) -> Prop.
Admitted.

(*Why logic*) Definition is_fresh : (array data) -> (array Z) -> Z -> Prop.
Admitted.

(*Why axiom*) Lemma fresh :
  (forall (mem:(array data)),
   (forall (ta:(array Z)),
    (forall (ta':(array Z)),
     (forall (x:Z),
      (forall (p:Z),
       (forall (n:Z),
        ((is_fresh mem ta x) ->
         ((access ta x) = 0 ->
          ((access ta (base p)) = (access ta' (base p)) ->
           ((valid ta' p n) -> (n > 0 -> (forall (d:Z), (addr x d) <> p)))))))))))).
Admitted.

(*Why axiom*) Lemma fresh_access :
  (forall (mem:(array data)),
   (forall (mem':(array data)),
    (forall (ta:(array Z)),
     (forall (ta':(array Z)),
      (forall (b:Z),
       (forall (p:Z),
        (forall (n:Z),
         ((is_fresh mem ta b) ->
          ((access ta b) = 0 ->
           ((valid ta' p n) ->
            (n > 0 ->
             ((access ta (base p)) = (access ta' (base p)) ->
              ((access mem p) = (access mem' p) ->
               (forall (d:Z), (addr b d) <> (addr_of_data (access mem' p)))))))))))))))).
Admitted.

(*Why function*) Definition addr_shift  (p:Z) (dofs:Z)
  := (addr (base p) ((offset p) + dofs)).

(*Why predicate*) Definition separated_on_addr  (p:Z) (p':Z) (n1:Z) (n2:Z)
  := ((base p) = (base p') -> ((offset p) + n1) <= (offset p') \/
      (offset p) >= ((offset p') + n2)).

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

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

(*Why logic*) Definition zempty : zone.
Admitted.

(*Why logic*) Definition zunion : zone -> zone -> zone.
Admitted.

(*Why logic*) Definition included : zone -> zone -> Prop.
Admitted.

(*Why logic*) Definition is_havoc :
  (array Z) -> (array data) -> zone -> (array data) -> Prop.
Admitted.

(*Why logic*) Definition is_block : zone -> Prop.
Admitted.

(*Why axiom*) Lemma is_block_zrange :
  (forall (x:Z),
   (forall (ofs:Z),
    (forall (len:Z), (len > 0 -> (is_block (zrange x ofs len)))))).
Admitted.

(*Why axiom*) Lemma is_not_block_zempty : ~(is_block zempty).
Admitted.

(*Why function*) Definition zrange_of_addr  (p:Z)
  := (zrange (base p) (offset p) 1).

(*Why function*) Definition zrange_of_addr_range  (p:Z) (dofs:Z) (n:Z)
  := (zrange (base p) ((offset p) + dofs) n).

(*Why logic*) Definition separated : zone -> zone -> Prop.
Admitted.

(*Why axiom*) Lemma sep_zrange :
  (forall (b:Z),
   (forall (b':Z),
    (forall (d:Z),
     (forall (d':Z),
      (forall (sz:Z),
       (forall (sz':Z),
        ((separated (zrange b d sz) (zrange b' d' sz')) <->
         (separated_on_addr (addr b d) (addr b' d') sz sz')))))))).
Admitted.

(*Why axiom*) Lemma separated_sym :
  (forall (z:zone),
   (forall (z':zone), ((separated z z') -> (separated z' z)))).
Admitted.

(*Why axiom*) Lemma sep_empty : (forall (z:zone), (separated zempty z)).
Admitted.

(*Why axiom*) Lemma sep_union :
  (forall (z:zone),
   (forall (z':zone),
    (forall (r:zone),
     ((separated z (zunion z' r)) <-> (separated z z') /\ (separated z r))))).
Admitted.

(*Why axiom*) Lemma left_empty : (forall (z:zone), (zunion z zempty) = z).
Admitted.

(*Why axiom*) Lemma right_empty : (forall (z:zone), (zunion zempty z) = z).
Admitted.

(*Why axiom*) Lemma union_same : (forall (z:zone), (zunion z z) = z).
Admitted.

(*Why axiom*) Lemma union_sym :
  (forall (z:zone), (forall (z':zone), (zunion z z') = (zunion z' z))).
Admitted.

(*Why axiom*) Lemma union_assoc :
  (forall (z:zone),
   (forall (r:zone),
    (forall (s:zone), (zunion (zunion z r) s) = (zunion z (zunion r s))))).
Admitted.

(*Why axiom*) Lemma inc_range_range :
  (forall (b:Z),
   (forall (d:Z),
    (forall (sz:Z),
     (forall (b':Z),
      (forall (d':Z),
       (forall (sz':Z),
        ((included (zrange b d sz) (zrange b' d' sz')) <->
         (d < (d + sz) -> b = b' /\ d' <= d /\ (d + sz) <= (d' + sz'))))))))).
Admitted.

(*Why axiom*) Lemma inc_empty : (forall (z:zone), (included zempty z)).
Admitted.

(*Why axiom*) Lemma inc_same : (forall (z:zone), (included z z)).
Admitted.

(*Why axiom*) Lemma inc_range_empty :
  (forall (b:Z),
   (forall (d:Z),
    (forall (sz:Z), ((included (zrange b d sz) zempty) <-> sz <= 0)))).
Admitted.

(*Why axiom*) Lemma inc_union_right :
  (forall (z:zone),
   (forall (r:zone),
    (forall (s:zone),
     ((included z r) \/ (included z s) -> (included z (zunion r s)))))).
Admitted.

(*Why axiom*) Lemma inc_union_left :
  (forall (s:zone),
   (forall (z:zone),
    (forall (z':zone),
     ((included s z) -> ((included z' z) -> (included (zunion s z') z)))))).
Admitted.

(*Why logic*) Definition access_range : (array data) -> zone -> data.
Admitted.

(*Why logic*) Definition update_range :
  (array data) -> zone -> data -> (array data).
Admitted.

(*Why axiom*) Lemma access_update_range_same :
  (forall (m:(array data)),
   (forall (z:zone),
    (forall (d:data),
     ((is_block z) -> (access_range (update_range m z d) z) = d)))).
Admitted.

(*Why axiom*) Lemma access_update_range_sep :
  (forall (m:(array data)),
   (forall (v:data),
    (forall (z:zone),
     (forall (z':zone),
      ((is_block z) ->
       ((is_block z') ->
        ((separated z z') ->
         (access_range (update_range m z v) z') = (access_range m z')))))))).
Admitted.

(*Why axiom*) Lemma access_range_update_addr_sep :
  (forall (m:(array data)),
   (forall (v:data),
    (forall (z:zone),
     (forall (p:Z),
      ((is_block z) ->
       ((separated z (zrange_of_addr p)) ->
        (access_range (update m p v) z) = (access_range m z))))))).
Admitted.

(*Why axiom*) Lemma access_update_range_addr_sep :
  (forall (m:(array data)),
   (forall (v:data),
    (forall (z:zone),
     (forall (p:Z),
      ((is_block z) ->
       ((separated z (zrange_of_addr p)) ->
        (access (update_range m z v) p) = (access m p))))))).
Admitted.

(*Why axiom*) Lemma access_update_sep :
  (forall (m:(array data)),
   (forall (v:data),
    (forall (p:Z),
     (forall (q:Z),
      ((separated (zrange_of_addr p) (zrange_of_addr q)) ->
       (access (update m p v) q) = (access m q)))))).
Admitted.

(*Why logic*) Definition update_havoc :
  (array data) -> zone -> data -> (array data).
Admitted.

(*Why axiom*) Lemma load_havoc :
  (forall (m:(array data)),
   (forall (v:data),
    (forall (z:zone),
     (forall (p:Z),
      ((separated z (zrange_of_addr p)) ->
       (access (update_havoc m z v) p) = (access m p)))))).
Admitted.

(*Why axiom*) Lemma load_is_havoc :
  (forall (alloc:(array Z)),
   (forall (mem:(array data)),
    (forall (mem':(array data)),
     (forall (p:Z),
      (forall (z:zone),
       ((included (zrange_of_addr p) z) ->
        ((is_havoc alloc mem z mem') -> (access mem' p) = (access mem p)))))))).
Admitted.

(*Why logic*) Definition is_assignable : (array Z) -> zone -> zone -> Prop.
Admitted.

(*Why axiom*) Lemma is_assignable_range_free :
  (forall (alloc:(array Z)),
   (forall (p:Z),
    (forall (z:zone),
     ((access alloc (base p)) = 0 ->
      (is_assignable alloc (zrange_of_addr p) z))))).
Admitted.

(*Why axiom*) Lemma is_assignable_included :
  (forall (alloc:(array Z)),
   (forall (z:zone),
    (forall (z':zone), ((included z z') -> (is_assignable alloc z z'))))).
Admitted.

(*Why axiom*) Lemma same_havoc :
  (forall (alloc:(array Z)),
   (forall (mem:(array data)), (forall (z:zone), (is_havoc alloc mem z mem)))).
Admitted.

(*Why axiom*) Lemma havoc_sym :
  (forall (alloc:(array Z)),
   (forall (m1:(array data)),
    (forall (m2:(array data)),
     (forall (z:zone), ((is_havoc alloc m2 z m1) -> (is_havoc alloc m1 z m2)))))).
Admitted.

(*Why axiom*) Lemma store_havoc :
  (forall (alloc:(array Z)),
   (forall (mem:(array data)),
    (forall (mem':(array data)),
     (forall (p:Z),
      (forall (v:data),
       (forall (z:zone),
        ((is_assignable alloc (zrange_of_addr p) z) ->
         ((is_havoc alloc mem z mem') ->
          (is_havoc alloc mem z (update mem' p v)))))))))).
Admitted.

(*Why axiom*) Lemma store_havoc_havoc :
  (forall (alloc:(array Z)),
   (forall (mem:(array data)),
    (forall (mem':(array data)),
     (forall (v:data),
      (forall (z':zone),
       (forall (z:zone),
        ((is_assignable alloc z' z) ->
         ((is_havoc alloc mem z mem') ->
          (is_havoc alloc mem z (update_havoc mem' z' v)))))))))).
Admitted.

(*Why axiom*) Lemma store_range_havoc :
  (forall (alloc:(array Z)),
   (forall (mem:(array data)),
    (forall (mem':(array data)),
     (forall (v:data),
      (forall (z':zone),
       (forall (z:zone),
        ((is_block z') ->
         ((is_assignable alloc z' z) ->
          ((is_havoc alloc mem z mem') ->
           (is_havoc alloc mem z (update_range mem' z' v))))))))))).
Admitted.

(*Why axiom*) Lemma addr_base :
  (forall (b:Z), (forall (d:Z), (base (addr b d)) = b)).
Admitted.

(*Why axiom*) Lemma addr_offset :
  (forall (b:Z), (forall (d:Z), (offset (addr b d)) = d)).
Admitted.

(*Why axiom*) Lemma base_sep :
  (forall (b:Z),
   (forall (b':Z),
    (forall (d:Z), (forall (d':Z), (b <> b' -> (addr b d) <> (addr b' d')))))).
Admitted.

(*Why axiom*) Lemma addr_inj1 :
  (forall (b:Z),
   (forall (b':Z), (forall (d:Z), (b = b' <-> (addr b d) = (addr b' d))))).
Admitted.

(*Why axiom*) Lemma addr_inj2 :
  (forall (b:Z),
   (forall (d:Z), (forall (d':Z), (d = d' <-> (addr b d) = (addr b d'))))).
Admitted.

(*Why axiom*) Lemma addr_lt_eq : (forall (a:Z), ~(addr_lt a a)).
Admitted.

(*Why axiom*) Lemma addr_le_eq : (forall (a:Z), (addr_le a a)).
Admitted.

(*Why axiom*) Lemma minus_pos_lt :
  (forall (a:Z),
   (forall (b:Z),
    ((base a) = (base b) -> (((offset b) - (offset a)) > 0 -> (addr_lt a b))))).
Admitted.

(*Why axiom*) Lemma minus_pos_le :
  (forall (a:Z),
   (forall (b:Z),
    ((base a) = (base b) -> (((offset b) - (offset a)) >= 0 -> (addr_le a b))))).
Admitted.

(*Why axiom*) Lemma addr_lt_le :
  (forall (a:Z), (forall (b:Z), ((addr_lt a b) -> (addr_le a b)))).
Admitted.

(*Why axiom*) Lemma havoc_union_update_left :
  (forall (alloc:(array Z)),
   (forall (m:(array data)),
    (forall (m':(array data)),
     (forall (p:Z),
      (forall (v:data),
       (forall (asgns:zone),
        ((is_havoc alloc m (zunion (zrange_of_addr p) asgns) m') ->
         (is_havoc alloc m (zunion (zrange_of_addr p) asgns) (update m' p v))))))))).
Admitted.

(*Why axiom*) Lemma havoc_union_update_right :
  (forall (alloc:(array Z)),
   (forall (m:(array data)),
    (forall (m':(array data)),
     (forall (p:Z),
      (forall (v:data),
       (forall (z:zone),
        (forall (asgns:zone),
         ((included (zrange_of_addr p) asgns) ->
          ((is_havoc alloc m (zunion z asgns) m') ->
           (is_havoc alloc m (zunion z asgns) (update m' p v))))))))))).
Admitted.

(*Why axiom*) Lemma havoc_union_update_range_left :
  (forall (alloc:(array Z)),
   (forall (m:(array data)),
    (forall (m':(array data)),
     (forall (v:data),
      (forall (p:Z),
       (forall (asgns:zone),
        ((is_havoc alloc m (zunion (zrange_of_addr p) asgns) m') ->
         (is_havoc
          alloc m (zunion (zrange_of_addr p) asgns) (update_range
                                                     m' (zrange_of_addr p) v))))))))).
Admitted.

(*Why axiom*) Lemma havoc_union_update_range_right :
  (forall (alloc:(array Z)),
   (forall (m:(array data)),
    (forall (m':(array data)),
     (forall (v:data),
      (forall (p:Z),
       (forall (z:zone),
        (forall (asgns:zone),
         ((included (zrange_of_addr p) asgns) ->
          ((is_havoc alloc m (zunion z asgns) m') ->
           (is_havoc
            alloc m (zunion z asgns) (update_range m' (zrange_of_addr p) v))))))))))).
Admitted.

(*Why axiom*) Lemma inc_union_union :
  (forall (z0:zone),
   (forall (z1:zone),
    (forall (z2:zone),
     (forall (z3:zone),
      ((included z0 z2) ->
       ((included z1 z3) -> (included (zunion z0 z1) (zunion z2 z3)))))))).
Admitted.

(*Why axiom*) Lemma inc_sub_zone :
  (forall (z:zone),
   (forall (z':zone),
    (included (zunion (zunion z z') (zunion z' z)) (zunion z' z)))).
Admitted.

(*Why axiom*) Lemma inc_permut_union :
  (forall (z:zone),
   (forall (z':zone),
    (forall (r:zone),
     (included (zunion (zunion z z') r) (zunion (zunion z r) z'))))).
Admitted.

(*Why axiom*) Lemma inc_permut2 :
  (forall (z:zone),
   (forall (s:zone),
    (forall (r:zone),
     (included
      (zunion (zunion (zunion (zunion z s) r) r) s) (zunion (zunion z r) s))))).
Admitted.

(*Why axiom*) Lemma union_assoc2 :
  (forall (z:zone),
   (forall (z':zone), (zunion z (zunion z z')) = (zunion z z'))).
Admitted.

(*Why axiom*) Lemma addr_shift_0 : (forall (p:Z), (addr_shift p 0) = p).
Admitted.

(*Why axiom*) Lemma addr_shift_shift :
  (forall (p:Z),
   (forall (d:Z),
    (forall (d':Z), (addr_shift (addr_shift p d) d') =
     (addr_shift p (d + d'))))).
Admitted.

(*Why axiom*) Lemma valid_elt :
  (forall (ta:(array Z)),
   (forall (p:Z),
    (forall (i:Z),
     (forall (n:Z),
      (n > 0 ->
       ((valid ta p n) ->
        (0 <= i -> ((i + 1) <= n -> (valid ta (addr_shift p i) 1))))))))).
Admitted.

(*Why axiom*) Lemma separated_on_addr_sym :
  (forall (p:Z),
   (forall (q:Z),
    (forall (n:Z),
     (forall (m:Z),
      ((separated_on_addr p q n m) -> (separated_on_addr q p m n)))))).
Admitted.

(*Why axiom*) Lemma separated_on_addr_inc :
  (forall (b:Z),
   (forall (d:Z),
    (forall (d':Z),
     (forall (sz:Z),
      (forall (sz':Z),
       (forall (b1:Z),
        (forall (d1:Z),
         (forall (sz1:Z),
          ((separated_on_addr (addr b1 d1) (addr b d) sz1 sz) ->
           (d <= d' ->
            ((d' + sz') <= (d + sz) ->
             (separated_on_addr (addr b1 d1) (addr b d') sz1 sz')))))))))))).
Admitted.

(*Why axiom*) Lemma separated_inc :
  (forall (b:Z),
   (forall (d:Z),
    (forall (d':Z),
     (forall (sz:Z),
      (forall (sz':Z),
       (forall (b1:Z),
        (forall (d1:Z),
         (forall (sz1:Z),
          ((separated (zrange b1 d1 sz1) (zrange b d sz)) ->
           (d <= d' ->
            ((d' + sz') <= (d + sz) ->
             (separated (zrange b1 d1 sz1) (zrange b d' sz'))))))))))))).
Admitted.

(*Why axiom*) Lemma separated_one_elt :
  (forall (n:Z),
   (forall (m:Z),
    (forall (b:Z),
     (forall (d:Z),
      (forall (sz:Z),
       (forall (b':Z),
        (forall (d':Z),
         (forall (sz':Z),
          (0 < n ->
           (0 < m ->
            ((separated (zrange b d (sz * n)) (zrange b' d' (sz' * m))) ->
             (forall (i:Z),
              (forall (j:Z),
               (0 <= i ->
                (0 <= j ->
                 ((d + i + sz) <= (d + sz * n) ->
                  ((d' + j + sz') <= (d' + sz' * m) ->
                   (separated (zrange b (d + i) sz) (zrange b' (d' + j) sz'))))))))))))))))))).
Admitted.

(*Why axiom*) Lemma separated_same_base :
  (forall (b:Z),
   (forall (d:Z),
    (forall (d':Z),
     (forall (sz:Z),
      ((separated (zrange b d sz) (zrange b d' 1)) <-> (d + sz - 1) < d' \/
       d' < d))))).
Admitted.

(*Why axiom*) Lemma store_pointer :
  (forall (x:Z),
   (forall (ofs:Z),
    (forall (y:Z),
     (forall (ofs':Z), (separated_on_addr (addr x ofs) (addr y ofs') 1 1) \/
      (addr x ofs) = (addr y ofs'))))).
Admitted.

