open Preamble

open Hide

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 ByteValues

val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod

type opAccs =
| Mul
| DivuModu

val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1

val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1

val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1

val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1

val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1

val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1

val opAccs_inv_rect_Type4 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val opAccs_inv_rect_Type3 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val opAccs_inv_rect_Type2 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val opAccs_inv_rect_Type1 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val opAccs_inv_rect_Type0 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val opAccs_discr : opAccs -> opAccs -> __

val opAccs_jmdiscr : opAccs -> opAccs -> __

type op1 =
| Cmpl
| Inc
| Rl

val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1

val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1

val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1

val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1

val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1

val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1

val op1_inv_rect_Type4 :
  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val op1_inv_rect_Type3 :
  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val op1_inv_rect_Type2 :
  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val op1_inv_rect_Type1 :
  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val op1_inv_rect_Type0 :
  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val op1_discr : op1 -> op1 -> __

val op1_jmdiscr : op1 -> op1 -> __

type op2 =
| Add
| Addc
| Sub
| And
| Or
| Xor

val op2_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1

val op2_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1

val op2_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1

val op2_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1

val op2_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1

val op2_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1

val op2_inv_rect_Type4 :
  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> 'a1

val op2_inv_rect_Type3 :
  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> 'a1

val op2_inv_rect_Type2 :
  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> 'a1

val op2_inv_rect_Type1 :
  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> 'a1

val op2_inv_rect_Type0 :
  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> 'a1

val op2_discr : op2 -> op2 -> __

val op2_jmdiscr : op2 -> op2 -> __

type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
                       (BitVector.byte, BitVector.byte) Types.prod);
              op0 : (op1 -> BitVector.byte -> BitVector.byte);
              op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
                    -> (BitVector.byte, BitVector.bit) Types.prod) }

val eval_rect_Type4 :
  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1

val eval_rect_Type5 :
  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1

val eval_rect_Type3 :
  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1

val eval_rect_Type2 :
  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1

val eval_rect_Type1 :
  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1

val eval_rect_Type0 :
  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1

val opaccs :
  eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod

val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte

val op3 :
  eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod

val eval_inv_rect_Type4 :
  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1

val eval_inv_rect_Type3 :
  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1

val eval_inv_rect_Type2 :
  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1

val eval_inv_rect_Type1 :
  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1

val eval_inv_rect_Type0 :
  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1

val eval_discr : eval -> eval -> __

val eval_jmdiscr : eval -> eval -> __

val opaccs_implementation :
  opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
  BitVector.byte) Types.prod

val op1_implementation : op1 -> BitVector.byte -> BitVector.byte

val op2_implementation :
  BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
  (BitVector.byte, BitVector.bit) Types.prod

val eval0 : eval

val be_opaccs :
  opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
  ByteValues.beval) Types.prod Errors.res

val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res

val op2_bytes :
  op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
  BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
  BitVector.bit) Types.prod

val op_of_add_or_sub : ByteValues.add_or_sub -> op2

val be_add_sub_byte :
  ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
  BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
  Errors.res

val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte

val eq_opt :
  ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
  Bool.bool

val be_op2 :
  ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
  (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res