source: extracted/aSM.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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