open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open Hide

type cpointer = Pointers.pointer Types.sig0

type xpointer = Pointers.pointer Types.sig0

type program_counter = { pc_block : Pointers.block Types.sig0;
                         pc_offset : Positive.pos }

val program_counter_rect_Type4 :
  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  'a1

val program_counter_rect_Type5 :
  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  'a1

val program_counter_rect_Type3 :
  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  'a1

val program_counter_rect_Type2 :
  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  'a1

val program_counter_rect_Type1 :
  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  'a1

val program_counter_rect_Type0 :
  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  'a1

val pc_block : program_counter -> Pointers.block Types.sig0

val pc_offset : program_counter -> Positive.pos

val program_counter_inv_rect_Type4 :
  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
  -> 'a1

val program_counter_inv_rect_Type3 :
  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
  -> 'a1

val program_counter_inv_rect_Type2 :
  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
  -> 'a1

val program_counter_inv_rect_Type1 :
  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
  -> 'a1

val program_counter_inv_rect_Type0 :
  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
  -> 'a1

val program_counter_discr : program_counter -> program_counter -> __

val program_counter_jmdiscr : program_counter -> program_counter -> __

val eq_program_counter : program_counter -> program_counter -> Bool.bool

val bitvector_from_pos : Nat.nat -> Positive.pos -> BitVector.bitVector

val pos_from_bitvector : Nat.nat -> BitVector.bitVector -> Positive.pos

val cpointer_of_pc : program_counter -> cpointer Types.option

type part =
  Nat.nat
  (* singleton inductive, whose constructor was mk_part *)

val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1

val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1

val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1

val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1

val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1

val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1

val part_no : part -> Nat.nat

val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1

val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1

val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1

val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1

val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1

val part_discr : part -> part -> __

val part_jmdiscr : part -> part -> __

val dpi1__o__part_no__o__inject :
  (part, 'a1) Types.dPair -> Nat.nat Types.sig0

val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z

val eject__o__part_no__o__inject : part Types.sig0 -> Nat.nat Types.sig0

val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z

val part_no__o__Z_of_nat : part -> Z.z

val part_no__o__inject : part -> Nat.nat Types.sig0

val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat

val eject__o__part_no : part Types.sig0 -> Nat.nat

val part_from_sig : Nat.nat Types.sig0 -> part

val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
  (part, 'a1) Types.dPair -> part Types.sig0

val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
  (part, 'a1) Types.dPair -> Nat.nat Types.sig0

val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
  (part, 'a1) Types.dPair -> Z.z

val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
  (part, 'a1) Types.dPair -> Nat.nat

val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
  part Types.sig0 -> part Types.sig0

val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
  part Types.sig0 -> Nat.nat Types.sig0

val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
  part Types.sig0 -> Z.z

val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
  part Types.sig0 -> Nat.nat

val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0

val inject__o__sig_to_part__o__part_no__o__inject :
  Nat.nat -> Nat.nat Types.sig0

val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z

val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat

val part_no__o__inject__o__sig_to_part__o__inject : part -> part Types.sig0

val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
  part -> Nat.nat Types.sig0

val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat : part -> Z.z

val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat

val dpi1__o__sig_to_part__o__inject :
  (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0

val dpi1__o__sig_to_part__o__part_no__o__inject :
  (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0

val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
  (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z

val dpi1__o__sig_to_part__o__part_no :
  (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat

val eject__o__sig_to_part__o__inject :
  Nat.nat Types.sig0 Types.sig0 -> part Types.sig0

val eject__o__sig_to_part__o__part_no__o__inject :
  Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0

val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
  Nat.nat Types.sig0 Types.sig0 -> Z.z

val eject__o__sig_to_part__o__part_no :
  Nat.nat Types.sig0 Types.sig0 -> Nat.nat

val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat

val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z

val sig_to_part__o__part_no__o__inject :
  Nat.nat Types.sig0 -> Nat.nat Types.sig0

val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0

val dpi1__o__part_no__o__inject__o__sig_to_part :
  (part, 'a1) Types.dPair -> part

val eject__o__part_no__o__inject__o__sig_to_part : part Types.sig0 -> part

val inject__o__sig_to_part : Nat.nat -> part

val part_no__o__inject__o__sig_to_part : part -> part

val dpi1__o__sig_to_part : (Nat.nat Types.sig0, 'a1) Types.dPair -> part

val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part

type beval =
| BVundef
| BVnonzero
| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
   * part
| BVByte of BitVector.byte
| BVnull of part
| BVptr of Pointers.pointer * part
| BVpc of program_counter * part

val beval_rect_Type4 :
  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
  beval -> 'a1

val beval_rect_Type5 :
  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
  beval -> 'a1

val beval_rect_Type3 :
  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
  beval -> 'a1

val beval_rect_Type2 :
  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
  beval -> 'a1

val beval_rect_Type1 :
  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
  beval -> 'a1

val beval_rect_Type0 :
  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
  beval -> 'a1

val beval_inv_rect_Type4 :
  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1

val beval_inv_rect_Type3 :
  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1

val beval_inv_rect_Type2 :
  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1

val beval_inv_rect_Type1 :
  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1

val beval_inv_rect_Type0 :
  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1

val beval_discr : beval -> beval -> __

val beval_jmdiscr : beval -> beval -> __

val eq_bv_suffix :
  Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
  -> Bool.bool

val pointer_of_bevals : beval List.list -> Pointers.pointer Errors.res

val pc_of_bevals : beval List.list -> program_counter Errors.res

val bevals_of_pointer : Pointers.pointer -> beval List.list

val bevals_of_pc : program_counter -> beval List.list

val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod

val beval_pair_of_pointer : Pointers.pointer -> (beval, beval) Types.prod

val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod

val bool_of_beval : beval -> Bool.bool Errors.res

val byte_of_val :
  ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res

val word_of_list_beval : beval List.list -> Integers.int Errors.res

type add_or_sub =
| Do_add
| Do_sub

val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1

val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1

val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1

val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1

val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1

val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1

val add_or_sub_inv_rect_Type4 :
  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val add_or_sub_inv_rect_Type3 :
  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val add_or_sub_inv_rect_Type2 :
  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val add_or_sub_inv_rect_Type1 :
  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val add_or_sub_inv_rect_Type0 :
  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val add_or_sub_discr : add_or_sub -> add_or_sub -> __

val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __

val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool

type bebit =
| BBbit of Bool.bool
| BBundef
| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector

val bebit_rect_Type4 :
  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
  BitVector.bitVector -> 'a1) -> bebit -> 'a1

val bebit_rect_Type5 :
  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
  BitVector.bitVector -> 'a1) -> bebit -> 'a1

val bebit_rect_Type3 :
  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
  BitVector.bitVector -> 'a1) -> bebit -> 'a1

val bebit_rect_Type2 :
  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
  BitVector.bitVector -> 'a1) -> bebit -> 'a1

val bebit_rect_Type1 :
  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
  BitVector.bitVector -> 'a1) -> bebit -> 'a1

val bebit_rect_Type0 :
  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
  BitVector.bitVector -> 'a1) -> bebit -> 'a1

val bebit_inv_rect_Type4 :
  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1

val bebit_inv_rect_Type3 :
  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1

val bebit_inv_rect_Type2 :
  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1

val bebit_inv_rect_Type1 :
  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1

val bebit_inv_rect_Type0 :
  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1

val bebit_discr : bebit -> bebit -> __

val bebit_jmdiscr : bebit -> bebit -> __

val bit_of_val :
  ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res