open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Identifiers

open CostLabel

open LabelledObjects

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open String

open BitVectorTrie

type identifier = PreIdentifiers.identifier

val toASM_ident :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier

type addressing_mode =
| DIRECT of BitVector.byte
| INDIRECT of BitVector.bit
| EXT_INDIRECT of BitVector.bit
| REGISTER of BitVector.bitVector
| ACC_A
| ACC_B
| DPTR
| DATA of BitVector.byte
| DATA16 of BitVector.word
| ACC_DPTR
| ACC_PC
| EXT_INDIRECT_DPTR
| INDIRECT_DPTR
| CARRY
| BIT_ADDR of BitVector.byte
| N_BIT_ADDR of BitVector.byte
| RELATIVE of BitVector.byte
| ADDR11 of BitVector.word11
| ADDR16 of BitVector.word

val addressing_mode_rect_Type4 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
  addressing_mode -> 'a1

val addressing_mode_rect_Type5 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
  addressing_mode -> 'a1

val addressing_mode_rect_Type3 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
  addressing_mode -> 'a1

val addressing_mode_rect_Type2 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
  addressing_mode -> 'a1

val addressing_mode_rect_Type1 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
  addressing_mode -> 'a1

val addressing_mode_rect_Type0 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
  addressing_mode -> 'a1

val addressing_mode_inv_rect_Type4 :
  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1

val addressing_mode_inv_rect_Type3 :
  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1

val addressing_mode_inv_rect_Type2 :
  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1

val addressing_mode_inv_rect_Type1 :
  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1

val addressing_mode_inv_rect_Type0 :
  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1

val addressing_mode_discr : addressing_mode -> addressing_mode -> __

val addressing_mode_jmdiscr : addressing_mode -> addressing_mode -> __

val eq_addressing_mode : addressing_mode -> addressing_mode -> Bool.bool

type addressing_mode_tag =
| Direct
| Indirect
| Ext_indirect
| Registr
| Acc_a
| Acc_b
| Dptr
| Data
| Data16
| Acc_dptr
| Acc_pc
| Ext_indirect_dptr
| Indirect_dptr
| Carry
| Bit_addr
| N_bit_addr
| Relative
| Addr11
| Addr16

val addressing_mode_tag_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  addressing_mode_tag -> 'a1

val addressing_mode_tag_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  addressing_mode_tag -> 'a1

val addressing_mode_tag_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  addressing_mode_tag -> 'a1

val addressing_mode_tag_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  addressing_mode_tag -> 'a1

val addressing_mode_tag_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  addressing_mode_tag -> 'a1

val addressing_mode_tag_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  addressing_mode_tag -> 'a1

val addressing_mode_tag_inv_rect_Type4 :
  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> 'a1

val addressing_mode_tag_inv_rect_Type3 :
  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> 'a1

val addressing_mode_tag_inv_rect_Type2 :
  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> 'a1

val addressing_mode_tag_inv_rect_Type1 :
  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> 'a1

val addressing_mode_tag_inv_rect_Type0 :
  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> 'a1

val addressing_mode_tag_discr :
  addressing_mode_tag -> addressing_mode_tag -> __

val addressing_mode_tag_jmdiscr :
  addressing_mode_tag -> addressing_mode_tag -> __

val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool

val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool

val is_in :
  Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
  Bool.bool

type subaddressing_mode =
  addressing_mode
  (* singleton inductive, whose constructor was mk_subaddressing_mode *)

val subaddressing_mode_rect_Type4 :
  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
  'a1) -> subaddressing_mode -> 'a1

val subaddressing_mode_rect_Type5 :
  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
  'a1) -> subaddressing_mode -> 'a1

val subaddressing_mode_rect_Type3 :
  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
  'a1) -> subaddressing_mode -> 'a1

val subaddressing_mode_rect_Type2 :
  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
  'a1) -> subaddressing_mode -> 'a1

val subaddressing_mode_rect_Type1 :
  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
  'a1) -> subaddressing_mode -> 'a1

val subaddressing_mode_rect_Type0 :
  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
  'a1) -> subaddressing_mode -> 'a1

val subaddressing_modeel :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  addressing_mode

val subaddressing_mode_inv_rect_Type4 :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  (addressing_mode -> __ -> __ -> 'a1) -> 'a1

val subaddressing_mode_inv_rect_Type3 :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  (addressing_mode -> __ -> __ -> 'a1) -> 'a1

val subaddressing_mode_inv_rect_Type2 :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  (addressing_mode -> __ -> __ -> 'a1) -> 'a1

val subaddressing_mode_inv_rect_Type1 :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  (addressing_mode -> __ -> __ -> 'a1) -> 'a1

val subaddressing_mode_inv_rect_Type0 :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  (addressing_mode -> __ -> __ -> 'a1) -> 'a1

val subaddressing_mode_discr :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  subaddressing_mode -> __

val subaddressing_mode_jmdiscr :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  subaddressing_mode -> __

val dpi1__o__subaddressing_modeel__o__inject :
  Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
  Types.dPair -> addressing_mode Types.sig0

val eject__o__subaddressing_modeel__o__inject :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
  Types.sig0 -> addressing_mode Types.sig0

val subaddressing_modeel__o__inject :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
  addressing_mode Types.sig0

val dpi1__o__subaddressing_modeel :
  Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
  Types.dPair -> addressing_mode

val eject__o__subaddressing_modeel :
  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
  Types.sig0 -> addressing_mode

type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode

type eject__o__subaddressing_mode = subaddressing_mode

val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
  -> subaddressing_mode Types.sig0

val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
  -> addressing_mode Types.sig0

val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
  -> addressing_mode

val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
  subaddressing_mode Types.sig0

val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
  addressing_mode Types.sig0

val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
  addressing_mode

val subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode ->
  subaddressing_mode Types.sig0

val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
  Types.sig0

val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode

val dpi1__o__mk_subaddressing_mode__o__inject :
  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
  Vector.vector -> subaddressing_mode Types.sig0

val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
  Vector.vector -> addressing_mode Types.sig0

val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
  Vector.vector -> addressing_mode

val eject__o__mk_subaddressing_mode__o__inject :
  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
  -> subaddressing_mode Types.sig0

val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
  -> addressing_mode Types.sig0

val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
  -> addressing_mode

val mk_subaddressing_mode__o__subaddressing_modeel :
  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
  addressing_mode

val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
  addressing_mode Types.sig0

val mk_subaddressing_mode__o__inject :
  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
  subaddressing_mode Types.sig0

val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
  -> subaddressing_mode

val eject__o__subaddressing_modeel__o__mk_subaddressing_mode :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
  subaddressing_mode

val subaddressing_modeel__o__mk_subaddressing_mode :
  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
  addressing_mode_tag Vector.vector -> subaddressing_mode ->
  subaddressing_mode

val dpi1__o__mk_subaddressing_mode :
  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
  Vector.vector -> subaddressing_mode

val eject__o__mk_subaddressing_mode :
  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
  -> subaddressing_mode

type 'a preinstruction =
| ADD of subaddressing_mode * subaddressing_mode
| ADDC of subaddressing_mode * subaddressing_mode
| SUBB of subaddressing_mode * subaddressing_mode
| INC of subaddressing_mode
| DEC of subaddressing_mode
| MUL of subaddressing_mode * subaddressing_mode
| DIV of subaddressing_mode * subaddressing_mode
| DA of subaddressing_mode
| JC of 'a
| JNC of 'a
| JB of subaddressing_mode * 'a
| JNB of subaddressing_mode * 'a
| JBC of subaddressing_mode * 'a
| JZ of 'a
| JNZ of 'a
| CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * 
   'a
| DJNZ of subaddressing_mode * 'a
| ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
| ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
| XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
| CLR of subaddressing_mode
| CPL of subaddressing_mode
| RL of subaddressing_mode
| RLC of subaddressing_mode
| RR of subaddressing_mode
| RRC of subaddressing_mode
| SWAP of subaddressing_mode
| MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
| MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
| SETB of subaddressing_mode
| PUSH of subaddressing_mode
| POP of subaddressing_mode
| XCH of subaddressing_mode * subaddressing_mode
| XCHD of subaddressing_mode * subaddressing_mode
| RET
| RETI
| NOP
| JMP of subaddressing_mode

val preinstruction_rect_Type4 :
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
  'a2) -> 'a1 preinstruction -> 'a2

val preinstruction_rect_Type5 :
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
  'a2) -> 'a1 preinstruction -> 'a2

val preinstruction_rect_Type3 :
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
  'a2) -> 'a1 preinstruction -> 'a2

val preinstruction_rect_Type2 :
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
  'a2) -> 'a1 preinstruction -> 'a2

val preinstruction_rect_Type1 :
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
  'a2) -> 'a1 preinstruction -> 'a2

val preinstruction_rect_Type0 :
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
  'a2) -> 'a1 preinstruction -> 'a2

val preinstruction_inv_rect_Type4 :
  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2

val preinstruction_inv_rect_Type3 :
  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2

val preinstruction_inv_rect_Type2 :
  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2

val preinstruction_inv_rect_Type1 :
  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2

val preinstruction_inv_rect_Type0 :
  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
  ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2

val preinstruction_discr : 'a1 preinstruction -> 'a1 preinstruction -> __

val preinstruction_jmdiscr : 'a1 preinstruction -> 'a1 preinstruction -> __

val eq_preinstruction :
  subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
  Bool.bool

type instruction =
| ACALL of subaddressing_mode
| LCALL of subaddressing_mode
| AJMP of subaddressing_mode
| LJMP of subaddressing_mode
| SJMP of subaddressing_mode
| MOVC of subaddressing_mode * subaddressing_mode
| RealInstruction of subaddressing_mode preinstruction

val instruction_rect_Type4 :
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1

val instruction_rect_Type5 :
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1

val instruction_rect_Type3 :
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1

val instruction_rect_Type2 :
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1

val instruction_rect_Type1 :
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1

val instruction_rect_Type0 :
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1

val instruction_inv_rect_Type4 :
  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
  __ -> 'a1) -> 'a1

val instruction_inv_rect_Type3 :
  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
  __ -> 'a1) -> 'a1

val instruction_inv_rect_Type2 :
  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
  __ -> 'a1) -> 'a1

val instruction_inv_rect_Type1 :
  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
  __ -> 'a1) -> 'a1

val instruction_inv_rect_Type0 :
  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
  __ -> 'a1) -> 'a1

val instruction_discr : instruction -> instruction -> __

val instruction_jmdiscr : instruction -> instruction -> __

val dpi1__o__RealInstruction__o__inject :
  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
  Types.sig0

val eject__o__RealInstruction__o__inject :
  subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0

val realInstruction__o__inject :
  subaddressing_mode preinstruction -> instruction Types.sig0

val dpi1__o__RealInstruction :
  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction

val eject__o__RealInstruction :
  subaddressing_mode preinstruction Types.sig0 -> instruction

val eq_instruction : instruction -> instruction -> Bool.bool

type word_side =
| HIGH
| LOW

val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1

val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1

val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1

val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1

val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1

val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1

val word_side_inv_rect_Type4 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val word_side_inv_rect_Type3 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val word_side_inv_rect_Type2 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val word_side_inv_rect_Type1 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val word_side_inv_rect_Type0 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val word_side_discr : word_side -> word_side -> __

val word_side_jmdiscr : word_side -> word_side -> __

type pseudo_instruction =
| Instruction of identifier preinstruction
| Comment of String.string
| Cost of CostLabel.costlabel
| Jmp of identifier
| Jnz of subaddressing_mode * identifier * identifier
| Call of identifier
| Mov of (subaddressing_mode, (subaddressing_mode, word_side) Types.prod)
         Types.sum * identifier * BitVector.word

val pseudo_instruction_rect_Type4 :
  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1

val pseudo_instruction_rect_Type5 :
  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1

val pseudo_instruction_rect_Type3 :
  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1

val pseudo_instruction_rect_Type2 :
  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1

val pseudo_instruction_rect_Type1 :
  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1

val pseudo_instruction_rect_Type0 :
  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1

val pseudo_instruction_inv_rect_Type4 :
  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1

val pseudo_instruction_inv_rect_Type3 :
  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1

val pseudo_instruction_inv_rect_Type2 :
  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1

val pseudo_instruction_inv_rect_Type1 :
  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1

val pseudo_instruction_inv_rect_Type0 :
  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1

val pseudo_instruction_discr : pseudo_instruction -> pseudo_instruction -> __

val pseudo_instruction_jmdiscr :
  pseudo_instruction -> pseudo_instruction -> __

type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj

type assembly_program = instruction List.list

val fetch_pseudo_instruction :
  labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
  BitVector.word) Types.prod

val is_jump' : identifier preinstruction -> Bool.bool

val is_relative_jump : pseudo_instruction -> Bool.bool

val is_jump : pseudo_instruction -> Bool.bool

val is_call : pseudo_instruction -> Bool.bool

val asm_cost_label :
  labelled_instruction List.list -> BitVector.word Types.sig0 ->
  CostLabel.costlabel Types.option

val aDDRESS_WIDTH : Nat.nat

val mAX_CODE_SIZE : Nat.nat

val code_size_opt : labelled_instruction List.list -> __ Types.option

type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
                                            Types.prod List.list;
                                 code : labelled_instruction List.list;
                                 renamed_symbols : (identifier, AST.ident)
                                                   Types.prod List.list;
                                 final_label : identifier }

val pseudo_assembly_program_rect_Type4 :
  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1

val pseudo_assembly_program_rect_Type5 :
  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1

val pseudo_assembly_program_rect_Type3 :
  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1

val pseudo_assembly_program_rect_Type2 :
  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1

val pseudo_assembly_program_rect_Type1 :
  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1

val pseudo_assembly_program_rect_Type0 :
  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1

val preamble :
  pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
  List.list

val code : pseudo_assembly_program -> labelled_instruction List.list

val renamed_symbols :
  pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list

val final_label : pseudo_assembly_program -> identifier

val pseudo_assembly_program_inv_rect_Type4 :
  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
  List.list -> labelled_instruction List.list -> __ -> (identifier,
  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
  'a1

val pseudo_assembly_program_inv_rect_Type3 :
  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
  List.list -> labelled_instruction List.list -> __ -> (identifier,
  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
  'a1

val pseudo_assembly_program_inv_rect_Type2 :
  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
  List.list -> labelled_instruction List.list -> __ -> (identifier,
  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
  'a1

val pseudo_assembly_program_inv_rect_Type1 :
  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
  List.list -> labelled_instruction List.list -> __ -> (identifier,
  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
  'a1

val pseudo_assembly_program_inv_rect_Type0 :
  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
  List.list -> labelled_instruction List.list -> __ -> (identifier,
  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
  'a1

val pseudo_assembly_program_jmdiscr :
  pseudo_assembly_program -> pseudo_assembly_program -> __

type object_code = BitVector.byte List.list

val next :
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
  (BitVector.word, BitVector.byte) Types.prod

val load_code_memory0 :
  object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0

val load_code_memory :
  object_code -> BitVector.byte BitVectorTrie.bitVectorTrie

type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie

type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie

type labelled_object_code = { oc : object_code;
                              cm : BitVector.byte BitVectorTrie.bitVectorTrie;
                              costlabels : costlabel_map;
                              symboltable : symboltable_type;
                              final_pc : BitVector.word }

val labelled_object_code_rect_Type4 :
  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
  labelled_object_code -> 'a1

val labelled_object_code_rect_Type5 :
  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
  labelled_object_code -> 'a1

val labelled_object_code_rect_Type3 :
  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
  labelled_object_code -> 'a1

val labelled_object_code_rect_Type2 :
  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
  labelled_object_code -> 'a1

val labelled_object_code_rect_Type1 :
  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
  labelled_object_code -> 'a1

val labelled_object_code_rect_Type0 :
  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
  labelled_object_code -> 'a1

val oc : labelled_object_code -> object_code

val cm : labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie

val costlabels : labelled_object_code -> costlabel_map

val symboltable : labelled_object_code -> symboltable_type

val final_pc : labelled_object_code -> BitVector.word

val labelled_object_code_inv_rect_Type4 :
  labelled_object_code -> (object_code -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
  BitVector.word -> __ -> __ -> 'a1) -> 'a1

val labelled_object_code_inv_rect_Type3 :
  labelled_object_code -> (object_code -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
  BitVector.word -> __ -> __ -> 'a1) -> 'a1

val labelled_object_code_inv_rect_Type2 :
  labelled_object_code -> (object_code -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
  BitVector.word -> __ -> __ -> 'a1) -> 'a1

val labelled_object_code_inv_rect_Type1 :
  labelled_object_code -> (object_code -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
  BitVector.word -> __ -> __ -> 'a1) -> 'a1

val labelled_object_code_inv_rect_Type0 :
  labelled_object_code -> (object_code -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
  BitVector.word -> __ -> __ -> 'a1) -> 'a1

val labelled_object_code_jmdiscr :
  labelled_object_code -> labelled_object_code -> __