open Preamble

open CostLabel

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 Events

type transrel =
| Mk_transrel

(** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
let rec transrel_rect_Type4 h_mk_transrel = function
| Mk_transrel -> h_mk_transrel __ __ __

(** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
let rec transrel_rect_Type5 h_mk_transrel = function
| Mk_transrel -> h_mk_transrel __ __ __

(** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
let rec transrel_rect_Type3 h_mk_transrel = function
| Mk_transrel -> h_mk_transrel __ __ __

(** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
let rec transrel_rect_Type2 h_mk_transrel = function
| Mk_transrel -> h_mk_transrel __ __ __

(** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
let rec transrel_rect_Type1 h_mk_transrel = function
| Mk_transrel -> h_mk_transrel __ __ __

(** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
let rec transrel_rect_Type0 h_mk_transrel = function
| Mk_transrel -> h_mk_transrel __ __ __

type genv = __

type state = __

(** val transrel_inv_rect_Type4 :
    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let transrel_inv_rect_Type4 hterm h1 =
  let hcut = transrel_rect_Type4 h1 hterm in hcut __

(** val transrel_inv_rect_Type3 :
    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let transrel_inv_rect_Type3 hterm h1 =
  let hcut = transrel_rect_Type3 h1 hterm in hcut __

(** val transrel_inv_rect_Type2 :
    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let transrel_inv_rect_Type2 hterm h1 =
  let hcut = transrel_rect_Type2 h1 hterm in hcut __

(** val transrel_inv_rect_Type1 :
    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let transrel_inv_rect_Type1 hterm h1 =
  let hcut = transrel_rect_Type1 h1 hterm in hcut __

(** val transrel_inv_rect_Type0 :
    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let transrel_inv_rect_Type0 hterm h1 =
  let hcut = transrel_rect_Type0 h1 hterm in hcut __

(** val transrel_jmdiscr : transrel -> transrel -> __ **)
let transrel_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let Mk_transrel = x in Obj.magic (fun _ dH -> dH __ __ __)) y

type program_behavior =
| Terminates of Events.trace * Integers.int
| Diverges of Events.trace
| Reacts of Events.traceinf
| Goes_wrong of Events.trace

(** val program_behavior_rect_Type4 :
    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
    'a1 **)
let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
| Terminates (x_6965, x_6964) -> h_Terminates x_6965 x_6964
| Diverges x_6966 -> h_Diverges x_6966
| Reacts x_6967 -> h_Reacts x_6967
| Goes_wrong x_6968 -> h_Goes_wrong x_6968

(** val program_behavior_rect_Type5 :
    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
    'a1 **)
let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
| Terminates (x_6975, x_6974) -> h_Terminates x_6975 x_6974
| Diverges x_6976 -> h_Diverges x_6976
| Reacts x_6977 -> h_Reacts x_6977
| Goes_wrong x_6978 -> h_Goes_wrong x_6978

(** val program_behavior_rect_Type3 :
    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
    'a1 **)
let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
| Terminates (x_6985, x_6984) -> h_Terminates x_6985 x_6984
| Diverges x_6986 -> h_Diverges x_6986
| Reacts x_6987 -> h_Reacts x_6987
| Goes_wrong x_6988 -> h_Goes_wrong x_6988

(** val program_behavior_rect_Type2 :
    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
    'a1 **)
let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
| Terminates (x_6995, x_6994) -> h_Terminates x_6995 x_6994
| Diverges x_6996 -> h_Diverges x_6996
| Reacts x_6997 -> h_Reacts x_6997
| Goes_wrong x_6998 -> h_Goes_wrong x_6998

(** val program_behavior_rect_Type1 :
    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
    'a1 **)
let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
| Terminates (x_7005, x_7004) -> h_Terminates x_7005 x_7004
| Diverges x_7006 -> h_Diverges x_7006
| Reacts x_7007 -> h_Reacts x_7007
| Goes_wrong x_7008 -> h_Goes_wrong x_7008

(** val program_behavior_rect_Type0 :
    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
    'a1 **)
let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
| Terminates (x_7015, x_7014) -> h_Terminates x_7015 x_7014
| Diverges x_7016 -> h_Diverges x_7016
| Reacts x_7017 -> h_Reacts x_7017
| Goes_wrong x_7018 -> h_Goes_wrong x_7018

(** val program_behavior_inv_rect_Type4 :
    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> 'a1 **)
let program_behavior_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = program_behavior_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val program_behavior_inv_rect_Type3 :
    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> 'a1 **)
let program_behavior_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = program_behavior_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val program_behavior_inv_rect_Type2 :
    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> 'a1 **)
let program_behavior_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = program_behavior_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val program_behavior_inv_rect_Type1 :
    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> 'a1 **)
let program_behavior_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = program_behavior_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val program_behavior_inv_rect_Type0 :
    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
    (Events.trace -> __ -> 'a1) -> 'a1 **)
let program_behavior_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = program_behavior_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val program_behavior_discr :
    program_behavior -> program_behavior -> __ **)
let program_behavior_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val program_behavior_jmdiscr :
    program_behavior -> program_behavior -> __ **)
let program_behavior_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y

type semantics = { trans : transrel; ge : __ }

(** val semantics_rect_Type4 :
    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
let rec semantics_rect_Type4 h_mk_semantics x_7345 =
  let { trans = trans0; ge = ge0 } = x_7345 in
  h_mk_semantics trans0 __ __ ge0

(** val semantics_rect_Type5 :
    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
let rec semantics_rect_Type5 h_mk_semantics x_7347 =
  let { trans = trans0; ge = ge0 } = x_7347 in
  h_mk_semantics trans0 __ __ ge0

(** val semantics_rect_Type3 :
    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
let rec semantics_rect_Type3 h_mk_semantics x_7349 =
  let { trans = trans0; ge = ge0 } = x_7349 in
  h_mk_semantics trans0 __ __ ge0

(** val semantics_rect_Type2 :
    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
let rec semantics_rect_Type2 h_mk_semantics x_7351 =
  let { trans = trans0; ge = ge0 } = x_7351 in
  h_mk_semantics trans0 __ __ ge0

(** val semantics_rect_Type1 :
    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
let rec semantics_rect_Type1 h_mk_semantics x_7353 =
  let { trans = trans0; ge = ge0 } = x_7353 in
  h_mk_semantics trans0 __ __ ge0

(** val semantics_rect_Type0 :
    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
let rec semantics_rect_Type0 h_mk_semantics x_7355 =
  let { trans = trans0; ge = ge0 } = x_7355 in
  h_mk_semantics trans0 __ __ ge0

(** val trans : semantics -> transrel **)
let rec trans xxx =
  xxx.trans

(** val ge : semantics -> __ **)
let rec ge xxx =
  xxx.ge

(** val semantics_inv_rect_Type4 :
    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let semantics_inv_rect_Type4 hterm h1 =
  let hcut = semantics_rect_Type4 h1 hterm in hcut __

(** val semantics_inv_rect_Type3 :
    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let semantics_inv_rect_Type3 hterm h1 =
  let hcut = semantics_rect_Type3 h1 hterm in hcut __

(** val semantics_inv_rect_Type2 :
    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let semantics_inv_rect_Type2 hterm h1 =
  let hcut = semantics_rect_Type2 h1 hterm in hcut __

(** val semantics_inv_rect_Type1 :
    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let semantics_inv_rect_Type1 hterm h1 =
  let hcut = semantics_rect_Type1 h1 hterm in hcut __

(** val semantics_inv_rect_Type0 :
    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let semantics_inv_rect_Type0 hterm h1 =
  let hcut = semantics_rect_Type0 h1 hterm in hcut __

(** val semantics_jmdiscr : semantics -> semantics -> __ **)
let semantics_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { trans = a0; ge = a3 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

type related_semantics = { sem1 : semantics; sem2 : semantics }

(** val related_semantics_rect_Type4 :
    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    'a1 **)
let rec related_semantics_rect_Type4 h_mk_related_semantics x_7374 =
  let { sem1 = sem3; sem2 = sem4 } = x_7374 in
  h_mk_related_semantics sem3 sem4 __ __ __

(** val related_semantics_rect_Type5 :
    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    'a1 **)
let rec related_semantics_rect_Type5 h_mk_related_semantics x_7376 =
  let { sem1 = sem3; sem2 = sem4 } = x_7376 in
  h_mk_related_semantics sem3 sem4 __ __ __

(** val related_semantics_rect_Type3 :
    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    'a1 **)
let rec related_semantics_rect_Type3 h_mk_related_semantics x_7378 =
  let { sem1 = sem3; sem2 = sem4 } = x_7378 in
  h_mk_related_semantics sem3 sem4 __ __ __

(** val related_semantics_rect_Type2 :
    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    'a1 **)
let rec related_semantics_rect_Type2 h_mk_related_semantics x_7380 =
  let { sem1 = sem3; sem2 = sem4 } = x_7380 in
  h_mk_related_semantics sem3 sem4 __ __ __

(** val related_semantics_rect_Type1 :
    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    'a1 **)
let rec related_semantics_rect_Type1 h_mk_related_semantics x_7382 =
  let { sem1 = sem3; sem2 = sem4 } = x_7382 in
  h_mk_related_semantics sem3 sem4 __ __ __

(** val related_semantics_rect_Type0 :
    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    'a1 **)
let rec related_semantics_rect_Type0 h_mk_related_semantics x_7384 =
  let { sem1 = sem3; sem2 = sem4 } = x_7384 in
  h_mk_related_semantics sem3 sem4 __ __ __

(** val sem1 : related_semantics -> semantics **)
let rec sem1 xxx =
  xxx.sem1

(** val sem2 : related_semantics -> semantics **)
let rec sem2 xxx =
  xxx.sem2

(** val related_semantics_inv_rect_Type4 :
    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let related_semantics_inv_rect_Type4 hterm h1 =
  let hcut = related_semantics_rect_Type4 h1 hterm in hcut __

(** val related_semantics_inv_rect_Type3 :
    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let related_semantics_inv_rect_Type3 hterm h1 =
  let hcut = related_semantics_rect_Type3 h1 hterm in hcut __

(** val related_semantics_inv_rect_Type2 :
    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let related_semantics_inv_rect_Type2 hterm h1 =
  let hcut = related_semantics_rect_Type2 h1 hterm in hcut __

(** val related_semantics_inv_rect_Type1 :
    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let related_semantics_inv_rect_Type1 hterm h1 =
  let hcut = related_semantics_rect_Type1 h1 hterm in hcut __

(** val related_semantics_inv_rect_Type0 :
    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let related_semantics_inv_rect_Type0 hterm h1 =
  let hcut = related_semantics_rect_Type0 h1 hterm in hcut __

(** val related_semantics_jmdiscr :
    related_semantics -> related_semantics -> __ **)
let related_semantics_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { sem1 = a0; sem2 = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y

type order_sim =
  related_semantics
  (* singleton inductive, whose constructor was mk_order_sim *)

(** val order_sim_rect_Type4 :
    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
let rec order_sim_rect_Type4 h_mk_order_sim x_7405 =
  let sem = x_7405 in h_mk_order_sim sem __ __

(** val order_sim_rect_Type5 :
    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
let rec order_sim_rect_Type5 h_mk_order_sim x_7407 =
  let sem = x_7407 in h_mk_order_sim sem __ __

(** val order_sim_rect_Type3 :
    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
let rec order_sim_rect_Type3 h_mk_order_sim x_7409 =
  let sem = x_7409 in h_mk_order_sim sem __ __

(** val order_sim_rect_Type2 :
    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
let rec order_sim_rect_Type2 h_mk_order_sim x_7411 =
  let sem = x_7411 in h_mk_order_sim sem __ __

(** val order_sim_rect_Type1 :
    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
let rec order_sim_rect_Type1 h_mk_order_sim x_7413 =
  let sem = x_7413 in h_mk_order_sim sem __ __

(** val order_sim_rect_Type0 :
    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
let rec order_sim_rect_Type0 h_mk_order_sim x_7415 =
  let sem = x_7415 in h_mk_order_sim sem __ __

(** val sem : order_sim -> related_semantics **)
let rec sem xxx =
  let yyy = xxx in yyy

(** val order_sim_inv_rect_Type4 :
    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let order_sim_inv_rect_Type4 hterm h1 =
  let hcut = order_sim_rect_Type4 h1 hterm in hcut __

(** val order_sim_inv_rect_Type3 :
    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let order_sim_inv_rect_Type3 hterm h1 =
  let hcut = order_sim_rect_Type3 h1 hterm in hcut __

(** val order_sim_inv_rect_Type2 :
    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let order_sim_inv_rect_Type2 hterm h1 =
  let hcut = order_sim_rect_Type2 h1 hterm in hcut __

(** val order_sim_inv_rect_Type1 :
    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let order_sim_inv_rect_Type1 hterm h1 =
  let hcut = order_sim_rect_Type1 h1 hterm in hcut __

(** val order_sim_inv_rect_Type0 :
    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let order_sim_inv_rect_Type0 hterm h1 =
  let hcut = order_sim_rect_Type0 h1 hterm in hcut __

(** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
let order_sim_jmdiscr x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y