open Preamble

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Coqlib

open Values

open CostLabel

type eventval =
| EVint of AST.intsize * AST.bvint

(** val eventval_rect_Type4 :
    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
let rec eventval_rect_Type4 h_EVint = function
| EVint (sz, x_5537) -> h_EVint sz x_5537

(** val eventval_rect_Type5 :
    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
let rec eventval_rect_Type5 h_EVint = function
| EVint (sz, x_5540) -> h_EVint sz x_5540

(** val eventval_rect_Type3 :
    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
let rec eventval_rect_Type3 h_EVint = function
| EVint (sz, x_5543) -> h_EVint sz x_5543

(** val eventval_rect_Type2 :
    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
let rec eventval_rect_Type2 h_EVint = function
| EVint (sz, x_5546) -> h_EVint sz x_5546

(** val eventval_rect_Type1 :
    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
let rec eventval_rect_Type1 h_EVint = function
| EVint (sz, x_5549) -> h_EVint sz x_5549

(** val eventval_rect_Type0 :
    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
let rec eventval_rect_Type0 h_EVint = function
| EVint (sz, x_5552) -> h_EVint sz x_5552

(** val eventval_inv_rect_Type4 :
    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
let eventval_inv_rect_Type4 hterm h1 =
  let hcut = eventval_rect_Type4 h1 hterm in hcut __

(** val eventval_inv_rect_Type3 :
    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
let eventval_inv_rect_Type3 hterm h1 =
  let hcut = eventval_rect_Type3 h1 hterm in hcut __

(** val eventval_inv_rect_Type2 :
    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
let eventval_inv_rect_Type2 hterm h1 =
  let hcut = eventval_rect_Type2 h1 hterm in hcut __

(** val eventval_inv_rect_Type1 :
    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
let eventval_inv_rect_Type1 hterm h1 =
  let hcut = eventval_rect_Type1 h1 hterm in hcut __

(** val eventval_inv_rect_Type0 :
    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
let eventval_inv_rect_Type0 hterm h1 =
  let hcut = eventval_rect_Type0 h1 hterm in hcut __

(** val eventval_discr : eventval -> eventval -> __ **)
let eventval_discr x y =
  Logic.eq_rect_Type2 x
    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val eventval_jmdiscr : eventval -> eventval -> __ **)
let eventval_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y

type event =
| EVcost of CostLabel.costlabel
| EVextcall of AST.ident * eventval List.list * eventval

(** val event_rect_Type4 :
    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
    eventval -> 'a1) -> event -> 'a1 **)
let rec event_rect_Type4 h_EVcost h_EVextcall = function
| EVcost x_5577 -> h_EVcost x_5577
| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res

(** val event_rect_Type5 :
    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
    eventval -> 'a1) -> event -> 'a1 **)
let rec event_rect_Type5 h_EVcost h_EVextcall = function
| EVcost x_5581 -> h_EVcost x_5581
| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res

(** val event_rect_Type3 :
    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
    eventval -> 'a1) -> event -> 'a1 **)
let rec event_rect_Type3 h_EVcost h_EVextcall = function
| EVcost x_5585 -> h_EVcost x_5585
| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res

(** val event_rect_Type2 :
    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
    eventval -> 'a1) -> event -> 'a1 **)
let rec event_rect_Type2 h_EVcost h_EVextcall = function
| EVcost x_5589 -> h_EVcost x_5589
| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res

(** val event_rect_Type1 :
    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
    eventval -> 'a1) -> event -> 'a1 **)
let rec event_rect_Type1 h_EVcost h_EVextcall = function
| EVcost x_5593 -> h_EVcost x_5593
| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res

(** val event_rect_Type0 :
    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
    eventval -> 'a1) -> event -> 'a1 **)
let rec event_rect_Type0 h_EVcost h_EVextcall = function
| EVcost x_5597 -> h_EVcost x_5597
| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res

(** val event_inv_rect_Type4 :
    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
let event_inv_rect_Type4 hterm h1 h2 =
  let hcut = event_rect_Type4 h1 h2 hterm in hcut __

(** val event_inv_rect_Type3 :
    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
let event_inv_rect_Type3 hterm h1 h2 =
  let hcut = event_rect_Type3 h1 h2 hterm in hcut __

(** val event_inv_rect_Type2 :
    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
let event_inv_rect_Type2 hterm h1 h2 =
  let hcut = event_rect_Type2 h1 h2 hterm in hcut __

(** val event_inv_rect_Type1 :
    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
let event_inv_rect_Type1 hterm h1 h2 =
  let hcut = event_rect_Type1 h1 h2 hterm in hcut __

(** val event_inv_rect_Type0 :
    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
let event_inv_rect_Type0 hterm h1 h2 =
  let hcut = event_rect_Type0 h1 h2 hterm in hcut __

(** val event_discr : event -> event -> __ **)
let event_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val event_jmdiscr : event -> event -> __ **)
let event_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

type trace = event List.list

(** val e0 : trace **)
let e0 =
  List.Nil

(** val echarge : CostLabel.costlabel -> trace **)
let echarge label =
  List.Cons ((EVcost label), List.Nil)

(** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
let eextcall name args res =
  List.Cons ((EVextcall (name, args, res)), List.Nil)

(** val eapp : trace -> trace -> trace **)
let eapp t1 t2 =
  List.append t1 t2

type traceinf = __traceinf Lazy.t
and __traceinf =
| Econsinf of event * traceinf

(** val traceinf_inv_rect_Type4 :
    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
let traceinf_inv_rect_Type4 hterm h1 =
  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __

(** val traceinf_inv_rect_Type3 :
    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
let traceinf_inv_rect_Type3 hterm h1 =
  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __

(** val traceinf_inv_rect_Type2 :
    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
let traceinf_inv_rect_Type2 hterm h1 =
  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __

(** val traceinf_inv_rect_Type1 :
    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
let traceinf_inv_rect_Type1 hterm h1 =
  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __

(** val traceinf_inv_rect_Type0 :
    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
let traceinf_inv_rect_Type0 hterm h1 =
  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __

(** val traceinf_discr : traceinf -> traceinf -> __ **)
let traceinf_discr x y =
  Logic.eq_rect_Type2 x
    (let Econsinf (a0, a1) = Lazy.force x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val traceinf_jmdiscr : traceinf -> traceinf -> __ **)
let traceinf_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let Econsinf (a0, a1) = Lazy.force x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val eappinf : trace -> traceinf -> traceinf **)
let rec eappinf t t0 =
  match t with
  | List.Nil -> t0
  | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0)))

(** val remove_costs : trace -> trace **)
let remove_costs =
  List.filter (fun e ->
    match e with
    | EVcost x -> Bool.False
    | EVextcall (x, x0, x1) -> Bool.True)

type traceinf' = __traceinf' Lazy.t
and __traceinf' =
| Econsinf' of trace * traceinf'

(** val traceinf'_inv_rect_Type4 :
    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
let traceinf'_inv_rect_Type4 hterm h1 =
  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
  hcut __

(** val traceinf'_inv_rect_Type3 :
    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
let traceinf'_inv_rect_Type3 hterm h1 =
  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
  hcut __

(** val traceinf'_inv_rect_Type2 :
    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
let traceinf'_inv_rect_Type2 hterm h1 =
  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
  hcut __

(** val traceinf'_inv_rect_Type1 :
    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
let traceinf'_inv_rect_Type1 hterm h1 =
  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
  hcut __

(** val traceinf'_inv_rect_Type0 :
    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
let traceinf'_inv_rect_Type0 hterm h1 =
  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
  hcut __

(** val traceinf'_discr : traceinf' -> traceinf' -> __ **)
let traceinf'_discr x y =
  Logic.eq_rect_Type2 x
    (let Econsinf' (a0, a1) = Lazy.force x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **)
let traceinf'_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let Econsinf' (a0, a1) = Lazy.force x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val split_traceinf' :
    trace -> traceinf' -> (event, traceinf') Types.prod **)
let split_traceinf' t t0 =
  (match t with
   | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
   | List.Cons (e, t') ->
     (fun _ ->
       (match t' with
        | List.Nil -> (fun _ -> { Types.fst = e; Types.snd = t0 })
        | List.Cons (e', t'') ->
          (fun _ -> { Types.fst = e; Types.snd = (lazy (Econsinf' (t',
            t0))) })) __)) __

(** val traceinf_of_traceinf' : traceinf' -> traceinf **)
let rec traceinf_of_traceinf' t' =
  let Econsinf' (t, t'') = Lazy.force t' in
  let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in
  lazy (Econsinf (e, (traceinf_of_traceinf' tl)))