Context Navigation

source: extracted/aSM.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 206.8 KB

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