source: extracted/aSM.ml @ 2620

Last change on this file since 2620 was 2620, checked in by campbell, 7 years ago

Sufficient hacking to run the extracted Clight semantics.

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