open Preamble

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 Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

type block =
  Z.z
  (* singleton inductive, whose constructor was mk_block *)

val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1

val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1

val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1

val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1

val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1

val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1

val block_id : block -> Z.z

val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1

val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1

val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1

val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1

val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1

val block_discr : block -> block -> __

val block_jmdiscr : block -> block -> __

val block_region : block -> AST.region

val dummy_block_code : block

val eq_block : block -> block -> Bool.bool

val block_eq : Deqsets.deqSet

val offset_size : Nat.nat

type offset =
  BitVector.bitVector
  (* singleton inductive, whose constructor was mk_offset *)

val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1

val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1

val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1

val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1

val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1

val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1

val offv : offset -> BitVector.bitVector

val offset_inv_rect_Type4 :
  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1

val offset_inv_rect_Type3 :
  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1

val offset_inv_rect_Type2 :
  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1

val offset_inv_rect_Type1 :
  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1

val offset_inv_rect_Type0 :
  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1

val offset_discr : offset -> offset -> __

val offset_jmdiscr : offset -> offset -> __

val eq_offset : offset -> offset -> Bool.bool

val offset_of_Z : Z.z -> offset

val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset

val shift_offset_n :
  Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
  offset

val neg_shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset

val neg_shift_offset_n :
  Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
  offset

val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector

val zero_offset : offset

val lt_offset : offset -> offset -> Bool.bool

type pointer = { pblock : block; poff : offset }

val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1

val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1

val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1

val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1

val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1

val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1

val pblock : pointer -> block

val poff : pointer -> offset

val pointer_inv_rect_Type4 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1

val pointer_inv_rect_Type3 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1

val pointer_inv_rect_Type2 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1

val pointer_inv_rect_Type1 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1

val pointer_inv_rect_Type0 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1

val pointer_discr : pointer -> pointer -> __

val pointer_jmdiscr : pointer -> pointer -> __

val ptype : pointer -> AST.region

val shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer

val shift_pointer_n :
  Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
  pointer

val neg_shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer

val neg_shift_pointer_n :
  Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
  pointer

val eq_pointer : pointer -> pointer -> Bool.bool