source: extracted/aSM.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 198.5 KB
Line 
1open Preamble
2
3open Extranat
4
5open Vector
6
7open Div_and_mod
8
9open Jmeq
10
11open Russell
12
13open Types
14
15open List
16
17open Util
18
19open FoldStuff
20
21open Bool
22
23open Hints_declaration
24
25open Core_notation
26
27open Pts
28
29open Logic
30
31open Relations
32
33open Nat
34
35open BitVector
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Lists
58
59open Positive
60
61open Identifiers
62
63open Arithmetic
64
65open Integers
66
67open AST
68
69open CostLabel
70
71open LabelledObjects
72
73open String
74
75type identifier0 = PreIdentifiers.identifier
76
77(** val toASM_ident :
78    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0 **)
79let toASM_ident t i =
80  let id = i in id
81
82type addressing_mode =
83| DIRECT of BitVector.byte
84| INDIRECT of BitVector.bit
85| EXT_INDIRECT of BitVector.bit
86| REGISTER of BitVector.bitVector
87| ACC_A
88| ACC_B
89| DPTR
90| DATA of BitVector.byte
91| DATA16 of BitVector.word
92| ACC_DPTR
93| ACC_PC
94| EXT_INDIRECT_DPTR
95| INDIRECT_DPTR
96| CARRY
97| BIT_ADDR of BitVector.byte
98| N_BIT_ADDR of BitVector.byte
99| RELATIVE of BitVector.byte
100| ADDR11 of BitVector.word11
101| ADDR16 of BitVector.word
102
103(** val addressing_mode_rect_Type4 :
104    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
105    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
106    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
107    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
108    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
109    -> 'a1) -> addressing_mode -> 'a1 **)
110let 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
111| DIRECT x_59 -> h_DIRECT x_59
112| INDIRECT x_60 -> h_INDIRECT x_60
113| EXT_INDIRECT x_61 -> h_EXT_INDIRECT x_61
114| REGISTER x_62 -> h_REGISTER x_62
115| ACC_A -> h_ACC_A
116| ACC_B -> h_ACC_B
117| DPTR -> h_DPTR
118| DATA x_63 -> h_DATA x_63
119| DATA16 x_64 -> h_DATA16 x_64
120| ACC_DPTR -> h_ACC_DPTR
121| ACC_PC -> h_ACC_PC
122| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
123| INDIRECT_DPTR -> h_INDIRECT_DPTR
124| CARRY -> h_CARRY
125| BIT_ADDR x_65 -> h_BIT_ADDR x_65
126| N_BIT_ADDR x_66 -> h_N_BIT_ADDR x_66
127| RELATIVE x_67 -> h_RELATIVE x_67
128| ADDR11 x_68 -> h_ADDR11 x_68
129| ADDR16 x_69 -> h_ADDR16 x_69
130
131(** val addressing_mode_rect_Type5 :
132    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
133    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
134    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
135    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
136    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
137    -> 'a1) -> addressing_mode -> 'a1 **)
138let 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
139| DIRECT x_90 -> h_DIRECT x_90
140| INDIRECT x_91 -> h_INDIRECT x_91
141| EXT_INDIRECT x_92 -> h_EXT_INDIRECT x_92
142| REGISTER x_93 -> h_REGISTER x_93
143| ACC_A -> h_ACC_A
144| ACC_B -> h_ACC_B
145| DPTR -> h_DPTR
146| DATA x_94 -> h_DATA x_94
147| DATA16 x_95 -> h_DATA16 x_95
148| ACC_DPTR -> h_ACC_DPTR
149| ACC_PC -> h_ACC_PC
150| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
151| INDIRECT_DPTR -> h_INDIRECT_DPTR
152| CARRY -> h_CARRY
153| BIT_ADDR x_96 -> h_BIT_ADDR x_96
154| N_BIT_ADDR x_97 -> h_N_BIT_ADDR x_97
155| RELATIVE x_98 -> h_RELATIVE x_98
156| ADDR11 x_99 -> h_ADDR11 x_99
157| ADDR16 x_100 -> h_ADDR16 x_100
158
159(** val addressing_mode_rect_Type3 :
160    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
161    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
162    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
163    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
164    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
165    -> 'a1) -> addressing_mode -> 'a1 **)
166let 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
167| DIRECT x_121 -> h_DIRECT x_121
168| INDIRECT x_122 -> h_INDIRECT x_122
169| EXT_INDIRECT x_123 -> h_EXT_INDIRECT x_123
170| REGISTER x_124 -> h_REGISTER x_124
171| ACC_A -> h_ACC_A
172| ACC_B -> h_ACC_B
173| DPTR -> h_DPTR
174| DATA x_125 -> h_DATA x_125
175| DATA16 x_126 -> h_DATA16 x_126
176| ACC_DPTR -> h_ACC_DPTR
177| ACC_PC -> h_ACC_PC
178| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
179| INDIRECT_DPTR -> h_INDIRECT_DPTR
180| CARRY -> h_CARRY
181| BIT_ADDR x_127 -> h_BIT_ADDR x_127
182| N_BIT_ADDR x_128 -> h_N_BIT_ADDR x_128
183| RELATIVE x_129 -> h_RELATIVE x_129
184| ADDR11 x_130 -> h_ADDR11 x_130
185| ADDR16 x_131 -> h_ADDR16 x_131
186
187(** val addressing_mode_rect_Type2 :
188    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
189    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
190    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
191    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
192    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
193    -> 'a1) -> addressing_mode -> 'a1 **)
194let 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
195| DIRECT x_152 -> h_DIRECT x_152
196| INDIRECT x_153 -> h_INDIRECT x_153
197| EXT_INDIRECT x_154 -> h_EXT_INDIRECT x_154
198| REGISTER x_155 -> h_REGISTER x_155
199| ACC_A -> h_ACC_A
200| ACC_B -> h_ACC_B
201| DPTR -> h_DPTR
202| DATA x_156 -> h_DATA x_156
203| DATA16 x_157 -> h_DATA16 x_157
204| ACC_DPTR -> h_ACC_DPTR
205| ACC_PC -> h_ACC_PC
206| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
207| INDIRECT_DPTR -> h_INDIRECT_DPTR
208| CARRY -> h_CARRY
209| BIT_ADDR x_158 -> h_BIT_ADDR x_158
210| N_BIT_ADDR x_159 -> h_N_BIT_ADDR x_159
211| RELATIVE x_160 -> h_RELATIVE x_160
212| ADDR11 x_161 -> h_ADDR11 x_161
213| ADDR16 x_162 -> h_ADDR16 x_162
214
215(** val addressing_mode_rect_Type1 :
216    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
217    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
218    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
219    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
220    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
221    -> 'a1) -> addressing_mode -> 'a1 **)
222let 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
223| DIRECT x_183 -> h_DIRECT x_183
224| INDIRECT x_184 -> h_INDIRECT x_184
225| EXT_INDIRECT x_185 -> h_EXT_INDIRECT x_185
226| REGISTER x_186 -> h_REGISTER x_186
227| ACC_A -> h_ACC_A
228| ACC_B -> h_ACC_B
229| DPTR -> h_DPTR
230| DATA x_187 -> h_DATA x_187
231| DATA16 x_188 -> h_DATA16 x_188
232| ACC_DPTR -> h_ACC_DPTR
233| ACC_PC -> h_ACC_PC
234| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
235| INDIRECT_DPTR -> h_INDIRECT_DPTR
236| CARRY -> h_CARRY
237| BIT_ADDR x_189 -> h_BIT_ADDR x_189
238| N_BIT_ADDR x_190 -> h_N_BIT_ADDR x_190
239| RELATIVE x_191 -> h_RELATIVE x_191
240| ADDR11 x_192 -> h_ADDR11 x_192
241| ADDR16 x_193 -> h_ADDR16 x_193
242
243(** val addressing_mode_rect_Type0 :
244    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
245    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
246    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
247    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
248    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
249    -> 'a1) -> addressing_mode -> 'a1 **)
250let 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
251| DIRECT x_214 -> h_DIRECT x_214
252| INDIRECT x_215 -> h_INDIRECT x_215
253| EXT_INDIRECT x_216 -> h_EXT_INDIRECT x_216
254| REGISTER x_217 -> h_REGISTER x_217
255| ACC_A -> h_ACC_A
256| ACC_B -> h_ACC_B
257| DPTR -> h_DPTR
258| DATA x_218 -> h_DATA x_218
259| DATA16 x_219 -> h_DATA16 x_219
260| ACC_DPTR -> h_ACC_DPTR
261| ACC_PC -> h_ACC_PC
262| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
263| INDIRECT_DPTR -> h_INDIRECT_DPTR
264| CARRY -> h_CARRY
265| BIT_ADDR x_220 -> h_BIT_ADDR x_220
266| N_BIT_ADDR x_221 -> h_N_BIT_ADDR x_221
267| RELATIVE x_222 -> h_RELATIVE x_222
268| ADDR11 x_223 -> h_ADDR11 x_223
269| ADDR16 x_224 -> h_ADDR16 x_224
270
271(** val addressing_mode_inv_rect_Type4 :
272    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
273    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
274    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
275    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
276    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
277    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
278    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
279let 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 =
280  let hcut =
281    addressing_mode_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
282      h15 h16 h17 h18 h19 hterm
283  in
284  hcut __
285
286(** val addressing_mode_inv_rect_Type3 :
287    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
288    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
289    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
290    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
291    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
292    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
293    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
294let 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 =
295  let hcut =
296    addressing_mode_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
297      h15 h16 h17 h18 h19 hterm
298  in
299  hcut __
300
301(** val addressing_mode_inv_rect_Type2 :
302    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
303    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
304    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
305    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
306    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
307    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
308    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
309let 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 =
310  let hcut =
311    addressing_mode_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
312      h15 h16 h17 h18 h19 hterm
313  in
314  hcut __
315
316(** val addressing_mode_inv_rect_Type1 :
317    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
318    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
319    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
320    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
321    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
322    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
323    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
324let 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 =
325  let hcut =
326    addressing_mode_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
327      h15 h16 h17 h18 h19 hterm
328  in
329  hcut __
330
331(** val addressing_mode_inv_rect_Type0 :
332    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
333    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
334    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
335    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
336    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
337    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
338    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
339let 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 =
340  let hcut =
341    addressing_mode_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
342      h15 h16 h17 h18 h19 hterm
343  in
344  hcut __
345
346(** val addressing_mode_discr : addressing_mode -> addressing_mode -> __ **)
347let addressing_mode_discr x y =
348  Logic.eq_rect_Type2 x
349    (match x with
350     | DIRECT a0 -> Obj.magic (fun _ dH -> dH __)
351     | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
352     | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
353     | REGISTER a0 -> Obj.magic (fun _ dH -> dH __)
354     | ACC_A -> Obj.magic (fun _ dH -> dH)
355     | ACC_B -> Obj.magic (fun _ dH -> dH)
356     | DPTR -> Obj.magic (fun _ dH -> dH)
357     | DATA a0 -> Obj.magic (fun _ dH -> dH __)
358     | DATA16 a0 -> Obj.magic (fun _ dH -> dH __)
359     | ACC_DPTR -> Obj.magic (fun _ dH -> dH)
360     | ACC_PC -> Obj.magic (fun _ dH -> dH)
361     | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
362     | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
363     | CARRY -> Obj.magic (fun _ dH -> dH)
364     | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
365     | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
366     | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __)
367     | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __)
368     | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y
369
370(** val addressing_mode_jmdiscr :
371    addressing_mode -> addressing_mode -> __ **)
372let addressing_mode_jmdiscr x y =
373  Logic.eq_rect_Type2 x
374    (match x with
375     | DIRECT a0 -> Obj.magic (fun _ dH -> dH __)
376     | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
377     | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
378     | REGISTER a0 -> Obj.magic (fun _ dH -> dH __)
379     | ACC_A -> Obj.magic (fun _ dH -> dH)
380     | ACC_B -> Obj.magic (fun _ dH -> dH)
381     | DPTR -> Obj.magic (fun _ dH -> dH)
382     | DATA a0 -> Obj.magic (fun _ dH -> dH __)
383     | DATA16 a0 -> Obj.magic (fun _ dH -> dH __)
384     | ACC_DPTR -> Obj.magic (fun _ dH -> dH)
385     | ACC_PC -> Obj.magic (fun _ dH -> dH)
386     | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
387     | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
388     | CARRY -> Obj.magic (fun _ dH -> dH)
389     | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
390     | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
391     | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __)
392     | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __)
393     | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y
394
395(** val eq_addressing_mode :
396    addressing_mode -> addressing_mode -> Bool.bool **)
397let eq_addressing_mode a b =
398  match a with
399  | DIRECT d ->
400    (match b with
401     | DIRECT e0 ->
402       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
403         (Nat.S Nat.O)))))))) d e0
404     | INDIRECT x -> Bool.False
405     | EXT_INDIRECT x -> Bool.False
406     | REGISTER x -> Bool.False
407     | ACC_A -> Bool.False
408     | ACC_B -> Bool.False
409     | DPTR -> Bool.False
410     | DATA x -> Bool.False
411     | DATA16 x -> Bool.False
412     | ACC_DPTR -> Bool.False
413     | ACC_PC -> Bool.False
414     | EXT_INDIRECT_DPTR -> Bool.False
415     | INDIRECT_DPTR -> Bool.False
416     | CARRY -> Bool.False
417     | BIT_ADDR x -> Bool.False
418     | N_BIT_ADDR x -> Bool.False
419     | RELATIVE x -> Bool.False
420     | ADDR11 x -> Bool.False
421     | ADDR16 x -> Bool.False)
422  | INDIRECT b' ->
423    (match b with
424     | DIRECT x -> Bool.False
425     | INDIRECT e0 -> BitVector.eq_b b' e0
426     | EXT_INDIRECT x -> Bool.False
427     | REGISTER x -> Bool.False
428     | ACC_A -> Bool.False
429     | ACC_B -> Bool.False
430     | DPTR -> Bool.False
431     | DATA x -> Bool.False
432     | DATA16 x -> Bool.False
433     | ACC_DPTR -> Bool.False
434     | ACC_PC -> Bool.False
435     | EXT_INDIRECT_DPTR -> Bool.False
436     | INDIRECT_DPTR -> Bool.False
437     | CARRY -> Bool.False
438     | BIT_ADDR x -> Bool.False
439     | N_BIT_ADDR x -> Bool.False
440     | RELATIVE x -> Bool.False
441     | ADDR11 x -> Bool.False
442     | ADDR16 x -> Bool.False)
443  | EXT_INDIRECT b' ->
444    (match b with
445     | DIRECT x -> Bool.False
446     | INDIRECT x -> Bool.False
447     | EXT_INDIRECT e0 -> BitVector.eq_b b' e0
448     | REGISTER x -> Bool.False
449     | ACC_A -> Bool.False
450     | ACC_B -> Bool.False
451     | DPTR -> Bool.False
452     | DATA x -> Bool.False
453     | DATA16 x -> Bool.False
454     | ACC_DPTR -> Bool.False
455     | ACC_PC -> Bool.False
456     | EXT_INDIRECT_DPTR -> Bool.False
457     | INDIRECT_DPTR -> Bool.False
458     | CARRY -> Bool.False
459     | BIT_ADDR x -> Bool.False
460     | N_BIT_ADDR x -> Bool.False
461     | RELATIVE x -> Bool.False
462     | ADDR11 x -> Bool.False
463     | ADDR16 x -> Bool.False)
464  | REGISTER bv ->
465    (match b with
466     | DIRECT x -> Bool.False
467     | INDIRECT x -> Bool.False
468     | EXT_INDIRECT x -> Bool.False
469     | REGISTER bv' -> BitVector.eq_bv (Nat.S (Nat.S (Nat.S Nat.O))) bv bv'
470     | ACC_A -> Bool.False
471     | ACC_B -> Bool.False
472     | DPTR -> Bool.False
473     | DATA x -> Bool.False
474     | DATA16 x -> Bool.False
475     | ACC_DPTR -> Bool.False
476     | ACC_PC -> Bool.False
477     | EXT_INDIRECT_DPTR -> Bool.False
478     | INDIRECT_DPTR -> Bool.False
479     | CARRY -> Bool.False
480     | BIT_ADDR x -> Bool.False
481     | N_BIT_ADDR x -> Bool.False
482     | RELATIVE x -> Bool.False
483     | ADDR11 x -> Bool.False
484     | ADDR16 x -> Bool.False)
485  | ACC_A ->
486    (match b with
487     | DIRECT x -> Bool.False
488     | INDIRECT x -> Bool.False
489     | EXT_INDIRECT x -> Bool.False
490     | REGISTER x -> Bool.False
491     | ACC_A -> Bool.True
492     | ACC_B -> Bool.False
493     | DPTR -> Bool.False
494     | DATA x -> Bool.False
495     | DATA16 x -> Bool.False
496     | ACC_DPTR -> Bool.False
497     | ACC_PC -> Bool.False
498     | EXT_INDIRECT_DPTR -> Bool.False
499     | INDIRECT_DPTR -> Bool.False
500     | CARRY -> Bool.False
501     | BIT_ADDR x -> Bool.False
502     | N_BIT_ADDR x -> Bool.False
503     | RELATIVE x -> Bool.False
504     | ADDR11 x -> Bool.False
505     | ADDR16 x -> Bool.False)
506  | ACC_B ->
507    (match b with
508     | DIRECT x -> Bool.False
509     | INDIRECT x -> Bool.False
510     | EXT_INDIRECT x -> Bool.False
511     | REGISTER x -> Bool.False
512     | ACC_A -> Bool.False
513     | ACC_B -> Bool.True
514     | DPTR -> Bool.False
515     | DATA x -> Bool.False
516     | DATA16 x -> Bool.False
517     | ACC_DPTR -> Bool.False
518     | ACC_PC -> Bool.False
519     | EXT_INDIRECT_DPTR -> Bool.False
520     | INDIRECT_DPTR -> Bool.False
521     | CARRY -> Bool.False
522     | BIT_ADDR x -> Bool.False
523     | N_BIT_ADDR x -> Bool.False
524     | RELATIVE x -> Bool.False
525     | ADDR11 x -> Bool.False
526     | ADDR16 x -> Bool.False)
527  | DPTR ->
528    (match b with
529     | DIRECT x -> Bool.False
530     | INDIRECT x -> Bool.False
531     | EXT_INDIRECT x -> Bool.False
532     | REGISTER x -> Bool.False
533     | ACC_A -> Bool.False
534     | ACC_B -> Bool.False
535     | DPTR -> Bool.True
536     | DATA x -> Bool.False
537     | DATA16 x -> Bool.False
538     | ACC_DPTR -> Bool.False
539     | ACC_PC -> Bool.False
540     | EXT_INDIRECT_DPTR -> Bool.False
541     | INDIRECT_DPTR -> Bool.False
542     | CARRY -> Bool.False
543     | BIT_ADDR x -> Bool.False
544     | N_BIT_ADDR x -> Bool.False
545     | RELATIVE x -> Bool.False
546     | ADDR11 x -> Bool.False
547     | ADDR16 x -> Bool.False)
548  | DATA b' ->
549    (match b with
550     | DIRECT x -> Bool.False
551     | INDIRECT x -> Bool.False
552     | EXT_INDIRECT x -> Bool.False
553     | REGISTER x -> Bool.False
554     | ACC_A -> Bool.False
555     | ACC_B -> Bool.False
556     | DPTR -> Bool.False
557     | DATA e0 ->
558       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
559         (Nat.S Nat.O)))))))) b' e0
560     | DATA16 x -> Bool.False
561     | ACC_DPTR -> Bool.False
562     | ACC_PC -> Bool.False
563     | EXT_INDIRECT_DPTR -> Bool.False
564     | INDIRECT_DPTR -> Bool.False
565     | CARRY -> Bool.False
566     | BIT_ADDR x -> Bool.False
567     | N_BIT_ADDR x -> Bool.False
568     | RELATIVE x -> Bool.False
569     | ADDR11 x -> Bool.False
570     | ADDR16 x -> Bool.False)
571  | DATA16 w ->
572    (match b with
573     | DIRECT x -> Bool.False
574     | INDIRECT x -> Bool.False
575     | EXT_INDIRECT x -> Bool.False
576     | REGISTER x -> Bool.False
577     | ACC_A -> Bool.False
578     | ACC_B -> Bool.False
579     | DPTR -> Bool.False
580     | DATA x -> Bool.False
581     | DATA16 e0 ->
582       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
583         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
584         Nat.O)))))))))))))))) w e0
585     | ACC_DPTR -> Bool.False
586     | ACC_PC -> Bool.False
587     | EXT_INDIRECT_DPTR -> Bool.False
588     | INDIRECT_DPTR -> Bool.False
589     | CARRY -> Bool.False
590     | BIT_ADDR x -> Bool.False
591     | N_BIT_ADDR x -> Bool.False
592     | RELATIVE x -> Bool.False
593     | ADDR11 x -> Bool.False
594     | ADDR16 x -> Bool.False)
595  | ACC_DPTR ->
596    (match b with
597     | DIRECT x -> Bool.False
598     | INDIRECT x -> Bool.False
599     | EXT_INDIRECT x -> Bool.False
600     | REGISTER x -> Bool.False
601     | ACC_A -> Bool.False
602     | ACC_B -> Bool.False
603     | DPTR -> Bool.False
604     | DATA x -> Bool.False
605     | DATA16 x -> Bool.False
606     | ACC_DPTR -> Bool.True
607     | ACC_PC -> Bool.False
608     | EXT_INDIRECT_DPTR -> Bool.False
609     | INDIRECT_DPTR -> Bool.False
610     | CARRY -> Bool.False
611     | BIT_ADDR x -> Bool.False
612     | N_BIT_ADDR x -> Bool.False
613     | RELATIVE x -> Bool.False
614     | ADDR11 x -> Bool.False
615     | ADDR16 x -> Bool.False)
616  | ACC_PC ->
617    (match b with
618     | DIRECT x -> Bool.False
619     | INDIRECT x -> Bool.False
620     | EXT_INDIRECT x -> Bool.False
621     | REGISTER x -> Bool.False
622     | ACC_A -> Bool.False
623     | ACC_B -> Bool.False
624     | DPTR -> Bool.False
625     | DATA x -> Bool.False
626     | DATA16 x -> Bool.False
627     | ACC_DPTR -> Bool.False
628     | ACC_PC -> Bool.True
629     | EXT_INDIRECT_DPTR -> Bool.False
630     | INDIRECT_DPTR -> Bool.False
631     | CARRY -> Bool.False
632     | BIT_ADDR x -> Bool.False
633     | N_BIT_ADDR x -> Bool.False
634     | RELATIVE x -> Bool.False
635     | ADDR11 x -> Bool.False
636     | ADDR16 x -> Bool.False)
637  | EXT_INDIRECT_DPTR ->
638    (match b with
639     | DIRECT x -> Bool.False
640     | INDIRECT x -> Bool.False
641     | EXT_INDIRECT x -> Bool.False
642     | REGISTER x -> Bool.False
643     | ACC_A -> Bool.False
644     | ACC_B -> Bool.False
645     | DPTR -> Bool.False
646     | DATA x -> Bool.False
647     | DATA16 x -> Bool.False
648     | ACC_DPTR -> Bool.False
649     | ACC_PC -> Bool.False
650     | EXT_INDIRECT_DPTR -> Bool.True
651     | INDIRECT_DPTR -> Bool.False
652     | CARRY -> Bool.False
653     | BIT_ADDR x -> Bool.False
654     | N_BIT_ADDR x -> Bool.False
655     | RELATIVE x -> Bool.False
656     | ADDR11 x -> Bool.False
657     | ADDR16 x -> Bool.False)
658  | INDIRECT_DPTR ->
659    (match b with
660     | DIRECT x -> Bool.False
661     | INDIRECT x -> Bool.False
662     | EXT_INDIRECT x -> Bool.False
663     | REGISTER x -> Bool.False
664     | ACC_A -> Bool.False
665     | ACC_B -> Bool.False
666     | DPTR -> Bool.False
667     | DATA x -> Bool.False
668     | DATA16 x -> Bool.False
669     | ACC_DPTR -> Bool.False
670     | ACC_PC -> Bool.False
671     | EXT_INDIRECT_DPTR -> Bool.False
672     | INDIRECT_DPTR -> Bool.True
673     | CARRY -> Bool.False
674     | BIT_ADDR x -> Bool.False
675     | N_BIT_ADDR x -> Bool.False
676     | RELATIVE x -> Bool.False
677     | ADDR11 x -> Bool.False
678     | ADDR16 x -> Bool.False)
679  | CARRY ->
680    (match b with
681     | DIRECT x -> Bool.False
682     | INDIRECT x -> Bool.False
683     | EXT_INDIRECT x -> Bool.False
684     | REGISTER x -> Bool.False
685     | ACC_A -> Bool.False
686     | ACC_B -> Bool.False
687     | DPTR -> Bool.False
688     | DATA x -> Bool.False
689     | DATA16 x -> Bool.False
690     | ACC_DPTR -> Bool.False
691     | ACC_PC -> Bool.False
692     | EXT_INDIRECT_DPTR -> Bool.False
693     | INDIRECT_DPTR -> Bool.False
694     | CARRY -> Bool.True
695     | BIT_ADDR x -> Bool.False
696     | N_BIT_ADDR x -> Bool.False
697     | RELATIVE x -> Bool.False
698     | ADDR11 x -> Bool.False
699     | ADDR16 x -> Bool.False)
700  | BIT_ADDR b' ->
701    (match b with
702     | DIRECT x -> Bool.False
703     | INDIRECT x -> Bool.False
704     | EXT_INDIRECT x -> Bool.False
705     | REGISTER x -> Bool.False
706     | ACC_A -> Bool.False
707     | ACC_B -> Bool.False
708     | DPTR -> Bool.False
709     | DATA x -> Bool.False
710     | DATA16 x -> Bool.False
711     | ACC_DPTR -> Bool.False
712     | ACC_PC -> Bool.False
713     | EXT_INDIRECT_DPTR -> Bool.False
714     | INDIRECT_DPTR -> Bool.False
715     | CARRY -> Bool.False
716     | BIT_ADDR e0 ->
717       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
718         (Nat.S Nat.O)))))))) b' e0
719     | N_BIT_ADDR x -> Bool.False
720     | RELATIVE x -> Bool.False
721     | ADDR11 x -> Bool.False
722     | ADDR16 x -> Bool.False)
723  | N_BIT_ADDR b' ->
724    (match b with
725     | DIRECT x -> Bool.False
726     | INDIRECT x -> Bool.False
727     | EXT_INDIRECT x -> Bool.False
728     | REGISTER x -> Bool.False
729     | ACC_A -> Bool.False
730     | ACC_B -> Bool.False
731     | DPTR -> Bool.False
732     | DATA x -> Bool.False
733     | DATA16 x -> Bool.False
734     | ACC_DPTR -> Bool.False
735     | ACC_PC -> Bool.False
736     | EXT_INDIRECT_DPTR -> Bool.False
737     | INDIRECT_DPTR -> Bool.False
738     | CARRY -> Bool.False
739     | BIT_ADDR x -> Bool.False
740     | N_BIT_ADDR e0 ->
741       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
742         (Nat.S Nat.O)))))))) b' e0
743     | RELATIVE x -> Bool.False
744     | ADDR11 x -> Bool.False
745     | ADDR16 x -> Bool.False)
746  | RELATIVE n ->
747    (match b with
748     | DIRECT x -> Bool.False
749     | INDIRECT x -> Bool.False
750     | EXT_INDIRECT x -> Bool.False
751     | REGISTER x -> Bool.False
752     | ACC_A -> Bool.False
753     | ACC_B -> Bool.False
754     | DPTR -> Bool.False
755     | DATA x -> Bool.False
756     | DATA16 x -> Bool.False
757     | ACC_DPTR -> Bool.False
758     | ACC_PC -> Bool.False
759     | EXT_INDIRECT_DPTR -> Bool.False
760     | INDIRECT_DPTR -> Bool.False
761     | CARRY -> Bool.False
762     | BIT_ADDR x -> Bool.False
763     | N_BIT_ADDR x -> Bool.False
764     | RELATIVE e0 ->
765       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
766         (Nat.S Nat.O)))))))) n e0
767     | ADDR11 x -> Bool.False
768     | ADDR16 x -> Bool.False)
769  | ADDR11 w ->
770    (match b with
771     | DIRECT x -> Bool.False
772     | INDIRECT x -> Bool.False
773     | EXT_INDIRECT x -> Bool.False
774     | REGISTER x -> Bool.False
775     | ACC_A -> Bool.False
776     | ACC_B -> Bool.False
777     | DPTR -> Bool.False
778     | DATA x -> Bool.False
779     | DATA16 x -> Bool.False
780     | ACC_DPTR -> Bool.False
781     | ACC_PC -> Bool.False
782     | EXT_INDIRECT_DPTR -> Bool.False
783     | INDIRECT_DPTR -> Bool.False
784     | CARRY -> Bool.False
785     | BIT_ADDR x -> Bool.False
786     | N_BIT_ADDR x -> Bool.False
787     | RELATIVE x -> Bool.False
788     | ADDR11 e0 ->
789       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
790         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e0
791     | ADDR16 x -> Bool.False)
792  | ADDR16 w ->
793    (match b with
794     | DIRECT x -> Bool.False
795     | INDIRECT x -> Bool.False
796     | EXT_INDIRECT x -> Bool.False
797     | REGISTER x -> Bool.False
798     | ACC_A -> Bool.False
799     | ACC_B -> Bool.False
800     | DPTR -> Bool.False
801     | DATA x -> Bool.False
802     | DATA16 x -> Bool.False
803     | ACC_DPTR -> Bool.False
804     | ACC_PC -> Bool.False
805     | EXT_INDIRECT_DPTR -> Bool.False
806     | INDIRECT_DPTR -> Bool.False
807     | CARRY -> Bool.False
808     | BIT_ADDR x -> Bool.False
809     | N_BIT_ADDR x -> Bool.False
810     | RELATIVE x -> Bool.False
811     | ADDR11 x -> Bool.False
812     | ADDR16 e0 ->
813       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
814         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
815         Nat.O)))))))))))))))) w e0)
816
817type addressing_mode_tag =
818| Direct
819| Indirect
820| Ext_indirect
821| Registr
822| Acc_a
823| Acc_b
824| Dptr
825| Data
826| Data16
827| Acc_dptr
828| Acc_pc
829| Ext_indirect_dptr
830| Indirect_dptr
831| Carry
832| Bit_addr
833| N_bit_addr
834| Relative
835| Addr11
836| Addr16
837
838(** val addressing_mode_tag_rect_Type4 :
839    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
840    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
841    addressing_mode_tag -> 'a1 **)
842let 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
843| Direct -> h_direct
844| Indirect -> h_indirect
845| Ext_indirect -> h_ext_indirect
846| Registr -> h_registr
847| Acc_a -> h_acc_a
848| Acc_b -> h_acc_b
849| Dptr -> h_dptr
850| Data -> h_data
851| Data16 -> h_data16
852| Acc_dptr -> h_acc_dptr
853| Acc_pc -> h_acc_pc
854| Ext_indirect_dptr -> h_ext_indirect_dptr
855| Indirect_dptr -> h_indirect_dptr
856| Carry -> h_carry
857| Bit_addr -> h_bit_addr
858| N_bit_addr -> h_n_bit_addr
859| Relative -> h_relative
860| Addr11 -> h_addr11
861| Addr16 -> h_addr16
862
863(** val addressing_mode_tag_rect_Type5 :
864    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
865    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
866    addressing_mode_tag -> 'a1 **)
867let 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
868| Direct -> h_direct
869| Indirect -> h_indirect
870| Ext_indirect -> h_ext_indirect
871| Registr -> h_registr
872| Acc_a -> h_acc_a
873| Acc_b -> h_acc_b
874| Dptr -> h_dptr
875| Data -> h_data
876| Data16 -> h_data16
877| Acc_dptr -> h_acc_dptr
878| Acc_pc -> h_acc_pc
879| Ext_indirect_dptr -> h_ext_indirect_dptr
880| Indirect_dptr -> h_indirect_dptr
881| Carry -> h_carry
882| Bit_addr -> h_bit_addr
883| N_bit_addr -> h_n_bit_addr
884| Relative -> h_relative
885| Addr11 -> h_addr11
886| Addr16 -> h_addr16
887
888(** val addressing_mode_tag_rect_Type3 :
889    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
890    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
891    addressing_mode_tag -> 'a1 **)
892let 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
893| Direct -> h_direct
894| Indirect -> h_indirect
895| Ext_indirect -> h_ext_indirect
896| Registr -> h_registr
897| Acc_a -> h_acc_a
898| Acc_b -> h_acc_b
899| Dptr -> h_dptr
900| Data -> h_data
901| Data16 -> h_data16
902| Acc_dptr -> h_acc_dptr
903| Acc_pc -> h_acc_pc
904| Ext_indirect_dptr -> h_ext_indirect_dptr
905| Indirect_dptr -> h_indirect_dptr
906| Carry -> h_carry
907| Bit_addr -> h_bit_addr
908| N_bit_addr -> h_n_bit_addr
909| Relative -> h_relative
910| Addr11 -> h_addr11
911| Addr16 -> h_addr16
912
913(** val addressing_mode_tag_rect_Type2 :
914    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
915    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
916    addressing_mode_tag -> 'a1 **)
917let 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
918| Direct -> h_direct
919| Indirect -> h_indirect
920| Ext_indirect -> h_ext_indirect
921| Registr -> h_registr
922| Acc_a -> h_acc_a
923| Acc_b -> h_acc_b
924| Dptr -> h_dptr
925| Data -> h_data
926| Data16 -> h_data16
927| Acc_dptr -> h_acc_dptr
928| Acc_pc -> h_acc_pc
929| Ext_indirect_dptr -> h_ext_indirect_dptr
930| Indirect_dptr -> h_indirect_dptr
931| Carry -> h_carry
932| Bit_addr -> h_bit_addr
933| N_bit_addr -> h_n_bit_addr
934| Relative -> h_relative
935| Addr11 -> h_addr11
936| Addr16 -> h_addr16
937
938(** val addressing_mode_tag_rect_Type1 :
939    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
940    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
941    addressing_mode_tag -> 'a1 **)
942let 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
943| Direct -> h_direct
944| Indirect -> h_indirect
945| Ext_indirect -> h_ext_indirect
946| Registr -> h_registr
947| Acc_a -> h_acc_a
948| Acc_b -> h_acc_b
949| Dptr -> h_dptr
950| Data -> h_data
951| Data16 -> h_data16
952| Acc_dptr -> h_acc_dptr
953| Acc_pc -> h_acc_pc
954| Ext_indirect_dptr -> h_ext_indirect_dptr
955| Indirect_dptr -> h_indirect_dptr
956| Carry -> h_carry
957| Bit_addr -> h_bit_addr
958| N_bit_addr -> h_n_bit_addr
959| Relative -> h_relative
960| Addr11 -> h_addr11
961| Addr16 -> h_addr16
962
963(** val addressing_mode_tag_rect_Type0 :
964    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
965    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
966    addressing_mode_tag -> 'a1 **)
967let 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
968| Direct -> h_direct
969| Indirect -> h_indirect
970| Ext_indirect -> h_ext_indirect
971| Registr -> h_registr
972| Acc_a -> h_acc_a
973| Acc_b -> h_acc_b
974| Dptr -> h_dptr
975| Data -> h_data
976| Data16 -> h_data16
977| Acc_dptr -> h_acc_dptr
978| Acc_pc -> h_acc_pc
979| Ext_indirect_dptr -> h_ext_indirect_dptr
980| Indirect_dptr -> h_indirect_dptr
981| Carry -> h_carry
982| Bit_addr -> h_bit_addr
983| N_bit_addr -> h_n_bit_addr
984| Relative -> h_relative
985| Addr11 -> h_addr11
986| Addr16 -> h_addr16
987
988(** val addressing_mode_tag_inv_rect_Type4 :
989    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
990    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
991    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
992    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
993    'a1) -> (__ -> 'a1) -> 'a1 **)
994let 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 =
995  let hcut =
996    addressing_mode_tag_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
997      h14 h15 h16 h17 h18 h19 hterm
998  in
999  hcut __
1000
1001(** val addressing_mode_tag_inv_rect_Type3 :
1002    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1003    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1004    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1005    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1006    'a1) -> (__ -> 'a1) -> 'a1 **)
1007let 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 =
1008  let hcut =
1009    addressing_mode_tag_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1010      h14 h15 h16 h17 h18 h19 hterm
1011  in
1012  hcut __
1013
1014(** val addressing_mode_tag_inv_rect_Type2 :
1015    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1016    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1017    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1018    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1019    'a1) -> (__ -> 'a1) -> 'a1 **)
1020let 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 =
1021  let hcut =
1022    addressing_mode_tag_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1023      h14 h15 h16 h17 h18 h19 hterm
1024  in
1025  hcut __
1026
1027(** val addressing_mode_tag_inv_rect_Type1 :
1028    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1029    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1030    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1031    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1032    'a1) -> (__ -> 'a1) -> 'a1 **)
1033let 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 =
1034  let hcut =
1035    addressing_mode_tag_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1036      h14 h15 h16 h17 h18 h19 hterm
1037  in
1038  hcut __
1039
1040(** val addressing_mode_tag_inv_rect_Type0 :
1041    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1042    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1043    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1044    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1045    'a1) -> (__ -> 'a1) -> 'a1 **)
1046let 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 =
1047  let hcut =
1048    addressing_mode_tag_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1049      h14 h15 h16 h17 h18 h19 hterm
1050  in
1051  hcut __
1052
1053(** val addressing_mode_tag_discr :
1054    addressing_mode_tag -> addressing_mode_tag -> __ **)
1055let addressing_mode_tag_discr x y =
1056  Logic.eq_rect_Type2 x
1057    (match x with
1058     | Direct -> Obj.magic (fun _ dH -> dH)
1059     | Indirect -> Obj.magic (fun _ dH -> dH)
1060     | Ext_indirect -> Obj.magic (fun _ dH -> dH)
1061     | Registr -> Obj.magic (fun _ dH -> dH)
1062     | Acc_a -> Obj.magic (fun _ dH -> dH)
1063     | Acc_b -> Obj.magic (fun _ dH -> dH)
1064     | Dptr -> Obj.magic (fun _ dH -> dH)
1065     | Data -> Obj.magic (fun _ dH -> dH)
1066     | Data16 -> Obj.magic (fun _ dH -> dH)
1067     | Acc_dptr -> Obj.magic (fun _ dH -> dH)
1068     | Acc_pc -> Obj.magic (fun _ dH -> dH)
1069     | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH)
1070     | Indirect_dptr -> Obj.magic (fun _ dH -> dH)
1071     | Carry -> Obj.magic (fun _ dH -> dH)
1072     | Bit_addr -> Obj.magic (fun _ dH -> dH)
1073     | N_bit_addr -> Obj.magic (fun _ dH -> dH)
1074     | Relative -> Obj.magic (fun _ dH -> dH)
1075     | Addr11 -> Obj.magic (fun _ dH -> dH)
1076     | Addr16 -> Obj.magic (fun _ dH -> dH)) y
1077
1078(** val addressing_mode_tag_jmdiscr :
1079    addressing_mode_tag -> addressing_mode_tag -> __ **)
1080let addressing_mode_tag_jmdiscr x y =
1081  Logic.eq_rect_Type2 x
1082    (match x with
1083     | Direct -> Obj.magic (fun _ dH -> dH)
1084     | Indirect -> Obj.magic (fun _ dH -> dH)
1085     | Ext_indirect -> Obj.magic (fun _ dH -> dH)
1086     | Registr -> Obj.magic (fun _ dH -> dH)
1087     | Acc_a -> Obj.magic (fun _ dH -> dH)
1088     | Acc_b -> Obj.magic (fun _ dH -> dH)
1089     | Dptr -> Obj.magic (fun _ dH -> dH)
1090     | Data -> Obj.magic (fun _ dH -> dH)
1091     | Data16 -> Obj.magic (fun _ dH -> dH)
1092     | Acc_dptr -> Obj.magic (fun _ dH -> dH)
1093     | Acc_pc -> Obj.magic (fun _ dH -> dH)
1094     | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH)
1095     | Indirect_dptr -> Obj.magic (fun _ dH -> dH)
1096     | Carry -> Obj.magic (fun _ dH -> dH)
1097     | Bit_addr -> Obj.magic (fun _ dH -> dH)
1098     | N_bit_addr -> Obj.magic (fun _ dH -> dH)
1099     | Relative -> Obj.magic (fun _ dH -> dH)
1100     | Addr11 -> Obj.magic (fun _ dH -> dH)
1101     | Addr16 -> Obj.magic (fun _ dH -> dH)) y
1102
1103(** val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool **)
1104let eq_a a b =
1105  match a with
1106  | Direct ->
1107    (match b with
1108     | Direct -> Bool.True
1109     | Indirect -> Bool.False
1110     | Ext_indirect -> Bool.False
1111     | Registr -> Bool.False
1112     | Acc_a -> Bool.False
1113     | Acc_b -> Bool.False
1114     | Dptr -> Bool.False
1115     | Data -> Bool.False
1116     | Data16 -> Bool.False
1117     | Acc_dptr -> Bool.False
1118     | Acc_pc -> Bool.False
1119     | Ext_indirect_dptr -> Bool.False
1120     | Indirect_dptr -> Bool.False
1121     | Carry -> Bool.False
1122     | Bit_addr -> Bool.False
1123     | N_bit_addr -> Bool.False
1124     | Relative -> Bool.False
1125     | Addr11 -> Bool.False
1126     | Addr16 -> Bool.False)
1127  | Indirect ->
1128    (match b with
1129     | Direct -> Bool.False
1130     | Indirect -> Bool.True
1131     | Ext_indirect -> Bool.False
1132     | Registr -> Bool.False
1133     | Acc_a -> Bool.False
1134     | Acc_b -> Bool.False
1135     | Dptr -> Bool.False
1136     | Data -> Bool.False
1137     | Data16 -> Bool.False
1138     | Acc_dptr -> Bool.False
1139     | Acc_pc -> Bool.False
1140     | Ext_indirect_dptr -> Bool.False
1141     | Indirect_dptr -> Bool.False
1142     | Carry -> Bool.False
1143     | Bit_addr -> Bool.False
1144     | N_bit_addr -> Bool.False
1145     | Relative -> Bool.False
1146     | Addr11 -> Bool.False
1147     | Addr16 -> Bool.False)
1148  | Ext_indirect ->
1149    (match b with
1150     | Direct -> Bool.False
1151     | Indirect -> Bool.False
1152     | Ext_indirect -> Bool.True
1153     | Registr -> Bool.False
1154     | Acc_a -> Bool.False
1155     | Acc_b -> Bool.False
1156     | Dptr -> Bool.False
1157     | Data -> Bool.False
1158     | Data16 -> Bool.False
1159     | Acc_dptr -> Bool.False
1160     | Acc_pc -> Bool.False
1161     | Ext_indirect_dptr -> Bool.False
1162     | Indirect_dptr -> Bool.False
1163     | Carry -> Bool.False
1164     | Bit_addr -> Bool.False
1165     | N_bit_addr -> Bool.False
1166     | Relative -> Bool.False
1167     | Addr11 -> Bool.False
1168     | Addr16 -> Bool.False)
1169  | Registr ->
1170    (match b with
1171     | Direct -> Bool.False
1172     | Indirect -> Bool.False
1173     | Ext_indirect -> Bool.False
1174     | Registr -> Bool.True
1175     | Acc_a -> Bool.False
1176     | Acc_b -> Bool.False
1177     | Dptr -> Bool.False
1178     | Data -> Bool.False
1179     | Data16 -> Bool.False
1180     | Acc_dptr -> Bool.False
1181     | Acc_pc -> Bool.False
1182     | Ext_indirect_dptr -> Bool.False
1183     | Indirect_dptr -> Bool.False
1184     | Carry -> Bool.False
1185     | Bit_addr -> Bool.False
1186     | N_bit_addr -> Bool.False
1187     | Relative -> Bool.False
1188     | Addr11 -> Bool.False
1189     | Addr16 -> Bool.False)
1190  | Acc_a ->
1191    (match b with
1192     | Direct -> Bool.False
1193     | Indirect -> Bool.False
1194     | Ext_indirect -> Bool.False
1195     | Registr -> Bool.False
1196     | Acc_a -> Bool.True
1197     | Acc_b -> Bool.False
1198     | Dptr -> Bool.False
1199     | Data -> Bool.False
1200     | Data16 -> Bool.False
1201     | Acc_dptr -> Bool.False
1202     | Acc_pc -> Bool.False
1203     | Ext_indirect_dptr -> Bool.False
1204     | Indirect_dptr -> Bool.False
1205     | Carry -> Bool.False
1206     | Bit_addr -> Bool.False
1207     | N_bit_addr -> Bool.False
1208     | Relative -> Bool.False
1209     | Addr11 -> Bool.False
1210     | Addr16 -> Bool.False)
1211  | Acc_b ->
1212    (match b with
1213     | Direct -> Bool.False
1214     | Indirect -> Bool.False
1215     | Ext_indirect -> Bool.False
1216     | Registr -> Bool.False
1217     | Acc_a -> Bool.False
1218     | Acc_b -> Bool.True
1219     | Dptr -> Bool.False
1220     | Data -> Bool.False
1221     | Data16 -> Bool.False
1222     | Acc_dptr -> Bool.False
1223     | Acc_pc -> Bool.False
1224     | Ext_indirect_dptr -> Bool.False
1225     | Indirect_dptr -> Bool.False
1226     | Carry -> Bool.False
1227     | Bit_addr -> Bool.False
1228     | N_bit_addr -> Bool.False
1229     | Relative -> Bool.False
1230     | Addr11 -> Bool.False
1231     | Addr16 -> Bool.False)
1232  | Dptr ->
1233    (match b with
1234     | Direct -> Bool.False
1235     | Indirect -> Bool.False
1236     | Ext_indirect -> Bool.False
1237     | Registr -> Bool.False
1238     | Acc_a -> Bool.False
1239     | Acc_b -> Bool.False
1240     | Dptr -> Bool.True
1241     | Data -> Bool.False
1242     | Data16 -> Bool.False
1243     | Acc_dptr -> Bool.False
1244     | Acc_pc -> Bool.False
1245     | Ext_indirect_dptr -> Bool.False
1246     | Indirect_dptr -> Bool.False
1247     | Carry -> Bool.False
1248     | Bit_addr -> Bool.False
1249     | N_bit_addr -> Bool.False
1250     | Relative -> Bool.False
1251     | Addr11 -> Bool.False
1252     | Addr16 -> Bool.False)
1253  | Data ->
1254    (match b with
1255     | Direct -> Bool.False
1256     | Indirect -> Bool.False
1257     | Ext_indirect -> Bool.False
1258     | Registr -> Bool.False
1259     | Acc_a -> Bool.False
1260     | Acc_b -> Bool.False
1261     | Dptr -> Bool.False
1262     | Data -> Bool.True
1263     | Data16 -> Bool.False
1264     | Acc_dptr -> Bool.False
1265     | Acc_pc -> Bool.False
1266     | Ext_indirect_dptr -> Bool.False
1267     | Indirect_dptr -> Bool.False
1268     | Carry -> Bool.False
1269     | Bit_addr -> Bool.False
1270     | N_bit_addr -> Bool.False
1271     | Relative -> Bool.False
1272     | Addr11 -> Bool.False
1273     | Addr16 -> Bool.False)
1274  | Data16 ->
1275    (match b with
1276     | Direct -> Bool.False
1277     | Indirect -> Bool.False
1278     | Ext_indirect -> Bool.False
1279     | Registr -> Bool.False
1280     | Acc_a -> Bool.False
1281     | Acc_b -> Bool.False
1282     | Dptr -> Bool.False
1283     | Data -> Bool.False
1284     | Data16 -> Bool.True
1285     | Acc_dptr -> Bool.False
1286     | Acc_pc -> Bool.False
1287     | Ext_indirect_dptr -> Bool.False
1288     | Indirect_dptr -> Bool.False
1289     | Carry -> Bool.False
1290     | Bit_addr -> Bool.False
1291     | N_bit_addr -> Bool.False
1292     | Relative -> Bool.False
1293     | Addr11 -> Bool.False
1294     | Addr16 -> Bool.False)
1295  | Acc_dptr ->
1296    (match b with
1297     | Direct -> Bool.False
1298     | Indirect -> Bool.False
1299     | Ext_indirect -> Bool.False
1300     | Registr -> Bool.False
1301     | Acc_a -> Bool.False
1302     | Acc_b -> Bool.False
1303     | Dptr -> Bool.False
1304     | Data -> Bool.False
1305     | Data16 -> Bool.False
1306     | Acc_dptr -> Bool.True
1307     | Acc_pc -> Bool.False
1308     | Ext_indirect_dptr -> Bool.False
1309     | Indirect_dptr -> Bool.False
1310     | Carry -> Bool.False
1311     | Bit_addr -> Bool.False
1312     | N_bit_addr -> Bool.False
1313     | Relative -> Bool.False
1314     | Addr11 -> Bool.False
1315     | Addr16 -> Bool.False)
1316  | Acc_pc ->
1317    (match b with
1318     | Direct -> Bool.False
1319     | Indirect -> Bool.False
1320     | Ext_indirect -> Bool.False
1321     | Registr -> Bool.False
1322     | Acc_a -> Bool.False
1323     | Acc_b -> Bool.False
1324     | Dptr -> Bool.False
1325     | Data -> Bool.False
1326     | Data16 -> Bool.False
1327     | Acc_dptr -> Bool.False
1328     | Acc_pc -> Bool.True
1329     | Ext_indirect_dptr -> Bool.False
1330     | Indirect_dptr -> Bool.False
1331     | Carry -> Bool.False
1332     | Bit_addr -> Bool.False
1333     | N_bit_addr -> Bool.False
1334     | Relative -> Bool.False
1335     | Addr11 -> Bool.False
1336     | Addr16 -> Bool.False)
1337  | Ext_indirect_dptr ->
1338    (match b with
1339     | Direct -> Bool.False
1340     | Indirect -> Bool.False
1341     | Ext_indirect -> Bool.False
1342     | Registr -> Bool.False
1343     | Acc_a -> Bool.False
1344     | Acc_b -> Bool.False
1345     | Dptr -> Bool.False
1346     | Data -> Bool.False
1347     | Data16 -> Bool.False
1348     | Acc_dptr -> Bool.False
1349     | Acc_pc -> Bool.False
1350     | Ext_indirect_dptr -> Bool.True
1351     | Indirect_dptr -> Bool.False
1352     | Carry -> Bool.False
1353     | Bit_addr -> Bool.False
1354     | N_bit_addr -> Bool.False
1355     | Relative -> Bool.False
1356     | Addr11 -> Bool.False
1357     | Addr16 -> Bool.False)
1358  | Indirect_dptr ->
1359    (match b with
1360     | Direct -> Bool.False
1361     | Indirect -> Bool.False
1362     | Ext_indirect -> Bool.False
1363     | Registr -> Bool.False
1364     | Acc_a -> Bool.False
1365     | Acc_b -> Bool.False
1366     | Dptr -> Bool.False
1367     | Data -> Bool.False
1368     | Data16 -> Bool.False
1369     | Acc_dptr -> Bool.False
1370     | Acc_pc -> Bool.False
1371     | Ext_indirect_dptr -> Bool.False
1372     | Indirect_dptr -> Bool.True
1373     | Carry -> Bool.False
1374     | Bit_addr -> Bool.False
1375     | N_bit_addr -> Bool.False
1376     | Relative -> Bool.False
1377     | Addr11 -> Bool.False
1378     | Addr16 -> Bool.False)
1379  | Carry ->
1380    (match b with
1381     | Direct -> Bool.False
1382     | Indirect -> Bool.False
1383     | Ext_indirect -> Bool.False
1384     | Registr -> Bool.False
1385     | Acc_a -> Bool.False
1386     | Acc_b -> Bool.False
1387     | Dptr -> Bool.False
1388     | Data -> Bool.False
1389     | Data16 -> Bool.False
1390     | Acc_dptr -> Bool.False
1391     | Acc_pc -> Bool.False
1392     | Ext_indirect_dptr -> Bool.False
1393     | Indirect_dptr -> Bool.False
1394     | Carry -> Bool.True
1395     | Bit_addr -> Bool.False
1396     | N_bit_addr -> Bool.False
1397     | Relative -> Bool.False
1398     | Addr11 -> Bool.False
1399     | Addr16 -> Bool.False)
1400  | Bit_addr ->
1401    (match b with
1402     | Direct -> Bool.False
1403     | Indirect -> Bool.False
1404     | Ext_indirect -> Bool.False
1405     | Registr -> Bool.False
1406     | Acc_a -> Bool.False
1407     | Acc_b -> Bool.False
1408     | Dptr -> Bool.False
1409     | Data -> Bool.False
1410     | Data16 -> Bool.False
1411     | Acc_dptr -> Bool.False
1412     | Acc_pc -> Bool.False
1413     | Ext_indirect_dptr -> Bool.False
1414     | Indirect_dptr -> Bool.False
1415     | Carry -> Bool.False
1416     | Bit_addr -> Bool.True
1417     | N_bit_addr -> Bool.False
1418     | Relative -> Bool.False
1419     | Addr11 -> Bool.False
1420     | Addr16 -> Bool.False)
1421  | N_bit_addr ->
1422    (match b with
1423     | Direct -> Bool.False
1424     | Indirect -> Bool.False
1425     | Ext_indirect -> Bool.False
1426     | Registr -> Bool.False
1427     | Acc_a -> Bool.False
1428     | Acc_b -> Bool.False
1429     | Dptr -> Bool.False
1430     | Data -> Bool.False
1431     | Data16 -> Bool.False
1432     | Acc_dptr -> Bool.False
1433     | Acc_pc -> Bool.False
1434     | Ext_indirect_dptr -> Bool.False
1435     | Indirect_dptr -> Bool.False
1436     | Carry -> Bool.False
1437     | Bit_addr -> Bool.False
1438     | N_bit_addr -> Bool.True
1439     | Relative -> Bool.False
1440     | Addr11 -> Bool.False
1441     | Addr16 -> Bool.False)
1442  | Relative ->
1443    (match b with
1444     | Direct -> Bool.False
1445     | Indirect -> Bool.False
1446     | Ext_indirect -> Bool.False
1447     | Registr -> Bool.False
1448     | Acc_a -> Bool.False
1449     | Acc_b -> Bool.False
1450     | Dptr -> Bool.False
1451     | Data -> Bool.False
1452     | Data16 -> Bool.False
1453     | Acc_dptr -> Bool.False
1454     | Acc_pc -> Bool.False
1455     | Ext_indirect_dptr -> Bool.False
1456     | Indirect_dptr -> Bool.False
1457     | Carry -> Bool.False
1458     | Bit_addr -> Bool.False
1459     | N_bit_addr -> Bool.False
1460     | Relative -> Bool.True
1461     | Addr11 -> Bool.False
1462     | Addr16 -> Bool.False)
1463  | Addr11 ->
1464    (match b with
1465     | Direct -> Bool.False
1466     | Indirect -> Bool.False
1467     | Ext_indirect -> Bool.False
1468     | Registr -> Bool.False
1469     | Acc_a -> Bool.False
1470     | Acc_b -> Bool.False
1471     | Dptr -> Bool.False
1472     | Data -> Bool.False
1473     | Data16 -> Bool.False
1474     | Acc_dptr -> Bool.False
1475     | Acc_pc -> Bool.False
1476     | Ext_indirect_dptr -> Bool.False
1477     | Indirect_dptr -> Bool.False
1478     | Carry -> Bool.False
1479     | Bit_addr -> Bool.False
1480     | N_bit_addr -> Bool.False
1481     | Relative -> Bool.False
1482     | Addr11 -> Bool.True
1483     | Addr16 -> Bool.False)
1484  | Addr16 ->
1485    (match b with
1486     | Direct -> Bool.False
1487     | Indirect -> Bool.False
1488     | Ext_indirect -> Bool.False
1489     | Registr -> Bool.False
1490     | Acc_a -> Bool.False
1491     | Acc_b -> Bool.False
1492     | Dptr -> Bool.False
1493     | Data -> Bool.False
1494     | Data16 -> Bool.False
1495     | Acc_dptr -> Bool.False
1496     | Acc_pc -> Bool.False
1497     | Ext_indirect_dptr -> Bool.False
1498     | Indirect_dptr -> Bool.False
1499     | Carry -> Bool.False
1500     | Bit_addr -> Bool.False
1501     | N_bit_addr -> Bool.False
1502     | Relative -> Bool.False
1503     | Addr11 -> Bool.False
1504     | Addr16 -> Bool.True)
1505
1506type member_addressing_mode_tag = __
1507
1508(** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **)
1509let rec is_a d a =
1510  match d with
1511  | Direct ->
1512    (match a with
1513     | DIRECT x -> Bool.True
1514     | INDIRECT x -> Bool.False
1515     | EXT_INDIRECT x -> Bool.False
1516     | REGISTER x -> Bool.False
1517     | ACC_A -> Bool.False
1518     | ACC_B -> Bool.False
1519     | DPTR -> Bool.False
1520     | DATA x -> Bool.False
1521     | DATA16 x -> Bool.False
1522     | ACC_DPTR -> Bool.False
1523     | ACC_PC -> Bool.False
1524     | EXT_INDIRECT_DPTR -> Bool.False
1525     | INDIRECT_DPTR -> Bool.False
1526     | CARRY -> Bool.False
1527     | BIT_ADDR x -> Bool.False
1528     | N_BIT_ADDR x -> Bool.False
1529     | RELATIVE x -> Bool.False
1530     | ADDR11 x -> Bool.False
1531     | ADDR16 x -> Bool.False)
1532  | Indirect ->
1533    (match a with
1534     | DIRECT x -> Bool.False
1535     | INDIRECT x -> Bool.True
1536     | EXT_INDIRECT x -> Bool.False
1537     | REGISTER x -> Bool.False
1538     | ACC_A -> Bool.False
1539     | ACC_B -> Bool.False
1540     | DPTR -> Bool.False
1541     | DATA x -> Bool.False
1542     | DATA16 x -> Bool.False
1543     | ACC_DPTR -> Bool.False
1544     | ACC_PC -> Bool.False
1545     | EXT_INDIRECT_DPTR -> Bool.False
1546     | INDIRECT_DPTR -> Bool.False
1547     | CARRY -> Bool.False
1548     | BIT_ADDR x -> Bool.False
1549     | N_BIT_ADDR x -> Bool.False
1550     | RELATIVE x -> Bool.False
1551     | ADDR11 x -> Bool.False
1552     | ADDR16 x -> Bool.False)
1553  | Ext_indirect ->
1554    (match a with
1555     | DIRECT x -> Bool.False
1556     | INDIRECT x -> Bool.False
1557     | EXT_INDIRECT x -> Bool.True
1558     | REGISTER x -> Bool.False
1559     | ACC_A -> Bool.False
1560     | ACC_B -> Bool.False
1561     | DPTR -> Bool.False
1562     | DATA x -> Bool.False
1563     | DATA16 x -> Bool.False
1564     | ACC_DPTR -> Bool.False
1565     | ACC_PC -> Bool.False
1566     | EXT_INDIRECT_DPTR -> Bool.False
1567     | INDIRECT_DPTR -> Bool.False
1568     | CARRY -> Bool.False
1569     | BIT_ADDR x -> Bool.False
1570     | N_BIT_ADDR x -> Bool.False
1571     | RELATIVE x -> Bool.False
1572     | ADDR11 x -> Bool.False
1573     | ADDR16 x -> Bool.False)
1574  | Registr ->
1575    (match a with
1576     | DIRECT x -> Bool.False
1577     | INDIRECT x -> Bool.False
1578     | EXT_INDIRECT x -> Bool.False
1579     | REGISTER x -> Bool.True
1580     | ACC_A -> Bool.False
1581     | ACC_B -> Bool.False
1582     | DPTR -> Bool.False
1583     | DATA x -> Bool.False
1584     | DATA16 x -> Bool.False
1585     | ACC_DPTR -> Bool.False
1586     | ACC_PC -> Bool.False
1587     | EXT_INDIRECT_DPTR -> Bool.False
1588     | INDIRECT_DPTR -> Bool.False
1589     | CARRY -> Bool.False
1590     | BIT_ADDR x -> Bool.False
1591     | N_BIT_ADDR x -> Bool.False
1592     | RELATIVE x -> Bool.False
1593     | ADDR11 x -> Bool.False
1594     | ADDR16 x -> Bool.False)
1595  | Acc_a ->
1596    (match a with
1597     | DIRECT x -> Bool.False
1598     | INDIRECT x -> Bool.False
1599     | EXT_INDIRECT x -> Bool.False
1600     | REGISTER x -> Bool.False
1601     | ACC_A -> Bool.True
1602     | ACC_B -> Bool.False
1603     | DPTR -> Bool.False
1604     | DATA x -> Bool.False
1605     | DATA16 x -> Bool.False
1606     | ACC_DPTR -> Bool.False
1607     | ACC_PC -> Bool.False
1608     | EXT_INDIRECT_DPTR -> Bool.False
1609     | INDIRECT_DPTR -> Bool.False
1610     | CARRY -> Bool.False
1611     | BIT_ADDR x -> Bool.False
1612     | N_BIT_ADDR x -> Bool.False
1613     | RELATIVE x -> Bool.False
1614     | ADDR11 x -> Bool.False
1615     | ADDR16 x -> Bool.False)
1616  | Acc_b ->
1617    (match a with
1618     | DIRECT x -> Bool.False
1619     | INDIRECT x -> Bool.False
1620     | EXT_INDIRECT x -> Bool.False
1621     | REGISTER x -> Bool.False
1622     | ACC_A -> Bool.False
1623     | ACC_B -> Bool.True
1624     | DPTR -> Bool.False
1625     | DATA x -> Bool.False
1626     | DATA16 x -> Bool.False
1627     | ACC_DPTR -> Bool.False
1628     | ACC_PC -> Bool.False
1629     | EXT_INDIRECT_DPTR -> Bool.False
1630     | INDIRECT_DPTR -> Bool.False
1631     | CARRY -> Bool.False
1632     | BIT_ADDR x -> Bool.False
1633     | N_BIT_ADDR x -> Bool.False
1634     | RELATIVE x -> Bool.False
1635     | ADDR11 x -> Bool.False
1636     | ADDR16 x -> Bool.False)
1637  | Dptr ->
1638    (match a with
1639     | DIRECT x -> Bool.False
1640     | INDIRECT x -> Bool.False
1641     | EXT_INDIRECT x -> Bool.False
1642     | REGISTER x -> Bool.False
1643     | ACC_A -> Bool.False
1644     | ACC_B -> Bool.False
1645     | DPTR -> Bool.True
1646     | DATA x -> Bool.False
1647     | DATA16 x -> Bool.False
1648     | ACC_DPTR -> Bool.False
1649     | ACC_PC -> Bool.False
1650     | EXT_INDIRECT_DPTR -> Bool.False
1651     | INDIRECT_DPTR -> Bool.False
1652     | CARRY -> Bool.False
1653     | BIT_ADDR x -> Bool.False
1654     | N_BIT_ADDR x -> Bool.False
1655     | RELATIVE x -> Bool.False
1656     | ADDR11 x -> Bool.False
1657     | ADDR16 x -> Bool.False)
1658  | Data ->
1659    (match a with
1660     | DIRECT x -> Bool.False
1661     | INDIRECT x -> Bool.False
1662     | EXT_INDIRECT x -> Bool.False
1663     | REGISTER x -> Bool.False
1664     | ACC_A -> Bool.False
1665     | ACC_B -> Bool.False
1666     | DPTR -> Bool.False
1667     | DATA x -> Bool.True
1668     | DATA16 x -> Bool.False
1669     | ACC_DPTR -> Bool.False
1670     | ACC_PC -> Bool.False
1671     | EXT_INDIRECT_DPTR -> Bool.False
1672     | INDIRECT_DPTR -> Bool.False
1673     | CARRY -> Bool.False
1674     | BIT_ADDR x -> Bool.False
1675     | N_BIT_ADDR x -> Bool.False
1676     | RELATIVE x -> Bool.False
1677     | ADDR11 x -> Bool.False
1678     | ADDR16 x -> Bool.False)
1679  | Data16 ->
1680    (match a with
1681     | DIRECT x -> Bool.False
1682     | INDIRECT x -> Bool.False
1683     | EXT_INDIRECT x -> Bool.False
1684     | REGISTER x -> Bool.False
1685     | ACC_A -> Bool.False
1686     | ACC_B -> Bool.False
1687     | DPTR -> Bool.False
1688     | DATA x -> Bool.False
1689     | DATA16 x -> Bool.True
1690     | ACC_DPTR -> Bool.False
1691     | ACC_PC -> Bool.False
1692     | EXT_INDIRECT_DPTR -> Bool.False
1693     | INDIRECT_DPTR -> Bool.False
1694     | CARRY -> Bool.False
1695     | BIT_ADDR x -> Bool.False
1696     | N_BIT_ADDR x -> Bool.False
1697     | RELATIVE x -> Bool.False
1698     | ADDR11 x -> Bool.False
1699     | ADDR16 x -> Bool.False)
1700  | Acc_dptr ->
1701    (match a with
1702     | DIRECT x -> Bool.False
1703     | INDIRECT x -> Bool.False
1704     | EXT_INDIRECT x -> Bool.False
1705     | REGISTER x -> Bool.False
1706     | ACC_A -> Bool.False
1707     | ACC_B -> Bool.False
1708     | DPTR -> Bool.False
1709     | DATA x -> Bool.False
1710     | DATA16 x -> Bool.False
1711     | ACC_DPTR -> Bool.True
1712     | ACC_PC -> Bool.False
1713     | EXT_INDIRECT_DPTR -> Bool.False
1714     | INDIRECT_DPTR -> Bool.False
1715     | CARRY -> Bool.False
1716     | BIT_ADDR x -> Bool.False
1717     | N_BIT_ADDR x -> Bool.False
1718     | RELATIVE x -> Bool.False
1719     | ADDR11 x -> Bool.False
1720     | ADDR16 x -> Bool.False)
1721  | Acc_pc ->
1722    (match a with
1723     | DIRECT x -> Bool.False
1724     | INDIRECT x -> Bool.False
1725     | EXT_INDIRECT x -> Bool.False
1726     | REGISTER x -> Bool.False
1727     | ACC_A -> Bool.False
1728     | ACC_B -> Bool.False
1729     | DPTR -> Bool.False
1730     | DATA x -> Bool.False
1731     | DATA16 x -> Bool.False
1732     | ACC_DPTR -> Bool.False
1733     | ACC_PC -> Bool.True
1734     | EXT_INDIRECT_DPTR -> Bool.False
1735     | INDIRECT_DPTR -> Bool.False
1736     | CARRY -> Bool.False
1737     | BIT_ADDR x -> Bool.False
1738     | N_BIT_ADDR x -> Bool.False
1739     | RELATIVE x -> Bool.False
1740     | ADDR11 x -> Bool.False
1741     | ADDR16 x -> Bool.False)
1742  | Ext_indirect_dptr ->
1743    (match a with
1744     | DIRECT x -> Bool.False
1745     | INDIRECT x -> Bool.False
1746     | EXT_INDIRECT x -> Bool.False
1747     | REGISTER x -> Bool.False
1748     | ACC_A -> Bool.False
1749     | ACC_B -> Bool.False
1750     | DPTR -> Bool.False
1751     | DATA x -> Bool.False
1752     | DATA16 x -> Bool.False
1753     | ACC_DPTR -> Bool.False
1754     | ACC_PC -> Bool.False
1755     | EXT_INDIRECT_DPTR -> Bool.True
1756     | INDIRECT_DPTR -> Bool.False
1757     | CARRY -> Bool.False
1758     | BIT_ADDR x -> Bool.False
1759     | N_BIT_ADDR x -> Bool.False
1760     | RELATIVE x -> Bool.False
1761     | ADDR11 x -> Bool.False
1762     | ADDR16 x -> Bool.False)
1763  | Indirect_dptr ->
1764    (match a with
1765     | DIRECT x -> Bool.False
1766     | INDIRECT x -> Bool.False
1767     | EXT_INDIRECT x -> Bool.False
1768     | REGISTER x -> Bool.False
1769     | ACC_A -> Bool.False
1770     | ACC_B -> Bool.False
1771     | DPTR -> Bool.False
1772     | DATA x -> Bool.False
1773     | DATA16 x -> Bool.False
1774     | ACC_DPTR -> Bool.False
1775     | ACC_PC -> Bool.False
1776     | EXT_INDIRECT_DPTR -> Bool.False
1777     | INDIRECT_DPTR -> Bool.True
1778     | CARRY -> Bool.False
1779     | BIT_ADDR x -> Bool.False
1780     | N_BIT_ADDR x -> Bool.False
1781     | RELATIVE x -> Bool.False
1782     | ADDR11 x -> Bool.False
1783     | ADDR16 x -> Bool.False)
1784  | Carry ->
1785    (match a with
1786     | DIRECT x -> Bool.False
1787     | INDIRECT x -> Bool.False
1788     | EXT_INDIRECT x -> Bool.False
1789     | REGISTER x -> Bool.False
1790     | ACC_A -> Bool.False
1791     | ACC_B -> Bool.False
1792     | DPTR -> Bool.False
1793     | DATA x -> Bool.False
1794     | DATA16 x -> Bool.False
1795     | ACC_DPTR -> Bool.False
1796     | ACC_PC -> Bool.False
1797     | EXT_INDIRECT_DPTR -> Bool.False
1798     | INDIRECT_DPTR -> Bool.False
1799     | CARRY -> Bool.True
1800     | BIT_ADDR x -> Bool.False
1801     | N_BIT_ADDR x -> Bool.False
1802     | RELATIVE x -> Bool.False
1803     | ADDR11 x -> Bool.False
1804     | ADDR16 x -> Bool.False)
1805  | Bit_addr ->
1806    (match a with
1807     | DIRECT x -> Bool.False
1808     | INDIRECT x -> Bool.False
1809     | EXT_INDIRECT x -> Bool.False
1810     | REGISTER x -> Bool.False
1811     | ACC_A -> Bool.False
1812     | ACC_B -> Bool.False
1813     | DPTR -> Bool.False
1814     | DATA x -> Bool.False
1815     | DATA16 x -> Bool.False
1816     | ACC_DPTR -> Bool.False
1817     | ACC_PC -> Bool.False
1818     | EXT_INDIRECT_DPTR -> Bool.False
1819     | INDIRECT_DPTR -> Bool.False
1820     | CARRY -> Bool.False
1821     | BIT_ADDR x -> Bool.True
1822     | N_BIT_ADDR x -> Bool.False
1823     | RELATIVE x -> Bool.False
1824     | ADDR11 x -> Bool.False
1825     | ADDR16 x -> Bool.False)
1826  | N_bit_addr ->
1827    (match a with
1828     | DIRECT x -> Bool.False
1829     | INDIRECT x -> Bool.False
1830     | EXT_INDIRECT x -> Bool.False
1831     | REGISTER x -> Bool.False
1832     | ACC_A -> Bool.False
1833     | ACC_B -> Bool.False
1834     | DPTR -> Bool.False
1835     | DATA x -> Bool.False
1836     | DATA16 x -> Bool.False
1837     | ACC_DPTR -> Bool.False
1838     | ACC_PC -> Bool.False
1839     | EXT_INDIRECT_DPTR -> Bool.False
1840     | INDIRECT_DPTR -> Bool.False
1841     | CARRY -> Bool.False
1842     | BIT_ADDR x -> Bool.False
1843     | N_BIT_ADDR x -> Bool.True
1844     | RELATIVE x -> Bool.False
1845     | ADDR11 x -> Bool.False
1846     | ADDR16 x -> Bool.False)
1847  | Relative ->
1848    (match a with
1849     | DIRECT x -> Bool.False
1850     | INDIRECT x -> Bool.False
1851     | EXT_INDIRECT x -> Bool.False
1852     | REGISTER x -> Bool.False
1853     | ACC_A -> Bool.False
1854     | ACC_B -> Bool.False
1855     | DPTR -> Bool.False
1856     | DATA x -> Bool.False
1857     | DATA16 x -> Bool.False
1858     | ACC_DPTR -> Bool.False
1859     | ACC_PC -> Bool.False
1860     | EXT_INDIRECT_DPTR -> Bool.False
1861     | INDIRECT_DPTR -> Bool.False
1862     | CARRY -> Bool.False
1863     | BIT_ADDR x -> Bool.False
1864     | N_BIT_ADDR x -> Bool.False
1865     | RELATIVE x -> Bool.True
1866     | ADDR11 x -> Bool.False
1867     | ADDR16 x -> Bool.False)
1868  | Addr11 ->
1869    (match a with
1870     | DIRECT x -> Bool.False
1871     | INDIRECT x -> Bool.False
1872     | EXT_INDIRECT x -> Bool.False
1873     | REGISTER x -> Bool.False
1874     | ACC_A -> Bool.False
1875     | ACC_B -> Bool.False
1876     | DPTR -> Bool.False
1877     | DATA x -> Bool.False
1878     | DATA16 x -> Bool.False
1879     | ACC_DPTR -> Bool.False
1880     | ACC_PC -> Bool.False
1881     | EXT_INDIRECT_DPTR -> Bool.False
1882     | INDIRECT_DPTR -> Bool.False
1883     | CARRY -> Bool.False
1884     | BIT_ADDR x -> Bool.False
1885     | N_BIT_ADDR x -> Bool.False
1886     | RELATIVE x -> Bool.False
1887     | ADDR11 x -> Bool.True
1888     | ADDR16 x -> Bool.False)
1889  | Addr16 ->
1890    (match a with
1891     | DIRECT x -> Bool.False
1892     | INDIRECT x -> Bool.False
1893     | EXT_INDIRECT x -> Bool.False
1894     | REGISTER x -> Bool.False
1895     | ACC_A -> Bool.False
1896     | ACC_B -> Bool.False
1897     | DPTR -> Bool.False
1898     | DATA x -> Bool.False
1899     | DATA16 x -> Bool.False
1900     | ACC_DPTR -> Bool.False
1901     | ACC_PC -> Bool.False
1902     | EXT_INDIRECT_DPTR -> Bool.False
1903     | INDIRECT_DPTR -> Bool.False
1904     | CARRY -> Bool.False
1905     | BIT_ADDR x -> Bool.False
1906     | N_BIT_ADDR x -> Bool.False
1907     | RELATIVE x -> Bool.False
1908     | ADDR11 x -> Bool.False
1909     | ADDR16 x -> Bool.True)
1910
1911(** val is_in :
1912    Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
1913    Bool.bool **)
1914let rec is_in n l a =
1915  match l with
1916  | Vector.VEmpty -> Bool.False
1917  | Vector.VCons (m, he, tl) -> Bool.orb (is_a he a) (is_in m tl a)
1918
1919type subaddressing_mode =
1920  addressing_mode
1921  (* singleton inductive, whose constructor was mk_subaddressing_mode *)
1922
1923(** val subaddressing_mode_rect_Type4 :
1924    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1925    'a1) -> subaddressing_mode -> 'a1 **)
1926let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_692 =
1927  let subaddressing_modeel = x_692 in
1928  h_mk_subaddressing_mode subaddressing_modeel __
1929
1930(** val subaddressing_mode_rect_Type5 :
1931    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1932    'a1) -> subaddressing_mode -> 'a1 **)
1933let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_694 =
1934  let subaddressing_modeel = x_694 in
1935  h_mk_subaddressing_mode subaddressing_modeel __
1936
1937(** val subaddressing_mode_rect_Type3 :
1938    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1939    'a1) -> subaddressing_mode -> 'a1 **)
1940let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_696 =
1941  let subaddressing_modeel = x_696 in
1942  h_mk_subaddressing_mode subaddressing_modeel __
1943
1944(** val subaddressing_mode_rect_Type2 :
1945    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1946    'a1) -> subaddressing_mode -> 'a1 **)
1947let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_698 =
1948  let subaddressing_modeel = x_698 in
1949  h_mk_subaddressing_mode subaddressing_modeel __
1950
1951(** val subaddressing_mode_rect_Type1 :
1952    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1953    'a1) -> subaddressing_mode -> 'a1 **)
1954let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_700 =
1955  let subaddressing_modeel = x_700 in
1956  h_mk_subaddressing_mode subaddressing_modeel __
1957
1958(** val subaddressing_mode_rect_Type0 :
1959    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1960    'a1) -> subaddressing_mode -> 'a1 **)
1961let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_702 =
1962  let subaddressing_modeel = x_702 in
1963  h_mk_subaddressing_mode subaddressing_modeel __
1964
1965(** val subaddressing_modeel :
1966    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1967    addressing_mode **)
1968let rec subaddressing_modeel n l xxx =
1969  let yyy = xxx in yyy
1970
1971(** val subaddressing_mode_inv_rect_Type4 :
1972    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1973    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1974let subaddressing_mode_inv_rect_Type4 x1 x2 hterm h1 =
1975  let hcut = subaddressing_mode_rect_Type4 x1 x2 h1 hterm in hcut __
1976
1977(** val subaddressing_mode_inv_rect_Type3 :
1978    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1979    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1980let subaddressing_mode_inv_rect_Type3 x1 x2 hterm h1 =
1981  let hcut = subaddressing_mode_rect_Type3 x1 x2 h1 hterm in hcut __
1982
1983(** val subaddressing_mode_inv_rect_Type2 :
1984    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1985    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1986let subaddressing_mode_inv_rect_Type2 x1 x2 hterm h1 =
1987  let hcut = subaddressing_mode_rect_Type2 x1 x2 h1 hterm in hcut __
1988
1989(** val subaddressing_mode_inv_rect_Type1 :
1990    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1991    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1992let subaddressing_mode_inv_rect_Type1 x1 x2 hterm h1 =
1993  let hcut = subaddressing_mode_rect_Type1 x1 x2 h1 hterm in hcut __
1994
1995(** val subaddressing_mode_inv_rect_Type0 :
1996    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1997    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1998let subaddressing_mode_inv_rect_Type0 x1 x2 hterm h1 =
1999  let hcut = subaddressing_mode_rect_Type0 x1 x2 h1 hterm in hcut __
2000
2001(** val subaddressing_mode_discr :
2002    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2003    subaddressing_mode -> __ **)
2004let subaddressing_mode_discr a1 a2 x y =
2005  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
2006
2007(** val subaddressing_mode_jmdiscr :
2008    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2009    subaddressing_mode -> __ **)
2010let subaddressing_mode_jmdiscr a1 a2 x y =
2011  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
2012
2013(** val dpi1__o__subaddressing_modeel__o__inject :
2014    Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
2015    Types.dPair -> addressing_mode Types.sig0 **)
2016let dpi1__o__subaddressing_modeel__o__inject x1 x2 x4 =
2017  subaddressing_modeel x1 x2 x4.Types.dpi1
2018
2019(** val eject__o__subaddressing_modeel__o__inject :
2020    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
2021    Types.sig0 -> addressing_mode Types.sig0 **)
2022let eject__o__subaddressing_modeel__o__inject x1 x2 x4 =
2023  subaddressing_modeel x1 x2 (Types.pi1 x4)
2024
2025(** val subaddressing_modeel__o__inject :
2026    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2027    addressing_mode Types.sig0 **)
2028let subaddressing_modeel__o__inject x1 x2 x3 =
2029  subaddressing_modeel x1 x2 x3
2030
2031(** val dpi1__o__subaddressing_modeel :
2032    Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
2033    Types.dPair -> addressing_mode **)
2034let dpi1__o__subaddressing_modeel x0 x1 x3 =
2035  subaddressing_modeel x0 x1 x3.Types.dpi1
2036
2037(** val eject__o__subaddressing_modeel :
2038    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
2039    Types.sig0 -> addressing_mode **)
2040let eject__o__subaddressing_modeel x0 x1 x3 =
2041  subaddressing_modeel x0 x1 (Types.pi1 x3)
2042
2043type subaddressing_mode_elim_type = __
2044
2045type 'a preinstruction =
2046| ADD of subaddressing_mode * subaddressing_mode
2047| ADDC of subaddressing_mode * subaddressing_mode
2048| SUBB of subaddressing_mode * subaddressing_mode
2049| INC of subaddressing_mode
2050| DEC of subaddressing_mode
2051| MUL of subaddressing_mode * subaddressing_mode
2052| DIV of subaddressing_mode * subaddressing_mode
2053| DA of subaddressing_mode
2054| JC of 'a
2055| JNC of 'a
2056| JB of subaddressing_mode * 'a
2057| JNB of subaddressing_mode * 'a
2058| JBC of subaddressing_mode * 'a
2059| JZ of 'a
2060| JNZ of 'a
2061| CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
2062          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * 
2063   'a
2064| DJNZ of subaddressing_mode * 'a
2065| ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
2066         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2067         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2068| ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
2069         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2070         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2071| XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
2072         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2073| CLR of subaddressing_mode
2074| CPL of subaddressing_mode
2075| RL of subaddressing_mode
2076| RLC of subaddressing_mode
2077| RR of subaddressing_mode
2078| RRC of subaddressing_mode
2079| SWAP of subaddressing_mode
2080| MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
2081         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2082         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2083         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2084         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2085         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2086| MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
2087          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2088| SETB of subaddressing_mode
2089| PUSH of subaddressing_mode
2090| POP of subaddressing_mode
2091| XCH of subaddressing_mode * subaddressing_mode
2092| XCHD of subaddressing_mode * subaddressing_mode
2093| RET
2094| RETI
2095| NOP
2096
2097(** val preinstruction_rect_Type4 :
2098    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2099    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2100    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2101    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2102    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2103    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2104    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2105    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2106    (((subaddressing_mode, subaddressing_mode) Types.prod,
2107    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2108    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2109    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2110    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2111    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2112    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2113    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2114    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2115    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2116    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2117    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2118    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2119    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2120    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2121    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2122    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2123    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2124    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2125    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2126    (((subaddressing_mode, subaddressing_mode) Types.prod,
2127    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2128    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2129    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2130    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2131    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2132let 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 = function
2133| ADD (x_802, x_801) -> h_ADD x_802 x_801
2134| ADDC (x_804, x_803) -> h_ADDC x_804 x_803
2135| SUBB (x_806, x_805) -> h_SUBB x_806 x_805
2136| INC x_807 -> h_INC x_807
2137| DEC x_808 -> h_DEC x_808
2138| MUL (x_810, x_809) -> h_MUL x_810 x_809
2139| DIV (x_812, x_811) -> h_DIV x_812 x_811
2140| DA x_813 -> h_DA x_813
2141| JC x_814 -> h_JC x_814
2142| JNC x_815 -> h_JNC x_815
2143| JB (x_817, x_816) -> h_JB x_817 x_816
2144| JNB (x_819, x_818) -> h_JNB x_819 x_818
2145| JBC (x_821, x_820) -> h_JBC x_821 x_820
2146| JZ x_822 -> h_JZ x_822
2147| JNZ x_823 -> h_JNZ x_823
2148| CJNE (x_825, x_824) -> h_CJNE x_825 x_824
2149| DJNZ (x_827, x_826) -> h_DJNZ x_827 x_826
2150| ANL x_828 -> h_ANL x_828
2151| ORL x_829 -> h_ORL x_829
2152| XRL x_830 -> h_XRL x_830
2153| CLR x_831 -> h_CLR x_831
2154| CPL x_832 -> h_CPL x_832
2155| RL x_833 -> h_RL x_833
2156| RLC x_834 -> h_RLC x_834
2157| RR x_835 -> h_RR x_835
2158| RRC x_836 -> h_RRC x_836
2159| SWAP x_837 -> h_SWAP x_837
2160| MOV x_838 -> h_MOV x_838
2161| MOVX x_839 -> h_MOVX x_839
2162| SETB x_840 -> h_SETB x_840
2163| PUSH x_841 -> h_PUSH x_841
2164| POP x_842 -> h_POP x_842
2165| XCH (x_844, x_843) -> h_XCH x_844 x_843
2166| XCHD (x_846, x_845) -> h_XCHD x_846 x_845
2167| RET -> h_RET
2168| RETI -> h_RETI
2169| NOP -> h_NOP
2170
2171(** val preinstruction_rect_Type5 :
2172    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2173    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2174    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2175    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2176    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2177    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2178    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2179    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2180    (((subaddressing_mode, subaddressing_mode) Types.prod,
2181    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2182    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2183    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2184    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2185    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2186    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2187    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2188    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2189    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2190    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2191    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2192    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2193    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2194    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2195    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2196    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2197    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2198    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2199    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2200    (((subaddressing_mode, subaddressing_mode) Types.prod,
2201    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2202    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2203    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2204    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2205    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2206let 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 = function
2207| ADD (x_886, x_885) -> h_ADD x_886 x_885
2208| ADDC (x_888, x_887) -> h_ADDC x_888 x_887
2209| SUBB (x_890, x_889) -> h_SUBB x_890 x_889
2210| INC x_891 -> h_INC x_891
2211| DEC x_892 -> h_DEC x_892
2212| MUL (x_894, x_893) -> h_MUL x_894 x_893
2213| DIV (x_896, x_895) -> h_DIV x_896 x_895
2214| DA x_897 -> h_DA x_897
2215| JC x_898 -> h_JC x_898
2216| JNC x_899 -> h_JNC x_899
2217| JB (x_901, x_900) -> h_JB x_901 x_900
2218| JNB (x_903, x_902) -> h_JNB x_903 x_902
2219| JBC (x_905, x_904) -> h_JBC x_905 x_904
2220| JZ x_906 -> h_JZ x_906
2221| JNZ x_907 -> h_JNZ x_907
2222| CJNE (x_909, x_908) -> h_CJNE x_909 x_908
2223| DJNZ (x_911, x_910) -> h_DJNZ x_911 x_910
2224| ANL x_912 -> h_ANL x_912
2225| ORL x_913 -> h_ORL x_913
2226| XRL x_914 -> h_XRL x_914
2227| CLR x_915 -> h_CLR x_915
2228| CPL x_916 -> h_CPL x_916
2229| RL x_917 -> h_RL x_917
2230| RLC x_918 -> h_RLC x_918
2231| RR x_919 -> h_RR x_919
2232| RRC x_920 -> h_RRC x_920
2233| SWAP x_921 -> h_SWAP x_921
2234| MOV x_922 -> h_MOV x_922
2235| MOVX x_923 -> h_MOVX x_923
2236| SETB x_924 -> h_SETB x_924
2237| PUSH x_925 -> h_PUSH x_925
2238| POP x_926 -> h_POP x_926
2239| XCH (x_928, x_927) -> h_XCH x_928 x_927
2240| XCHD (x_930, x_929) -> h_XCHD x_930 x_929
2241| RET -> h_RET
2242| RETI -> h_RETI
2243| NOP -> h_NOP
2244
2245(** val preinstruction_rect_Type3 :
2246    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2247    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2248    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2249    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2250    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2251    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2252    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2253    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2254    (((subaddressing_mode, subaddressing_mode) Types.prod,
2255    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2256    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2257    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2258    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2259    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2260    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2261    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2262    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2263    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2264    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2265    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2266    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2267    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2268    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2269    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2270    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2271    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2272    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2273    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2274    (((subaddressing_mode, subaddressing_mode) Types.prod,
2275    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2276    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2277    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2278    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2279    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2280let 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 = function
2281| ADD (x_970, x_969) -> h_ADD x_970 x_969
2282| ADDC (x_972, x_971) -> h_ADDC x_972 x_971
2283| SUBB (x_974, x_973) -> h_SUBB x_974 x_973
2284| INC x_975 -> h_INC x_975
2285| DEC x_976 -> h_DEC x_976
2286| MUL (x_978, x_977) -> h_MUL x_978 x_977
2287| DIV (x_980, x_979) -> h_DIV x_980 x_979
2288| DA x_981 -> h_DA x_981
2289| JC x_982 -> h_JC x_982
2290| JNC x_983 -> h_JNC x_983
2291| JB (x_985, x_984) -> h_JB x_985 x_984
2292| JNB (x_987, x_986) -> h_JNB x_987 x_986
2293| JBC (x_989, x_988) -> h_JBC x_989 x_988
2294| JZ x_990 -> h_JZ x_990
2295| JNZ x_991 -> h_JNZ x_991
2296| CJNE (x_993, x_992) -> h_CJNE x_993 x_992
2297| DJNZ (x_995, x_994) -> h_DJNZ x_995 x_994
2298| ANL x_996 -> h_ANL x_996
2299| ORL x_997 -> h_ORL x_997
2300| XRL x_998 -> h_XRL x_998
2301| CLR x_999 -> h_CLR x_999
2302| CPL x_1000 -> h_CPL x_1000
2303| RL x_1001 -> h_RL x_1001
2304| RLC x_1002 -> h_RLC x_1002
2305| RR x_1003 -> h_RR x_1003
2306| RRC x_1004 -> h_RRC x_1004
2307| SWAP x_1005 -> h_SWAP x_1005
2308| MOV x_1006 -> h_MOV x_1006
2309| MOVX x_1007 -> h_MOVX x_1007
2310| SETB x_1008 -> h_SETB x_1008
2311| PUSH x_1009 -> h_PUSH x_1009
2312| POP x_1010 -> h_POP x_1010
2313| XCH (x_1012, x_1011) -> h_XCH x_1012 x_1011
2314| XCHD (x_1014, x_1013) -> h_XCHD x_1014 x_1013
2315| RET -> h_RET
2316| RETI -> h_RETI
2317| NOP -> h_NOP
2318
2319(** val preinstruction_rect_Type2 :
2320    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2321    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2322    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2323    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2324    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2325    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2326    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2327    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2328    (((subaddressing_mode, subaddressing_mode) Types.prod,
2329    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2330    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2331    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2332    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2333    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2334    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2335    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2336    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2337    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2338    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2339    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2340    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2341    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2342    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2343    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2344    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2345    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2346    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2347    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2348    (((subaddressing_mode, subaddressing_mode) Types.prod,
2349    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2350    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2351    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2352    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2353    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2354let 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 = function
2355| ADD (x_1054, x_1053) -> h_ADD x_1054 x_1053
2356| ADDC (x_1056, x_1055) -> h_ADDC x_1056 x_1055
2357| SUBB (x_1058, x_1057) -> h_SUBB x_1058 x_1057
2358| INC x_1059 -> h_INC x_1059
2359| DEC x_1060 -> h_DEC x_1060
2360| MUL (x_1062, x_1061) -> h_MUL x_1062 x_1061
2361| DIV (x_1064, x_1063) -> h_DIV x_1064 x_1063
2362| DA x_1065 -> h_DA x_1065
2363| JC x_1066 -> h_JC x_1066
2364| JNC x_1067 -> h_JNC x_1067
2365| JB (x_1069, x_1068) -> h_JB x_1069 x_1068
2366| JNB (x_1071, x_1070) -> h_JNB x_1071 x_1070
2367| JBC (x_1073, x_1072) -> h_JBC x_1073 x_1072
2368| JZ x_1074 -> h_JZ x_1074
2369| JNZ x_1075 -> h_JNZ x_1075
2370| CJNE (x_1077, x_1076) -> h_CJNE x_1077 x_1076
2371| DJNZ (x_1079, x_1078) -> h_DJNZ x_1079 x_1078
2372| ANL x_1080 -> h_ANL x_1080
2373| ORL x_1081 -> h_ORL x_1081
2374| XRL x_1082 -> h_XRL x_1082
2375| CLR x_1083 -> h_CLR x_1083
2376| CPL x_1084 -> h_CPL x_1084
2377| RL x_1085 -> h_RL x_1085
2378| RLC x_1086 -> h_RLC x_1086
2379| RR x_1087 -> h_RR x_1087
2380| RRC x_1088 -> h_RRC x_1088
2381| SWAP x_1089 -> h_SWAP x_1089
2382| MOV x_1090 -> h_MOV x_1090
2383| MOVX x_1091 -> h_MOVX x_1091
2384| SETB x_1092 -> h_SETB x_1092
2385| PUSH x_1093 -> h_PUSH x_1093
2386| POP x_1094 -> h_POP x_1094
2387| XCH (x_1096, x_1095) -> h_XCH x_1096 x_1095
2388| XCHD (x_1098, x_1097) -> h_XCHD x_1098 x_1097
2389| RET -> h_RET
2390| RETI -> h_RETI
2391| NOP -> h_NOP
2392
2393(** val preinstruction_rect_Type1 :
2394    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2395    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2396    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2397    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2398    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2399    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2400    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2401    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2402    (((subaddressing_mode, subaddressing_mode) Types.prod,
2403    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2404    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2405    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2406    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2407    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2408    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2409    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2410    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2411    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2412    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2413    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2414    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2415    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2416    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2417    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2418    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2419    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2420    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2421    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2422    (((subaddressing_mode, subaddressing_mode) Types.prod,
2423    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2424    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2425    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2426    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2427    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2428let 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 = function
2429| ADD (x_1138, x_1137) -> h_ADD x_1138 x_1137
2430| ADDC (x_1140, x_1139) -> h_ADDC x_1140 x_1139
2431| SUBB (x_1142, x_1141) -> h_SUBB x_1142 x_1141
2432| INC x_1143 -> h_INC x_1143
2433| DEC x_1144 -> h_DEC x_1144
2434| MUL (x_1146, x_1145) -> h_MUL x_1146 x_1145
2435| DIV (x_1148, x_1147) -> h_DIV x_1148 x_1147
2436| DA x_1149 -> h_DA x_1149
2437| JC x_1150 -> h_JC x_1150
2438| JNC x_1151 -> h_JNC x_1151
2439| JB (x_1153, x_1152) -> h_JB x_1153 x_1152
2440| JNB (x_1155, x_1154) -> h_JNB x_1155 x_1154
2441| JBC (x_1157, x_1156) -> h_JBC x_1157 x_1156
2442| JZ x_1158 -> h_JZ x_1158
2443| JNZ x_1159 -> h_JNZ x_1159
2444| CJNE (x_1161, x_1160) -> h_CJNE x_1161 x_1160
2445| DJNZ (x_1163, x_1162) -> h_DJNZ x_1163 x_1162
2446| ANL x_1164 -> h_ANL x_1164
2447| ORL x_1165 -> h_ORL x_1165
2448| XRL x_1166 -> h_XRL x_1166
2449| CLR x_1167 -> h_CLR x_1167
2450| CPL x_1168 -> h_CPL x_1168
2451| RL x_1169 -> h_RL x_1169
2452| RLC x_1170 -> h_RLC x_1170
2453| RR x_1171 -> h_RR x_1171
2454| RRC x_1172 -> h_RRC x_1172
2455| SWAP x_1173 -> h_SWAP x_1173
2456| MOV x_1174 -> h_MOV x_1174
2457| MOVX x_1175 -> h_MOVX x_1175
2458| SETB x_1176 -> h_SETB x_1176
2459| PUSH x_1177 -> h_PUSH x_1177
2460| POP x_1178 -> h_POP x_1178
2461| XCH (x_1180, x_1179) -> h_XCH x_1180 x_1179
2462| XCHD (x_1182, x_1181) -> h_XCHD x_1182 x_1181
2463| RET -> h_RET
2464| RETI -> h_RETI
2465| NOP -> h_NOP
2466
2467(** val preinstruction_rect_Type0 :
2468    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2469    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2470    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2471    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2472    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2473    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2474    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2475    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2476    (((subaddressing_mode, subaddressing_mode) Types.prod,
2477    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2478    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2479    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2480    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2481    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2482    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2483    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2484    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2485    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2486    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2487    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2488    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2489    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2490    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2491    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2492    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2493    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2494    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2495    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2496    (((subaddressing_mode, subaddressing_mode) Types.prod,
2497    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2498    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2499    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2500    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2501    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2502let 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 = function
2503| ADD (x_1222, x_1221) -> h_ADD x_1222 x_1221
2504| ADDC (x_1224, x_1223) -> h_ADDC x_1224 x_1223
2505| SUBB (x_1226, x_1225) -> h_SUBB x_1226 x_1225
2506| INC x_1227 -> h_INC x_1227
2507| DEC x_1228 -> h_DEC x_1228
2508| MUL (x_1230, x_1229) -> h_MUL x_1230 x_1229
2509| DIV (x_1232, x_1231) -> h_DIV x_1232 x_1231
2510| DA x_1233 -> h_DA x_1233
2511| JC x_1234 -> h_JC x_1234
2512| JNC x_1235 -> h_JNC x_1235
2513| JB (x_1237, x_1236) -> h_JB x_1237 x_1236
2514| JNB (x_1239, x_1238) -> h_JNB x_1239 x_1238
2515| JBC (x_1241, x_1240) -> h_JBC x_1241 x_1240
2516| JZ x_1242 -> h_JZ x_1242
2517| JNZ x_1243 -> h_JNZ x_1243
2518| CJNE (x_1245, x_1244) -> h_CJNE x_1245 x_1244
2519| DJNZ (x_1247, x_1246) -> h_DJNZ x_1247 x_1246
2520| ANL x_1248 -> h_ANL x_1248
2521| ORL x_1249 -> h_ORL x_1249
2522| XRL x_1250 -> h_XRL x_1250
2523| CLR x_1251 -> h_CLR x_1251
2524| CPL x_1252 -> h_CPL x_1252
2525| RL x_1253 -> h_RL x_1253
2526| RLC x_1254 -> h_RLC x_1254
2527| RR x_1255 -> h_RR x_1255
2528| RRC x_1256 -> h_RRC x_1256
2529| SWAP x_1257 -> h_SWAP x_1257
2530| MOV x_1258 -> h_MOV x_1258
2531| MOVX x_1259 -> h_MOVX x_1259
2532| SETB x_1260 -> h_SETB x_1260
2533| PUSH x_1261 -> h_PUSH x_1261
2534| POP x_1262 -> h_POP x_1262
2535| XCH (x_1264, x_1263) -> h_XCH x_1264 x_1263
2536| XCHD (x_1266, x_1265) -> h_XCHD x_1266 x_1265
2537| RET -> h_RET
2538| RETI -> h_RETI
2539| NOP -> h_NOP
2540
2541(** val preinstruction_inv_rect_Type4 :
2542    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2543    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2544    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2545    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2546    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2547    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2548    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2549    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2550    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2551    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2552    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2553    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2554    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2555    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2556    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2557    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2558    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2559    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2560    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2561    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2562    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2563    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2564    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2565    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2566    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2567    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2568    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2569    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2570    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2571    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2572    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2573    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2574    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2575    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2576    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2577    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2578let 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 =
2579  let hcut =
2580    preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2581      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2582      h33 h34 h35 h36 h37 hterm
2583  in
2584  hcut __
2585
2586(** val preinstruction_inv_rect_Type3 :
2587    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2588    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2589    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2590    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2591    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2592    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2593    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2594    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2595    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2596    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2597    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2598    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2599    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2600    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2601    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2602    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2603    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2604    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2605    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2606    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2607    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2608    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2609    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2610    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2611    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2612    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2613    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2614    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2615    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2616    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2617    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2618    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2619    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2620    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2621    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2622    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2623let 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 =
2624  let hcut =
2625    preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2626      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2627      h33 h34 h35 h36 h37 hterm
2628  in
2629  hcut __
2630
2631(** val preinstruction_inv_rect_Type2 :
2632    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2633    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2634    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2635    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2636    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2637    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2638    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2639    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2640    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2641    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2642    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2643    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2644    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2645    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2646    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2647    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2648    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2649    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2650    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2651    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2652    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2653    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2654    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2655    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2656    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2657    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2658    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2659    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2660    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2661    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2662    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2663    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2664    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2665    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2666    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2667    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2668let 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 =
2669  let hcut =
2670    preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2671      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2672      h33 h34 h35 h36 h37 hterm
2673  in
2674  hcut __
2675
2676(** val preinstruction_inv_rect_Type1 :
2677    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2678    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2679    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2680    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2681    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2682    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2683    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2684    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2685    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2686    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2687    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2688    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2689    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2690    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2691    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2692    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2693    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2694    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2695    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2696    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2697    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2698    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2699    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2700    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2701    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2702    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2703    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2704    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2705    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2706    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2707    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2708    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2709    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2710    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2711    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2712    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2713let 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 =
2714  let hcut =
2715    preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2716      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2717      h33 h34 h35 h36 h37 hterm
2718  in
2719  hcut __
2720
2721(** val preinstruction_inv_rect_Type0 :
2722    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2723    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2724    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2725    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2726    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2727    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2728    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2729    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2730    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2731    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2732    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2733    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2734    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2735    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2736    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2737    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2738    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2739    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2740    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2741    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2742    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2743    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2744    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2745    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2746    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2747    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2748    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2749    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2750    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2751    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2752    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2753    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2754    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2755    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2756    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2757    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2758let 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 =
2759  let hcut =
2760    preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2761      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2762      h33 h34 h35 h36 h37 hterm
2763  in
2764  hcut __
2765
2766(** val preinstruction_discr :
2767    'a1 preinstruction -> 'a1 preinstruction -> __ **)
2768let preinstruction_discr x y =
2769  Logic.eq_rect_Type2 x
2770    (match x with
2771     | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2772     | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2773     | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2774     | INC a0 -> Obj.magic (fun _ dH -> dH __)
2775     | DEC a0 -> Obj.magic (fun _ dH -> dH __)
2776     | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2777     | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2778     | DA a0 -> Obj.magic (fun _ dH -> dH __)
2779     | JC a0 -> Obj.magic (fun _ dH -> dH __)
2780     | JNC a0 -> Obj.magic (fun _ dH -> dH __)
2781     | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2782     | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2783     | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2784     | JZ a0 -> Obj.magic (fun _ dH -> dH __)
2785     | JNZ a0 -> Obj.magic (fun _ dH -> dH __)
2786     | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2787     | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2788     | ANL a0 -> Obj.magic (fun _ dH -> dH __)
2789     | ORL a0 -> Obj.magic (fun _ dH -> dH __)
2790     | XRL a0 -> Obj.magic (fun _ dH -> dH __)
2791     | CLR a0 -> Obj.magic (fun _ dH -> dH __)
2792     | CPL a0 -> Obj.magic (fun _ dH -> dH __)
2793     | RL a0 -> Obj.magic (fun _ dH -> dH __)
2794     | RLC a0 -> Obj.magic (fun _ dH -> dH __)
2795     | RR a0 -> Obj.magic (fun _ dH -> dH __)
2796     | RRC a0 -> Obj.magic (fun _ dH -> dH __)
2797     | SWAP a0 -> Obj.magic (fun _ dH -> dH __)
2798     | MOV a0 -> Obj.magic (fun _ dH -> dH __)
2799     | MOVX a0 -> Obj.magic (fun _ dH -> dH __)
2800     | SETB a0 -> Obj.magic (fun _ dH -> dH __)
2801     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
2802     | POP a0 -> Obj.magic (fun _ dH -> dH __)
2803     | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2804     | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2805     | RET -> Obj.magic (fun _ dH -> dH)
2806     | RETI -> Obj.magic (fun _ dH -> dH)
2807     | NOP -> Obj.magic (fun _ dH -> dH)) y
2808
2809(** val preinstruction_jmdiscr :
2810    'a1 preinstruction -> 'a1 preinstruction -> __ **)
2811let preinstruction_jmdiscr x y =
2812  Logic.eq_rect_Type2 x
2813    (match x with
2814     | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2815     | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2816     | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2817     | INC a0 -> Obj.magic (fun _ dH -> dH __)
2818     | DEC a0 -> Obj.magic (fun _ dH -> dH __)
2819     | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2820     | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2821     | DA a0 -> Obj.magic (fun _ dH -> dH __)
2822     | JC a0 -> Obj.magic (fun _ dH -> dH __)
2823     | JNC a0 -> Obj.magic (fun _ dH -> dH __)
2824     | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2825     | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2826     | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2827     | JZ a0 -> Obj.magic (fun _ dH -> dH __)
2828     | JNZ a0 -> Obj.magic (fun _ dH -> dH __)
2829     | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2830     | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2831     | ANL a0 -> Obj.magic (fun _ dH -> dH __)
2832     | ORL a0 -> Obj.magic (fun _ dH -> dH __)
2833     | XRL a0 -> Obj.magic (fun _ dH -> dH __)
2834     | CLR a0 -> Obj.magic (fun _ dH -> dH __)
2835     | CPL a0 -> Obj.magic (fun _ dH -> dH __)
2836     | RL a0 -> Obj.magic (fun _ dH -> dH __)
2837     | RLC a0 -> Obj.magic (fun _ dH -> dH __)
2838     | RR a0 -> Obj.magic (fun _ dH -> dH __)
2839     | RRC a0 -> Obj.magic (fun _ dH -> dH __)
2840     | SWAP a0 -> Obj.magic (fun _ dH -> dH __)
2841     | MOV a0 -> Obj.magic (fun _ dH -> dH __)
2842     | MOVX a0 -> Obj.magic (fun _ dH -> dH __)
2843     | SETB a0 -> Obj.magic (fun _ dH -> dH __)
2844     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
2845     | POP a0 -> Obj.magic (fun _ dH -> dH __)
2846     | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2847     | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2848     | RET -> Obj.magic (fun _ dH -> dH)
2849     | RETI -> Obj.magic (fun _ dH -> dH)
2850     | NOP -> Obj.magic (fun _ dH -> dH)) y
2851
2852(** val eq_preinstruction :
2853    subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
2854    Bool.bool **)
2855let eq_preinstruction i j =
2856  match i with
2857  | ADD (arg1, arg2) ->
2858    (match j with
2859     | ADD (arg1', arg2') ->
2860       Bool.andb
2861         (eq_addressing_mode
2862           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2863             Vector.VEmpty)) arg1)
2864           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2865             Vector.VEmpty)) arg1'))
2866         (eq_addressing_mode
2867           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2868             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2869             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2870             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
2871           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2872             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2873             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2874             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
2875     | ADDC (x, x0) -> Bool.False
2876     | SUBB (x, x0) -> Bool.False
2877     | INC x -> Bool.False
2878     | DEC x -> Bool.False
2879     | MUL (x, x0) -> Bool.False
2880     | DIV (x, x0) -> Bool.False
2881     | DA x -> Bool.False
2882     | JC x -> Bool.False
2883     | JNC x -> Bool.False
2884     | JB (x, x0) -> Bool.False
2885     | JNB (x, x0) -> Bool.False
2886     | JBC (x, x0) -> Bool.False
2887     | JZ x -> Bool.False
2888     | JNZ x -> Bool.False
2889     | CJNE (x, x0) -> Bool.False
2890     | DJNZ (x, x0) -> Bool.False
2891     | ANL x -> Bool.False
2892     | ORL x -> Bool.False
2893     | XRL x -> Bool.False
2894     | CLR x -> Bool.False
2895     | CPL x -> Bool.False
2896     | RL x -> Bool.False
2897     | RLC x -> Bool.False
2898     | RR x -> Bool.False
2899     | RRC x -> Bool.False
2900     | SWAP x -> Bool.False
2901     | MOV x -> Bool.False
2902     | MOVX x -> Bool.False
2903     | SETB x -> Bool.False
2904     | PUSH x -> Bool.False
2905     | POP x -> Bool.False
2906     | XCH (x, x0) -> Bool.False
2907     | XCHD (x, x0) -> Bool.False
2908     | RET -> Bool.False
2909     | RETI -> Bool.False
2910     | NOP -> Bool.False)
2911  | ADDC (arg1, arg2) ->
2912    (match j with
2913     | ADD (x, x0) -> Bool.False
2914     | ADDC (arg1', arg2') ->
2915       Bool.andb
2916         (eq_addressing_mode
2917           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2918             Vector.VEmpty)) arg1)
2919           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2920             Vector.VEmpty)) arg1'))
2921         (eq_addressing_mode
2922           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2923             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2924             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2925             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
2926           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2927             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2928             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2929             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
2930     | SUBB (x, x0) -> Bool.False
2931     | INC x -> Bool.False
2932     | DEC x -> Bool.False
2933     | MUL (x, x0) -> Bool.False
2934     | DIV (x, x0) -> Bool.False
2935     | DA x -> Bool.False
2936     | JC x -> Bool.False
2937     | JNC x -> Bool.False
2938     | JB (x, x0) -> Bool.False
2939     | JNB (x, x0) -> Bool.False
2940     | JBC (x, x0) -> Bool.False
2941     | JZ x -> Bool.False
2942     | JNZ x -> Bool.False
2943     | CJNE (x, x0) -> Bool.False
2944     | DJNZ (x, x0) -> Bool.False
2945     | ANL x -> Bool.False
2946     | ORL x -> Bool.False
2947     | XRL x -> Bool.False
2948     | CLR x -> Bool.False
2949     | CPL x -> Bool.False
2950     | RL x -> Bool.False
2951     | RLC x -> Bool.False
2952     | RR x -> Bool.False
2953     | RRC x -> Bool.False
2954     | SWAP x -> Bool.False
2955     | MOV x -> Bool.False
2956     | MOVX x -> Bool.False
2957     | SETB x -> Bool.False
2958     | PUSH x -> Bool.False
2959     | POP x -> Bool.False
2960     | XCH (x, x0) -> Bool.False
2961     | XCHD (x, x0) -> Bool.False
2962     | RET -> Bool.False
2963     | RETI -> Bool.False
2964     | NOP -> Bool.False)
2965  | SUBB (arg1, arg2) ->
2966    (match j with
2967     | ADD (x, x0) -> Bool.False
2968     | ADDC (x, x0) -> Bool.False
2969     | SUBB (arg1', arg2') ->
2970       Bool.andb
2971         (eq_addressing_mode
2972           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2973             Vector.VEmpty)) arg1)
2974           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2975             Vector.VEmpty)) arg1'))
2976         (eq_addressing_mode
2977           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2978             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2979             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2980             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
2981           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2982             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2983             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2984             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
2985     | INC x -> Bool.False
2986     | DEC x -> Bool.False
2987     | MUL (x, x0) -> Bool.False
2988     | DIV (x, x0) -> Bool.False
2989     | DA x -> Bool.False
2990     | JC x -> Bool.False
2991     | JNC x -> Bool.False
2992     | JB (x, x0) -> Bool.False
2993     | JNB (x, x0) -> Bool.False
2994     | JBC (x, x0) -> Bool.False
2995     | JZ x -> Bool.False
2996     | JNZ x -> Bool.False
2997     | CJNE (x, x0) -> Bool.False
2998     | DJNZ (x, x0) -> Bool.False
2999     | ANL x -> Bool.False
3000     | ORL x -> Bool.False
3001     | XRL x -> Bool.False
3002     | CLR x -> Bool.False
3003     | CPL x -> Bool.False
3004     | RL x -> Bool.False
3005     | RLC x -> Bool.False
3006     | RR x -> Bool.False
3007     | RRC x -> Bool.False
3008     | SWAP x -> Bool.False
3009     | MOV x -> Bool.False
3010     | MOVX x -> Bool.False
3011     | SETB x -> Bool.False
3012     | PUSH x -> Bool.False
3013     | POP x -> Bool.False
3014     | XCH (x, x0) -> Bool.False
3015     | XCHD (x, x0) -> Bool.False
3016     | RET -> Bool.False
3017     | RETI -> Bool.False
3018     | NOP -> Bool.False)
3019  | INC arg ->
3020    (match j with
3021     | ADD (x, x0) -> Bool.False
3022     | ADDC (x, x0) -> Bool.False
3023     | SUBB (x, x0) -> Bool.False
3024     | INC arg' ->
3025       eq_addressing_mode
3026         (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
3027           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
3028           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3029           (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
3030           ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr,
3031           Vector.VEmpty)))))))))) arg)
3032         (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
3033           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
3034           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3035           (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
3036           ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr,
3037           Vector.VEmpty)))))))))) arg')
3038     | DEC x -> Bool.False
3039     | MUL (x, x0) -> Bool.False
3040     | DIV (x, x0) -> Bool.False
3041     | DA x -> Bool.False
3042     | JC x -> Bool.False
3043     | JNC x -> Bool.False
3044     | JB (x, x0) -> Bool.False
3045     | JNB (x, x0) -> Bool.False
3046     | JBC (x, x0) -> Bool.False
3047     | JZ x -> Bool.False
3048     | JNZ x -> Bool.False
3049     | CJNE (x, x0) -> Bool.False
3050     | DJNZ (x, x0) -> Bool.False
3051     | ANL x -> Bool.False
3052     | ORL x -> Bool.False
3053     | XRL x -> Bool.False
3054     | CLR x -> Bool.False
3055     | CPL x -> Bool.False
3056     | RL x -> Bool.False
3057     | RLC x -> Bool.False
3058     | RR x -> Bool.False
3059     | RRC x -> Bool.False
3060     | SWAP x -> Bool.False
3061     | MOV x -> Bool.False
3062     | MOVX x -> Bool.False
3063     | SETB x -> Bool.False
3064     | PUSH x -> Bool.False
3065     | POP x -> Bool.False
3066     | XCH (x, x0) -> Bool.False
3067     | XCHD (x, x0) -> Bool.False
3068     | RET -> Bool.False
3069     | RETI -> Bool.False
3070     | NOP -> Bool.False)
3071  | DEC arg ->
3072    (match j with
3073     | ADD (x, x0) -> Bool.False
3074     | ADDC (x, x0) -> Bool.False
3075     | SUBB (x, x0) -> Bool.False
3076     | INC x -> Bool.False
3077     | DEC arg' ->
3078       eq_addressing_mode
3079         (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
3080           ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S
3081           (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
3082           (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg)
3083         (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
3084           ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S
3085           (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
3086           (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg')
3087     | MUL (x, x0) -> Bool.False
3088     | DIV (x, x0) -> Bool.False
3089     | DA x -> Bool.False
3090     | JC x -> Bool.False
3091     | JNC x -> Bool.False
3092     | JB (x, x0) -> Bool.False
3093     | JNB (x, x0) -> Bool.False
3094     | JBC (x, x0) -> Bool.False
3095     | JZ x -> Bool.False
3096     | JNZ x -> Bool.False
3097     | CJNE (x, x0) -> Bool.False
3098     | DJNZ (x, x0) -> Bool.False
3099     | ANL x -> Bool.False
3100     | ORL x -> Bool.False
3101     | XRL x -> Bool.False
3102     | CLR x -> Bool.False
3103     | CPL x -> Bool.False
3104     | RL x -> Bool.False
3105     | RLC x -> Bool.False
3106     | RR x -> Bool.False
3107     | RRC x -> Bool.False
3108     | SWAP x -> Bool.False
3109     | MOV x -> Bool.False
3110     | MOVX x -> Bool.False
3111     | SETB x -> Bool.False
3112     | PUSH x -> Bool.False
3113     | POP x -> Bool.False
3114     | XCH (x, x0) -> Bool.False
3115     | XCHD (x, x0) -> Bool.False
3116     | RET -> Bool.False
3117     | RETI -> Bool.False
3118     | NOP -> Bool.False)
3119  | MUL (arg1, arg2) ->
3120    (match j with
3121     | ADD (x, x0) -> Bool.False
3122     | ADDC (x, x0) -> Bool.False
3123     | SUBB (x, x0) -> Bool.False
3124     | INC x -> Bool.False
3125     | DEC x -> Bool.False
3126     | MUL (arg1', arg2') ->
3127       Bool.andb
3128         (eq_addressing_mode
3129           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3130             Vector.VEmpty)) arg1)
3131           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3132             Vector.VEmpty)) arg1'))
3133         (eq_addressing_mode
3134           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3135             Vector.VEmpty)) arg2)
3136           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3137             Vector.VEmpty)) arg2'))
3138     | DIV (x, x0) -> Bool.False
3139     | DA x -> Bool.False
3140     | JC x -> Bool.False
3141     | JNC x -> Bool.False
3142     | JB (x, x0) -> Bool.False
3143     | JNB (x, x0) -> Bool.False
3144     | JBC (x, x0) -> Bool.False
3145     | JZ x -> Bool.False
3146     | JNZ x -> Bool.False
3147     | CJNE (x, x0) -> Bool.False
3148     | DJNZ (x, x0) -> Bool.False
3149     | ANL x -> Bool.False
3150     | ORL x -> Bool.False
3151     | XRL x -> Bool.False
3152     | CLR x -> Bool.False
3153     | CPL x -> Bool.False
3154     | RL x -> Bool.False
3155     | RLC x -> Bool.False
3156     | RR x -> Bool.False
3157     | RRC x -> Bool.False
3158     | SWAP x -> Bool.False
3159     | MOV x -> Bool.False
3160     | MOVX x -> Bool.False
3161     | SETB x -> Bool.False
3162     | PUSH x -> Bool.False
3163     | POP x -> Bool.False
3164     | XCH (x, x0) -> Bool.False
3165     | XCHD (x, x0) -> Bool.False
3166     | RET -> Bool.False
3167     | RETI -> Bool.False
3168     | NOP -> Bool.False)
3169  | DIV (arg1, arg2) ->
3170    (match j with
3171     | ADD (x, x0) -> Bool.False
3172     | ADDC (x, x0) -> Bool.False
3173     | SUBB (x, x0) -> Bool.False
3174     | INC x -> Bool.False
3175     | DEC x -> Bool.False
3176     | MUL (x, x0) -> Bool.False
3177     | DIV (arg1', arg2') ->
3178       Bool.andb
3179         (eq_addressing_mode
3180           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3181             Vector.VEmpty)) arg1)
3182           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3183             Vector.VEmpty)) arg1'))
3184         (eq_addressing_mode
3185           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3186             Vector.VEmpty)) arg2)
3187           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3188             Vector.VEmpty)) arg2'))
3189     | DA x -> Bool.False
3190     | JC x -> Bool.False
3191     | JNC x -> Bool.False
3192     | JB (x, x0) -> Bool.False
3193     | JNB (x, x0) -> Bool.False
3194     | JBC (x, x0) -> Bool.False
3195     | JZ x -> Bool.False
3196     | JNZ x -> Bool.False
3197     | CJNE (x, x0) -> Bool.False
3198     | DJNZ (x, x0) -> Bool.False
3199     | ANL x -> Bool.False
3200     | ORL x -> Bool.False
3201     | XRL x -> Bool.False
3202     | CLR x -> Bool.False
3203     | CPL x -> Bool.False
3204     | RL x -> Bool.False
3205     | RLC x -> Bool.False
3206     | RR x -> Bool.False
3207     | RRC x -> Bool.False
3208     | SWAP x -> Bool.False
3209     | MOV x -> Bool.False
3210     | MOVX x -> Bool.False
3211     | SETB x -> Bool.False
3212     | PUSH x -> Bool.False
3213     | POP x -> Bool.False
3214     | XCH (x, x0) -> Bool.False
3215     | XCHD (x, x0) -> Bool.False
3216     | RET -> Bool.False
3217     | RETI -> Bool.False
3218     | NOP -> Bool.False)
3219  | DA arg ->
3220    (match j with
3221     | ADD (x, x0) -> Bool.False
3222     | ADDC (x, x0) -> Bool.False
3223     | SUBB (x, x0) -> Bool.False
3224     | INC x -> Bool.False
3225     | DEC x -> Bool.False
3226     | MUL (x, x0) -> Bool.False
3227     | DIV (x, x0) -> Bool.False
3228     | DA arg' ->
3229       eq_addressing_mode
3230         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3231           Vector.VEmpty)) arg)
3232         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3233           Vector.VEmpty)) arg')
3234     | JC x -> Bool.False
3235     | JNC x -> Bool.False
3236     | JB (x, x0) -> Bool.False
3237     | JNB (x, x0) -> Bool.False
3238     | JBC (x, x0) -> Bool.False
3239     | JZ x -> Bool.False
3240     | JNZ x -> Bool.False
3241     | CJNE (x, x0) -> Bool.False
3242     | DJNZ (x, x0) -> Bool.False
3243     | ANL x -> Bool.False
3244     | ORL x -> Bool.False
3245     | XRL x -> Bool.False
3246     | CLR x -> Bool.False
3247     | CPL x -> Bool.False
3248     | RL x -> Bool.False
3249     | RLC x -> Bool.False
3250     | RR x -> Bool.False
3251     | RRC x -> Bool.False
3252     | SWAP x -> Bool.False
3253     | MOV x -> Bool.False
3254     | MOVX x -> Bool.False
3255     | SETB x -> Bool.False
3256     | PUSH x -> Bool.False
3257     | POP x -> Bool.False
3258     | XCH (x, x0) -> Bool.False
3259     | XCHD (x, x0) -> Bool.False
3260     | RET -> Bool.False
3261     | RETI -> Bool.False
3262     | NOP -> Bool.False)
3263  | JC arg ->
3264    (match j with
3265     | ADD (x, x0) -> Bool.False
3266     | ADDC (x, x0) -> Bool.False
3267     | SUBB (x, x0) -> Bool.False
3268     | INC x -> Bool.False
3269     | DEC x -> Bool.False
3270     | MUL (x, x0) -> Bool.False
3271     | DIV (x, x0) -> Bool.False
3272     | DA x -> Bool.False
3273     | JC arg' ->
3274       eq_addressing_mode
3275         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3276           Vector.VEmpty)) arg)
3277         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3278           Vector.VEmpty)) arg')
3279     | JNC x -> Bool.False
3280     | JB (x, x0) -> Bool.False
3281     | JNB (x, x0) -> Bool.False
3282     | JBC (x, x0) -> Bool.False
3283     | JZ x -> Bool.False
3284     | JNZ x -> Bool.False
3285     | CJNE (x, x0) -> Bool.False
3286     | DJNZ (x, x0) -> Bool.False
3287     | ANL x -> Bool.False
3288     | ORL x -> Bool.False
3289     | XRL x -> Bool.False
3290     | CLR x -> Bool.False
3291     | CPL x -> Bool.False
3292     | RL x -> Bool.False
3293     | RLC x -> Bool.False
3294     | RR x -> Bool.False
3295     | RRC x -> Bool.False
3296     | SWAP x -> Bool.False
3297     | MOV x -> Bool.False
3298     | MOVX x -> Bool.False
3299     | SETB x -> Bool.False
3300     | PUSH x -> Bool.False
3301     | POP x -> Bool.False
3302     | XCH (x, x0) -> Bool.False
3303     | XCHD (x, x0) -> Bool.False
3304     | RET -> Bool.False
3305     | RETI -> Bool.False
3306     | NOP -> Bool.False)
3307  | JNC arg ->
3308    (match j with
3309     | ADD (x, x0) -> Bool.False
3310     | ADDC (x, x0) -> Bool.False
3311     | SUBB (x, x0) -> Bool.False
3312     | INC x -> Bool.False
3313     | DEC x -> Bool.False
3314     | MUL (x, x0) -> Bool.False
3315     | DIV (x, x0) -> Bool.False
3316     | DA x -> Bool.False
3317     | JC x -> Bool.False
3318     | JNC arg' ->
3319       eq_addressing_mode
3320         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3321           Vector.VEmpty)) arg)
3322         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3323           Vector.VEmpty)) arg')
3324     | JB (x, x0) -> Bool.False
3325     | JNB (x, x0) -> Bool.False
3326     | JBC (x, x0) -> Bool.False
3327     | JZ x -> Bool.False
3328     | JNZ x -> Bool.False
3329     | CJNE (x, x0) -> Bool.False
3330     | DJNZ (x, x0) -> Bool.False
3331     | ANL x -> Bool.False
3332     | ORL x -> Bool.False
3333     | XRL x -> Bool.False
3334     | CLR x -> Bool.False
3335     | CPL x -> Bool.False
3336     | RL x -> Bool.False
3337     | RLC x -> Bool.False
3338     | RR x -> Bool.False
3339     | RRC x -> Bool.False
3340     | SWAP x -> Bool.False
3341     | MOV x -> Bool.False
3342     | MOVX x -> Bool.False
3343     | SETB x -> Bool.False
3344     | PUSH x -> Bool.False
3345     | POP x -> Bool.False
3346     | XCH (x, x0) -> Bool.False
3347     | XCHD (x, x0) -> Bool.False
3348     | RET -> Bool.False
3349     | RETI -> Bool.False
3350     | NOP -> Bool.False)
3351  | JB (arg1, arg2) ->
3352    (match j with
3353     | ADD (x, x0) -> Bool.False
3354     | ADDC (x, x0) -> Bool.False
3355     | SUBB (x, x0) -> Bool.False
3356     | INC x -> Bool.False
3357     | DEC x -> Bool.False
3358     | MUL (x, x0) -> Bool.False
3359     | DIV (x, x0) -> Bool.False
3360     | DA x -> Bool.False
3361     | JC x -> Bool.False
3362     | JNC x -> Bool.False
3363     | JB (arg1', arg2') ->
3364       Bool.andb
3365         (eq_addressing_mode
3366           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
3367             Vector.VEmpty)) arg1)
3368           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
3369             Vector.VEmpty)) arg1'))
3370         (eq_addressing_mode
3371           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3372             Vector.VEmpty)) arg2)
3373           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3374             Vector.VEmpty)) arg2'))
3375     | JNB (x, x0) -> Bool.False
3376     | JBC (x, x0) -> Bool.False
3377     | JZ x -> Bool.False
3378     | JNZ x -> Bool.False
3379     | CJNE (x, x0) -> Bool.False
3380     | DJNZ (x, x0) -> Bool.False
3381     | ANL x -> Bool.False
3382     | ORL x -> Bool.False
3383     | XRL x -> Bool.False
3384     | CLR x -> Bool.False
3385     | CPL x -> Bool.False
3386     | RL x -> Bool.False
3387     | RLC x -> Bool.False
3388     | RR x -> Bool.False
3389     | RRC x -> Bool.False
3390     | SWAP x -> Bool.False
3391     | MOV x -> Bool.False
3392     | MOVX x -> Bool.False
3393     | SETB x -> Bool.False
3394     | PUSH x -> Bool.False
3395     | POP x -> Bool.False
3396     | XCH (x, x0) -> Bool.False
3397     | XCHD (x, x0) -> Bool.False
3398     | RET -> Bool.False
3399     | RETI -> Bool.False
3400     | NOP -> Bool.False)
3401  | JNB (arg1, arg2) ->
3402    (match j with
3403     | ADD (x, x0) -> Bool.False
3404     | ADDC (x, x0) -> Bool.False
3405     | SUBB (x, x0) -> Bool.False
3406     | INC x -> Bool.False
3407     | DEC x -> Bool.False
3408     | MUL (x, x0) -> Bool.False
3409     | DIV (x, x0) -> Bool.False
3410     | DA x -> Bool.False
3411     | JC x -> Bool.False
3412     | JNC x -> Bool.False
3413     | JB (x, x0) -> Bool.False
3414     | JNB (arg1', arg2') ->
3415       Bool.andb
3416         (eq_addressing_mode
3417           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
3418             Vector.VEmpty)) arg1)
3419           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
3420             Vector.VEmpty)) arg1'))
3421         (eq_addressing_mode
3422           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3423             Vector.VEmpty)) arg2)
3424           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3425             Vector.VEmpty)) arg2'))
3426     | JBC (x, x0) -> Bool.False
3427     | JZ x -> Bool.False
3428     | JNZ x -> Bool.False
3429     | CJNE (x, x0) -> Bool.False
3430     | DJNZ (x, x0) -> Bool.False
3431     | ANL x -> Bool.False
3432     | ORL x -> Bool.False
3433     | XRL x -> Bool.False
3434     | CLR x -> Bool.False
3435     | CPL x -> Bool.False
3436     | RL x -> Bool.False
3437     | RLC x -> Bool.False
3438     | RR x -> Bool.False
3439     | RRC x -> Bool.False
3440     | SWAP x -> Bool.False
3441     | MOV x -> Bool.False
3442     | MOVX x -> Bool.False
3443     | SETB x -> Bool.False
3444     | PUSH x -> Bool.False
3445     | POP x -> Bool.False
3446     | XCH (x, x0) -> Bool.False
3447     | XCHD (x, x0) -> Bool.False
3448     | RET -> Bool.False
3449     | RETI -> Bool.False
3450     | NOP -> Bool.False)
3451  | JBC (arg1, arg2) ->
3452    (match j with
3453     | ADD (x, x0) -> Bool.False
3454     | ADDC (x, x0) -> Bool.False
3455     | SUBB (x, x0) -> Bool.False
3456     | INC x -> Bool.False
3457     | DEC x -> Bool.False
3458     | MUL (x, x0) -> Bool.False
3459     | DIV (x, x0) -> Bool.False
3460     | DA x -> Bool.False
3461     | JC x -> Bool.False
3462     | JNC x -> Bool.False
3463     | JB (x, x0) -> Bool.False
3464     | JNB (x, x0) -> Bool.False
3465     | JBC (arg1', arg2') ->
3466       Bool.andb
3467         (eq_addressing_mode
3468           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
3469             Vector.VEmpty)) arg1)
3470           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
3471             Vector.VEmpty)) arg1'))
3472         (eq_addressing_mode
3473           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3474             Vector.VEmpty)) arg2)
3475           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3476             Vector.VEmpty)) arg2'))
3477     | JZ x -> Bool.False
3478     | JNZ x -> Bool.False
3479     | CJNE (x, x0) -> Bool.False
3480     | DJNZ (x, x0) -> Bool.False
3481     | ANL x -> Bool.False
3482     | ORL x -> Bool.False
3483     | XRL x -> Bool.False
3484     | CLR x -> Bool.False
3485     | CPL x -> Bool.False
3486     | RL x -> Bool.False
3487     | RLC x -> Bool.False
3488     | RR x -> Bool.False
3489     | RRC x -> Bool.False
3490     | SWAP x -> Bool.False
3491     | MOV x -> Bool.False
3492     | MOVX x -> Bool.False
3493     | SETB x -> Bool.False
3494     | PUSH x -> Bool.False
3495     | POP x -> Bool.False
3496     | XCH (x, x0) -> Bool.False
3497     | XCHD (x, x0) -> Bool.False
3498     | RET -> Bool.False
3499     | RETI -> Bool.False
3500     | NOP -> Bool.False)
3501  | JZ arg ->
3502    (match j with
3503     | ADD (x, x0) -> Bool.False
3504     | ADDC (x, x0) -> Bool.False
3505     | SUBB (x, x0) -> Bool.False
3506     | INC x -> Bool.False
3507     | DEC x -> Bool.False
3508     | MUL (x, x0) -> Bool.False
3509     | DIV (x, x0) -> Bool.False
3510     | DA x -> Bool.False
3511     | JC x -> Bool.False
3512     | JNC x -> Bool.False
3513     | JB (x, x0) -> Bool.False
3514     | JNB (x, x0) -> Bool.False
3515     | JBC (x, x0) -> Bool.False
3516     | JZ arg' ->
3517       eq_addressing_mode
3518         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3519           Vector.VEmpty)) arg)
3520         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3521           Vector.VEmpty)) arg')
3522     | JNZ x -> Bool.False
3523     | CJNE (x, x0) -> Bool.False
3524     | DJNZ (x, x0) -> Bool.False
3525     | ANL x -> Bool.False
3526     | ORL x -> Bool.False
3527     | XRL x -> Bool.False
3528     | CLR x -> Bool.False
3529     | CPL x -> Bool.False
3530     | RL x -> Bool.False
3531     | RLC x -> Bool.False
3532     | RR x -> Bool.False
3533     | RRC x -> Bool.False
3534     | SWAP x -> Bool.False
3535     | MOV x -> Bool.False
3536     | MOVX x -> Bool.False
3537     | SETB x -> Bool.False
3538     | PUSH x -> Bool.False
3539     | POP x -> Bool.False
3540     | XCH (x, x0) -> Bool.False
3541     | XCHD (x, x0) -> Bool.False
3542     | RET -> Bool.False
3543     | RETI -> Bool.False
3544     | NOP -> Bool.False)
3545  | JNZ arg ->
3546    (match j with
3547     | ADD (x, x0) -> Bool.False
3548     | ADDC (x, x0) -> Bool.False
3549     | SUBB (x, x0) -> Bool.False
3550     | INC x -> Bool.False
3551     | DEC x -> Bool.False
3552     | MUL (x, x0) -> Bool.False
3553     | DIV (x, x0) -> Bool.False
3554     | DA x -> Bool.False
3555     | JC x -> Bool.False
3556     | JNC x -> Bool.False
3557     | JB (x, x0) -> Bool.False
3558     | JNB (x, x0) -> Bool.False
3559     | JBC (x, x0) -> Bool.False
3560     | JZ x -> Bool.False
3561     | JNZ arg' ->
3562       eq_addressing_mode
3563         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3564           Vector.VEmpty)) arg)
3565         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3566           Vector.VEmpty)) arg')
3567     | CJNE (x, x0) -> Bool.False
3568     | DJNZ (x, x0) -> Bool.False
3569     | ANL x -> Bool.False
3570     | ORL x -> Bool.False
3571     | XRL x -> Bool.False
3572     | CLR x -> Bool.False
3573     | CPL x -> Bool.False
3574     | RL x -> Bool.False
3575     | RLC x -> Bool.False
3576     | RR x -> Bool.False
3577     | RRC x -> Bool.False
3578     | SWAP x -> Bool.False
3579     | MOV x -> Bool.False
3580     | MOVX x -> Bool.False
3581     | SETB x -> Bool.False
3582     | PUSH x -> Bool.False
3583     | POP x -> Bool.False
3584     | XCH (x, x0) -> Bool.False
3585     | XCHD (x, x0) -> Bool.False
3586     | RET -> Bool.False
3587     | RETI -> Bool.False
3588     | NOP -> Bool.False)
3589  | CJNE (arg1, arg2) ->
3590    (match j with
3591     | ADD (x, x0) -> Bool.False
3592     | ADDC (x, x0) -> Bool.False
3593     | SUBB (x, x0) -> Bool.False
3594     | INC x -> Bool.False
3595     | DEC x -> Bool.False
3596     | MUL (x, x0) -> Bool.False
3597     | DIV (x, x0) -> Bool.False
3598     | DA x -> Bool.False
3599     | JC x -> Bool.False
3600     | JNC x -> Bool.False
3601     | JB (x, x0) -> Bool.False
3602     | JNB (x, x0) -> Bool.False
3603     | JBC (x, x0) -> Bool.False
3604     | JZ x -> Bool.False
3605     | JNZ x -> Bool.False
3606     | CJNE (arg1', arg2') ->
3607       let prod_eq_left =
3608         Util.eq_prod (fun h h1 ->
3609           eq_addressing_mode
3610             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3611               Vector.VEmpty)) h)
3612             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3613               Vector.VEmpty)) h1)) (fun h h1 ->
3614           eq_addressing_mode
3615             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3616               Nat.O), Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3617               h)
3618             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3619               Nat.O), Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3620               h1))
3621       in
3622       let prod_eq_right =
3623         Util.eq_prod (fun h h1 ->
3624           eq_addressing_mode
3625             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3626               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
3627               Vector.VEmpty)))) h)
3628             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3629               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
3630               Vector.VEmpty)))) h1)) (fun h h1 ->
3631           eq_addressing_mode
3632             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data,
3633               Vector.VEmpty)) h)
3634             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data,
3635               Vector.VEmpty)) h1))
3636       in
3637       let arg1_eq = Util.eq_sum prod_eq_left prod_eq_right in
3638       Bool.andb (arg1_eq arg1 arg1')
3639         (eq_addressing_mode
3640           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3641             Vector.VEmpty)) arg2)
3642           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3643             Vector.VEmpty)) arg2'))
3644     | DJNZ (x, x0) -> Bool.False
3645     | ANL x -> Bool.False
3646     | ORL x -> Bool.False
3647     | XRL x -> Bool.False
3648     | CLR x -> Bool.False
3649     | CPL x -> Bool.False
3650     | RL x -> Bool.False
3651     | RLC x -> Bool.False
3652     | RR x -> Bool.False
3653     | RRC x -> Bool.False
3654     | SWAP x -> Bool.False
3655     | MOV x -> Bool.False
3656     | MOVX x -> Bool.False
3657     | SETB x -> Bool.False
3658     | PUSH x -> Bool.False
3659     | POP x -> Bool.False
3660     | XCH (x, x0) -> Bool.False
3661     | XCHD (x, x0) -> Bool.False
3662     | RET -> Bool.False
3663     | RETI -> Bool.False
3664     | NOP -> Bool.False)
3665  | DJNZ (arg1, arg2) ->
3666    (match j with
3667     | ADD (x, x0) -> Bool.False
3668     | ADDC (x, x0) -> Bool.False
3669     | SUBB (x, x0) -> Bool.False
3670     | INC x -> Bool.False
3671     | DEC x -> Bool.False
3672     | MUL (x, x0) -> Bool.False
3673     | DIV (x, x0) -> Bool.False
3674     | DA x -> Bool.False
3675     | JC x -> Bool.False
3676     | JNC x -> Bool.False
3677     | JB (x, x0) -> Bool.False
3678     | JNB (x, x0) -> Bool.False
3679     | JBC (x, x0) -> Bool.False
3680     | JZ x -> Bool.False
3681     | JNZ x -> Bool.False
3682     | CJNE (x, x0) -> Bool.False
3683     | DJNZ (arg1', arg2') ->
3684       Bool.andb
3685         (eq_addressing_mode
3686           (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
3687             Registr, (Vector.VCons (Nat.O, Direct, Vector.VEmpty)))) arg1)
3688           (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
3689             Registr, (Vector.VCons (Nat.O, Direct, Vector.VEmpty)))) arg1'))
3690         (eq_addressing_mode
3691           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3692             Vector.VEmpty)) arg2)
3693           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3694             Vector.VEmpty)) arg2'))
3695     | ANL x -> Bool.False
3696     | ORL x -> Bool.False
3697     | XRL x -> Bool.False
3698     | CLR x -> Bool.False
3699     | CPL x -> Bool.False
3700     | RL x -> Bool.False
3701     | RLC x -> Bool.False
3702     | RR x -> Bool.False
3703     | RRC x -> Bool.False
3704     | SWAP x -> Bool.False
3705     | MOV x -> Bool.False
3706     | MOVX x -> Bool.False
3707     | SETB x -> Bool.False
3708     | PUSH x -> Bool.False
3709     | POP x -> Bool.False
3710     | XCH (x, x0) -> Bool.False
3711     | XCHD (x, x0) -> Bool.False
3712     | RET -> Bool.False
3713     | RETI -> Bool.False
3714     | NOP -> Bool.False)
3715  | ANL arg ->
3716    (match j with
3717     | ADD (x, x0) -> Bool.False
3718     | ADDC (x, x0) -> Bool.False
3719     | SUBB (x, x0) -> Bool.False
3720     | INC x -> Bool.False
3721     | DEC x -> Bool.False
3722     | MUL (x, x0) -> Bool.False
3723     | DIV (x, x0) -> Bool.False
3724     | DA x -> Bool.False
3725     | JC x -> Bool.False
3726     | JNC x -> Bool.False
3727     | JB (x, x0) -> Bool.False
3728     | JNB (x, x0) -> Bool.False
3729     | JBC (x, x0) -> Bool.False
3730     | JZ x -> Bool.False
3731     | JNZ x -> Bool.False
3732     | CJNE (x, x0) -> Bool.False
3733     | DJNZ (x, x0) -> Bool.False
3734     | ANL arg' ->
3735       let prod_eq_left1 =
3736         Util.eq_prod (fun h h1 ->
3737           eq_addressing_mode
3738             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3739               Vector.VEmpty)) h)
3740             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3741               Vector.VEmpty)) h1)) (fun h h1 ->
3742           eq_addressing_mode
3743             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
3744               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3745               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
3746               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
3747               Vector.VEmpty)))))))) h)
3748             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
3749               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3750               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
3751               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
3752               Vector.VEmpty)))))))) h1))
3753       in
3754       let prod_eq_left2 =
3755         Util.eq_prod (fun h h1 ->
3756           eq_addressing_mode
3757             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
3758               Vector.VEmpty)) h)
3759             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
3760               Vector.VEmpty)) h1)) (fun h h1 ->
3761           eq_addressing_mode
3762             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3763               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3764               h)
3765             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3766               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3767               h1))
3768       in
3769       let prod_eq_left = Util.eq_sum prod_eq_left1 prod_eq_left2 in
3770       let prod_eq_right =
3771         Util.eq_prod (fun h h1 ->
3772           eq_addressing_mode
3773             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
3774               Vector.VEmpty)) h)
3775             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
3776               Vector.VEmpty)) h1)) (fun h h1 ->
3777           eq_addressing_mode
3778             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3779               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
3780               Vector.VEmpty)))) h)
3781             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3782               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
3783               Vector.VEmpty)))) h1))
3784       in
3785       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
3786     | ORL x -> Bool.False
3787     | XRL x -> Bool.False
3788     | CLR x -> Bool.False
3789     | CPL x -> Bool.False
3790     | RL x -> Bool.False
3791     | RLC x -> Bool.False
3792     | RR x -> Bool.False
3793     | RRC x -> Bool.False
3794     | SWAP x -> Bool.False
3795     | MOV x -> Bool.False
3796     | MOVX x -> Bool.False
3797     | SETB x -> Bool.False
3798     | PUSH x -> Bool.False
3799     | POP x -> Bool.False
3800     | XCH (x, x0) -> Bool.False
3801     | XCHD (x, x0) -> Bool.False
3802     | RET -> Bool.False
3803     | RETI -> Bool.False
3804     | NOP -> Bool.False)
3805  | ORL arg ->
3806    (match j with
3807     | ADD (x, x0) -> Bool.False
3808     | ADDC (x, x0) -> Bool.False
3809     | SUBB (x, x0) -> Bool.False
3810     | INC x -> Bool.False
3811     | DEC x -> Bool.False
3812     | MUL (x, x0) -> Bool.False
3813     | DIV (x, x0) -> Bool.False
3814     | DA x -> Bool.False
3815     | JC x -> Bool.False
3816     | JNC x -> Bool.False
3817     | JB (x, x0) -> Bool.False
3818     | JNB (x, x0) -> Bool.False
3819     | JBC (x, x0) -> Bool.False
3820     | JZ x -> Bool.False
3821     | JNZ x -> Bool.False
3822     | CJNE (x, x0) -> Bool.False
3823     | DJNZ (x, x0) -> Bool.False
3824     | ANL x -> Bool.False
3825     | ORL arg' ->
3826       let prod_eq_left1 =
3827         Util.eq_prod (fun h h1 ->
3828           eq_addressing_mode
3829             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3830               Vector.VEmpty)) h)
3831             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3832               Vector.VEmpty)) h1)) (fun h h1 ->
3833           eq_addressing_mode
3834             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
3835               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3836               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Data, (Vector.VCons
3837               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
3838               Vector.VEmpty)))))))) h)
3839             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
3840               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3841               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Data, (Vector.VCons
3842               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
3843               Vector.VEmpty)))))))) h1))
3844       in
3845       let prod_eq_left2 =
3846         Util.eq_prod (fun h h1 ->
3847           eq_addressing_mode
3848             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
3849               Vector.VEmpty)) h)
3850             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
3851               Vector.VEmpty)) h1)) (fun h h1 ->
3852           eq_addressing_mode
3853             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3854               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3855               h)
3856             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3857               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3858               h1))
3859       in
3860       let prod_eq_left = Util.eq_sum prod_eq_left1 prod_eq_left2 in
3861       let prod_eq_right =
3862         Util.eq_prod (fun h h1 ->
3863           eq_addressing_mode
3864             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
3865               Vector.VEmpty)) h)
3866             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
3867               Vector.VEmpty)) h1)) (fun h h1 ->
3868           eq_addressing_mode
3869             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3870               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
3871               Vector.VEmpty)))) h)
3872             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3873               Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr,
3874               Vector.VEmpty)))) h1))
3875       in
3876       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
3877     | XRL x -> Bool.False
3878     | CLR x -> Bool.False
3879     | CPL x -> Bool.False
3880     | RL x -> Bool.False
3881     | RLC x -> Bool.False
3882     | RR x -> Bool.False
3883     | RRC x -> Bool.False
3884     | SWAP x -> Bool.False
3885     | MOV x -> Bool.False
3886     | MOVX x -> Bool.False
3887     | SETB x -> Bool.False
3888     | PUSH x -> Bool.False
3889     | POP x -> Bool.False
3890     | XCH (x, x0) -> Bool.False
3891     | XCHD (x, x0) -> Bool.False
3892     | RET -> Bool.False
3893     | RETI -> Bool.False
3894     | NOP -> Bool.False)
3895  | XRL arg ->
3896    (match j with
3897     | ADD (x, x0) -> Bool.False
3898     | ADDC (x, x0) -> Bool.False
3899     | SUBB (x, x0) -> Bool.False
3900     | INC x -> Bool.False
3901     | DEC x -> Bool.False
3902     | MUL (x, x0) -> Bool.False
3903     | DIV (x, x0) -> Bool.False
3904     | DA x -> Bool.False
3905     | JC x -> Bool.False
3906     | JNC x -> Bool.False
3907     | JB (x, x0) -> Bool.False
3908     | JNB (x, x0) -> Bool.False
3909     | JBC (x, x0) -> Bool.False
3910     | JZ x -> Bool.False
3911     | JNZ x -> Bool.False
3912     | CJNE (x, x0) -> Bool.False
3913     | DJNZ (x, x0) -> Bool.False
3914     | ANL x -> Bool.False
3915     | ORL x -> Bool.False
3916     | XRL arg' ->
3917       let prod_eq_left =
3918         Util.eq_prod (fun h h1 ->
3919           eq_addressing_mode
3920             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3921               Vector.VEmpty)) h)
3922             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3923               Vector.VEmpty)) h1)) (fun h h1 ->
3924           eq_addressing_mode
3925             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
3926               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Data,
3927               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Registr, (Vector.VCons
3928               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
3929               Vector.VEmpty)))))))) h)
3930             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
3931               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Data,
3932               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Registr, (Vector.VCons
3933               ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect,
3934               Vector.VEmpty)))))))) h1))
3935       in
3936       let prod_eq_right =
3937         Util.eq_prod (fun h h1 ->
3938           eq_addressing_mode
3939             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
3940               Vector.VEmpty)) h)
3941             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
3942               Vector.VEmpty)) h1)) (fun h h1 ->
3943           eq_addressing_mode
3944             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3945               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3946               h)
3947             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
3948               Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty))))
3949               h1))
3950       in
3951       let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg'
3952     | CLR x -> Bool.False
3953     | CPL x -> Bool.False
3954     | RL x -> Bool.False
3955     | RLC x -> Bool.False
3956     | RR x -> Bool.False
3957     | RRC x -> Bool.False
3958     | SWAP x -> Bool.False
3959     | MOV x -> Bool.False
3960     | MOVX x -> Bool.False
3961     | SETB x -> Bool.False
3962     | PUSH x -> Bool.False
3963     | POP x -> Bool.False
3964     | XCH (x, x0) -> Bool.False
3965     | XCHD (x, x0) -> Bool.False
3966     | RET -> Bool.False
3967     | RETI -> Bool.False
3968     | NOP -> Bool.False)
3969  | CLR arg ->
3970    (match j with
3971     | ADD (x, x0) -> Bool.False
3972     | ADDC (x, x0) -> Bool.False
3973     | SUBB (x, x0) -> Bool.False
3974     | INC x -> Bool.False
3975     | DEC x -> Bool.False
3976     | MUL (x, x0) -> Bool.False
3977     | DIV (x, x0) -> Bool.False
3978     | DA x -> Bool.False
3979     | JC x -> Bool.False
3980     | JNC x -> Bool.False
3981     | JB (x, x0) -> Bool.False
3982     | JNB (x, x0) -> Bool.False
3983     | JBC (x, x0) -> Bool.False
3984     | JZ x -> Bool.False
3985     | JNZ x -> Bool.False
3986     | CJNE (x, x0) -> Bool.False
3987     | DJNZ (x, x0) -> Bool.False
3988     | ANL x -> Bool.False
3989     | ORL x -> Bool.False
3990     | XRL x -> Bool.False
3991     | CLR arg' ->
3992       eq_addressing_mode
3993         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
3994           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
3995           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg)
3996         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
3997           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
3998           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg')
3999     | CPL x -> Bool.False
4000     | RL x -> Bool.False
4001     | RLC x -> Bool.False
4002     | RR x -> Bool.False
4003     | RRC x -> Bool.False
4004     | SWAP x -> Bool.False
4005     | MOV x -> Bool.False
4006     | MOVX x -> Bool.False
4007     | SETB x -> Bool.False
4008     | PUSH x -> Bool.False
4009     | POP x -> Bool.False
4010     | XCH (x, x0) -> Bool.False
4011     | XCHD (x, x0) -> Bool.False
4012     | RET -> Bool.False
4013     | RETI -> Bool.False
4014     | NOP -> Bool.False)
4015  | CPL arg ->
4016    (match j with
4017     | ADD (x, x0) -> Bool.False
4018     | ADDC (x, x0) -> Bool.False
4019     | SUBB (x, x0) -> Bool.False
4020     | INC x -> Bool.False
4021     | DEC x -> Bool.False
4022     | MUL (x, x0) -> Bool.False
4023     | DIV (x, x0) -> Bool.False
4024     | DA x -> Bool.False
4025     | JC x -> Bool.False
4026     | JNC x -> Bool.False
4027     | JB (x, x0) -> Bool.False
4028     | JNB (x, x0) -> Bool.False
4029     | JBC (x, x0) -> Bool.False
4030     | JZ x -> Bool.False
4031     | JNZ x -> Bool.False
4032     | CJNE (x, x0) -> Bool.False
4033     | DJNZ (x, x0) -> Bool.False
4034     | ANL x -> Bool.False
4035     | ORL x -> Bool.False
4036     | XRL x -> Bool.False
4037     | CLR x -> Bool.False
4038     | CPL arg' ->
4039       eq_addressing_mode
4040         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
4041           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
4042           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg)
4043         (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
4044           (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry,
4045           (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg')
4046     | RL x -> Bool.False
4047     | RLC x -> Bool.False
4048     | RR x -> Bool.False
4049     | RRC x -> Bool.False
4050     | SWAP x -> Bool.False
4051     | MOV x -> Bool.False
4052     | MOVX x -> Bool.False
4053     | SETB x -> Bool.False
4054     | PUSH x -> Bool.False
4055     | POP x -> Bool.False
4056     | XCH (x, x0) -> Bool.False
4057     | XCHD (x, x0) -> Bool.False
4058     | RET -> Bool.False
4059     | RETI -> Bool.False
4060     | NOP -> Bool.False)
4061  | RL arg ->
4062    (match j with
4063     | ADD (x, x0) -> Bool.False
4064     | ADDC (x, x0) -> Bool.False
4065     | SUBB (x, x0) -> Bool.False
4066     | INC x -> Bool.False
4067     | DEC x -> Bool.False
4068     | MUL (x, x0) -> Bool.False
4069     | DIV (x, x0) -> Bool.False
4070     | DA x -> Bool.False
4071     | JC x -> Bool.False
4072     | JNC x -> Bool.False
4073     | JB (x, x0) -> Bool.False
4074     | JNB (x, x0) -> Bool.False
4075     | JBC (x, x0) -> Bool.False
4076     | JZ x -> Bool.False
4077     | JNZ x -> Bool.False
4078     | CJNE (x, x0) -> Bool.False
4079     | DJNZ (x, x0) -> Bool.False
4080     | ANL x -> Bool.False
4081     | ORL x -> Bool.False
4082     | XRL x -> Bool.False
4083     | CLR x -> Bool.False
4084     | CPL x -> Bool.False
4085     | RL arg' ->
4086       eq_addressing_mode
4087         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4088           Vector.VEmpty)) arg)
4089         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4090           Vector.VEmpty)) arg')
4091     | RLC x -> Bool.False
4092     | RR x -> Bool.False
4093     | RRC x -> Bool.False
4094     | SWAP x -> Bool.False
4095     | MOV x -> Bool.False
4096     | MOVX x -> Bool.False
4097     | SETB x -> Bool.False
4098     | PUSH x -> Bool.False
4099     | POP x -> Bool.False
4100     | XCH (x, x0) -> Bool.False
4101     | XCHD (x, x0) -> Bool.False
4102     | RET -> Bool.False
4103     | RETI -> Bool.False
4104     | NOP -> Bool.False)
4105  | RLC arg ->
4106    (match j with
4107     | ADD (x, x0) -> Bool.False
4108     | ADDC (x, x0) -> Bool.False
4109     | SUBB (x, x0) -> Bool.False
4110     | INC x -> Bool.False
4111     | DEC x -> Bool.False
4112     | MUL (x, x0) -> Bool.False
4113     | DIV (x, x0) -> Bool.False
4114     | DA x -> Bool.False
4115     | JC x -> Bool.False
4116     | JNC x -> Bool.False
4117     | JB (x, x0) -> Bool.False
4118     | JNB (x, x0) -> Bool.False
4119     | JBC (x, x0) -> Bool.False
4120     | JZ x -> Bool.False
4121     | JNZ x -> Bool.False
4122     | CJNE (x, x0) -> Bool.False
4123     | DJNZ (x, x0) -> Bool.False
4124     | ANL x -> Bool.False
4125     | ORL x -> Bool.False
4126     | XRL x -> Bool.False
4127     | CLR x -> Bool.False
4128     | CPL x -> Bool.False
4129     | RL x -> Bool.False
4130     | RLC arg' ->
4131       eq_addressing_mode
4132         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4133           Vector.VEmpty)) arg)
4134         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4135           Vector.VEmpty)) arg')
4136     | RR x -> Bool.False
4137     | RRC x -> Bool.False
4138     | SWAP x -> Bool.False
4139     | MOV x -> Bool.False
4140     | MOVX x -> Bool.False
4141     | SETB x -> Bool.False
4142     | PUSH x -> Bool.False
4143     | POP x -> Bool.False
4144     | XCH (x, x0) -> Bool.False
4145     | XCHD (x, x0) -> Bool.False
4146     | RET -> Bool.False
4147     | RETI -> Bool.False
4148     | NOP -> Bool.False)
4149  | RR arg ->
4150    (match j with
4151     | ADD (x, x0) -> Bool.False
4152     | ADDC (x, x0) -> Bool.False
4153     | SUBB (x, x0) -> Bool.False
4154     | INC x -> Bool.False
4155     | DEC x -> Bool.False
4156     | MUL (x, x0) -> Bool.False
4157     | DIV (x, x0) -> Bool.False
4158     | DA x -> Bool.False
4159     | JC x -> Bool.False
4160     | JNC x -> Bool.False
4161     | JB (x, x0) -> Bool.False
4162     | JNB (x, x0) -> Bool.False
4163     | JBC (x, x0) -> Bool.False
4164     | JZ x -> Bool.False
4165     | JNZ x -> Bool.False
4166     | CJNE (x, x0) -> Bool.False
4167     | DJNZ (x, x0) -> Bool.False
4168     | ANL x -> Bool.False
4169     | ORL x -> Bool.False
4170     | XRL x -> Bool.False
4171     | CLR x -> Bool.False
4172     | CPL x -> Bool.False
4173     | RL x -> Bool.False
4174     | RLC x -> Bool.False
4175     | RR arg' ->
4176       eq_addressing_mode
4177         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4178           Vector.VEmpty)) arg)
4179         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4180           Vector.VEmpty)) arg')
4181     | RRC x -> Bool.False
4182     | SWAP x -> Bool.False
4183     | MOV x -> Bool.False
4184     | MOVX x -> Bool.False
4185     | SETB x -> Bool.False
4186     | PUSH x -> Bool.False
4187     | POP x -> Bool.False
4188     | XCH (x, x0) -> Bool.False
4189     | XCHD (x, x0) -> Bool.False
4190     | RET -> Bool.False
4191     | RETI -> Bool.False
4192     | NOP -> Bool.False)
4193  | RRC arg ->
4194    (match j with
4195     | ADD (x, x0) -> Bool.False
4196     | ADDC (x, x0) -> Bool.False
4197     | SUBB (x, x0) -> Bool.False
4198     | INC x -> Bool.False
4199     | DEC x -> Bool.False
4200     | MUL (x, x0) -> Bool.False
4201     | DIV (x, x0) -> Bool.False
4202     | DA x -> Bool.False
4203     | JC x -> Bool.False
4204     | JNC x -> Bool.False
4205     | JB (x, x0) -> Bool.False
4206     | JNB (x, x0) -> Bool.False
4207     | JBC (x, x0) -> Bool.False
4208     | JZ x -> Bool.False
4209     | JNZ x -> Bool.False
4210     | CJNE (x, x0) -> Bool.False
4211     | DJNZ (x, x0) -> Bool.False
4212     | ANL x -> Bool.False
4213     | ORL x -> Bool.False
4214     | XRL x -> Bool.False
4215     | CLR x -> Bool.False
4216     | CPL x -> Bool.False
4217     | RL x -> Bool.False
4218     | RLC x -> Bool.False
4219     | RR x -> Bool.False
4220     | RRC arg' ->
4221       eq_addressing_mode
4222         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4223           Vector.VEmpty)) arg)
4224         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4225           Vector.VEmpty)) arg')
4226     | SWAP x -> Bool.False
4227     | MOV x -> Bool.False
4228     | MOVX x -> Bool.False
4229     | SETB x -> Bool.False
4230     | PUSH x -> Bool.False
4231     | POP x -> Bool.False
4232     | XCH (x, x0) -> Bool.False
4233     | XCHD (x, x0) -> Bool.False
4234     | RET -> Bool.False
4235     | RETI -> Bool.False
4236     | NOP -> Bool.False)
4237  | SWAP arg ->
4238    (match j with
4239     | ADD (x, x0) -> Bool.False
4240     | ADDC (x, x0) -> Bool.False
4241     | SUBB (x, x0) -> Bool.False
4242     | INC x -> Bool.False
4243     | DEC x -> Bool.False
4244     | MUL (x, x0) -> Bool.False
4245     | DIV (x, x0) -> Bool.False
4246     | DA x -> Bool.False
4247     | JC x -> Bool.False
4248     | JNC x -> Bool.False
4249     | JB (x, x0) -> Bool.False
4250     | JNB (x, x0) -> Bool.False
4251     | JBC (x, x0) -> Bool.False
4252     | JZ x -> Bool.False
4253     | JNZ x -> Bool.False
4254     | CJNE (x, x0) -> Bool.False
4255     | DJNZ (x, x0) -> Bool.False
4256     | ANL x -> Bool.False
4257     | ORL x -> Bool.False
4258     | XRL x -> Bool.False
4259     | CLR x -> Bool.False
4260     | CPL x -> Bool.False
4261     | RL x -> Bool.False
4262     | RLC x -> Bool.False
4263     | RR x -> Bool.False
4264     | RRC x -> Bool.False
4265     | SWAP arg' ->
4266       eq_addressing_mode
4267         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4268           Vector.VEmpty)) arg)
4269         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4270           Vector.VEmpty)) arg')
4271     | MOV x -> Bool.False
4272     | MOVX x -> Bool.False
4273     | SETB x -> Bool.False
4274     | PUSH x -> Bool.False
4275     | POP x -> Bool.False
4276     | XCH (x, x0) -> Bool.False
4277     | XCHD (x, x0) -> Bool.False
4278     | RET -> Bool.False
4279     | RETI -> Bool.False
4280     | NOP -> Bool.False)
4281  | MOV arg ->
4282    (match j with
4283     | ADD (x, x0) -> Bool.False
4284     | ADDC (x, x0) -> Bool.False
4285     | SUBB (x, x0) -> Bool.False
4286     | INC x -> Bool.False
4287     | DEC x -> Bool.False
4288     | MUL (x, x0) -> Bool.False
4289     | DIV (x, x0) -> Bool.False
4290     | DA x -> Bool.False
4291     | JC x -> Bool.False
4292     | JNC x -> Bool.False
4293     | JB (x, x0) -> Bool.False
4294     | JNB (x, x0) -> Bool.False
4295     | JBC (x, x0) -> Bool.False
4296     | JZ x -> Bool.False
4297     | JNZ x -> Bool.False
4298     | CJNE (x, x0) -> Bool.False
4299     | DJNZ (x, x0) -> Bool.False
4300     | ANL x -> Bool.False
4301     | ORL x -> Bool.False
4302     | XRL x -> Bool.False
4303     | CLR x -> Bool.False
4304     | CPL x -> Bool.False
4305     | RL x -> Bool.False
4306     | RLC x -> Bool.False
4307     | RR x -> Bool.False
4308     | RRC x -> Bool.False
4309     | SWAP x -> Bool.False
4310     | MOV arg' ->
4311       let prod_eq_6 =
4312         Util.eq_prod (fun h h1 ->
4313           eq_addressing_mode
4314             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4315               Vector.VEmpty)) h)
4316             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
4317               Vector.VEmpty)) h1)) (fun h h1 ->
4318           eq_addressing_mode
4319             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
4320               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
4321               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
4322               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
4323               Vector.VEmpty)))))))) h)
4324             (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
4325               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
4326               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
4327               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
4328               Vector.VEmpty)))))))) h1))
4329       in
4330       let prod_eq_5 =
4331         Util.eq_prod (fun h h1 ->
4332           eq_addressing_mode
4333             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
4334               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
4335               Vector.VEmpty)))) h)
4336             (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
4337               Nat.O), Registr, (Vector.VCons (Nat.O, Indirect,
4338               Vector.VEmpty)))) h1)) (fun h h1 ->
4339           eq_addressing_mode
4340             (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
4341               ((Nat.S (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O),
4342               Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))) h)
4343             (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
4344               ((Nat.S (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O),
4345               Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))) h1))
4346       in
4347       let prod_eq_4 =
4348         Util.eq_prod (fun h h1 ->
4349           eq_addressing_mode
4350             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
4351               Vector.VEmpty)) h)
4352             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct,
4353               Vector.VEmpty)) h1)) (fun h h1 ->
4354           eq_addressing_mode
4355             (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
4356               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
4357               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
4358               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
4359               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
4360               Vector.VEmpty)))))))))) h)
4361             (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
4362               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
4363               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
4364               (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
4365               ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data,
4366               Vector.VEmpty)))))))))) h1))
4367       in
4368       let prod_eq_3 =
4369         Util.eq_prod (fun h h1 ->
4370           eq_addressing_mode
4371             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Dptr,
4372               Vector.VEmpty)) h)
4373             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Dptr,
4374               Vector.VEmpty)) h1)) (fun h h1 ->
4375           eq_addressing_mode
4376             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data16,
4377               Vector.VEmpty)) h)
4378             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data16,
4379               Vector.VEmpty)) h1))
4380       in
4381       let prod_eq_2 =
4382         Util.eq_prod (fun h h1 ->
4383           eq_addressing_mode
4384             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
4385               Vector.VEmpty)) h)
4386             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
4387               Vector.VEmpty)) h1)) (fun h h1 ->
4388           eq_addressing_mode
4389             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
4390               Vector.VEmpty)) h)
4391             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
4392               Vector.VEmpty)) h1))
4393       in
4394       let prod_eq_1 =
4395         Util.eq_prod (fun h h1 ->
4396           eq_addressing_mode
4397             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
4398               Vector.VEmpty)) h)
4399             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr,
4400               Vector.VEmpty)) h1)) (fun h h1 ->
4401           eq_addressing_mode
4402             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
4403               Vector.VEmpty)) h)
4404             (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry,
4405               Vector.VEmpty)) h1))
4406       in
4407       let sum_eq_1 = Util.eq_sum prod_eq_6 prod_eq_5 in
4408       let sum_eq_2 = Util.eq_sum sum_eq_1 prod_eq_4 in
4409       let sum_eq_3 = Util.eq_sum sum_eq_2 prod_eq_3 in
4410       let sum_eq_4 = Util.eq_sum sum_eq_3 prod_eq_2 in
4411       let sum_eq_5 = Util.eq_sum sum_eq_4 prod_eq_1 in sum_eq_5 arg arg'
4412     | MOVX x -> Bool.False
4413     | SETB x -> Bool.False
4414     | PUSH x -> Bool.False
4415