(**************************************************************************)
(*                                                                        *)
(*  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 (A302:Set) (a1:(array A302)) (a2:(array A302)) (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 (A311:Set) (a1:(array A311)) (a2:(array A311))
  := (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 type*) Definition format: Set ->Set.
Admitted.

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

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

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

(*Why logic*) Definition uint8_format : (format Z).
Admitted.

(*Why axiom*) Lemma uint8_format_size : (format_size uint8_format) = 8.
Admitted.

(*Why axiom*) Lemma uint8_format_sign : (signed_format uint8_format) = false.
Admitted.

(*Why logic*) Definition sint8_format : (format Z).
Admitted.

(*Why axiom*) Lemma sint8_format_size : (format_size sint8_format) = 8.
Admitted.

(*Why axiom*) Lemma sint8_format_sign : (signed_format sint8_format) = true.
Admitted.

(*Why logic*) Definition uint16_format : (format Z).
Admitted.

(*Why axiom*) Lemma uint16_format_size : (format_size uint16_format) = 16.
Admitted.

(*Why axiom*) Lemma uint16_format_sign :
  (signed_format uint16_format) = false.
Admitted.

(*Why logic*) Definition sint16_format : (format Z).
Admitted.

(*Why axiom*) Lemma sint16_format_size : (format_size sint16_format) = 16.
Admitted.

(*Why axiom*) Lemma sint16_format_sign :
  (signed_format sint16_format) = true.
Admitted.

(*Why logic*) Definition uint32_format : (format Z).
Admitted.

(*Why axiom*) Lemma uint32_format_size : (format_size uint32_format) = 32.
Admitted.

(*Why axiom*) Lemma uint32_format_sign :
  (signed_format uint32_format) = false.
Admitted.

(*Why logic*) Definition sint32_format : (format Z).
Admitted.

(*Why axiom*) Lemma sint32_format_size : (format_size sint32_format) = 32.
Admitted.

(*Why axiom*) Lemma sint32_format_sign :
  (signed_format sint32_format) = true.
Admitted.

(*Why logic*) Definition uint64_format : (format Z).
Admitted.

(*Why axiom*) Lemma uint64_format_size : (format_size uint64_format) = 64.
Admitted.

(*Why axiom*) Lemma uint64_format_sign :
  (signed_format uint64_format) = false.
Admitted.

(*Why logic*) Definition sint64_format : (format Z).
Admitted.

(*Why axiom*) Lemma sint64_format_size : (format_size sint64_format) = 64.
Admitted.

(*Why axiom*) Lemma sint64_format_sign :
  (signed_format sint64_format) = true.
Admitted.

(*Why axiom*) Lemma is_in_format_sint8 :
  (forall (x:Z), ((is_in_format sint8_format x) <-> (-128) <= x /\ x < 128)).
Admitted.

(*Why axiom*) Lemma is_in_format_uint8 :
  (forall (x:Z), ((is_in_format uint8_format x) <-> 0 <= x /\ x < 256)).
Admitted.

(*Why axiom*) Lemma is_in_format_sint16 :
  (forall (x:Z),
   ((is_in_format sint16_format x) <-> (-32768) <= x /\ x < 32768)).
Admitted.

(*Why axiom*) Lemma is_in_format_uint16 :
  (forall (x:Z), ((is_in_format uint16_format x) <-> 0 <= x /\ x < 65536)).
Admitted.

(*Why axiom*) Lemma is_in_format_sint32 :
  (forall (x:Z),
   ((is_in_format sint32_format x) <-> (-2147483648) <= x /\ x < 2147483648)).
Admitted.

(*Why axiom*) Lemma is_in_format_uint32 :
  (forall (x:Z),
   ((is_in_format uint32_format x) <-> 0 <= x /\ x < 4294967296)).
Admitted.

(*Why axiom*) Lemma is_in_format_sint64 :
  (forall (x:Z),
   ((is_in_format sint64_format x) <-> (-9223372036854775808) <= x /\ x <
    9223372036854775808)).
Admitted.

(*Why axiom*) Lemma is_in_format_uint64 :
  (forall (x:Z),
   ((is_in_format uint64_format x) <-> 0 <= x /\ x < 18446744073709551616)).
Admitted.

(*Why logic*) Definition float16_format : (format R).
Admitted.

(*Why axiom*) Lemma float16_format_size : (format_size float16_format) = 16.
Admitted.

(*Why logic*) Definition float32_format : (format R).
Admitted.

(*Why axiom*) Lemma float32_format_size : (format_size float32_format) = 32.
Admitted.

(*Why logic*) Definition float64_format : (format R).
Admitted.

(*Why axiom*) Lemma float64_format_size : (format_size float64_format) = 64.
Admitted.

(*Why logic*) Definition float96_format : (format R).
Admitted.

(*Why axiom*) Lemma float96_format_size : (format_size float96_format) = 96.
Admitted.

(*Why logic*) Definition float128_format : (format R).
Admitted.

(*Why axiom*) Lemma float128_format_size :
  (format_size float128_format) = 128.
Admitted.

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

(*Why logic*) Definition encode : forall (A1:Set), (format A1) -> A1 -> data.
Admitted.
Implicit Arguments encode.

(*Why logic*) Definition decode : forall (A1:Set), (format A1) -> data -> A1.
Admitted.
Implicit Arguments decode.

(*Why axiom*) Lemma encode_decode :
  forall (A1:Set),
  (forall (f:(format A1)), (forall (d:data), (encode f (decode f d)) = d)).
Admitted.

(*Why axiom*) Lemma decode_encode :
  forall (A1:Set),
  (forall (f:(format A1)), (forall (x:A1), (decode f (encode f x)) = x)).
Admitted.

(*Why axiom*) Lemma decode_inj :
  forall (A1:Set),
  (forall (d:data),
   (forall (d':data),
    (forall (f:(format A1)), (~((decode f d) = (decode f d')) <-> ~(d = d'))))).
Admitted.

(*Why axiom*) Lemma decode_eq :
  forall (A1:Set),
  (forall (d:data),
   (forall (d':data),
    (forall (f:(format A1)), ((decode f d) = (decode f d') <-> d = d')))).
Admitted.

(*Why logic*) Definition int_format : (format Z).
Admitted.

(*Why logic*) Definition real_format : (format R).
Admitted.

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

(*Why axiom*) Lemma simpl_as_int :
  (forall (f:(format Z)),
   (forall (x:Z), ((is_in_format f x) -> (as_int f x) = x))).
Admitted.

(*Why axiom*) Lemma as_int_def :
  (forall (f:(format Z)), (forall (x:Z), (is_in_format f (as_int f x)))).
Admitted.

(*Why axiom*) Lemma involve_as_int :
  (forall (f:(format Z)),
   (forall (x:Z), (as_int f (as_int f x)) = (as_int f x))).
Admitted.

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

(*Why axiom*) Lemma simpl_as_float :
  (forall (f:(format R)),
   (forall (x:R), ((is_in_format f x) -> (eq (as_float f x) x)))).
Admitted.

(*Why axiom*) Lemma as_float_def :
  (forall (f:(format R)), (forall (x:R), (is_in_format f (as_float f x)))).
Admitted.

(*Why axiom*) Lemma involve_as_float :
  (forall (f:(format R)),
   (forall (x:R), (eq (as_float f (as_float f x)) (as_float f x)))).
Admitted.

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

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

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

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

(*Why axiom*) Lemma addr_zone :
  (forall (a:Z), (forall (sz:Z), (z_addr (rt_zone a sz)) = a)).
Admitted.

(*Why axiom*) Lemma size_zone :
  (forall (a:Z), (forall (sz:Z), (0 <= sz -> (z_size (rt_zone a sz)) = sz))).
Admitted.

(*Why axiom*) Lemma rt_zone_inj :
  (forall (a1:Z),
   (forall (a2:Z),
    (forall (sz1:Z),
     (forall (sz2:Z),
      ((rt_zone a1 sz1) = (rt_zone a2 sz2) <-> a1 = a2 /\ sz1 = sz2))))).
Admitted.

(*Why predicate*) Definition rt_disj  (z1:zone) (z2:zone)
  := ((z_addr z1) + (z_size z1)) <= (z_addr z2) \/
     ((z_addr z2) + (z_size z2)) <= (z_addr z1).

(*Why predicate*) Definition rt_incl  (z1:zone) (z2:zone)
  := (z_addr z2) <= (z_addr z1) /\ ((z_addr z1) + (z_size z1)) <=
     ((z_addr z2) + (z_size z2)).

(*Why predicate*) Definition addr_in_zone  (a:Z) (z:zone)
  := (z_addr z) <= a /\ a < ((z_addr z) + (z_size z)).

(*Why function*) Definition rt_shift  (addr:Z) (offset:Z) := (addr + offset).

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

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

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

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

(*Why logic*) Definition zs_empty : zones.
Admitted.

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

(*Why logic*) Definition zs_union : zones -> zones -> zones.
Admitted.

(*Why logic*) Definition zs_incl : zones -> zones -> Prop.
Admitted.

(*Why logic*) Definition zs_disj : zones -> zones -> Prop.
Admitted.

(*Why predicate*) Definition zs_z_incl  (z:zone) (zs:zones)
  := (zs_incl (zs_singleton z) zs).

(*Why predicate*) Definition zs_z_disj  (z:zone) (zs:zones)
  := (zs_disj (zs_singleton z) zs).

(*Why axiom*) Lemma zs_empty_incl :
  (forall (zs:zones), (zs_incl zs_empty zs)).
Admitted.

(*Why axiom*) Lemma zs_z_not_incl_empty :
  (forall (z:zone), ~(zs_incl (zs_singleton z) zs_empty)).
Admitted.

(*Why axiom*) Lemma zs_incl_singleton :
  (forall (z1:zone),
   (forall (z2:zone),
    ((rt_incl z1 z2) <-> (zs_incl (zs_singleton z1) (zs_singleton z2))))).
Admitted.

(*Why axiom*) Lemma zs_incl_union_1 :
  (forall (z:zones),
   (forall (z1:zones),
    (forall (z2:zones), ((zs_incl z z1) -> (zs_incl z (zs_union z1 z2)))))).
Admitted.

(*Why axiom*) Lemma zs_incl_union_2 :
  (forall (z:zones),
   (forall (z1:zones),
    (forall (z2:zones), ((zs_incl z z2) -> (zs_incl z (zs_union z1 z2)))))).
Admitted.

(*Why axiom*) Lemma zs_incl_union_3 :
  (forall (z:zones),
   (forall (z1:zones),
    (forall (z2:zones),
     ((zs_incl z1 z) -> ((zs_incl z2 z) -> (zs_incl (zs_union z1 z2) z)))))).
Admitted.

(*Why axiom*) Lemma zs_disj_singleton :
  (forall (z1:zone),
   (forall (z2:zone),
    ((rt_disj z1 z2) <-> (zs_disj (zs_singleton z1) (zs_singleton z2))))).
Admitted.

(*Why axiom*) Lemma zs_incl_disj :
  (forall (z:zones),
   (forall (zi:zones),
    (forall (zd:zones),
     ((zs_incl zi z) -> ((zs_disj zd z) -> (zs_disj zi zd)))))).
Admitted.

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

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

(*Why axiom*) Lemma bits_size_pos : (forall (b:bits), (bits_size b) >= 0).
Admitted.

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

(*Why axiom*) Lemma eq_bits :
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (sz:Z),
     ((bits_size b1) = sz ->
      ((bits_size b2) = sz ->
       ((forall (i:Z), (0 <= i /\ i < sz -> (nth_bit b1 i) = (nth_bit b2 i))) <->
        b1 = b2)))))).
Admitted.

(*Why predicate*) Definition zero_bits  (b:bits)
  := (forall (i:Z), (0 <= i /\ i < (bits_size b) -> (nth_bit b i) = false)).

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

(*Why axiom*) Lemma bits_part_size :
  (forall (b:bits),
   (forall (off:Z),
    (forall (sz:Z),
     (0 <= off ->
      ((off + sz) <= (bits_size b) -> (bits_size (bits_part b off sz)) = sz))))).
Admitted.

(*Why axiom*) Lemma nth_bits_part :
  (forall (b:bits),
   (forall (off:Z),
    (forall (i:Z),
     (forall (sz:Z),
      (0 <= i /\ i < sz ->
       (0 <= off ->
        ((off + sz) <= (bits_size b) ->
         (nth_bit (bits_part b off sz) i) = (nth_bit b (off + i))))))))).
Admitted.

(*Why logic*) Definition bits_concat : bits -> bits -> bits.
Admitted.

(*Why axiom*) Lemma bits_concat_size :
  (forall (b1:bits),
   (forall (b2:bits), (bits_size (bits_concat b1 b2)) =
    ((bits_size b1) + (bits_size b2)))).
Admitted.

(*Why axiom*) Lemma nth_bits_concat_l :
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (i:Z),
     (0 <= i /\ i < (bits_size b1) ->
      (nth_bit (bits_concat b1 b2) i) = (nth_bit b1 i))))).
Admitted.

(*Why axiom*) Lemma nth_bits_concat_r :
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (i:Z),
     (forall (sz1:Z),
      (forall (sz2:Z),
       (sz1 = (bits_size b1) ->
        (sz2 = (bits_size b2) ->
         (sz1 <= i /\ i < (sz1 + sz2) ->
          (nth_bit (bits_concat b1 b2) i) = (nth_bit b2 (i - sz1)))))))))).
Admitted.

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

(*Why axiom*) Lemma wr_bits_part_size :
  (forall (b:bits),
   (forall (bw:bits),
    (forall (o:Z), (bits_size (wr_bits_part b o bw)) = (bits_size b)))).
Admitted.

(*Why axiom*) Lemma nth_wr_bits_part_1 :
  (forall (b:bits),
   (forall (b':bits),
    (forall (off:Z),
     (forall (i:Z),
      (0 <= i /\ i < off ->
       (nth_bit (wr_bits_part b off b') i) = (nth_bit b i)))))).
Admitted.

(*Why axiom*) Lemma nth_wr_bits_part_2 :
  (forall (b:bits),
   (forall (b':bits),
    (forall (off:Z),
     (forall (i:Z),
      ((0 <= off /\ off <= i) /\ i < (off + (bits_size b')) ->
       (nth_bit (wr_bits_part b off b') i) = (nth_bit b' (i - off))))))).
Admitted.

(*Why axiom*) Lemma nth_wr_bits_part_3 :
  (forall (b:bits),
   (forall (b':bits),
    (forall (off:Z),
     (forall (i:Z),
      ((0 <= (off + (bits_size b')) /\ (off + (bits_size b')) <= i) /\ i <
       (bits_size b) -> (nth_bit (wr_bits_part b off b') i) = (nth_bit b i)))))).
Admitted.

(*Why logic*) Definition rt_from_bits :
  forall (A1:Set), bits -> (format A1) -> A1.
Admitted.
Implicit Arguments rt_from_bits.

(*Why axiom*) Lemma rt_from_bits_format :
  forall (A1:Set),
  (forall (b:bits),
   (forall (fmt:(format A1)),
    ((bits_size b) = (format_size fmt) ->
     (is_in_format fmt (rt_from_bits b fmt))))).
Admitted.

(*Why logic*) Definition rt_to_bits :
  forall (A1:Set), (format A1) -> A1 -> bits.
Admitted.
Implicit Arguments rt_to_bits.

(*Why axiom*) Lemma rt_to_bits_size :
  forall (A1:Set),
  (forall (fmt:(format A1)),
   (forall (x:A1), (bits_size (rt_to_bits fmt x)) = (format_size fmt))).
Admitted.

(*Why axiom*) Lemma rt_to_bits_from_bits :
  forall (A1:Set),
  (forall (fmt:(format A1)),
   (forall (b:bits),
    ((bits_size b) = (format_size fmt) ->
     (rt_to_bits fmt (rt_from_bits b fmt)) = b))).
Admitted.

(*Why axiom*) Lemma rt_from_bits_to_bits :
  forall (A1:Set),
  (forall (fmt:(format A1)),
   (forall (v:A1),
    ((is_in_format fmt v) -> (rt_from_bits (rt_to_bits fmt v) fmt) = v))).
Admitted.

(*Why axiom*) Lemma same_int_val_same_bits :
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (fmt:(format Z)),
     ((bits_size b1) = (format_size fmt) ->
      ((bits_size b2) = (format_size fmt) ->
       ((rt_from_bits b1 fmt) = (rt_from_bits b2 fmt) -> b1 = b2)))))).
Admitted.

(*Why axiom*) Lemma rt_to_bits_zero :
  (forall (fmt:(format Z)),
   (forall (b:bits), (b = (rt_to_bits fmt 0) -> (zero_bits b)))).
Admitted.

(*Why axiom*) Lemma rt_from_bits_zero :
  (forall (b:bits),
   (forall (fmt:(format Z)), ((zero_bits b) -> (rt_from_bits b fmt) = 0))).
Admitted.

(*Why logic*) Definition mbyte_to_bbits : bits -> (array bool).
Admitted.

(*Why axiom*) Lemma mbyte_to_bbits_def :
  (forall (b:bits),
   ((bits_size b) = 8 ->
    (forall (i:Z),
     (0 <= i /\ i < 8 -> (access (mbyte_to_bbits b) i) = (nth_bit b (7 - i)))))).
Admitted.

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

(*Why axiom*) Lemma nth_mbyte_size :
  (forall (b:bits), (forall (k:Z), (bits_size (nth_mbyte k b)) = 8)).
Admitted.

(*Why axiom*) Lemma nth_byte_def :
  (forall (b:bits),
   (forall (k:Z),
    (0 <= (8 * (k + 1)) /\ (8 * (k + 1)) <= (bits_size b) ->
     (forall (i:Z),
      (0 <= i /\ i < 8 ->
       (nth_bit (nth_mbyte k b) i) = (nth_bit b (8 * k + i))))))).
Admitted.

(*Why function*) Definition nth_byte  (k:Z) (b:bits)
  := (mbyte_to_bbits (nth_mbyte k b)).

(*Why logic*) Definition little_endian : Prop.
Admitted.

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

(*Why axiom*) Lemma concat_bytes_left :
  (forall (w:(array bool)),
   (forall (b:(array bool)),
    (forall (i:Z),
     (8 <= i -> (access (concat_bytes w b) i) = (access w (i - 8)))))).
Admitted.

(*Why axiom*) Lemma concat_bytes_right :
  (forall (w:(array bool)),
   (forall (b:(array bool)),
    (forall (i:Z),
     (0 <= i /\ i < 8 -> (access (concat_bytes w b) i) = (access b i))))).
Admitted.

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

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

(*Why function*) Definition cint_of_bits  (fmt:(format Z)) (b:(array bool))
  := (if_then_else (signed_format fmt)
      (sint_of_bits ((format_size fmt) - 1) b)
      (uint_of_bits ((format_size fmt) - 1) b)).

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

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

(*Why function*) Definition bits_of_cint  (fmt:(format Z)) (x:Z)
  := (if_then_else (signed_format fmt)
      (bits_of_sint ((format_size fmt) - 1) x)
      (bits_of_uint ((format_size fmt) - 1) x)).

(*Why logic*) Definition mbits_to_bbits : bits -> (array bool).
Admitted.

(*Why axiom*) Lemma mb8_to_bbits :
  (forall (b:bits),
   ((bits_size b) = 8 -> (mbits_to_bbits b) = (nth_byte 0 b))).
Admitted.

(*Why axiom*) Lemma little_mb16_to_bbits :
  (forall (b:bits),
   ((bits_size b) = 16 ->
    (little_endian ->
     (mbits_to_bbits b) = (concat_bytes (nth_byte 1 b) (nth_byte 0 b))))).
Admitted.

(*Why axiom*) Lemma big_mb16_to_bbits :
  (forall (b:bits),
   ((bits_size b) = 16 ->
    (~little_endian ->
     (mbits_to_bbits b) = (concat_bytes (nth_byte 0 b) (nth_byte 1 b))))).
Admitted.

(*Why axiom*) Lemma little_mb32_to_bbits :
  (forall (b:bits),
   ((bits_size b) = 32 ->
    (little_endian ->
     (mbits_to_bbits b) =
     (concat_bytes
      (concat_bytes
       (concat_bytes (nth_byte 3 b) (nth_byte 2 b)) (nth_byte 1 b)) (
      nth_byte 0 b))))).
Admitted.

(*Why axiom*) Lemma big_mb32_to_bbits :
  (forall (b:bits),
   ((bits_size b) = 32 ->
    (~little_endian ->
     (mbits_to_bbits b) =
     (concat_bytes
      (concat_bytes
       (concat_bytes (nth_byte 0 b) (nth_byte 1 b)) (nth_byte 2 b)) (
      nth_byte 3 b))))).
Admitted.

(*Why axiom*) Lemma rt_int_from_bits :
  (forall (b:bits),
   (forall (fmt:(format Z)), (rt_from_bits b fmt) =
    (cint_of_bits fmt (mbits_to_bbits b)))).
Admitted.

(*Why logic*) Definition bbits_to_mbyte : Z -> (array bool) -> bits.
Admitted.

(*Why axiom*) Lemma bbits_to_mbyte_size :
  (forall (b:(array bool)),
   (forall (k:Z), (bits_size (bbits_to_mbyte k b)) = 8)).
Admitted.

(*Why axiom*) Lemma bbits_to_mbyte_def :
  (forall (b:(array bool)),
   (forall (k:Z),
    (forall (i:Z),
     (0 <= i /\ i < 8 ->
      (nth_bit (bbits_to_mbyte k b) i) = (access b (8 * k + 7 - i)))))).
Admitted.

(*Why logic*) Definition bbits_to_mbits : Z -> (array bool) -> bits.
Admitted.

(*Why axiom*) Lemma bbits_to_mb8 :
  (forall (b:(array bool)), (bbits_to_mbits 8 b) = (bbits_to_mbyte 0 b)).
Admitted.

(*Why axiom*) Lemma bbits_to_little_mb16 :
  (forall (b:(array bool)),
   (little_endian ->
    (bbits_to_mbits 16 b) =
    (bits_concat (bbits_to_mbyte 0 b) (bbits_to_mbyte 1 b)))).
Admitted.

(*Why axiom*) Lemma bbits_to_big_mb16 :
  (forall (b:(array bool)),
   (~little_endian ->
    (bbits_to_mbits 16 b) =
    (bits_concat (bbits_to_mbyte 1 b) (bbits_to_mbyte 0 b)))).
Admitted.

(*Why axiom*) Lemma bbits_to_little_mb32 :
  (forall (b:(array bool)),
   (little_endian ->
    (bbits_to_mbits 32 b) =
    (bits_concat
     (bbits_to_mbyte 0 b) (bits_concat
                           (bbits_to_mbyte 1 b) (bits_concat
                                                 (bbits_to_mbyte 2 b) (
                                                 bbits_to_mbyte 3 b)))))).
Admitted.

(*Why axiom*) Lemma bbits_to_not_mb32 :
  (forall (b:(array bool)),
   (~little_endian ->
    (bbits_to_mbits 32 b) =
    (bits_concat
     (bbits_to_mbyte 3 b) (bits_concat
                           (bbits_to_mbyte 2 b) (bits_concat
                                                 (bbits_to_mbyte 1 b) (
                                                 bbits_to_mbyte 0 b)))))).
Admitted.

(*Why axiom*) Lemma rt_int_to_bits :
  (forall (x:Z),
   (forall (fmt:(format Z)),
    (rt_to_bits fmt x) =
    (bbits_to_mbits (format_size fmt) (bits_of_cint fmt x)))).
Admitted.

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

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

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

(*Why axiom*) Lemma incl_valid :
  (forall (m:memalloc),
   (forall (z:zone),
    (forall (z':zone),
     ((rt_incl z' z) -> ((rt_valid m z) -> (rt_valid m z')))))).
Admitted.

(*Why axiom*) Lemma disj_valid :
  (forall (m:memalloc),
   (forall (z:zone),
    (forall (z':zone),
     ((rt_valid m z) -> (~(rt_valid m z') -> (rt_disj z z')))))).
Admitted.

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

(*Why function*) Definition rt_abase  (m:memalloc) (addr:Z)
  := (z_addr (rt_zbase m addr)).

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

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

(*Why logic*) Definition mem_of_mz : mz -> memalloc.
Admitted.

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

(*Why logic*) Definition rt_alloc : memalloc -> Z -> mz.
Admitted.

(*Why function*) Definition alloc_zone  (m:memalloc) (sz:Z)
  := (rt_zone (addr_of_mz (rt_alloc m sz)) sz).

(*Why axiom*) Lemma alloc_is_base :
  (forall (m:memalloc),
   (forall (sz:Z),
    let mz := (rt_alloc m sz) in
    (rt_zbase (mem_of_mz mz) (addr_of_mz mz)) = (alloc_zone m sz))).
Admitted.

(*Why axiom*) Lemma valid_alloc :
  (forall (m:memalloc),
   (forall (sz:Z),
    let mz := (rt_alloc m sz) in
    (rt_valid (mem_of_mz mz) (alloc_zone m sz)))).
Admitted.

(*Why axiom*) Lemma not_valid_before_alloc :
  (forall (m:memalloc), (forall (sz:Z), ~(rt_valid m (alloc_zone m sz)))).
Admitted.

(*Why axiom*) Lemma alloc_keep_valid :
  (forall (m:memalloc),
   (forall (sz:Z),
    (forall (z:zone),
     ((rt_valid m z) ->
      let mz := (rt_alloc m sz) in
      (rt_valid (mem_of_mz mz) z))))).
Admitted.

(*Why axiom*) Lemma alloc_keep_invalid :
  (forall (m:memalloc),
   (forall (sz:Z),
    (forall (z:zone),
     let mz := (rt_alloc m sz) in
     ((rt_valid (mem_of_mz mz) z) ->
      ((rt_disj (alloc_zone m sz) z) -> (rt_valid m z)))))).
Admitted.

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

(*Why axiom*) Lemma not_valid_after_free :
  (forall (m:memalloc),
   (forall (addr:Z),
    (forall (z:zone),
     (z = (rt_zbase m addr) ->
      (addr = (z_addr z) -> ~(rt_valid (rt_free m addr) z)))))).
Admitted.

(*Why axiom*) Lemma valid_free_disj :
  (forall (m:memalloc),
   (forall (z:zone),
    (forall (z':zone),
     ((rt_valid (rt_free m (z_addr z)) z') <-> (rt_disj z z'))))).
Admitted.

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

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

(*Why function*) Definition rt_vzone  (ma:memalloc) (var:Z)
  := (rt_zone (rt_vaddr ma var) (rt_vsize var)).

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

(*Why axiom*) Lemma rt_global_vaddr :
  (forall (v:Z),
   ((rt_global v) ->
    (forall (ma:memalloc),
     (forall (ma':memalloc), (rt_vaddr ma v) = (rt_vaddr ma' v))))).
Admitted.

(*Why axiom*) Lemma rt_global_valid :
  (forall (ma:memalloc),
   (forall (v:Z),
    ((rt_global v) ->
     (forall (ma:memalloc),
      (forall (ma':memalloc), (rt_valid ma (rt_vzone ma' v))))))).
Admitted.

(*Why axiom*) Lemma vzone_disj :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v2:Z),
     (v1 <> v2 ->
      let z1 := (rt_vzone ma v1) in
      let z2 := (rt_vzone ma v2) in
      ((rt_valid ma z1) -> ((rt_valid ma z2) -> (rt_disj z1 z2))))))).
Admitted.

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

(*Why axiom*) Lemma rt_valloc_mem :
  (forall (ma:memalloc),
   (forall (var:Z),
    (rt_valloc ma var) = (mem_of_mz (rt_alloc ma (rt_vsize var))))).
Admitted.

(*Why axiom*) Lemma rt_valloc_addr :
  (forall (ma:memalloc),
   (forall (var:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma var) ->
      (forall (mz:mz),
       (mz = (rt_alloc ma (rt_vsize var)) -> (rt_vaddr ma' var) =
        (addr_of_mz mz))))))).
Admitted.

(*Why axiom*) Lemma vzone_valloc_neq :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v2:Z),
     (forall (ma':memalloc),
      (ma' = (rt_valloc ma v1) ->
       (v1 <> v2 -> (rt_vzone ma' v2) = (rt_vzone ma v2))))))).
Admitted.

(*Why function*) Definition rt_vfree  (ma:memalloc) (var:Z)
  := (rt_free ma (rt_vaddr ma var)).

(*Why axiom*) Lemma rt_vaddr_vfree :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v2:Z),
     (v1 <> v2 -> (rt_vaddr (rt_vfree ma v1) v2) = (rt_vaddr ma v2))))).
Admitted.

(*Why axiom*) Lemma addr_base :
  (forall (m:memalloc),
   (forall (v:Z), (rt_abase m (rt_vaddr m v)) = (rt_vaddr m v))).
Admitted.

(*Why logic*) Definition rt_load : memory -> zone -> bits.
Admitted.

(*Why logic*) Definition rt_store : memory -> Z -> bits -> memory.
Admitted.

(*Why axiom*) Lemma load_store_same :
  (forall (m:memory),
   (forall (a:Z),
    (forall (z:zone),
     (forall (v:bits),
      (z = (rt_zone a (bits_size v)) -> (rt_load (rt_store m a v) z) = v))))).
Admitted.

(*Why axiom*) Lemma load_store_disj :
  (forall (m:memory),
   (forall (a:Z),
    (forall (z:zone),
     (forall (v:bits),
      ((rt_disj (rt_zone a (bits_size v)) z) ->
       (rt_load (rt_store m a v) z) = (rt_load m z)))))).
Admitted.

(*Why axiom*) Lemma load_store_incl_part :
  (forall (m:memory),
   (forall (a:Z),
    (forall (z1:zone),
     (forall (z2:zone),
      (forall (v:bits),
       (z2 = (rt_zone a (bits_size v)) ->
        ((rt_incl z1 z2) ->
         (rt_load (rt_store m a v) z1) =
         (bits_part v ((z_addr z1) - a) (z_size z1))))))))).
Admitted.

(*Why axiom*) Lemma load_incl_part_store :
  (forall (m:memory),
   (forall (z1:zone),
    (forall (z2:zone),
     (forall (v:bits),
      (forall (a:Z),
       (z1 = (rt_zone a (bits_size v)) ->
        (forall (off:Z),
         (off = (a - (z_addr z2)) ->
          ((rt_incl z1 z2) ->
           (rt_load (rt_store m a v) z2) =
           (wr_bits_part (rt_load m z2) off v)))))))))).
Admitted.

(*Why axiom*) Lemma rt_load_size :
  (forall (m:memory),
   (forall (z:zone), (bits_size (rt_load m z)) = (z_size z))).
Admitted.

(*Why axiom*) Lemma bits_part_rt_load :
  (forall (z:zone),
   (forall (z':zone),
    (forall (a':Z),
     (forall (off:Z),
      (forall (sz:Z),
       (a' = ((z_addr z) + off) ->
        (z' = (rt_zone a' sz) ->
         ((rt_incl z' z) ->
          (forall (m:memory),
           (rt_load m z') = (bits_part (rt_load m z) off sz)))))))))).
Admitted.

(*Why axiom*) Lemma rt_same_mem :
  (forall (m1:memory),
   (forall (m2:memory),
    ((forall (z:zone), (rt_load m1 z) = (rt_load m2 z)) -> m1 = m2))).
Admitted.

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

(*Why predicate*) Definition rt_is_havoc  (ma:memalloc) (m1:memory) (zs:zones) (m2:memory)
  := (forall (z:zone),
      ((rt_valid ma z) ->
       ((zs_z_disj z zs) -> (rt_load m1 z) = (rt_load m2 z)))).

(*Why axiom*) Lemma rt_havoc_is_havoc :
  (forall (ma:memalloc),
   (forall (m:memory),
    (forall (zs:zones),
     (forall (z:zone),
      ((zs_z_incl z zs) -> (rt_is_havoc ma m zs (rt_havoc m z))))))).
Admitted.

(*Why logic*) Definition rt_addr_format : (format Z).
Admitted.

(*Why axiom*) Lemma rt_vaddr_format :
  (forall (ma:memalloc),
   (forall (v:Z), (is_in_format rt_addr_format (rt_vaddr ma v)))).
Admitted.

(*Why axiom*) Lemma bits_part_vs_access :
  (forall (bs:bits),
   (forall (fs:(format (array data))),
    (forall (f:Z),
     (forall (off:Z),
      (forall (sz:Z),
       (off = (rt_foffset f) ->
        (sz = (rt_fsize f) ->
         (rt_from_bits (bits_part bs off sz) (rt_fformat f)) =
         (decode int_format (access (rt_from_bits bs fs) f))))))))).
Admitted.

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

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

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

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

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

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

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

(*Why axiom*) Lemma rt_disj_sym :
  (forall (z1:zone),
   (forall (z2:zone), ((rt_disj z1 z2) <-> (rt_disj z2 z1)))).
Admitted.

(*Why axiom*) Lemma rt_disj_shift :
  (forall (addr:Z),
   (forall (i:Z),
    (forall (j:Z),
     (forall (sz:Z),
      (sz > 0 ->
       (i <> j ->
        (rt_disj
         (rt_zone (rt_shift addr (i * sz)) sz) (rt_zone
                                                (rt_shift addr (j * sz)) sz)))))))).
Admitted.

(*Why axiom*) Lemma vzone_of_zone :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (a:Z),
     (forall (sz:Z),
      (a = (rt_vaddr ma v) ->
       (sz = (rt_vsize v) -> (rt_zone a sz) = (rt_vzone ma v))))))).
Admitted.

(*Why axiom*) Lemma bits_part_full :
  (forall (v:bits),
   (forall (sz:Z), (sz = (bits_size v) -> (bits_part v 0 sz) = v))).
Admitted.

(*Why axiom*) Lemma bits_part_of_bits_part :
  (forall (b:bits),
   (forall (o1:Z),
    (forall (o2:Z),
     (forall (sz1:Z),
      (forall (sz2:Z),
       (0 <= o1 ->
        ((o1 + sz1) <= (bits_size b) ->
         (0 <= o2 ->
          ((o2 + sz2) <= sz1 ->
           (bits_part (bits_part b o1 sz1) o2 sz2) =
           (bits_part b (o1 + o2) sz2)))))))))).
Admitted.

(*Why axiom*) Lemma eq_bits_split :
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (sz:Z),
     ((bits_size b1) = sz ->
      ((bits_size b2) = sz ->
       (forall (sz1:Z),
        (forall (sz2:Z),
         (sz1 >= 0 ->
          (sz2 >= 0 ->
           ((sz1 + sz2) = sz ->
            ((bits_part b1 0 sz1) = (bits_part b2 0 sz1) ->
             ((bits_part b1 sz1 sz2) = (bits_part b2 sz1 sz2) -> b1 = b2)))))))))))).
Admitted.

(*Why axiom*) Lemma wr_bits_part_all :
  (forall (v:bits),
   (forall (v':bits),
    ((bits_size v) = (bits_size v') -> (wr_bits_part v 0 v') = v'))).
Admitted.

(*Why axiom*) Lemma wr_bits_part_concat :
  (forall (b:bits),
   (forall (b':bits),
    (forall (sz1:Z),
     (forall (sz2:Z),
      (forall (sz3:Z),
       (0 <= sz1 ->
        (sz2 = (bits_size b') ->
         (0 <= sz3 ->
          ((sz1 + sz2 + sz3) = (bits_size b) ->
           (wr_bits_part b sz1 b') =
           (bits_concat
            (bits_part b 0 sz1) (bits_concat b' (bits_part b (sz1 + sz2) sz3)))))))))))).
Admitted.

(*Why axiom*) Lemma wr_bits_part_same :
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (off:Z),
     (0 <= off ->
      ((off + (bits_size b2)) <= (bits_size b1) ->
       (bits_part (wr_bits_part b1 off b2) off (bits_size b2)) = b2))))).
Admitted.

(*Why axiom*) Lemma wr_bits_part_disj :
  (forall (b:bits),
   (forall (b1:bits),
    (forall (off2:Z),
     (forall (off1:Z),
      (forall (sz:Z),
       (forall (sz1:Z),
        (forall (sz2:Z),
         (sz = (bits_size b) ->
          (sz1 = (bits_size b1) ->
           (0 <= off1 ->
            ((off1 + sz1) <= sz ->
             (0 <= off2 ->
              ((off2 + sz2) <= sz ->
               ((off2 + sz2) <= off1 \/ (off1 + sz1) <= off2 ->
                (bits_part (wr_bits_part b off1 b1) off2 sz2) =
                (bits_part b off2 sz2))))))))))))))).
Admitted.

(*Why axiom*) Lemma rt_z_from_bits_to_bits_zero :
  (forall (fmt:(format Z)),
   (forall (fmt':(format Z)), (rt_from_bits (rt_to_bits fmt 0) fmt') = 0)).
Admitted.

(*Why axiom*) Lemma bits_part_zero :
  (forall (b:bits),
   (forall (b':bits),
    (forall (off:Z),
     (forall (sz:Z),
      (0 <= off ->
       ((off + sz) <= (bits_size b) ->
        (b' = (bits_part b off sz) -> ((zero_bits b) -> (zero_bits b'))))))))).
Admitted.

(*Why axiom*) Lemma rw_same_var :
  (forall (m:memory),
   (forall (ma:memalloc),
    (forall (v:Z),
     (forall (val:bits),
      ((bits_size val) = (rt_vsize v) ->
       (rt_load (rt_store m (rt_vaddr ma v) val) (rt_vzone ma v)) = val))))).
Admitted.

(*Why axiom*) Lemma rw_disj_var :
  (forall (ma:memalloc),
   (forall (m:memory),
    (forall (v1:Z),
     (forall (v2:Z),
      (forall (z1:zone),
       (forall (z2:zone),
        (forall (b:bits),
         (v1 <> v2 ->
          (z1 = (rt_vzone ma v1) ->
           (z2 = (rt_vzone ma v2) ->
            ((rt_valid ma z1) ->
             ((rt_valid ma z2) ->
              ((rt_vsize v2) = (bits_size b) ->
               (rt_load (rt_store m (rt_vaddr ma v2) b) z1) = (rt_load m z1)))))))))))))).
Admitted.

(*Why axiom*) Lemma store_concat :
  (forall (m:memory),
   (forall (m1:memory),
    (forall (a:Z),
     (forall (b1:bits),
      (forall (b2:bits),
       (forall (sz1:Z),
        (sz1 = (bits_size b1) ->
         (m1 = (rt_store m a b1) ->
          (rt_store m1 (a + sz1) b2) = (rt_store m a (bits_concat b1 b2)))))))))).
Admitted.

(*Why axiom*) Lemma store_disj_commut :
  (forall (m:memory),
   (forall (a1:Z),
    (forall (a2:Z),
     (forall (b1:bits),
      (forall (b2:bits),
       ((rt_disj (rt_zone a1 (bits_size b1)) (rt_zone a2 (bits_size b2))) ->
        (rt_store (rt_store m a1 b1) a2 b2) =
        (rt_store (rt_store m a2 b2) a1 b1))))))).
Admitted.

(*Why axiom*) Lemma not_valid_before_valloc :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma v) -> ~(rt_valid ma (rt_vzone ma' v)))))).
Admitted.

(*Why axiom*) Lemma valid_valloc :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma v) -> (rt_valid ma' (rt_vzone ma' v)))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_valid_zone :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma v) ->
      (forall (z:zone), ((rt_valid ma z) -> (rt_valid ma' z))))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_valid_disj_zone :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma v) ->
      (forall (z:zone),
       ((rt_disj (rt_vzone ma' v) z) -> ((rt_valid ma' z) -> (rt_valid ma z)))))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_invalid_zone :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma v) ->
      (forall (z:zone),
       ((rt_disj (rt_vzone ma' v) z) ->
        (~(rt_valid ma z) -> ~(rt_valid ma' z)))))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_invalid_zone_rev :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_valloc ma v) ->
      (forall (z:zone),
       ((rt_disj (rt_vzone ma' v) z) ->
        (~(rt_valid ma' z) -> ~(rt_valid ma z)))))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_valid_var :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v:Z),
     (forall (ma':memalloc),
      (ma' = (rt_valloc ma v) ->
       (v <> v1 ->
        ((rt_valid ma (rt_vzone ma v1)) -> (rt_valid ma' (rt_vzone ma' v1))))))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_vaddr :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v:Z),
     (forall (ma':memalloc),
      (ma' = (rt_valloc ma v) ->
       (v <> v1 -> (rt_vaddr ma' v1) = (rt_vaddr ma v1))))))).
Admitted.

(*Why axiom*) Lemma valloc_keep_vzone :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v:Z),
     (forall (ma':memalloc),
      (ma' = (rt_valloc ma v) ->
       (v <> v1 -> (rt_vzone ma' v1) = (rt_vzone ma v1))))))).
Admitted.

(*Why axiom*) Lemma vzone_vfree :
  (forall (ma:memalloc),
   (forall (v1:Z),
    (forall (v2:Z),
     (forall (ma':memalloc),
      (ma' = (rt_vfree ma v1) ->
       (v1 <> v2 -> (rt_vzone ma' v2) = (rt_vzone ma v2))))))).
Admitted.

(*Why axiom*) Lemma not_valid_after_vfree :
  (forall (ma:memalloc),
   (forall (v:Z),
    (forall (ma':memalloc),
     (ma' = (rt_vfree ma v) ->
      (forall (z:zone), (z = (rt_vzone ma v) -> ~(rt_valid ma' z))))))).
Admitted.

(*Why axiom*) Lemma havoc_store :
  (forall (ma:memalloc),
   (forall (m1:memory),
    (forall (m2:memory),
     (forall (zs:zones),
      (forall (z:zone),
       (forall (x:bits),
        (forall (a:Z),
         (z = (rt_zone a (bits_size x)) ->
          ((rt_is_havoc ma m1 zs m2) ->
           ((zs_z_incl z zs) -> (rt_is_havoc ma m1 zs (rt_store m2 a x)))))))))))).
Admitted.

(*Why axiom*) Lemma havoc_invalid :
  (forall (ma:memalloc),
   (forall (m1:memory),
    (forall (m2:memory),
     (forall (zs:zones),
      (forall (z:zone),
       (forall (x:bits),
        (forall (a:Z),
         (z = (rt_zone a (bits_size x)) ->
          ((rt_is_havoc ma m1 zs m2) ->
           (~(rt_valid ma z) -> (rt_is_havoc ma m1 zs (rt_store m2 a x)))))))))))).
Admitted.

(*Why axiom*) Lemma same_bits_same_val :
  forall (A1:Set),
  (forall (b1:bits),
   (forall (b2:bits),
    (forall (fmt:(format A1)),
     (b1 = b2 -> (rt_from_bits b1 fmt) = (rt_from_bits b2 fmt))))).
Admitted.

(*Why axiom*) Lemma valid_vglob :
  (forall (v:Z),
   ((rt_global v) ->
    (forall (ma:memalloc),
     (forall (ma':memalloc), (rt_valid ma (rt_vzone ma' v)))))).
Admitted.

