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 **)
let toASM_ident t i =
  let id = i in id

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 **)
let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
| DIRECT x_19160 -> h_DIRECT x_19160
| INDIRECT x_19161 -> h_INDIRECT x_19161
| EXT_INDIRECT x_19162 -> h_EXT_INDIRECT x_19162
| REGISTER x_19163 -> h_REGISTER x_19163
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_19164 -> h_DATA x_19164
| DATA16 x_19165 -> h_DATA16 x_19165
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
| BIT_ADDR x_19166 -> h_BIT_ADDR x_19166
| N_BIT_ADDR x_19167 -> h_N_BIT_ADDR x_19167
| RELATIVE x_19168 -> h_RELATIVE x_19168
| ADDR11 x_19169 -> h_ADDR11 x_19169
| ADDR16 x_19170 -> h_ADDR16 x_19170

(** 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 **)
let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
| DIRECT x_19191 -> h_DIRECT x_19191
| INDIRECT x_19192 -> h_INDIRECT x_19192
| EXT_INDIRECT x_19193 -> h_EXT_INDIRECT x_19193
| REGISTER x_19194 -> h_REGISTER x_19194
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_19195 -> h_DATA x_19195
| DATA16 x_19196 -> h_DATA16 x_19196
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
| BIT_ADDR x_19197 -> h_BIT_ADDR x_19197
| N_BIT_ADDR x_19198 -> h_N_BIT_ADDR x_19198
| RELATIVE x_19199 -> h_RELATIVE x_19199
| ADDR11 x_19200 -> h_ADDR11 x_19200
| ADDR16 x_19201 -> h_ADDR16 x_19201

(** 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 **)
let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
| DIRECT x_19222 -> h_DIRECT x_19222
| INDIRECT x_19223 -> h_INDIRECT x_19223
| EXT_INDIRECT x_19224 -> h_EXT_INDIRECT x_19224
| REGISTER x_19225 -> h_REGISTER x_19225
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_19226 -> h_DATA x_19226
| DATA16 x_19227 -> h_DATA16 x_19227
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
| BIT_ADDR x_19228 -> h_BIT_ADDR x_19228
| N_BIT_ADDR x_19229 -> h_N_BIT_ADDR x_19229
| RELATIVE x_19230 -> h_RELATIVE x_19230
| ADDR11 x_19231 -> h_ADDR11 x_19231
| ADDR16 x_19232 -> h_ADDR16 x_19232

(** 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 **)
let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
| DIRECT x_19253 -> h_DIRECT x_19253
| INDIRECT x_19254 -> h_INDIRECT x_19254
| EXT_INDIRECT x_19255 -> h_EXT_INDIRECT x_19255
| REGISTER x_19256 -> h_REGISTER x_19256
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_19257 -> h_DATA x_19257
| DATA16 x_19258 -> h_DATA16 x_19258
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
| BIT_ADDR x_19259 -> h_BIT_ADDR x_19259
| N_BIT_ADDR x_19260 -> h_N_BIT_ADDR x_19260
| RELATIVE x_19261 -> h_RELATIVE x_19261
| ADDR11 x_19262 -> h_ADDR11 x_19262
| ADDR16 x_19263 -> h_ADDR16 x_19263

(** 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 **)
let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
| DIRECT x_19284 -> h_DIRECT x_19284
| INDIRECT x_19285 -> h_INDIRECT x_19285
| EXT_INDIRECT x_19286 -> h_EXT_INDIRECT x_19286
| REGISTER x_19287 -> h_REGISTER x_19287
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_19288 -> h_DATA x_19288
| DATA16 x_19289 -> h_DATA16 x_19289
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
| BIT_ADDR x_19290 -> h_BIT_ADDR x_19290
| N_BIT_ADDR x_19291 -> h_N_BIT_ADDR x_19291
| RELATIVE x_19292 -> h_RELATIVE x_19292
| ADDR11 x_19293 -> h_ADDR11 x_19293
| ADDR16 x_19294 -> h_ADDR16 x_19294

(** 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 **)
let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
| DIRECT x_19315 -> h_DIRECT x_19315
| INDIRECT x_19316 -> h_INDIRECT x_19316
| EXT_INDIRECT x_19317 -> h_EXT_INDIRECT x_19317
| REGISTER x_19318 -> h_REGISTER x_19318
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_19319 -> h_DATA x_19319
| DATA16 x_19320 -> h_DATA16 x_19320
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
| BIT_ADDR x_19321 -> h_BIT_ADDR x_19321
| N_BIT_ADDR x_19322 -> h_N_BIT_ADDR x_19322
| RELATIVE x_19323 -> h_RELATIVE x_19323
| ADDR11 x_19324 -> h_ADDR11 x_19324
| ADDR16 x_19325 -> h_ADDR16 x_19325

(** 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 **)
let addressing_mode_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** val addressing_mode_discr : addressing_mode -> addressing_mode -> __ **)
let addressing_mode_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | DIRECT a0 -> Obj.magic (fun _ dH -> dH __)
     | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
     | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
     | REGISTER a0 -> Obj.magic (fun _ dH -> dH __)
     | ACC_A -> Obj.magic (fun _ dH -> dH)
     | ACC_B -> Obj.magic (fun _ dH -> dH)
     | DPTR -> Obj.magic (fun _ dH -> dH)
     | DATA a0 -> Obj.magic (fun _ dH -> dH __)
     | DATA16 a0 -> Obj.magic (fun _ dH -> dH __)
     | ACC_DPTR -> Obj.magic (fun _ dH -> dH)
     | ACC_PC -> Obj.magic (fun _ dH -> dH)
     | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
     | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
     | CARRY -> Obj.magic (fun _ dH -> dH)
     | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
     | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
     | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __)
     | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __)
     | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val addressing_mode_jmdiscr :
    addressing_mode -> addressing_mode -> __ **)
let addressing_mode_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | DIRECT a0 -> Obj.magic (fun _ dH -> dH __)
     | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
     | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
     | REGISTER a0 -> Obj.magic (fun _ dH -> dH __)
     | ACC_A -> Obj.magic (fun _ dH -> dH)
     | ACC_B -> Obj.magic (fun _ dH -> dH)
     | DPTR -> Obj.magic (fun _ dH -> dH)
     | DATA a0 -> Obj.magic (fun _ dH -> dH __)
     | DATA16 a0 -> Obj.magic (fun _ dH -> dH __)
     | ACC_DPTR -> Obj.magic (fun _ dH -> dH)
     | ACC_PC -> Obj.magic (fun _ dH -> dH)
     | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
     | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
     | CARRY -> Obj.magic (fun _ dH -> dH)
     | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
     | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
     | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __)
     | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __)
     | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val eq_addressing_mode :
    addressing_mode -> addressing_mode -> Bool.bool **)
let eq_addressing_mode a b =
  match a with
  | DIRECT d ->
    (match b with
     | DIRECT e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O)))))))) d e
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | INDIRECT b' ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT e -> BitVector.eq_b b' e
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | EXT_INDIRECT b' ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT e -> BitVector.eq_b b' e
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | REGISTER bv ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER bv' -> BitVector.eq_bv (Nat.S (Nat.S (Nat.S Nat.O))) bv bv'
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | ACC_A ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.True
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | ACC_B ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.True
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | DPTR ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.True
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | DATA b' ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O)))))))) b' e
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | DATA16 w ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O)))))))))))))))) w e
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | ACC_DPTR ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.True
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | ACC_PC ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.True
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | EXT_INDIRECT_DPTR ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.True
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | INDIRECT_DPTR ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.True
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | CARRY ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.True
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | BIT_ADDR b' ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O)))))))) b' e
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | N_BIT_ADDR b' ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O)))))))) b' e
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | RELATIVE n ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O)))))))) n e
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | ADDR11 w ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e
     | ADDR16 x -> Bool.False)
  | ADDR16 w ->
    (match b with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 e ->
       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O)))))))))))))))) w e)

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 **)
let rec addressing_mode_tag_rect_Type4 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
| Direct -> h_direct
| Indirect -> h_indirect
| Ext_indirect -> h_ext_indirect
| Registr -> h_registr
| Acc_a -> h_acc_a
| Acc_b -> h_acc_b
| Dptr -> h_dptr
| Data -> h_data
| Data16 -> h_data16
| Acc_dptr -> h_acc_dptr
| Acc_pc -> h_acc_pc
| Ext_indirect_dptr -> h_ext_indirect_dptr
| Indirect_dptr -> h_indirect_dptr
| Carry -> h_carry
| Bit_addr -> h_bit_addr
| N_bit_addr -> h_n_bit_addr
| Relative -> h_relative
| Addr11 -> h_addr11
| Addr16 -> h_addr16

(** 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 **)
let rec addressing_mode_tag_rect_Type5 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
| Direct -> h_direct
| Indirect -> h_indirect
| Ext_indirect -> h_ext_indirect
| Registr -> h_registr
| Acc_a -> h_acc_a
| Acc_b -> h_acc_b
| Dptr -> h_dptr
| Data -> h_data
| Data16 -> h_data16
| Acc_dptr -> h_acc_dptr
| Acc_pc -> h_acc_pc
| Ext_indirect_dptr -> h_ext_indirect_dptr
| Indirect_dptr -> h_indirect_dptr
| Carry -> h_carry
| Bit_addr -> h_bit_addr
| N_bit_addr -> h_n_bit_addr
| Relative -> h_relative
| Addr11 -> h_addr11
| Addr16 -> h_addr16

(** 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 **)
let rec addressing_mode_tag_rect_Type3 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
| Direct -> h_direct
| Indirect -> h_indirect
| Ext_indirect -> h_ext_indirect
| Registr -> h_registr
| Acc_a -> h_acc_a
| Acc_b -> h_acc_b
| Dptr -> h_dptr
| Data -> h_data
| Data16 -> h_data16
| Acc_dptr -> h_acc_dptr
| Acc_pc -> h_acc_pc
| Ext_indirect_dptr -> h_ext_indirect_dptr
| Indirect_dptr -> h_indirect_dptr
| Carry -> h_carry
| Bit_addr -> h_bit_addr
| N_bit_addr -> h_n_bit_addr
| Relative -> h_relative
| Addr11 -> h_addr11
| Addr16 -> h_addr16

(** 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 **)
let rec addressing_mode_tag_rect_Type2 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
| Direct -> h_direct
| Indirect -> h_indirect
| Ext_indirect -> h_ext_indirect
| Registr -> h_registr
| Acc_a -> h_acc_a
| Acc_b -> h_acc_b
| Dptr -> h_dptr
| Data -> h_data
| Data16 -> h_data16
| Acc_dptr -> h_acc_dptr
| Acc_pc -> h_acc_pc
| Ext_indirect_dptr -> h_ext_indirect_dptr
| Indirect_dptr -> h_indirect_dptr
| Carry -> h_carry
| Bit_addr -> h_bit_addr
| N_bit_addr -> h_n_bit_addr
| Relative -> h_relative
| Addr11 -> h_addr11
| Addr16 -> h_addr16

(** 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 **)
let rec addressing_mode_tag_rect_Type1 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
| Direct -> h_direct
| Indirect -> h_indirect
| Ext_indirect -> h_ext_indirect
| Registr -> h_registr
| Acc_a -> h_acc_a
| Acc_b -> h_acc_b
| Dptr -> h_dptr
| Data -> h_data
| Data16 -> h_data16
| Acc_dptr -> h_acc_dptr
| Acc_pc -> h_acc_pc
| Ext_indirect_dptr -> h_ext_indirect_dptr
| Indirect_dptr -> h_indirect_dptr
| Carry -> h_carry
| Bit_addr -> h_bit_addr
| N_bit_addr -> h_n_bit_addr
| Relative -> h_relative
| Addr11 -> h_addr11
| Addr16 -> h_addr16

(** 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 **)
let rec addressing_mode_tag_rect_Type0 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
| Direct -> h_direct
| Indirect -> h_indirect
| Ext_indirect -> h_ext_indirect
| Registr -> h_registr
| Acc_a -> h_acc_a
| Acc_b -> h_acc_b
| Dptr -> h_dptr
| Data -> h_data
| Data16 -> h_data16
| Acc_dptr -> h_acc_dptr
| Acc_pc -> h_acc_pc
| Ext_indirect_dptr -> h_ext_indirect_dptr
| Indirect_dptr -> h_indirect_dptr
| Carry -> h_carry
| Bit_addr -> h_bit_addr
| N_bit_addr -> h_n_bit_addr
| Relative -> h_relative
| Addr11 -> h_addr11
| Addr16 -> h_addr16

(** 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 **)
let addressing_mode_tag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_tag_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_tag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_tag_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_tag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_tag_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_tag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_tag_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** 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 **)
let addressing_mode_tag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    addressing_mode_tag_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 hterm
  in
  hcut __

(** val addressing_mode_tag_discr :
    addressing_mode_tag -> addressing_mode_tag -> __ **)
let addressing_mode_tag_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Direct -> Obj.magic (fun _ dH -> dH)
     | Indirect -> Obj.magic (fun _ dH -> dH)
     | Ext_indirect -> Obj.magic (fun _ dH -> dH)
     | Registr -> Obj.magic (fun _ dH -> dH)
     | Acc_a -> Obj.magic (fun _ dH -> dH)
     | Acc_b -> Obj.magic (fun _ dH -> dH)
     | Dptr -> Obj.magic (fun _ dH -> dH)
     | Data -> Obj.magic (fun _ dH -> dH)
     | Data16 -> Obj.magic (fun _ dH -> dH)
     | Acc_dptr -> Obj.magic (fun _ dH -> dH)
     | Acc_pc -> Obj.magic (fun _ dH -> dH)
     | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH)
     | Indirect_dptr -> Obj.magic (fun _ dH -> dH)
     | Carry -> Obj.magic (fun _ dH -> dH)
     | Bit_addr -> Obj.magic (fun _ dH -> dH)
     | N_bit_addr -> Obj.magic (fun _ dH -> dH)
     | Relative -> Obj.magic (fun _ dH -> dH)
     | Addr11 -> Obj.magic (fun _ dH -> dH)
     | Addr16 -> Obj.magic (fun _ dH -> dH)) y

(** val addressing_mode_tag_jmdiscr :
    addressing_mode_tag -> addressing_mode_tag -> __ **)
let addressing_mode_tag_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Direct -> Obj.magic (fun _ dH -> dH)
     | Indirect -> Obj.magic (fun _ dH -> dH)
     | Ext_indirect -> Obj.magic (fun _ dH -> dH)
     | Registr -> Obj.magic (fun _ dH -> dH)
     | Acc_a -> Obj.magic (fun _ dH -> dH)
     | Acc_b -> Obj.magic (fun _ dH -> dH)
     | Dptr -> Obj.magic (fun _ dH -> dH)
     | Data -> Obj.magic (fun _ dH -> dH)
     | Data16 -> Obj.magic (fun _ dH -> dH)
     | Acc_dptr -> Obj.magic (fun _ dH -> dH)
     | Acc_pc -> Obj.magic (fun _ dH -> dH)
     | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH)
     | Indirect_dptr -> Obj.magic (fun _ dH -> dH)
     | Carry -> Obj.magic (fun _ dH -> dH)
     | Bit_addr -> Obj.magic (fun _ dH -> dH)
     | N_bit_addr -> Obj.magic (fun _ dH -> dH)
     | Relative -> Obj.magic (fun _ dH -> dH)
     | Addr11 -> Obj.magic (fun _ dH -> dH)
     | Addr16 -> Obj.magic (fun _ dH -> dH)) y

(** val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool **)
let eq_a a b =
  match a with
  | Direct ->
    (match b with
     | Direct -> Bool.True
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Indirect ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.True
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Ext_indirect ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.True
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Registr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.True
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Acc_a ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.True
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Acc_b ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.True
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Dptr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.True
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Data ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.True
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Data16 ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.True
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Acc_dptr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.True
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Acc_pc ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.True
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Ext_indirect_dptr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.True
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Indirect_dptr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.True
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Carry ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.True
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Bit_addr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.True
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | N_bit_addr ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.True
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Relative ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.True
     | Addr11 -> Bool.False
     | Addr16 -> Bool.False)
  | Addr11 ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.True
     | Addr16 -> Bool.False)
  | Addr16 ->
    (match b with
     | Direct -> Bool.False
     | Indirect -> Bool.False
     | Ext_indirect -> Bool.False
     | Registr -> Bool.False
     | Acc_a -> Bool.False
     | Acc_b -> Bool.False
     | Dptr -> Bool.False
     | Data -> Bool.False
     | Data16 -> Bool.False
     | Acc_dptr -> Bool.False
     | Acc_pc -> Bool.False
     | Ext_indirect_dptr -> Bool.False
     | Indirect_dptr -> Bool.False
     | Carry -> Bool.False
     | Bit_addr -> Bool.False
     | N_bit_addr -> Bool.False
     | Relative -> Bool.False
     | Addr11 -> Bool.False
     | Addr16 -> Bool.True)

(** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **)
let rec is_a d a =
  match d with
  | Direct ->
    (match a with
     | DIRECT x -> Bool.True
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Indirect ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.True
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Ext_indirect ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.True
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Registr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.True
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Acc_a ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.True
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Acc_b ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.True
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Dptr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.True
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Data ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.True
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Data16 ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.True
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Acc_dptr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.True
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Acc_pc ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.True
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Ext_indirect_dptr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.True
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Indirect_dptr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.True
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Carry ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.True
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Bit_addr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.True
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | N_bit_addr ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.True
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Relative ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.True
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.False)
  | Addr11 ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.True
     | ADDR16 x -> Bool.False)
  | Addr16 ->
    (match a with
     | DIRECT x -> Bool.False
     | INDIRECT x -> Bool.False
     | EXT_INDIRECT x -> Bool.False
     | REGISTER x -> Bool.False
     | ACC_A -> Bool.False
     | ACC_B -> Bool.False
     | DPTR -> Bool.False
     | DATA x -> Bool.False
     | DATA16 x -> Bool.False
     | ACC_DPTR -> Bool.False
     | ACC_PC -> Bool.False
     | EXT_INDIRECT_DPTR -> Bool.False
     | INDIRECT_DPTR -> Bool.False
     | CARRY -> Bool.False
     | BIT_ADDR x -> Bool.False
     | N_BIT_ADDR x -> Bool.False
     | RELATIVE x -> Bool.False
     | ADDR11 x -> Bool.False
     | ADDR16 x -> Bool.True)

(** val is_in :
    Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
    Bool.bool **)
let rec is_in n l a =
  match l with
  | Vector.VEmpty -> Bool.False
  | Vector.VCons (m, he, tl) -> Bool.orb (is_a he a) (is_in m tl a)

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 **)
let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19793 =
  let subaddressing_modeel = x_19793 in
  h_mk_subaddressing_mode subaddressing_modeel __

(** val subaddressing_mode_rect_Type5 :
    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    'a1) -> subaddressing_mode -> 'a1 **)
let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19795 =
  let subaddressing_modeel = x_19795 in
  h_mk_subaddressing_mode subaddressing_modeel __

(** val subaddressing_mode_rect_Type3 :
    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    'a1) -> subaddressing_mode -> 'a1 **)
let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19797 =
  let subaddressing_modeel = x_19797 in
  h_mk_subaddressing_mode subaddressing_modeel __

(** val subaddressing_mode_rect_Type2 :
    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    'a1) -> subaddressing_mode -> 'a1 **)
let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19799 =
  let subaddressing_modeel = x_19799 in
  h_mk_subaddressing_mode subaddressing_modeel __

(** val subaddressing_mode_rect_Type1 :
    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    'a1) -> subaddressing_mode -> 'a1 **)
let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19801 =
  let subaddressing_modeel = x_19801 in
  h_mk_subaddressing_mode subaddressing_modeel __

(** val subaddressing_mode_rect_Type0 :
    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    'a1) -> subaddressing_mode -> 'a1 **)
let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19803 =
  let subaddressing_modeel = x_19803 in
  h_mk_subaddressing_mode subaddressing_modeel __

(** val subaddressing_modeel :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    addressing_mode **)
let rec subaddressing_modeel n l xxx =
  let yyy = xxx in yyy

(** val subaddressing_mode_inv_rect_Type4 :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
let subaddressing_mode_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = subaddressing_mode_rect_Type4 x1 x2 h1 hterm in hcut __

(** val subaddressing_mode_inv_rect_Type3 :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
let subaddressing_mode_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = subaddressing_mode_rect_Type3 x1 x2 h1 hterm in hcut __

(** val subaddressing_mode_inv_rect_Type2 :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
let subaddressing_mode_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = subaddressing_mode_rect_Type2 x1 x2 h1 hterm in hcut __

(** val subaddressing_mode_inv_rect_Type1 :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
let subaddressing_mode_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = subaddressing_mode_rect_Type1 x1 x2 h1 hterm in hcut __

(** val subaddressing_mode_inv_rect_Type0 :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
let subaddressing_mode_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = subaddressing_mode_rect_Type0 x1 x2 h1 hterm in hcut __

(** val subaddressing_mode_discr :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    subaddressing_mode -> __ **)
let subaddressing_mode_discr a1 a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val subaddressing_mode_jmdiscr :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    subaddressing_mode -> __ **)
let subaddressing_mode_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val dpi1__o__subaddressing_modeel__o__inject :
    Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
    Types.dPair -> addressing_mode Types.sig0 **)
let dpi1__o__subaddressing_modeel__o__inject x1 x2 x4 =
  subaddressing_modeel x1 x2 x4.Types.dpi1

(** val eject__o__subaddressing_modeel__o__inject :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
    Types.sig0 -> addressing_mode Types.sig0 **)
let eject__o__subaddressing_modeel__o__inject x1 x2 x4 =
  subaddressing_modeel x1 x2 (Types.pi1 x4)

(** val subaddressing_modeel__o__inject :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
    addressing_mode Types.sig0 **)
let subaddressing_modeel__o__inject x1 x2 x3 =
  subaddressing_modeel x1 x2 x3

(** val dpi1__o__subaddressing_modeel :
    Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
    Types.dPair -> addressing_mode **)
let dpi1__o__subaddressing_modeel x0 x1 x3 =
  subaddressing_modeel x0 x1 x3.Types.dpi1

(** val eject__o__subaddressing_modeel :
    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
    Types.sig0 -> addressing_mode **)
let eject__o__subaddressing_modeel x0 x1 x3 =
  subaddressing_modeel x0 x1 (Types.pi1 x3)

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 **)
let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x6 =
  dpi1__o__subaddressing_modeel x0 x2 x6

(** 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 **)
let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x6 =
  subaddressing_modeel__o__inject x2 x4
    (dpi1__o__subaddressing_modeel x0 x3 x6)

(** 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 **)
let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x5 =
  subaddressing_modeel x1 x3 (dpi1__o__subaddressing_modeel x0 x2 x5)

(** 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 **)
let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x6 =
  eject__o__subaddressing_modeel x0 x2 x6

(** 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 **)
let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x6 =
  subaddressing_modeel__o__inject x2 x4
    (eject__o__subaddressing_modeel x0 x3 x6)

(** 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 **)
let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x5 =
  subaddressing_modeel x1 x3 (eject__o__subaddressing_modeel x0 x2 x5)

(** 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 **)
let subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x4 =
  subaddressing_modeel x0 x2 x4

(** 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 **)
let subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x5 =
  subaddressing_modeel__o__inject x2 x4 (subaddressing_modeel x0 x3 x5)

(** 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 **)
let subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x4 =
  subaddressing_modeel x1 x3 (subaddressing_modeel x0 x2 x4)

(** val dpi1__o__mk_subaddressing_mode__o__inject :
    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
    Vector.vector -> subaddressing_mode Types.sig0 **)
let dpi1__o__mk_subaddressing_mode__o__inject x1 x2 x3 =
  x2.Types.dpi1

(** 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 **)
let dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x2 x3 x4 =
  subaddressing_modeel__o__inject x2 x4 x3.Types.dpi1

(** val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
    Vector.vector -> addressing_mode **)
let dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel x1 x2 x3 =
  subaddressing_modeel x1 x3 x2.Types.dpi1

(** val eject__o__mk_subaddressing_mode__o__inject :
    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
    Vector.vector -> subaddressing_mode Types.sig0 **)
let eject__o__mk_subaddressing_mode__o__inject x1 x2 x3 =
  Types.pi1 x2

(** 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 **)
let eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x2 x3 x4 =
  subaddressing_modeel__o__inject x2 x4 (Types.pi1 x3)

(** val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
    Vector.vector -> addressing_mode **)
let eject__o__mk_subaddressing_mode__o__subaddressing_modeel x1 x2 x3 =
  subaddressing_modeel x1 x3 (Types.pi1 x2)

(** val mk_subaddressing_mode__o__subaddressing_modeel :
    Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
    addressing_mode **)
let mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 =
  subaddressing_modeel x0 x2 x1

(** val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
    Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
    addressing_mode Types.sig0 **)
let mk_subaddressing_mode__o__subaddressing_modeel__o__inject x1 x2 x3 =
  subaddressing_modeel__o__inject x1 x3 x2

(** val mk_subaddressing_mode__o__inject :
    Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
    subaddressing_mode Types.sig0 **)
let mk_subaddressing_mode__o__inject x0 x1 x2 =
  x1

(** 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 **)
let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x5 =
  dpi1__o__subaddressing_modeel x0 x2 x5

(** 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 **)
let eject__o__subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x5 =
  eject__o__subaddressing_modeel x0 x2 x5

(** 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 **)
let subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x4 =
  subaddressing_modeel x0 x2 x4

(** val dpi1__o__mk_subaddressing_mode :
    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
    Vector.vector -> subaddressing_mode **)
let dpi1__o__mk_subaddressing_mode x1 x2 x3 =
  x2.Types.dpi1

(** val eject__o__mk_subaddressing_mode :
    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
    Vector.vector -> subaddressing_mode **)
let eject__o__mk_subaddressing_mode x1 x2 x3 =
  Types.pi1 x2

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 **)
let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
| ADD (x_19905, x_19904) -> h_ADD x_19905 x_19904
| ADDC (x_19907, x_19906) -> h_ADDC x_19907 x_19906
| SUBB (x_19909, x_19908) -> h_SUBB x_19909 x_19908
| INC x_19910 -> h_INC x_19910
| DEC x_19911 -> h_DEC x_19911
| MUL (x_19913, x_19912) -> h_MUL x_19913 x_19912
| DIV (x_19915, x_19914) -> h_DIV x_19915 x_19914
| DA x_19916 -> h_DA x_19916
| JC x_19917 -> h_JC x_19917
| JNC x_19918 -> h_JNC x_19918
| JB (x_19920, x_19919) -> h_JB x_19920 x_19919
| JNB (x_19922, x_19921) -> h_JNB x_19922 x_19921
| JBC (x_19924, x_19923) -> h_JBC x_19924 x_19923
| JZ x_19925 -> h_JZ x_19925
| JNZ x_19926 -> h_JNZ x_19926
| CJNE (x_19928, x_19927) -> h_CJNE x_19928 x_19927
| DJNZ (x_19930, x_19929) -> h_DJNZ x_19930 x_19929
| ANL x_19931 -> h_ANL x_19931
| ORL x_19932 -> h_ORL x_19932
| XRL x_19933 -> h_XRL x_19933
| CLR x_19934 -> h_CLR x_19934
| CPL x_19935 -> h_CPL x_19935
| RL x_19936 -> h_RL x_19936
| RLC x_19937 -> h_RLC x_19937
| RR x_19938 -> h_RR x_19938
| RRC x_19939 -> h_RRC x_19939
| SWAP x_19940 -> h_SWAP x_19940
| MOV x_19941 -> h_MOV x_19941
| MOVX x_19942 -> h_MOVX x_19942
| SETB x_19943 -> h_SETB x_19943
| PUSH x_19944 -> h_PUSH x_19944
| POP x_19945 -> h_POP x_19945
| XCH (x_19947, x_19946) -> h_XCH x_19947 x_19946
| XCHD (x_19949, x_19948) -> h_XCHD x_19949 x_19948
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_19950 -> h_JMP x_19950

(** 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 **)
let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
| ADD (x_19991, x_19990) -> h_ADD x_19991 x_19990
| ADDC (x_19993, x_19992) -> h_ADDC x_19993 x_19992
| SUBB (x_19995, x_19994) -> h_SUBB x_19995 x_19994
| INC x_19996 -> h_INC x_19996
| DEC x_19997 -> h_DEC x_19997
| MUL (x_19999, x_19998) -> h_MUL x_19999 x_19998
| DIV (x_20001, x_20000) -> h_DIV x_20001 x_20000
| DA x_20002 -> h_DA x_20002
| JC x_20003 -> h_JC x_20003
| JNC x_20004 -> h_JNC x_20004
| JB (x_20006, x_20005) -> h_JB x_20006 x_20005
| JNB (x_20008, x_20007) -> h_JNB x_20008 x_20007
| JBC (x_20010, x_20009) -> h_JBC x_20010 x_20009
| JZ x_20011 -> h_JZ x_20011
| JNZ x_20012 -> h_JNZ x_20012
| CJNE (x_20014, x_20013) -> h_CJNE x_20014 x_20013
| DJNZ (x_20016, x_20015) -> h_DJNZ x_20016 x_20015
| ANL x_20017 -> h_ANL x_20017
| ORL x_20018 -> h_ORL x_20018
| XRL x_20019 -> h_XRL x_20019
| CLR x_20020 -> h_CLR x_20020
| CPL x_20021 -> h_CPL x_20021
| RL x_20022 -> h_RL x_20022
| RLC x_20023 -> h_RLC x_20023
| RR x_20024 -> h_RR x_20024
| RRC x_20025 -> h_RRC x_20025
| SWAP x_20026 -> h_SWAP x_20026
| MOV x_20027 -> h_MOV x_20027
| MOVX x_20028 -> h_MOVX x_20028
| SETB x_20029 -> h_SETB x_20029
| PUSH x_20030 -> h_PUSH x_20030
| POP x_20031 -> h_POP x_20031
| XCH (x_20033, x_20032) -> h_XCH x_20033 x_20032
| XCHD (x_20035, x_20034) -> h_XCHD x_20035 x_20034
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_20036 -> h_JMP x_20036

(** 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 **)
let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
| ADD (x_20077, x_20076) -> h_ADD x_20077 x_20076
| ADDC (x_20079, x_20078) -> h_ADDC x_20079 x_20078
| SUBB (x_20081, x_20080) -> h_SUBB x_20081 x_20080
| INC x_20082 -> h_INC x_20082
| DEC x_20083 -> h_DEC x_20083
| MUL (x_20085, x_20084) -> h_MUL x_20085 x_20084
| DIV (x_20087, x_20086) -> h_DIV x_20087 x_20086
| DA x_20088 -> h_DA x_20088
| JC x_20089 -> h_JC x_20089
| JNC x_20090 -> h_JNC x_20090
| JB (x_20092, x_20091) -> h_JB x_20092 x_20091
| JNB (x_20094, x_20093) -> h_JNB x_20094 x_20093
| JBC (x_20096, x_20095) -> h_JBC x_20096 x_20095
| JZ x_20097 -> h_JZ x_20097
| JNZ x_20098 -> h_JNZ x_20098
| CJNE (x_20100, x_20099) -> h_CJNE x_20100 x_20099
| DJNZ (x_20102, x_20101) -> h_DJNZ x_20102 x_20101
| ANL x_20103 -> h_ANL x_20103
| ORL x_20104 -> h_ORL x_20104
| XRL x_20105 -> h_XRL x_20105
| CLR x_20106 -> h_CLR x_20106
| CPL x_20107 -> h_CPL x_20107
| RL x_20108 -> h_RL x_20108
| RLC x_20109 -> h_RLC x_20109
| RR x_20110 -> h_RR x_20110
| RRC x_20111 -> h_RRC x_20111
| SWAP x_20112 -> h_SWAP x_20112
| MOV x_20113 -> h_MOV x_20113
| MOVX x_20114 -> h_MOVX x_20114
| SETB x_20115 -> h_SETB x_20115
| PUSH x_20116 -> h_PUSH x_20116
| POP x_20117 -> h_POP x_20117
| XCH (x_20119, x_20118) -> h_XCH x_20119 x_20118
| XCHD (x_20121, x_20120) -> h_XCHD x_20121 x_20120
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_20122 -> h_JMP x_20122

(** 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 **)
let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
| ADD (x_20163, x_20162) -> h_ADD x_20163 x_20162
| ADDC (x_20165, x_20164) -> h_ADDC x_20165 x_20164
| SUBB (x_20167, x_20166) -> h_SUBB x_20167 x_20166
| INC x_20168 -> h_INC x_20168
| DEC x_20169 -> h_DEC x_20169
| MUL (x_20171, x_20170) -> h_MUL x_20171 x_20170
| DIV (x_20173, x_20172) -> h_DIV x_20173 x_20172
| DA x_20174 -> h_DA x_20174
| JC x_20175 -> h_JC x_20175
| JNC x_20176 -> h_JNC x_20176
| JB (x_20178, x_20177) -> h_JB x_20178 x_20177
| JNB (x_20180, x_20179) -> h_JNB x_20180 x_20179
| JBC (x_20182, x_20181) -> h_JBC x_20182 x_20181
| JZ x_20183 -> h_JZ x_20183
| JNZ x_20184 -> h_JNZ x_20184
| CJNE (x_20186, x_20185) -> h_CJNE x_20186 x_20185
| DJNZ (x_20188, x_20187) -> h_DJNZ x_20188 x_20187
| ANL x_20189 -> h_ANL x_20189
| ORL x_20190 -> h_ORL x_20190
| XRL x_20191 -> h_XRL x_20191
| CLR x_20192 -> h_CLR x_20192
| CPL x_20193 -> h_CPL x_20193
| RL x_20194 -> h_RL x_20194
| RLC x_20195 -> h_RLC x_20195
| RR x_20196 -> h_RR x_20196
| RRC x_20197 -> h_RRC x_20197
| SWAP x_20198 -> h_SWAP x_20198
| MOV x_20199 -> h_MOV x_20199
| MOVX x_20200 -> h_MOVX x_20200
| SETB x_20201 -> h_SETB x_20201
| PUSH x_20202 -> h_PUSH x_20202
| POP x_20203 -> h_POP x_20203
| XCH (x_20205, x_20204) -> h_XCH x_20205 x_20204
| XCHD (x_20207, x_20206) -> h_XCHD x_20207 x_20206
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_20208 -> h_JMP x_20208

(** 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 **)
let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
| ADD (x_20249, x_20248) -> h_ADD x_20249 x_20248
| ADDC (x_20251, x_20250) -> h_ADDC x_20251 x_20250
| SUBB (x_20253, x_20252) -> h_SUBB x_20253 x_20252
| INC x_20254 -> h_INC x_20254
| DEC x_20255 -> h_DEC x_20255
| MUL (x_20257, x_20256) -> h_MUL x_20257 x_20256
| DIV (x_20259, x_20258) -> h_DIV x_20259 x_20258
| DA x_20260 -> h_DA x_20260
| JC x_20261 -> h_JC x_20261
| JNC x_20262 -> h_JNC x_20262
| JB (x_20264, x_20263) -> h_JB x_20264 x_20263
| JNB (x_20266, x_20265) -> h_JNB x_20266 x_20265
| JBC (x_20268, x_20267) -> h_JBC x_20268 x_20267
| JZ x_20269 -> h_JZ x_20269
| JNZ x_20270 -> h_JNZ x_20270
| CJNE (x_20272, x_20271) -> h_CJNE x_20272 x_20271
| DJNZ (x_20274, x_20273) -> h_DJNZ x_20274 x_20273
| ANL x_20275 -> h_ANL x_20275
| ORL x_20276 -> h_ORL x_20276
| XRL x_20277 -> h_XRL x_20277
| CLR x_20278 -> h_CLR x_20278
| CPL x_20279 -> h_CPL x_20279
| RL x_20280 -> h_RL x_20280
| RLC x_20281 -> h_RLC x_20281
| RR x_20282 -> h_RR x_20282
| RRC x_20283 -> h_RRC x_20283
| SWAP x_20284 -> h_SWAP x_20284
| MOV x_20285 -> h_MOV x_20285
| MOVX x_20286 -> h_MOVX x_20286
| SETB x_20287 -> h_SETB x_20287
| PUSH x_20288 -> h_PUSH x_20288
| POP x_20289 -> h_POP x_20289
| XCH (x_20291, x_20290) -> h_XCH x_20291 x_20290
| XCHD (x_20293, x_20292) -> h_XCHD x_20293 x_20292
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_20294 -> h_JMP x_20294

(** 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 **)
let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
| ADD (x_20335, x_20334) -> h_ADD x_20335 x_20334
| ADDC (x_20337, x_20336) -> h_ADDC x_20337 x_20336
| SUBB (x_20339, x_20338) -> h_SUBB x_20339 x_20338
| INC x_20340 -> h_INC x_20340
| DEC x_20341 -> h_DEC x_20341
| MUL (x_20343, x_20342) -> h_MUL x_20343 x_20342
| DIV (x_20345, x_20344) -> h_DIV x_20345 x_20344
| DA x_20346 -> h_DA x_20346
| JC x_20347 -> h_JC x_20347
| JNC x_20348 -> h_JNC x_20348
| JB (x_20350, x_20349) -> h_JB x_20350 x_20349
| JNB (x_20352, x_20351) -> h_JNB x_20352 x_20351
| JBC (x_20354, x_20353) -> h_JBC x_20354 x_20353
| JZ x_20355 -> h_JZ x_20355
| JNZ x_20356 -> h_JNZ x_20356
| CJNE (x_20358, x_20357) -> h_CJNE x_20358 x_20357
| DJNZ (x_20360, x_20359) -> h_DJNZ x_20360 x_20359
| ANL x_20361 -> h_ANL x_20361
| ORL x_20362 -> h_ORL x_20362
| XRL x_20363 -> h_XRL x_20363
| CLR x_20364 -> h_CLR x_20364
| CPL x_20365 -> h_CPL x_20365
| RL x_20366 -> h_RL x_20366
| RLC x_20367 -> h_RLC x_20367
| RR x_20368 -> h_RR x_20368
| RRC x_20369 -> h_RRC x_20369
| SWAP x_20370 -> h_SWAP x_20370
| MOV x_20371 -> h_MOV x_20371
| MOVX x_20372 -> h_MOVX x_20372
| SETB x_20373 -> h_SETB x_20373
| PUSH x_20374 -> h_PUSH x_20374
| POP x_20375 -> h_POP x_20375
| XCH (x_20377, x_20376) -> h_XCH x_20377 x_20376
| XCHD (x_20379, x_20378) -> h_XCHD x_20379 x_20378
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_20380 -> h_JMP x_20380

(** 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 **)
let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
  let hcut =
    preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
      h33 h34 h35 h36 h37 h38 hterm
  in
  hcut __

(** 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 **)
let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
  let hcut =
    preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
      h33 h34 h35 h36 h37 h38 hterm
  in
  hcut __

(** 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 **)
let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
  let hcut =
    preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
      h33 h34 h35 h36 h37 h38 hterm
  in
  hcut __

(** 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 **)
let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
  let hcut =
    preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
      h33 h34 h35 h36 h37 h38 hterm
  in
  hcut __

(** 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 **)
let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
  let hcut =
    preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
      h33 h34 h35 h36 h37 h38 hterm
  in
  hcut __

(** val preinstruction_discr :
    'a1 preinstruction -> 'a1 preinstruction -> __ **)
let preinstruction_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | INC a0 -> Obj.magic (fun _ dH -> dH __)
     | DEC a0 -> Obj.magic (fun _ dH -> dH __)
     | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | DA a0 -> Obj.magic (fun _ dH -> dH __)
     | JC a0 -> Obj.magic (fun _ dH -> dH __)
     | JNC a0 -> Obj.magic (fun _ dH -> dH __)
     | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | JZ a0 -> Obj.magic (fun _ dH -> dH __)
     | JNZ a0 -> Obj.magic (fun _ dH -> dH __)
     | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | ANL a0 -> Obj.magic (fun _ dH -> dH __)
     | ORL a0 -> Obj.magic (fun _ dH -> dH __)
     | XRL a0 -> Obj.magic (fun _ dH -> dH __)
     | CLR a0 -> Obj.magic (fun _ dH -> dH __)
     | CPL a0 -> Obj.magic (fun _ dH -> dH __)
     | RL a0 -> Obj.magic (fun _ dH -> dH __)
     | RLC a0 -> Obj.magic (fun _ dH -> dH __)
     | RR a0 -> Obj.magic (fun _ dH -> dH __)
     | RRC a0 -> Obj.magic (fun _ dH -> dH __)
     | SWAP a0 -> Obj.magic (fun _ dH -> dH __)
     | MOV a0 -> Obj.magic (fun _ dH -> dH __)
     | MOVX a0 -> Obj.magic (fun _ dH -> dH __)
     | SETB a0 -> Obj.magic (fun _ dH -> dH __)
     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
     | POP a0 -> Obj.magic (fun _ dH -> dH __)
     | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | RET -> Obj.magic (fun _ dH -> dH)
     | RETI -> Obj.magic (fun _ dH -> dH)
     | NOP -> Obj.magic (fun _ dH -> dH)
     | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val preinstruction_jmdiscr :
    'a1 preinstruction -> 'a1 preinstruction -> __ **)
let preinstruction_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | INC a0 -> Obj.magic (fun _ dH -> dH __)
     | DEC a0 -> Obj.magic (fun _ dH -> dH __)
     | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | DA a0 -> Obj.magic (fun _ dH -> dH __)
     | JC a0 -> Obj.magic (fun _ dH -> dH __)
     | JNC a0 -> Obj.magic (fun _ dH -> dH __)
     | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | JZ a0 -> Obj.magic (fun _ dH -> dH __)
     | JNZ a0 -> Obj.magic (fun _ dH -> dH __)
     | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | ANL a0 -> Obj.magic (fun _ dH -> dH __)
     | ORL a0 -> Obj.magic (fun _ dH -> dH __)
     | XRL a0 -> Obj.magic (fun _ dH -> dH __)
     | CLR a0 -> Obj.magic (fun _ dH -> dH __)
     | CPL a0 -> Obj.magic (fun _ dH -> dH __)
     | RL a0 -> Obj.magic (fun _ dH -> dH __)
     | RLC a0 -> Obj.magic (fun _ dH -> dH __)
     | RR a0 -> Obj.magic (fun _ dH -> dH __)
     | RRC a0 -> Obj.magic (fun _ dH -> dH __)
     | SWAP a0 -> Obj.magic (fun _ dH -> dH __)
     | MOV a0 -> Obj.magic (fun _ dH -> dH __)
     | MOVX a0 -> Obj.magic (fun _ dH -> dH __)
     | SETB a0 -> Obj.magic (fun _ dH -> dH __)
     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
     | POP a0 -> Obj.magic (fun _ dH -> dH __)
     | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | RET -> Obj.magic (fun _ dH -> dH)
     | RETI -> Obj.magic (fun _ dH -> dH)
     | NOP -> Obj.magic (fun _ dH -> dH)
     | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val eq_preinstruction :
    subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
    Bool.bool **)
let eq_preinstruction i j =
  match i with
  | ADD (arg1, arg2) ->
    (match j with
     | ADD (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | ADDC (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | SUBB (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | INC arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC arg' ->
       eq_addressing_mode
         (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
           (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
           ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr,
           Vector.VEmpty)))))))))) arg)
         (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
           (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
           ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr,
           Vector.VEmpty)))))))))) arg')
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | DEC arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC arg' ->
       eq_addressing_mode
         (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
           ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
           (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg)
         (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
           ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
           (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg')
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | MUL (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
             Vector.VEmpty)) arg2'))
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | DIV (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
             Vector.VEmpty)) arg2'))
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | DA arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg')
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JC arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg')
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JNC arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg')
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JB (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2'))
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JNB (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2'))
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JBC (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2'))
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JZ arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg')
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | JNZ arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg')
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | CJNE (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (arg1', arg2') ->
       let prod_eq_left =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h1))
       in
       let prod_eq_right =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))) h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)) h1))
       in
       let arg1_eq = Util.eq_sum prod_eq_left prod_eq_right in
       Bool.andb (arg1_eq arg1 arg1')
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2'))
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | DJNZ (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
             Registr, (Vector.VCons (Nat.O, Direct, Vector.VEmpty)))) arg1)
           (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
             Registr, (Vector.VCons (Nat.O, Direct, Vector.VEmpty)))) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
             Vector.VEmpty)) arg2'))
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | ANL arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL arg' ->
       let prod_eq_left1 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)))))))) h)
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)))))))) h1))
       in
       let prod_eq_left2 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h1))
       in
       let prod_eq_left = Util.eq_sum prod_eq_left1 prod_eq_left2 in
       let prod_eq_right =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
               Vector.VEmpty)))) h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
               Vector.VEmpty)))) h1))
       in
       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | ORL arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL arg' ->
       let prod_eq_left1 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Data, (Vector.VCons
               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))))))) h)
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Data, (Vector.VCons
               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))))))) h1))
       in
       let prod_eq_left2 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h1))
       in
       let prod_eq_left = Util.eq_sum prod_eq_left1 prod_eq_left2 in
       let prod_eq_right =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
               Vector.VEmpty)))) h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
               Vector.VEmpty)))) h1))
       in
       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | XRL arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL arg' ->
       let prod_eq_left =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Data,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Registr, (Vector.VCons
               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))))))) h)
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Data,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Registr, (Vector.VCons
               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))))))) h1))
       in
       let prod_eq_right =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
               h1))
       in
       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | CLR arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR arg' ->
       eq_addressing_mode
         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg)
         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg')
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | CPL arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL arg' ->
       eq_addressing_mode
         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg)
         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg')
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | RL arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg')
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | RLC arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg')
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | RR arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg')
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | RRC arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg')
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | SWAP arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
           Vector.VEmpty)) arg')
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | MOV arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV arg' ->
       let prod_eq_6 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)))))))) h)
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)))))))) h1))
       in
       let prod_eq_5 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))) h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
               Vector.VEmpty)))) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
               ((Nat.S (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O),
               Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))) h)
             (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
               ((Nat.S (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O),
               Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))) h1))
       in
       let prod_eq_4 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)))))))))) h)
             (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
               Vector.VEmpty)))))))))) h1))
       in
       let prod_eq_3 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Dptr,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Dptr,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data16,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data16,
               Vector.VEmpty)) h1))
       in
       let prod_eq_2 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
               Vector.VEmpty)) h1))
       in
       let prod_eq_1 =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
               Vector.VEmpty)) h1))
       in
       let sum_eq_1 = Util.eq_sum prod_eq_6 prod_eq_5 in
       let sum_eq_2 = Util.eq_sum sum_eq_1 prod_eq_4 in
       let sum_eq_3 = Util.eq_sum sum_eq_2 prod_eq_3 in
       let sum_eq_4 = Util.eq_sum sum_eq_3 prod_eq_2 in
       let sum_eq_5 = Util.eq_sum sum_eq_4 prod_eq_1 in sum_eq_5 arg arg'
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | MOVX arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX arg' ->
       let prod_eq_left =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Ext_indirect, (Vector.VCons (Nat.O, Ext_indirect_dptr,
               Vector.VEmpty)))) h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Ext_indirect, (Vector.VCons (Nat.O, Ext_indirect_dptr,
               Vector.VEmpty)))) h1))
       in
       let prod_eq_right =
         Util.eq_prod (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Ext_indirect, (Vector.VCons (Nat.O, Ext_indirect_dptr,
               Vector.VEmpty)))) h)
             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
               Nat.O), Ext_indirect, (Vector.VCons (Nat.O, Ext_indirect_dptr,
               Vector.VEmpty)))) h1)) (fun h h1 ->
           eq_addressing_mode
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h)
             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
               Vector.VEmpty)) h1))
       in
       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | SETB arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB arg' ->
       eq_addressing_mode
         (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
           Carry, (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))) arg)
         (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
           Carry, (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))) arg')
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | PUSH arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
           Vector.VEmpty)) arg')
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | POP arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
           Vector.VEmpty)) arg')
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | XCH (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
             (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))) arg2)
           (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
             (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
             (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))) arg2'))
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | XCHD (arg1, arg2) ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect,
             Vector.VEmpty)) arg2)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect,
             Vector.VEmpty)) arg2'))
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | RET ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.True
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | RETI ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.True
     | NOP -> Bool.False
     | JMP x -> Bool.False)
  | NOP ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.True
     | JMP x -> Bool.False)
  | JMP arg ->
    (match j with
     | ADD (x, x0) -> Bool.False
     | ADDC (x, x0) -> Bool.False
     | SUBB (x, x0) -> Bool.False
     | INC x -> Bool.False
     | DEC x -> Bool.False
     | MUL (x, x0) -> Bool.False
     | DIV (x, x0) -> Bool.False
     | DA x -> Bool.False
     | JC x -> Bool.False
     | JNC x -> Bool.False
     | JB (x, x0) -> Bool.False
     | JNB (x, x0) -> Bool.False
     | JBC (x, x0) -> Bool.False
     | JZ x -> Bool.False
     | JNZ x -> Bool.False
     | CJNE (x, x0) -> Bool.False
     | DJNZ (x, x0) -> Bool.False
     | ANL x -> Bool.False
     | ORL x -> Bool.False
     | XRL x -> Bool.False
     | CLR x -> Bool.False
     | CPL x -> Bool.False
     | RL x -> Bool.False
     | RLC x -> Bool.False
     | RR x -> Bool.False
     | RRC x -> Bool.False
     | SWAP x -> Bool.False
     | MOV x -> Bool.False
     | MOVX x -> Bool.False
     | SETB x -> Bool.False
     | PUSH x -> Bool.False
     | POP x -> Bool.False
     | XCH (x, x0) -> Bool.False
     | XCHD (x, x0) -> Bool.False
     | RET -> Bool.False
     | RETI -> Bool.False
     | NOP -> Bool.False
     | JMP arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_dptr,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_dptr,
           Vector.VEmpty)) arg'))

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 **)
let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
| ACALL x_20952 -> h_ACALL x_20952
| LCALL x_20953 -> h_LCALL x_20953
| AJMP x_20954 -> h_AJMP x_20954
| LJMP x_20955 -> h_LJMP x_20955
| SJMP x_20956 -> h_SJMP x_20956
| MOVC (x_20958, x_20957) -> h_MOVC x_20958 x_20957
| RealInstruction x_20959 -> h_RealInstruction x_20959

(** 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 **)
let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
| ACALL x_20968 -> h_ACALL x_20968
| LCALL x_20969 -> h_LCALL x_20969
| AJMP x_20970 -> h_AJMP x_20970
| LJMP x_20971 -> h_LJMP x_20971
| SJMP x_20972 -> h_SJMP x_20972
| MOVC (x_20974, x_20973) -> h_MOVC x_20974 x_20973
| RealInstruction x_20975 -> h_RealInstruction x_20975

(** 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 **)
let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
| ACALL x_20984 -> h_ACALL x_20984
| LCALL x_20985 -> h_LCALL x_20985
| AJMP x_20986 -> h_AJMP x_20986
| LJMP x_20987 -> h_LJMP x_20987
| SJMP x_20988 -> h_SJMP x_20988
| MOVC (x_20990, x_20989) -> h_MOVC x_20990 x_20989
| RealInstruction x_20991 -> h_RealInstruction x_20991

(** 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 **)
let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
| ACALL x_21000 -> h_ACALL x_21000
| LCALL x_21001 -> h_LCALL x_21001
| AJMP x_21002 -> h_AJMP x_21002
| LJMP x_21003 -> h_LJMP x_21003
| SJMP x_21004 -> h_SJMP x_21004
| MOVC (x_21006, x_21005) -> h_MOVC x_21006 x_21005
| RealInstruction x_21007 -> h_RealInstruction x_21007

(** 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 **)
let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
| ACALL x_21016 -> h_ACALL x_21016
| LCALL x_21017 -> h_LCALL x_21017
| AJMP x_21018 -> h_AJMP x_21018
| LJMP x_21019 -> h_LJMP x_21019
| SJMP x_21020 -> h_SJMP x_21020
| MOVC (x_21022, x_21021) -> h_MOVC x_21022 x_21021
| RealInstruction x_21023 -> h_RealInstruction x_21023

(** 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 **)
let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
| ACALL x_21032 -> h_ACALL x_21032
| LCALL x_21033 -> h_LCALL x_21033
| AJMP x_21034 -> h_AJMP x_21034
| LJMP x_21035 -> h_LJMP x_21035
| SJMP x_21036 -> h_SJMP x_21036
| MOVC (x_21038, x_21037) -> h_MOVC x_21038 x_21037
| RealInstruction x_21039 -> h_RealInstruction x_21039

(** 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 **)
let instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** 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 **)
let instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** 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 **)
let instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** 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 **)
let instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** 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 **)
let instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** val instruction_discr : instruction -> instruction -> __ **)
let instruction_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | ACALL a0 -> Obj.magic (fun _ dH -> dH __)
     | LCALL a0 -> Obj.magic (fun _ dH -> dH __)
     | AJMP a0 -> Obj.magic (fun _ dH -> dH __)
     | LJMP a0 -> Obj.magic (fun _ dH -> dH __)
     | SJMP a0 -> Obj.magic (fun _ dH -> dH __)
     | MOVC (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | RealInstruction a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val instruction_jmdiscr : instruction -> instruction -> __ **)
let instruction_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | ACALL a0 -> Obj.magic (fun _ dH -> dH __)
     | LCALL a0 -> Obj.magic (fun _ dH -> dH __)
     | AJMP a0 -> Obj.magic (fun _ dH -> dH __)
     | LJMP a0 -> Obj.magic (fun _ dH -> dH __)
     | SJMP a0 -> Obj.magic (fun _ dH -> dH __)
     | MOVC (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | RealInstruction a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val dpi1__o__RealInstruction__o__inject :
    (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
    Types.sig0 **)
let dpi1__o__RealInstruction__o__inject x2 =
  RealInstruction x2.Types.dpi1

(** val eject__o__RealInstruction__o__inject :
    subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0 **)
let eject__o__RealInstruction__o__inject x2 =
  RealInstruction (Types.pi1 x2)

(** val realInstruction__o__inject :
    subaddressing_mode preinstruction -> instruction Types.sig0 **)
let realInstruction__o__inject x1 =
  RealInstruction x1

(** val dpi1__o__RealInstruction :
    (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction **)
let dpi1__o__RealInstruction x1 =
  RealInstruction x1.Types.dpi1

(** val eject__o__RealInstruction :
    subaddressing_mode preinstruction Types.sig0 -> instruction **)
let eject__o__RealInstruction x1 =
  RealInstruction (Types.pi1 x1)

(** val eq_instruction : instruction -> instruction -> Bool.bool **)
let eq_instruction i j =
  match i with
  | ACALL arg ->
    (match j with
     | ACALL arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr11,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr11,
           Vector.VEmpty)) arg')
     | LCALL x -> Bool.False
     | AJMP x -> Bool.False
     | LJMP x -> Bool.False
     | SJMP x -> Bool.False
     | MOVC (x, x0) -> Bool.False
     | RealInstruction x -> Bool.False)
  | LCALL arg ->
    (match j with
     | ACALL x -> Bool.False
     | LCALL arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr16,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr16,
           Vector.VEmpty)) arg')
     | AJMP x -> Bool.False
     | LJMP x -> Bool.False
     | SJMP x -> Bool.False
     | MOVC (x, x0) -> Bool.False
     | RealInstruction x -> Bool.False)
  | AJMP arg ->
    (match j with
     | ACALL x -> Bool.False
     | LCALL x -> Bool.False
     | AJMP arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr11,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr11,
           Vector.VEmpty)) arg')
     | LJMP x -> Bool.False
     | SJMP x -> Bool.False
     | MOVC (x, x0) -> Bool.False
     | RealInstruction x -> Bool.False)
  | LJMP arg ->
    (match j with
     | ACALL x -> Bool.False
     | LCALL x -> Bool.False
     | AJMP x -> Bool.False
     | LJMP arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr16,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Addr16,
           Vector.VEmpty)) arg')
     | SJMP x -> Bool.False
     | MOVC (x, x0) -> Bool.False
     | RealInstruction x -> Bool.False)
  | SJMP arg ->
    (match j with
     | ACALL x -> Bool.False
     | LCALL x -> Bool.False
     | AJMP x -> Bool.False
     | LJMP x -> Bool.False
     | SJMP arg' ->
       eq_addressing_mode
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg)
         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
           Vector.VEmpty)) arg')
     | MOVC (x, x0) -> Bool.False
     | RealInstruction x -> Bool.False)
  | MOVC (arg1, arg2) ->
    (match j with
     | ACALL x -> Bool.False
     | LCALL x -> Bool.False
     | AJMP x -> Bool.False
     | LJMP x -> Bool.False
     | SJMP x -> Bool.False
     | MOVC (arg1', arg2') ->
       Bool.andb
         (eq_addressing_mode
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1)
           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
             Vector.VEmpty)) arg1'))
         (eq_addressing_mode
           (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
             Acc_dptr, (Vector.VCons (Nat.O, Acc_pc, Vector.VEmpty)))) arg2)
           (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
             Acc_dptr, (Vector.VCons (Nat.O, Acc_pc, Vector.VEmpty)))) arg2'))
     | RealInstruction x -> Bool.False)
  | RealInstruction instr ->
    (match j with
     | ACALL x -> Bool.False
     | LCALL x -> Bool.False
     | AJMP x -> Bool.False
     | LJMP x -> Bool.False
     | SJMP x -> Bool.False
     | MOVC (x, x0) -> Bool.False
     | RealInstruction instr' -> eq_preinstruction instr instr')

type word_side =
| HIGH
| LOW

(** val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1 **)
let rec word_side_rect_Type4 h_HIGH h_LOW = function
| HIGH -> h_HIGH
| LOW -> h_LOW

(** val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1 **)
let rec word_side_rect_Type5 h_HIGH h_LOW = function
| HIGH -> h_HIGH
| LOW -> h_LOW

(** val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1 **)
let rec word_side_rect_Type3 h_HIGH h_LOW = function
| HIGH -> h_HIGH
| LOW -> h_LOW

(** val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1 **)
let rec word_side_rect_Type2 h_HIGH h_LOW = function
| HIGH -> h_HIGH
| LOW -> h_LOW

(** val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1 **)
let rec word_side_rect_Type1 h_HIGH h_LOW = function
| HIGH -> h_HIGH
| LOW -> h_LOW

(** val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1 **)
let rec word_side_rect_Type0 h_HIGH h_LOW = function
| HIGH -> h_HIGH
| LOW -> h_LOW

(** val word_side_inv_rect_Type4 :
    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let word_side_inv_rect_Type4 hterm h1 h2 =
  let hcut = word_side_rect_Type4 h1 h2 hterm in hcut __

(** val word_side_inv_rect_Type3 :
    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let word_side_inv_rect_Type3 hterm h1 h2 =
  let hcut = word_side_rect_Type3 h1 h2 hterm in hcut __

(** val word_side_inv_rect_Type2 :
    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let word_side_inv_rect_Type2 hterm h1 h2 =
  let hcut = word_side_rect_Type2 h1 h2 hterm in hcut __

(** val word_side_inv_rect_Type1 :
    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let word_side_inv_rect_Type1 hterm h1 h2 =
  let hcut = word_side_rect_Type1 h1 h2 hterm in hcut __

(** val word_side_inv_rect_Type0 :
    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let word_side_inv_rect_Type0 hterm h1 h2 =
  let hcut = word_side_rect_Type0 h1 h2 hterm in hcut __

(** val word_side_discr : word_side -> word_side -> __ **)
let word_side_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | HIGH -> Obj.magic (fun _ dH -> dH)
     | LOW -> Obj.magic (fun _ dH -> dH)) y

(** val word_side_jmdiscr : word_side -> word_side -> __ **)
let word_side_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | HIGH -> Obj.magic (fun _ dH -> dH)
     | LOW -> Obj.magic (fun _ dH -> dH)) y

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 **)
let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
| Instruction x_21202 -> h_Instruction x_21202
| Comment x_21203 -> h_Comment x_21203
| Cost x_21204 -> h_Cost x_21204
| Jmp x_21205 -> h_Jmp x_21205
| Jnz (x_21208, x_21207, x_21206) -> h_Jnz x_21208 x_21207 x_21206
| Call x_21209 -> h_Call x_21209
| Mov (x_21212, x_21211, x_21210) -> h_Mov x_21212 x_21211 x_21210

(** 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 **)
let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
| Instruction x_21221 -> h_Instruction x_21221
| Comment x_21222 -> h_Comment x_21222
| Cost x_21223 -> h_Cost x_21223
| Jmp x_21224 -> h_Jmp x_21224
| Jnz (x_21227, x_21226, x_21225) -> h_Jnz x_21227 x_21226 x_21225
| Call x_21228 -> h_Call x_21228
| Mov (x_21231, x_21230, x_21229) -> h_Mov x_21231 x_21230 x_21229

(** 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 **)
let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
| Instruction x_21240 -> h_Instruction x_21240
| Comment x_21241 -> h_Comment x_21241
| Cost x_21242 -> h_Cost x_21242
| Jmp x_21243 -> h_Jmp x_21243
| Jnz (x_21246, x_21245, x_21244) -> h_Jnz x_21246 x_21245 x_21244
| Call x_21247 -> h_Call x_21247
| Mov (x_21250, x_21249, x_21248) -> h_Mov x_21250 x_21249 x_21248

(** 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 **)
let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
| Instruction x_21259 -> h_Instruction x_21259
| Comment x_21260 -> h_Comment x_21260
| Cost x_21261 -> h_Cost x_21261
| Jmp x_21262 -> h_Jmp x_21262
| Jnz (x_21265, x_21264, x_21263) -> h_Jnz x_21265 x_21264 x_21263
| Call x_21266 -> h_Call x_21266
| Mov (x_21269, x_21268, x_21267) -> h_Mov x_21269 x_21268 x_21267

(** 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 **)
let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
| Instruction x_21278 -> h_Instruction x_21278
| Comment x_21279 -> h_Comment x_21279
| Cost x_21280 -> h_Cost x_21280
| Jmp x_21281 -> h_Jmp x_21281
| Jnz (x_21284, x_21283, x_21282) -> h_Jnz x_21284 x_21283 x_21282
| Call x_21285 -> h_Call x_21285
| Mov (x_21288, x_21287, x_21286) -> h_Mov x_21288 x_21287 x_21286

(** 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 **)
let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
| Instruction x_21297 -> h_Instruction x_21297
| Comment x_21298 -> h_Comment x_21298
| Cost x_21299 -> h_Cost x_21299
| Jmp x_21300 -> h_Jmp x_21300
| Jnz (x_21303, x_21302, x_21301) -> h_Jnz x_21303 x_21302 x_21301
| Call x_21304 -> h_Call x_21304
| Mov (x_21307, x_21306, x_21305) -> h_Mov x_21307 x_21306 x_21305

(** 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 **)
let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in
  hcut __

(** 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 **)
let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in
  hcut __

(** 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 **)
let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in
  hcut __

(** 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 **)
let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in
  hcut __

(** 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 **)
let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in
  hcut __

(** val pseudo_instruction_discr :
    pseudo_instruction -> pseudo_instruction -> __ **)
let pseudo_instruction_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Instruction a0 -> Obj.magic (fun _ dH -> dH __)
     | Comment a0 -> Obj.magic (fun _ dH -> dH __)
     | Cost a0 -> Obj.magic (fun _ dH -> dH __)
     | Jmp a0 -> Obj.magic (fun _ dH -> dH __)
     | Jnz (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Call a0 -> Obj.magic (fun _ dH -> dH __)
     | Mov (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val pseudo_instruction_jmdiscr :
    pseudo_instruction -> pseudo_instruction -> __ **)
let pseudo_instruction_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Instruction a0 -> Obj.magic (fun _ dH -> dH __)
     | Comment a0 -> Obj.magic (fun _ dH -> dH __)
     | Cost a0 -> Obj.magic (fun _ dH -> dH __)
     | Jmp a0 -> Obj.magic (fun _ dH -> dH __)
     | Jnz (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Call a0 -> Obj.magic (fun _ dH -> dH __)
     | Mov (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

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 **)
let fetch_pseudo_instruction code_mem pc =
  let { Types.fst = lbl; Types.snd = instr } =
    Util.nth_safe
      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) pc) code_mem
  in
  let new_pc =
    Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))))))))) pc
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.S Nat.O))
  in
  { Types.fst = instr; Types.snd = new_pc }

(** val is_jump' : identifier preinstruction -> Bool.bool **)
let is_jump' = function
| ADD (x0, x1) -> Bool.False
| ADDC (x0, x1) -> Bool.False
| SUBB (x0, x1) -> Bool.False
| INC x0 -> Bool.False
| DEC x0 -> Bool.False
| MUL (x0, x1) -> Bool.False
| DIV (x0, x1) -> Bool.False
| DA x0 -> Bool.False
| JC x0 -> Bool.True
| JNC x0 -> Bool.True
| JB (x0, x1) -> Bool.True
| JNB (x0, x1) -> Bool.True
| JBC (x0, x1) -> Bool.True
| JZ x0 -> Bool.True
| JNZ x0 -> Bool.True
| CJNE (x0, x1) -> Bool.True
| DJNZ (x0, x1) -> Bool.True
| ANL x0 -> Bool.False
| ORL x0 -> Bool.False
| XRL x0 -> Bool.False
| CLR x0 -> Bool.False
| CPL x0 -> Bool.False
| RL x0 -> Bool.False
| RLC x0 -> Bool.False
| RR x0 -> Bool.False
| RRC x0 -> Bool.False
| SWAP x0 -> Bool.False
| MOV x0 -> Bool.False
| MOVX x0 -> Bool.False
| SETB x0 -> Bool.False
| PUSH x0 -> Bool.False
| POP x0 -> Bool.False
| XCH (x0, x1) -> Bool.False
| XCHD (x0, x1) -> Bool.False
| RET -> Bool.False
| RETI -> Bool.False
| NOP -> Bool.False
| JMP x0 -> Bool.False

(** val is_relative_jump : pseudo_instruction -> Bool.bool **)
let is_relative_jump = function
| Instruction i -> is_jump' i
| Comment x -> Bool.False
| Cost x -> Bool.False
| Jmp x -> Bool.False
| Jnz (x, x0, x1) -> Bool.False
| Call x -> Bool.False
| Mov (x, x0, x1) -> Bool.False

(** val is_jump : pseudo_instruction -> Bool.bool **)
let is_jump = function
| Instruction i -> is_jump' i
| Comment x -> Bool.False
| Cost x -> Bool.False
| Jmp x -> Bool.True
| Jnz (x, x0, x1) -> Bool.False
| Call x -> Bool.True
| Mov (x, x0, x1) -> Bool.False

(** val is_call : pseudo_instruction -> Bool.bool **)
let is_call = function
| Instruction x -> Bool.False
| Comment x -> Bool.False
| Cost x -> Bool.False
| Jmp x -> Bool.False
| Jnz (x, x0, x1) -> Bool.False
| Call x -> Bool.True
| Mov (x, x0, x1) -> Bool.False

(** val asm_cost_label :
    labelled_instruction List.list -> BitVector.word Types.sig0 ->
    CostLabel.costlabel Types.option **)
let asm_cost_label mem w_prf =
  match (fetch_pseudo_instruction mem (Types.pi1 w_prf)).Types.fst with
  | Instruction x -> Types.None
  | Comment x -> Types.None
  | Cost c -> Types.Some c
  | Jmp x -> Types.None
  | Jnz (x, x0, x1) -> Types.None
  | Call x -> Types.None
  | Mov (x, x0, x1) -> Types.None

(** val aDDRESS_WIDTH : Nat.nat **)
let aDDRESS_WIDTH =
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))

(** val mAX_CODE_SIZE : Nat.nat **)
let mAX_CODE_SIZE =
  Exp.exp (Nat.S (Nat.S Nat.O)) aDDRESS_WIDTH

(** val code_size_opt : labelled_instruction List.list -> __ Types.option **)
let code_size_opt code =
  Extranat.nat_bound_opt mAX_CODE_SIZE (Nat.S (List.length code))

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 **)
let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_21431 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_21431
  in
  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
    final_label0 __ __

(** 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 **)
let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_21433 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_21433
  in
  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
    final_label0 __ __

(** 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 **)
let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_21435 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_21435
  in
  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
    final_label0 __ __

(** 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 **)
let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_21437 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_21437
  in
  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
    final_label0 __ __

(** 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 **)
let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_21439 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_21439
  in
  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
    final_label0 __ __

(** 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 **)
let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_21441 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_21441
  in
  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
    final_label0 __ __

(** val preamble :
    pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
    List.list **)
let rec preamble xxx =
  xxx.preamble

(** val code : pseudo_assembly_program -> labelled_instruction List.list **)
let rec code xxx =
  xxx.code

(** val renamed_symbols :
    pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list **)
let rec renamed_symbols xxx =
  xxx.renamed_symbols

(** val final_label : pseudo_assembly_program -> identifier **)
let rec final_label xxx =
  xxx.final_label

(** 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 **)
let pseudo_assembly_program_inv_rect_Type4 hterm h1 =
  let hcut = pseudo_assembly_program_rect_Type4 h1 hterm in hcut __

(** 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 **)
let pseudo_assembly_program_inv_rect_Type3 hterm h1 =
  let hcut = pseudo_assembly_program_rect_Type3 h1 hterm in hcut __

(** 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 **)
let pseudo_assembly_program_inv_rect_Type2 hterm h1 =
  let hcut = pseudo_assembly_program_rect_Type2 h1 hterm in hcut __

(** 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 **)
let pseudo_assembly_program_inv_rect_Type1 hterm h1 =
  let hcut = pseudo_assembly_program_rect_Type1 h1 hterm in hcut __

(** 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 **)
let pseudo_assembly_program_inv_rect_Type0 hterm h1 =
  let hcut = pseudo_assembly_program_rect_Type0 h1 hterm in hcut __

(** val pseudo_assembly_program_jmdiscr :
    pseudo_assembly_program -> pseudo_assembly_program -> __ **)
let pseudo_assembly_program_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { preamble = a0; code = a1; renamed_symbols = a3; final_label =
       a4 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y

type object_code = BitVector.byte List.list

(** val next :
    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    (BitVector.word, BitVector.byte) Types.prod **)
let next pmem pc =
  { Types.fst =
    (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))))))))) pc
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.S Nat.O))); Types.snd =
    (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))))))))) pc pmem
      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))) }

(** val load_code_memory0 :
    object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0 **)
let load_code_memory0 program =
  (Types.pi1
    (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
      (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in
      (fun _ -> { Types.fst = (Nat.S i); Types.snd =
      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O))))))))))))))))
        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =
      Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd

(** val load_code_memory :
    object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
let load_code_memory program =
  Types.pi1 (load_code_memory0 program)

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 **)
let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_21457 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_21457
  in
  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __

(** val labelled_object_code_rect_Type5 :
    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    labelled_object_code -> 'a1 **)
let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_21459 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_21459
  in
  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __

(** val labelled_object_code_rect_Type3 :
    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    labelled_object_code -> 'a1 **)
let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_21461 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_21461
  in
  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __

(** val labelled_object_code_rect_Type2 :
    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    labelled_object_code -> 'a1 **)
let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_21463 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_21463
  in
  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __

(** val labelled_object_code_rect_Type1 :
    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    labelled_object_code -> 'a1 **)
let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_21465 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_21465
  in
  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __

(** val labelled_object_code_rect_Type0 :
    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    labelled_object_code -> 'a1 **)
let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_21467 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_21467
  in
  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __

(** val oc : labelled_object_code -> object_code **)
let rec oc xxx =
  xxx.oc

(** val cm :
    labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
let rec cm xxx =
  xxx.cm

(** val costlabels : labelled_object_code -> costlabel_map **)
let rec costlabels xxx =
  xxx.costlabels

(** val symboltable : labelled_object_code -> symboltable_type **)
let rec symboltable xxx =
  xxx.symboltable

(** val final_pc : labelled_object_code -> BitVector.word **)
let rec final_pc xxx =
  xxx.final_pc

(** val labelled_object_code_inv_rect_Type4 :
    labelled_object_code -> (object_code -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
let labelled_object_code_inv_rect_Type4 hterm h1 =
  let hcut = labelled_object_code_rect_Type4 h1 hterm in hcut __

(** val labelled_object_code_inv_rect_Type3 :
    labelled_object_code -> (object_code -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
let labelled_object_code_inv_rect_Type3 hterm h1 =
  let hcut = labelled_object_code_rect_Type3 h1 hterm in hcut __

(** val labelled_object_code_inv_rect_Type2 :
    labelled_object_code -> (object_code -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
let labelled_object_code_inv_rect_Type2 hterm h1 =
  let hcut = labelled_object_code_rect_Type2 h1 hterm in hcut __

(** val labelled_object_code_inv_rect_Type1 :
    labelled_object_code -> (object_code -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
let labelled_object_code_inv_rect_Type1 hterm h1 =
  let hcut = labelled_object_code_rect_Type1 h1 hterm in hcut __

(** val labelled_object_code_inv_rect_Type0 :
    labelled_object_code -> (object_code -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
let labelled_object_code_inv_rect_Type0 hterm h1 =
  let hcut = labelled_object_code_rect_Type0 h1 hterm in hcut __

(** val labelled_object_code_jmdiscr :
    labelled_object_code -> labelled_object_code -> __ **)
let labelled_object_code_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { oc = a0; cm = a1; costlabels = a3; symboltable = a4; final_pc =
       a5 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y