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_33 -> h_DIRECT x_33
| INDIRECT x_34 -> h_INDIRECT x_34
| EXT_INDIRECT x_35 -> h_EXT_INDIRECT x_35
| REGISTER x_36 -> h_REGISTER x_36
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_37 -> h_DATA x_37
| DATA16 x_38 -> h_DATA16 x_38
| 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_39 -> h_BIT_ADDR x_39
| N_BIT_ADDR x_40 -> h_N_BIT_ADDR x_40
| RELATIVE x_41 -> h_RELATIVE x_41
| ADDR11 x_42 -> h_ADDR11 x_42
| ADDR16 x_43 -> h_ADDR16 x_43

(** 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_64 -> h_DIRECT x_64
| INDIRECT x_65 -> h_INDIRECT x_65
| EXT_INDIRECT x_66 -> h_EXT_INDIRECT x_66
| REGISTER x_67 -> h_REGISTER x_67
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_68 -> h_DATA x_68
| DATA16 x_69 -> h_DATA16 x_69
| 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_70 -> h_BIT_ADDR x_70
| N_BIT_ADDR x_71 -> h_N_BIT_ADDR x_71
| RELATIVE x_72 -> h_RELATIVE x_72
| ADDR11 x_73 -> h_ADDR11 x_73
| ADDR16 x_74 -> h_ADDR16 x_74

(** 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_95 -> h_DIRECT x_95
| INDIRECT x_96 -> h_INDIRECT x_96
| EXT_INDIRECT x_97 -> h_EXT_INDIRECT x_97
| REGISTER x_98 -> h_REGISTER x_98
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_99 -> h_DATA x_99
| DATA16 x_100 -> h_DATA16 x_100
| 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_101 -> h_BIT_ADDR x_101
| N_BIT_ADDR x_102 -> h_N_BIT_ADDR x_102
| RELATIVE x_103 -> h_RELATIVE x_103
| ADDR11 x_104 -> h_ADDR11 x_104
| ADDR16 x_105 -> h_ADDR16 x_105

(** 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_126 -> h_DIRECT x_126
| INDIRECT x_127 -> h_INDIRECT x_127
| EXT_INDIRECT x_128 -> h_EXT_INDIRECT x_128
| REGISTER x_129 -> h_REGISTER x_129
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_130 -> h_DATA x_130
| DATA16 x_131 -> h_DATA16 x_131
| 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_132 -> h_BIT_ADDR x_132
| N_BIT_ADDR x_133 -> h_N_BIT_ADDR x_133
| RELATIVE x_134 -> h_RELATIVE x_134
| ADDR11 x_135 -> h_ADDR11 x_135
| ADDR16 x_136 -> h_ADDR16 x_136

(** 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_157 -> h_DIRECT x_157
| INDIRECT x_158 -> h_INDIRECT x_158
| EXT_INDIRECT x_159 -> h_EXT_INDIRECT x_159
| REGISTER x_160 -> h_REGISTER x_160
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_161 -> h_DATA x_161
| DATA16 x_162 -> h_DATA16 x_162
| 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_163 -> h_BIT_ADDR x_163
| N_BIT_ADDR x_164 -> h_N_BIT_ADDR x_164
| RELATIVE x_165 -> h_RELATIVE x_165
| ADDR11 x_166 -> h_ADDR11 x_166
| ADDR16 x_167 -> h_ADDR16 x_167

(** 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_188 -> h_DIRECT x_188
| INDIRECT x_189 -> h_INDIRECT x_189
| EXT_INDIRECT x_190 -> h_EXT_INDIRECT x_190
| REGISTER x_191 -> h_REGISTER x_191
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
| DATA x_192 -> h_DATA x_192
| DATA16 x_193 -> h_DATA16 x_193
| 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_194 -> h_BIT_ADDR x_194
| N_BIT_ADDR x_195 -> h_N_BIT_ADDR x_195
| RELATIVE x_196 -> h_RELATIVE x_196
| ADDR11 x_197 -> h_ADDR11 x_197
| ADDR16 x_198 -> h_ADDR16 x_198

(** 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_666 =
  let subaddressing_modeel = x_666 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_668 =
  let subaddressing_modeel = x_668 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_670 =
  let subaddressing_modeel = x_670 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_672 =
  let subaddressing_modeel = x_672 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_674 =
  let subaddressing_modeel = x_674 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_676 =
  let subaddressing_modeel = x_676 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_778, x_777) -> h_ADD x_778 x_777
| ADDC (x_780, x_779) -> h_ADDC x_780 x_779
| SUBB (x_782, x_781) -> h_SUBB x_782 x_781
| INC x_783 -> h_INC x_783
| DEC x_784 -> h_DEC x_784
| MUL (x_786, x_785) -> h_MUL x_786 x_785
| DIV (x_788, x_787) -> h_DIV x_788 x_787
| DA x_789 -> h_DA x_789
| JC x_790 -> h_JC x_790
| JNC x_791 -> h_JNC x_791
| JB (x_793, x_792) -> h_JB x_793 x_792
| JNB (x_795, x_794) -> h_JNB x_795 x_794
| JBC (x_797, x_796) -> h_JBC x_797 x_796
| JZ x_798 -> h_JZ x_798
| JNZ x_799 -> h_JNZ x_799
| CJNE (x_801, x_800) -> h_CJNE x_801 x_800
| DJNZ (x_803, x_802) -> h_DJNZ x_803 x_802
| ANL x_804 -> h_ANL x_804
| ORL x_805 -> h_ORL x_805
| XRL x_806 -> h_XRL x_806
| CLR x_807 -> h_CLR x_807
| CPL x_808 -> h_CPL x_808
| RL x_809 -> h_RL x_809
| RLC x_810 -> h_RLC x_810
| RR x_811 -> h_RR x_811
| RRC x_812 -> h_RRC x_812
| SWAP x_813 -> h_SWAP x_813
| MOV x_814 -> h_MOV x_814
| MOVX x_815 -> h_MOVX x_815
| SETB x_816 -> h_SETB x_816
| PUSH x_817 -> h_PUSH x_817
| POP x_818 -> h_POP x_818
| XCH (x_820, x_819) -> h_XCH x_820 x_819
| XCHD (x_822, x_821) -> h_XCHD x_822 x_821
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_823 -> h_JMP x_823

(** 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_864, x_863) -> h_ADD x_864 x_863
| ADDC (x_866, x_865) -> h_ADDC x_866 x_865
| SUBB (x_868, x_867) -> h_SUBB x_868 x_867
| INC x_869 -> h_INC x_869
| DEC x_870 -> h_DEC x_870
| MUL (x_872, x_871) -> h_MUL x_872 x_871
| DIV (x_874, x_873) -> h_DIV x_874 x_873
| DA x_875 -> h_DA x_875
| JC x_876 -> h_JC x_876
| JNC x_877 -> h_JNC x_877
| JB (x_879, x_878) -> h_JB x_879 x_878
| JNB (x_881, x_880) -> h_JNB x_881 x_880
| JBC (x_883, x_882) -> h_JBC x_883 x_882
| JZ x_884 -> h_JZ x_884
| JNZ x_885 -> h_JNZ x_885
| CJNE (x_887, x_886) -> h_CJNE x_887 x_886
| DJNZ (x_889, x_888) -> h_DJNZ x_889 x_888
| ANL x_890 -> h_ANL x_890
| ORL x_891 -> h_ORL x_891
| XRL x_892 -> h_XRL x_892
| CLR x_893 -> h_CLR x_893
| CPL x_894 -> h_CPL x_894
| RL x_895 -> h_RL x_895
| RLC x_896 -> h_RLC x_896
| RR x_897 -> h_RR x_897
| RRC x_898 -> h_RRC x_898
| SWAP x_899 -> h_SWAP x_899
| MOV x_900 -> h_MOV x_900
| MOVX x_901 -> h_MOVX x_901
| SETB x_902 -> h_SETB x_902
| PUSH x_903 -> h_PUSH x_903
| POP x_904 -> h_POP x_904
| XCH (x_906, x_905) -> h_XCH x_906 x_905
| XCHD (x_908, x_907) -> h_XCHD x_908 x_907
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_909 -> h_JMP x_909

(** 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_950, x_949) -> h_ADD x_950 x_949
| ADDC (x_952, x_951) -> h_ADDC x_952 x_951
| SUBB (x_954, x_953) -> h_SUBB x_954 x_953
| INC x_955 -> h_INC x_955
| DEC x_956 -> h_DEC x_956
| MUL (x_958, x_957) -> h_MUL x_958 x_957
| DIV (x_960, x_959) -> h_DIV x_960 x_959
| DA x_961 -> h_DA x_961
| JC x_962 -> h_JC x_962
| JNC x_963 -> h_JNC x_963
| JB (x_965, x_964) -> h_JB x_965 x_964
| JNB (x_967, x_966) -> h_JNB x_967 x_966
| JBC (x_969, x_968) -> h_JBC x_969 x_968
| JZ x_970 -> h_JZ x_970
| JNZ x_971 -> h_JNZ x_971
| CJNE (x_973, x_972) -> h_CJNE x_973 x_972
| DJNZ (x_975, x_974) -> h_DJNZ x_975 x_974
| ANL x_976 -> h_ANL x_976
| ORL x_977 -> h_ORL x_977
| XRL x_978 -> h_XRL x_978
| CLR x_979 -> h_CLR x_979
| CPL x_980 -> h_CPL x_980
| RL x_981 -> h_RL x_981
| RLC x_982 -> h_RLC x_982
| RR x_983 -> h_RR x_983
| RRC x_984 -> h_RRC x_984
| SWAP x_985 -> h_SWAP x_985
| MOV x_986 -> h_MOV x_986
| MOVX x_987 -> h_MOVX x_987
| SETB x_988 -> h_SETB x_988
| PUSH x_989 -> h_PUSH x_989
| POP x_990 -> h_POP x_990
| XCH (x_992, x_991) -> h_XCH x_992 x_991
| XCHD (x_994, x_993) -> h_XCHD x_994 x_993
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_995 -> h_JMP x_995

(** 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_1036, x_1035) -> h_ADD x_1036 x_1035
| ADDC (x_1038, x_1037) -> h_ADDC x_1038 x_1037
| SUBB (x_1040, x_1039) -> h_SUBB x_1040 x_1039
| INC x_1041 -> h_INC x_1041
| DEC x_1042 -> h_DEC x_1042
| MUL (x_1044, x_1043) -> h_MUL x_1044 x_1043
| DIV (x_1046, x_1045) -> h_DIV x_1046 x_1045
| DA x_1047 -> h_DA x_1047
| JC x_1048 -> h_JC x_1048
| JNC x_1049 -> h_JNC x_1049
| JB (x_1051, x_1050) -> h_JB x_1051 x_1050
| JNB (x_1053, x_1052) -> h_JNB x_1053 x_1052
| JBC (x_1055, x_1054) -> h_JBC x_1055 x_1054
| JZ x_1056 -> h_JZ x_1056
| JNZ x_1057 -> h_JNZ x_1057
| CJNE (x_1059, x_1058) -> h_CJNE x_1059 x_1058
| DJNZ (x_1061, x_1060) -> h_DJNZ x_1061 x_1060
| ANL x_1062 -> h_ANL x_1062
| ORL x_1063 -> h_ORL x_1063
| XRL x_1064 -> h_XRL x_1064
| CLR x_1065 -> h_CLR x_1065
| CPL x_1066 -> h_CPL x_1066
| RL x_1067 -> h_RL x_1067
| RLC x_1068 -> h_RLC x_1068
| RR x_1069 -> h_RR x_1069
| RRC x_1070 -> h_RRC x_1070
| SWAP x_1071 -> h_SWAP x_1071
| MOV x_1072 -> h_MOV x_1072
| MOVX x_1073 -> h_MOVX x_1073
| SETB x_1074 -> h_SETB x_1074
| PUSH x_1075 -> h_PUSH x_1075
| POP x_1076 -> h_POP x_1076
| XCH (x_1078, x_1077) -> h_XCH x_1078 x_1077
| XCHD (x_1080, x_1079) -> h_XCHD x_1080 x_1079
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_1081 -> h_JMP x_1081

(** 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_1122, x_1121) -> h_ADD x_1122 x_1121
| ADDC (x_1124, x_1123) -> h_ADDC x_1124 x_1123
| SUBB (x_1126, x_1125) -> h_SUBB x_1126 x_1125
| INC x_1127 -> h_INC x_1127
| DEC x_1128 -> h_DEC x_1128
| MUL (x_1130, x_1129) -> h_MUL x_1130 x_1129
| DIV (x_1132, x_1131) -> h_DIV x_1132 x_1131
| DA x_1133 -> h_DA x_1133
| JC x_1134 -> h_JC x_1134
| JNC x_1135 -> h_JNC x_1135
| JB (x_1137, x_1136) -> h_JB x_1137 x_1136
| JNB (x_1139, x_1138) -> h_JNB x_1139 x_1138
| JBC (x_1141, x_1140) -> h_JBC x_1141 x_1140
| JZ x_1142 -> h_JZ x_1142
| JNZ x_1143 -> h_JNZ x_1143
| CJNE (x_1145, x_1144) -> h_CJNE x_1145 x_1144
| DJNZ (x_1147, x_1146) -> h_DJNZ x_1147 x_1146
| ANL x_1148 -> h_ANL x_1148
| ORL x_1149 -> h_ORL x_1149
| XRL x_1150 -> h_XRL x_1150
| CLR x_1151 -> h_CLR x_1151
| CPL x_1152 -> h_CPL x_1152
| RL x_1153 -> h_RL x_1153
| RLC x_1154 -> h_RLC x_1154
| RR x_1155 -> h_RR x_1155
| RRC x_1156 -> h_RRC x_1156
| SWAP x_1157 -> h_SWAP x_1157
| MOV x_1158 -> h_MOV x_1158
| MOVX x_1159 -> h_MOVX x_1159
| SETB x_1160 -> h_SETB x_1160
| PUSH x_1161 -> h_PUSH x_1161
| POP x_1162 -> h_POP x_1162
| XCH (x_1164, x_1163) -> h_XCH x_1164 x_1163
| XCHD (x_1166, x_1165) -> h_XCHD x_1166 x_1165
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_1167 -> h_JMP x_1167

(** 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_1208, x_1207) -> h_ADD x_1208 x_1207
| ADDC (x_1210, x_1209) -> h_ADDC x_1210 x_1209
| SUBB (x_1212, x_1211) -> h_SUBB x_1212 x_1211
| INC x_1213 -> h_INC x_1213
| DEC x_1214 -> h_DEC x_1214
| MUL (x_1216, x_1215) -> h_MUL x_1216 x_1215
| DIV (x_1218, x_1217) -> h_DIV x_1218 x_1217
| DA x_1219 -> h_DA x_1219
| JC x_1220 -> h_JC x_1220
| JNC x_1221 -> h_JNC x_1221
| JB (x_1223, x_1222) -> h_JB x_1223 x_1222
| JNB (x_1225, x_1224) -> h_JNB x_1225 x_1224
| JBC (x_1227, x_1226) -> h_JBC x_1227 x_1226
| JZ x_1228 -> h_JZ x_1228
| JNZ x_1229 -> h_JNZ x_1229
| CJNE (x_1231, x_1230) -> h_CJNE x_1231 x_1230
| DJNZ (x_1233, x_1232) -> h_DJNZ x_1233 x_1232
| ANL x_1234 -> h_ANL x_1234
| ORL x_1235 -> h_ORL x_1235
| XRL x_1236 -> h_XRL x_1236
| CLR x_1237 -> h_CLR x_1237
| CPL x_1238 -> h_CPL x_1238
| RL x_1239 -> h_RL x_1239
| RLC x_1240 -> h_RLC x_1240
| RR x_1241 -> h_RR x_1241
| RRC x_1242 -> h_RRC x_1242
| SWAP x_1243 -> h_SWAP x_1243
| MOV x_1244 -> h_MOV x_1244
| MOVX x_1245 -> h_MOVX x_1245
| SETB x_1246 -> h_SETB x_1246
| PUSH x_1247 -> h_PUSH x_1247
| POP x_1248 -> h_POP x_1248
| XCH (x_1250, x_1249) -> h_XCH x_1250 x_1249
| XCHD (x_1252, x_1251) -> h_XCHD x_1252 x_1251
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
| JMP x_1253 -> h_JMP x_1253

(** 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_1825 -> h_ACALL x_1825
| LCALL x_1826 -> h_LCALL x_1826
| AJMP x_1827 -> h_AJMP x_1827
| LJMP x_1828 -> h_LJMP x_1828
| SJMP x_1829 -> h_SJMP x_1829
| MOVC (x_1831, x_1830) -> h_MOVC x_1831 x_1830
| RealInstruction x_1832 -> h_RealInstruction x_1832

(** 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_1841 -> h_ACALL x_1841
| LCALL x_1842 -> h_LCALL x_1842
| AJMP x_1843 -> h_AJMP x_1843
| LJMP x_1844 -> h_LJMP x_1844
| SJMP x_1845 -> h_SJMP x_1845
| MOVC (x_1847, x_1846) -> h_MOVC x_1847 x_1846
| RealInstruction x_1848 -> h_RealInstruction x_1848

(** 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_1857 -> h_ACALL x_1857
| LCALL x_1858 -> h_LCALL x_1858
| AJMP x_1859 -> h_AJMP x_1859
| LJMP x_1860 -> h_LJMP x_1860
| SJMP x_1861 -> h_SJMP x_1861
| MOVC (x_1863, x_1862) -> h_MOVC x_1863 x_1862
| RealInstruction x_1864 -> h_RealInstruction x_1864

(** 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_1873 -> h_ACALL x_1873
| LCALL x_1874 -> h_LCALL x_1874
| AJMP x_1875 -> h_AJMP x_1875
| LJMP x_1876 -> h_LJMP x_1876
| SJMP x_1877 -> h_SJMP x_1877
| MOVC (x_1879, x_1878) -> h_MOVC x_1879 x_1878
| RealInstruction x_1880 -> h_RealInstruction x_1880

(** 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_1889 -> h_ACALL x_1889
| LCALL x_1890 -> h_LCALL x_1890
| AJMP x_1891 -> h_AJMP x_1891
| LJMP x_1892 -> h_LJMP x_1892
| SJMP x_1893 -> h_SJMP x_1893
| MOVC (x_1895, x_1894) -> h_MOVC x_1895 x_1894
| RealInstruction x_1896 -> h_RealInstruction x_1896

(** 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_1905 -> h_ACALL x_1905
| LCALL x_1906 -> h_LCALL x_1906
| AJMP x_1907 -> h_AJMP x_1907
| LJMP x_1908 -> h_LJMP x_1908
| SJMP x_1909 -> h_SJMP x_1909
| MOVC (x_1911, x_1910) -> h_MOVC x_1911 x_1910
| RealInstruction x_1912 -> h_RealInstruction x_1912

(** 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_2075 -> h_Instruction x_2075
| Comment x_2076 -> h_Comment x_2076
| Cost x_2077 -> h_Cost x_2077
| Jmp x_2078 -> h_Jmp x_2078
| Jnz (x_2081, x_2080, x_2079) -> h_Jnz x_2081 x_2080 x_2079
| Call x_2082 -> h_Call x_2082
| Mov (x_2085, x_2084, x_2083) -> h_Mov x_2085 x_2084 x_2083

(** 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_2094 -> h_Instruction x_2094
| Comment x_2095 -> h_Comment x_2095
| Cost x_2096 -> h_Cost x_2096
| Jmp x_2097 -> h_Jmp x_2097
| Jnz (x_2100, x_2099, x_2098) -> h_Jnz x_2100 x_2099 x_2098
| Call x_2101 -> h_Call x_2101
| Mov (x_2104, x_2103, x_2102) -> h_Mov x_2104 x_2103 x_2102

(** 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_2113 -> h_Instruction x_2113
| Comment x_2114 -> h_Comment x_2114
| Cost x_2115 -> h_Cost x_2115
| Jmp x_2116 -> h_Jmp x_2116
| Jnz (x_2119, x_2118, x_2117) -> h_Jnz x_2119 x_2118 x_2117
| Call x_2120 -> h_Call x_2120
| Mov (x_2123, x_2122, x_2121) -> h_Mov x_2123 x_2122 x_2121

(** 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_2132 -> h_Instruction x_2132
| Comment x_2133 -> h_Comment x_2133
| Cost x_2134 -> h_Cost x_2134
| Jmp x_2135 -> h_Jmp x_2135
| Jnz (x_2138, x_2137, x_2136) -> h_Jnz x_2138 x_2137 x_2136
| Call x_2139 -> h_Call x_2139
| Mov (x_2142, x_2141, x_2140) -> h_Mov x_2142 x_2141 x_2140

(** 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_2151 -> h_Instruction x_2151
| Comment x_2152 -> h_Comment x_2152
| Cost x_2153 -> h_Cost x_2153
| Jmp x_2154 -> h_Jmp x_2154
| Jnz (x_2157, x_2156, x_2155) -> h_Jnz x_2157 x_2156 x_2155
| Call x_2158 -> h_Call x_2158
| Mov (x_2161, x_2160, x_2159) -> h_Mov x_2161 x_2160 x_2159

(** 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_2170 -> h_Instruction x_2170
| Comment x_2171 -> h_Comment x_2171
| Cost x_2172 -> h_Cost x_2172
| Jmp x_2173 -> h_Jmp x_2173
| Jnz (x_2176, x_2175, x_2174) -> h_Jnz x_2176 x_2175 x_2174
| Call x_2177 -> h_Call x_2177
| Mov (x_2180, x_2179, x_2178) -> h_Mov x_2180 x_2179 x_2178

(** 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_2304 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_2304
  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_2306 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_2306
  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_2308 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_2308
  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_2310 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_2310
  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_2312 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_2312
  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_2314 =
  let { preamble = preamble0; code = code0; renamed_symbols =
    renamed_symbols0; final_label = final_label0 } = x_2314
  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 = eta24568; Types.snd = mem } = Types.pi1 i_mem in
      (fun _ ->
      (let { Types.fst = i; Types.snd = bvi } = eta24568 in
      (fun _ -> { Types.fst = { Types.fst = (Nat.S i); Types.snd =
      (Arithmetic.increment (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)))))))))))))))) bvi) }; 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)))))))))))))))) bvi v mem) })) __)) __) { Types.fst =
      { Types.fst = Nat.O; Types.snd =
      (BitVector.zero (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 = (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_2330 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_2330
  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_2332 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_2332
  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_2334 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_2334
  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_2336 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_2336
  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_2338 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_2338
  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_2340 =
  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    symboltable0; final_pc = final_pc0 } = x_2340
  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