open Preamble

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 Extralib

open Proper

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open IOMonad

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open CostLabel

open PositiveMap

open Deqsets

open Lists

open Identifiers

open AST

open Division

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
                                                 Types.option);
                                      step : (__ -> __ -> ('outty, 'inty,
                                             (Events.trace, __) Types.prod)
                                             IOMonad.iO) }

val trans_system_rect_Type4 :
  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  trans_system -> 'a3

val trans_system_rect_Type5 :
  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  trans_system -> 'a3

val trans_system_rect_Type3 :
  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  trans_system -> 'a3

val trans_system_rect_Type2 :
  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  trans_system -> 'a3

val trans_system_rect_Type1 :
  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  trans_system -> 'a3

val trans_system_rect_Type0 :
  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  trans_system -> 'a3

type ('outty, 'inty) global 

type ('outty, 'inty) state 

val is_final :
  ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option

val step :
  ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
  Types.prod) IOMonad.iO

val trans_system_inv_rect_Type4 :
  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
  IOMonad.iO) -> __ -> 'a3) -> 'a3

val trans_system_inv_rect_Type3 :
  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
  IOMonad.iO) -> __ -> 'a3) -> 'a3

val trans_system_inv_rect_Type2 :
  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
  IOMonad.iO) -> __ -> 'a3) -> 'a3

val trans_system_inv_rect_Type1 :
  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
  IOMonad.iO) -> __ -> 'a3) -> 'a3

val trans_system_inv_rect_Type0 :
  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
  IOMonad.iO) -> __ -> 'a3) -> 'a3

val repeat :
  Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace,
  __) Types.prod) IOMonad.iO

val trace_map :
  ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
  (Events.trace, 'a2 List.list) Types.prod Errors.res

type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g : 
                           __; avs_inv : (__ -> Bool.bool) }

val await_value_stuff_rect_Type4 :
  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
  await_value_stuff -> 'a1

val await_value_stuff_rect_Type5 :
  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
  await_value_stuff -> 'a1

val await_value_stuff_rect_Type3 :
  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
  await_value_stuff -> 'a1

val await_value_stuff_rect_Type2 :
  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
  await_value_stuff -> 'a1

val await_value_stuff_rect_Type1 :
  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
  await_value_stuff -> 'a1

val await_value_stuff_rect_Type0 :
  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
  await_value_stuff -> 'a1

type avs_O 

type avs_I 

val avs_exec : await_value_stuff -> (__, __) trans_system

val avs_g : await_value_stuff -> __

val avs_inv : await_value_stuff -> __ -> Bool.bool

val await_value_stuff_inv_rect_Type4 :
  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
  Bool.bool) -> __ -> 'a1) -> 'a1

val await_value_stuff_inv_rect_Type3 :
  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
  Bool.bool) -> __ -> 'a1) -> 'a1

val await_value_stuff_inv_rect_Type2 :
  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
  Bool.bool) -> __ -> 'a1) -> 'a1

val await_value_stuff_inv_rect_Type1 :
  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
  Bool.bool) -> __ -> 'a1) -> 'a1

val await_value_stuff_inv_rect_Type0 :
  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
  Bool.bool) -> __ -> 'a1) -> 'a1

type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
and ('state, 'output, 'input) __execution =
| E_stop of Events.trace * Integers.int * 'state
| E_step of Events.trace * 'state * ('state, 'output, 'input) execution
| E_wrong of Errors.errmsg
| E_interact of 'output * ('input -> ('state, 'output, 'input) execution)

val execution_inv_rect_Type4 :
  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
  -> __ -> 'a4) -> 'a4

val execution_inv_rect_Type3 :
  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
  -> __ -> 'a4) -> 'a4

val execution_inv_rect_Type2 :
  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
  -> __ -> 'a4) -> 'a4

val execution_inv_rect_Type1 :
  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
  -> __ -> 'a4) -> 'a4

val execution_inv_rect_Type0 :
  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
  -> __ -> 'a4) -> 'a4

val execution_discr :
  ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __

val execution_jmdiscr :
  ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __

val exec_inf_aux :
  ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
  IOMonad.iO -> (__, 'a1, 'a2) execution

type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
                                  make_global : (__ -> __);
                                  make_initial_state : (__ -> __ Errors.res) }

val fullexec_rect_Type4 :
  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
  'a3) -> ('a1, 'a2) fullexec -> 'a3

val fullexec_rect_Type5 :
  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
  'a3) -> ('a1, 'a2) fullexec -> 'a3

val fullexec_rect_Type3 :
  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
  'a3) -> ('a1, 'a2) fullexec -> 'a3

val fullexec_rect_Type2 :
  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
  'a3) -> ('a1, 'a2) fullexec -> 'a3

val fullexec_rect_Type1 :
  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
  'a3) -> ('a1, 'a2) fullexec -> 'a3

val fullexec_rect_Type0 :
  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
  'a3) -> ('a1, 'a2) fullexec -> 'a3

type ('outty, 'inty) program 

val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system

val make_global : ('a1, 'a2) fullexec -> __ -> __

val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res

val fullexec_inv_rect_Type4 :
  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
  -> __ Errors.res) -> __ -> 'a3) -> 'a3

val fullexec_inv_rect_Type3 :
  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
  -> __ Errors.res) -> __ -> 'a3) -> 'a3

val fullexec_inv_rect_Type2 :
  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
  -> __ Errors.res) -> __ -> 'a3) -> 'a3

val fullexec_inv_rect_Type1 :
  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
  -> __ Errors.res) -> __ -> 'a3) -> 'a3

val fullexec_inv_rect_Type0 :
  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
  -> __ Errors.res) -> __ -> 'a3) -> 'a3

val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution

type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list

val split_trace :
  ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
  'a2) execution) Types.prod Types.option

val exec_steps :
  Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
  Types.prod List.list, __) Types.prod Errors.res

val gather_trace : ('a1, Events.trace) Types.prod List.list -> Events.trace

val switch_trace_aux :
  Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
  (Events.trace, 'a1) Types.prod List.list

val switch_trace :
  ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
  Types.prod List.list