Context Navigation

source: extracted/interpret.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: 245.5 KB

Line
1	open Preamble
2
3	open Deqsets
4
5	open Sets
6
7	open Bool
8
9	open Relations
10
11	open Nat
12
13	open Hints_declaration
14
15	open Core_notation
16
17	open Pts
18
19	open Logic
20
21	open Types
22
23	open List
24
25	open Listb
26
27	open String
28
29	open LabelledObjects
30
31	open BitVectorTrie
32
33	open Exp
34
35	open Arithmetic
36
37	open Integers
38
39	open AST
40
41	open CostLabel
42
43	open Proper
44
45	open PositiveMap
46
47	open ErrorMessages
48
49	open PreIdentifiers
50
51	open Errors
52
53	open Extralib
54
55	open Setoids
56
57	open Monad
58
59	open Option
60
61	open Lists
62
63	open Positive
64
65	open Identifiers
66
67	open Extranat
68
69	open Vector
70
71	open Div_and_mod
72
73	open Jmeq
74
75	open Russell
76
77	open Util
78
79	open FoldStuff
80
81	open BitVector
82
83	open ASM
84
85	open Status
86
87	open StatusProofs
88
89	open Fetch
90
91	open StructuredTraces
92
93	open AbstractStatus
94
95	(** val execute_1_preinstruction :
96	(Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
97	BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
98	Status.preStatus **)
99	let execute_1_preinstruction ticks cm addr_of instr s =
100	let add_ticks1 = fun s0 ->
101	Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
102	in
103	let add_ticks2 = fun s0 ->
104	Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
105	in
106	(match instr with
107	\| ASM.ADD (addr1, addr2) ->
108	(fun _ ->
109	let s0 = add_ticks1 s in
110	let { Types.fst = result; Types.snd = flags } =
111	Arithmetic.add_8_with_carry
112	(Status.get_arg_8 cm s0 Bool.False
113	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
114	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
115	Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
116	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
117	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
118	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
119	(Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
120	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
121	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
122	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
123	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
124	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
125	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
126	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
127	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
128	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
129	Vector.VEmpty)))))))))))))))))))) addr1))
130	(Status.get_arg_8 cm s0 Bool.False
131	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
132	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
133	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
134	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
135	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
136	Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
137	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
138	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
139	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
140	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
141	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
142	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
143	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
144	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
145	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
146	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
147	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
148	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
149	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
150	Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False
151	in
152	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
153	let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
154	let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
155	let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
156	Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)
157	\| ASM.ADDC (addr1, addr2) ->
158	(fun _ ->
159	let s0 = add_ticks1 s in
160	let old_cy_flag = Status.get_cy_flag cm s0 in
161	let { Types.fst = result; Types.snd = flags } =
162	Arithmetic.add_8_with_carry
163	(Status.get_arg_8 cm s0 Bool.False
164	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
165	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
166	Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
167	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
168	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
169	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
170	(Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
171	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
172	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
173	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
174	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
175	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
176	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
177	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
178	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
179	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
180	Vector.VEmpty)))))))))))))))))))) addr1))
181	(Status.get_arg_8 cm s0 Bool.False
182	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
183	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
184	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
185	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
186	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
187	Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
188	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
189	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
190	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
191	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
192	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
193	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
194	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
195	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
196	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
197	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
198	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
199	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
200	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
201	Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
202	in
203	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
204	let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
205	let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
206	let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
207	Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)
208	\| ASM.SUBB (addr1, addr2) ->
209	(fun _ ->
210	let s0 = add_ticks1 s in
211	let old_cy_flag = Status.get_cy_flag cm s0 in
212	let { Types.fst = result; Types.snd = flags } =
213	Arithmetic.sub_8_with_carry
214	(Status.get_arg_8 cm s0 Bool.False
215	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
216	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
217	Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
218	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
219	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
220	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
221	(Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
222	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
223	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
224	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
225	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
226	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
227	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
228	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
229	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
230	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
231	Vector.VEmpty)))))))))))))))))))) addr1))
232	(Status.get_arg_8 cm s0 Bool.False
233	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
234	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
235	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
236	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
237	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
238	Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
239	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
240	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
241	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
242	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
243	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
244	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
245	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
246	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
247	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
248	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
249	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
250	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
251	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
252	Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
253	in
254	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
255	let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
256	let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
257	let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
258	Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)
259	\| ASM.INC addr ->
260	(fun _ ->
261	(match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
262	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
263	ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
264	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
265	ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
266	(Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with
267	\| ASM.DIRECT d ->
268	(fun _ ->
269	let s' = add_ticks1 s in
270	let result =
271	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
272	(Nat.S Nat.O))))))))
273	(Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d))
274	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
275	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
276	in
277	Status.set_arg_8 cm s' (ASM.DIRECT d) result)
278	\| ASM.INDIRECT i ->
279	(fun _ ->
280	let s' = add_ticks1 s in
281	let result =
282	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
283	(Nat.S Nat.O))))))))
284	(Status.get_arg_8 cm s' Bool.True (ASM.INDIRECT i))
285	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
286	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
287	in
288	Status.set_arg_8 cm s' (ASM.INDIRECT i) result)
289	\| ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
290	\| ASM.REGISTER r ->
291	(fun _ ->
292	let s' = add_ticks1 s in
293	let result =
294	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
295	(Nat.S Nat.O))))))))
296	(Status.get_arg_8 cm s' Bool.True (ASM.REGISTER r))
297	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
298	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
299	in
300	Status.set_arg_8 cm s' (ASM.REGISTER r) result)
301	\| ASM.ACC_A ->
302	(fun _ ->
303	let s' = add_ticks1 s in
304	let result =
305	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
306	(Nat.S Nat.O))))))))
307	(Status.get_arg_8 cm s' Bool.True ASM.ACC_A)
308	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
309	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
310	in
311	Status.set_arg_8 cm s' ASM.ACC_A result)
312	\| ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
313	\| ASM.DPTR ->
314	(fun _ ->
315	let s' = add_ticks1 s in
316	let { Types.fst = carry; Types.snd = bl } =
317	Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
318	(Nat.S (Nat.S Nat.O))))))))
319	(Status.get_8051_sfr cm s' Status.SFR_DPL)
320	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
321	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
322	in
323	let { Types.fst = carry0; Types.snd = bu } =
324	Arithmetic.full_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
325	(Nat.S (Nat.S Nat.O))))))))
326	(Status.get_8051_sfr cm s' Status.SFR_DPH)
327	(BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
328	(Nat.S (Nat.S Nat.O))))))))) carry
329	in
330	let s0 = Status.set_8051_sfr cm s' Status.SFR_DPL bl in
331	Status.set_8051_sfr cm s' Status.SFR_DPH bu)
332	\| ASM.DATA x -> (fun _ -> assert false (* absurd case *))
333	\| ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
334	\| ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
335	\| ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
336	\| ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
337	\| ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
338	\| ASM.CARRY -> (fun _ -> assert false (* absurd case *))
339	\| ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
340	\| ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
341	\| ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
342	\| ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
343	\| ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
344	\| ASM.DEC addr ->
345	(fun _ ->
346	let s0 = add_ticks1 s in
347	let { Types.fst = result; Types.snd = flags } =
348	Arithmetic.sub_8_with_carry
349	(Status.get_arg_8 cm s0 Bool.True
350	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
351	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
352	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
353	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons
354	((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S
355	Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
356	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
357	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
358	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
359	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
360	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
361	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
362	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
363	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
364	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
365	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
366	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
367	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
368	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
369	Vector.VEmpty)))))))))))))))))))) addr))
370	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
371	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
372	in
373	Status.set_arg_8 cm s0
374	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
375	(Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
376	Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
377	ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr,
378	(Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O,
379	ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S
380	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
381	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
382	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
383	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
384	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
385	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
386	ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) result)
387	\| ASM.MUL (addr1, addr2) ->
388	(fun _ ->
389	let s0 = add_ticks1 s in
390	let acc_a_nat =
391	Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
392	(Nat.S (Nat.S (Nat.S Nat.O))))))))
393	(Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
394	in
395	let acc_b_nat =
396	Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
397	(Nat.S (Nat.S (Nat.S Nat.O))))))))
398	(Status.get_8051_sfr cm s0 Status.SFR_ACC_B)
399	in
400	let product = Nat.times acc_a_nat acc_b_nat in
401	let low =
402	Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
403	(Nat.S (Nat.S (Nat.S Nat.O))))))))
404	(Util.modulus product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
405	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
406	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
407	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
408	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
409	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
410	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
411	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
412	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
413	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
414	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
415	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
416	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
417	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
418	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
419	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
420	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
421	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
422	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
423	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
424	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
425	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
426	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
427	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
428	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
429	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
430	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
431	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
432	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
433	Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
434	in
435	let high =
436	Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
437	(Nat.S (Nat.S (Nat.S Nat.O))))))))
438	(Util.division product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
439	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
440	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
443	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
444	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
445	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
446	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
447	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
448	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
449	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
450	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
451	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
452	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
453	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
454	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
455	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
456	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
457	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
458	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
459	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
460	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
461	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
462	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
463	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
464	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
465	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
466	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
467	Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
468	in
469	let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A low in
470	Status.set_8051_sfr cm s1 Status.SFR_ACC_B high)
471	\| ASM.DIV (addr1, addr2) ->
472	(fun _ ->
473	let s0 = add_ticks1 s in
474	let acc_a_nat =
475	Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
476	(Nat.S (Nat.S (Nat.S Nat.O))))))))
477	(Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
478	in
479	let acc_b_nat =
480	Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
481	(Nat.S (Nat.S (Nat.S Nat.O))))))))
482	(Status.get_8051_sfr cm s0 Status.SFR_ACC_B)
483	in
484	(match acc_b_nat with
485	\| Nat.O -> Status.set_flags cm s0 Bool.False Types.None Bool.True
486	\| Nat.S o ->
487	let q =
488	Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
489	(Nat.S (Nat.S (Nat.S Nat.O))))))))
490	(Util.division acc_a_nat (Nat.S o))
491	in
492	let r =
493	Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
494	(Nat.S (Nat.S (Nat.S Nat.O))))))))
495	(Util.modulus acc_a_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
496	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
497	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
498	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
499	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
500	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
501	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
502	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
503	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
504	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
505	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
506	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
507	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
508	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
509	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
510	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
511	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
512	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
513	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
514	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
515	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
516	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
519	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
520	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
521	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
522	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
523	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
524	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
525	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
526	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
527	(Nat.S (Nat.S (Nat.S
528	Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
529	in
530	let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A q in
531	let s2 = Status.set_8051_sfr cm s1 Status.SFR_ACC_B r in
532	Status.set_flags cm s2 Bool.False Types.None Bool.False))
533	\| ASM.DA addr ->
534	(fun _ ->
535	let s0 = add_ticks1 s in
536	let { Types.fst = acc_nu; Types.snd = acc_nl } =
537	Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
538	(Nat.S (Nat.S Nat.O))))
539	(Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
540	in
541	(match Bool.orb
542	(Util.gtb
543	(Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S
544	Nat.O)))) acc_nl) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
545	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
546	(Status.get_ac_flag cm s0) with
547	\| Bool.True ->
548	let { Types.fst = result; Types.snd = flags } =
549	Arithmetic.add_8_with_carry
550	(Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
551	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
552	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
553	(Nat.S (Nat.S (Nat.S Nat.O))))))) Bool.False
554	in
555	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags
556	in
557	let { Types.fst = acc_nu'; Types.snd = acc_nl' } =
558	Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
559	(Nat.S (Nat.S Nat.O)))) result
560	in
561	(match Bool.orb
562	(Util.gtb
563	(Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S
564	Nat.O)))) acc_nu') (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
565	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) cy_flag with
566	\| Bool.True ->
567	let nu =
568	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu'
569	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
570	Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571	Nat.O)))))))
572	in
573	let new_acc =
574	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S
575	(Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl'
576	in
577	let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in
578	Status.set_flags cm s1 cy_flag (Types.Some
579	(Status.get_ac_flag cm s1)) (Status.get_ov_flag cm s1)
580	\| Bool.False -> s0)
581	\| Bool.False -> s0))
582	\| ASM.JC addr ->
583	(fun _ ->
584	match Status.get_cy_flag cm s with
585	\| Bool.True ->
586	let s0 = add_ticks1 s in
587	Status.set_program_counter cm s0 (addr_of addr s0)
588	\| Bool.False -> let s0 = add_ticks2 s in s0)
589	\| ASM.JNC addr ->
590	(fun _ ->
591	match Bool.notb (Status.get_cy_flag cm s) with
592	\| Bool.True ->
593	let s0 = add_ticks1 s in
594	Status.set_program_counter cm s0 (addr_of addr s0)
595	\| Bool.False -> let s0 = add_ticks2 s in s0)
596	\| ASM.JB (addr1, addr2) ->
597	(fun _ ->
598	match Status.get_arg_1 cm s
599	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
600	(Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
601	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
602	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
603	(Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1)
604	Bool.False with
605	\| Bool.True ->
606	let s0 = add_ticks1 s in
607	Status.set_program_counter cm s0 (addr_of addr2 s0)
608	\| Bool.False -> let s0 = add_ticks2 s in s0)
609	\| ASM.JNB (addr1, addr2) ->
610	(fun _ ->
611	match Bool.notb
612	(Status.get_arg_1 cm s
613	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
614	(Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
615	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
616	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
617	ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
618	Vector.VEmpty)))))) addr1) Bool.False) with
619	\| Bool.True ->
620	let s0 = add_ticks1 s in
621	Status.set_program_counter cm s0 (addr_of addr2 s0)
622	\| Bool.False -> let s0 = add_ticks2 s in s0)
623	\| ASM.JBC (addr1, addr2) ->
624	(fun _ ->
625	let s0 =
626	Status.set_arg_1 cm s
627	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
628	Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))
629	(Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons
630	(Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) Bool.False
631	in
632	(match Status.get_arg_1 cm s0
633	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
634	(Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
635	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
636	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
637	(Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1)
638	Bool.False with
639	\| Bool.True ->
640	let s1 = add_ticks1 s0 in
641	Status.set_program_counter cm s1 (addr_of addr2 s1)
642	\| Bool.False -> let s1 = add_ticks2 s0 in s1))
643	\| ASM.JZ addr ->
644	(fun _ ->
645	match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
646	(Nat.S Nat.O))))))))
647	(Status.get_8051_sfr cm s Status.SFR_ACC_A)
648	(BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
649	(Nat.S (Nat.S Nat.O))))))))) with
650	\| Bool.True ->
651	let s0 = add_ticks1 s in
652	Status.set_program_counter cm s0 (addr_of addr s0)
653	\| Bool.False -> let s0 = add_ticks2 s in s0)
654	\| ASM.JNZ addr ->
655	(fun _ ->
656	match Bool.notb
657	(BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
658	(Nat.S (Nat.S Nat.O))))))))
659	(Status.get_8051_sfr cm s Status.SFR_ACC_A)
660	(BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
661	(Nat.S (Nat.S Nat.O)))))))))) with
662	\| Bool.True ->
663	let s0 = add_ticks1 s in
664	Status.set_program_counter cm s0 (addr_of addr s0)
665	\| Bool.False -> let s0 = add_ticks2 s in s0)
666	\| ASM.CJNE (addr1, addr2) ->
667	(fun _ ->
668	match addr1 with
669	\| Types.Inl l ->
670	let { Types.fst = addr10; Types.snd = addr2' } = l in
671	let new_cy =
672	Util.ltb
673	(Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
674	(Nat.S (Nat.S (Nat.S Nat.O))))))))
675	(Status.get_arg_8 cm s Bool.False
676	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
677	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
678	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
679	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
680	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
681	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
682	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
683	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
684	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
685	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
686	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
687	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
688	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
689	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
690	(Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
691	ASM.Ext_indirect, (Vector.VCons (Nat.O,
692	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
693	addr10)))
694	(Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
695	(Nat.S (Nat.S (Nat.S Nat.O))))))))
696	(Status.get_arg_8 cm s Bool.False
697	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
698	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
699	(Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
700	ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
701	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
702	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
703	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
704	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
705	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
706	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
707	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
708	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
709	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
710	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
711	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
712	(Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
713	ASM.Ext_indirect, (Vector.VCons (Nat.O,
714	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
715	addr2')))
716	in
717	(match Bool.notb
718	(BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
719	(Nat.S (Nat.S Nat.O))))))))
720	(Status.get_arg_8 cm s Bool.False
721	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
722	Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
723	(Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
724	(Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons
725	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
726	(Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
727	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
728	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
729	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
730	(Nat.S (Nat.S Nat.O))))))), ASM.Registr,
731	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
732	(Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S
733	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
734	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
735	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
736	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
737	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
738	ASM.Ext_indirect, (Vector.VCons (Nat.O,
739	ASM.Ext_indirect_dptr,
740	Vector.VEmpty)))))))))))))))))))) addr10))
741	(Status.get_arg_8 cm s Bool.False
742	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
743	(Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
744	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
745	(Vector.VCons ((Nat.S Nat.O), ASM.Direct,
746	(Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty))))
747	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
748	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
749	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
750	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
751	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
752	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
753	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
754	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
755	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
756	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
757	(Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
758	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr,
759	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
760	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
761	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
762	Vector.VEmpty)))))))))))))))))))) addr2'))) with
763	\| Bool.True ->
764	let s0 = add_ticks1 s in
765	let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in
766	Status.set_flags cm s1 new_cy Types.None
767	(Status.get_ov_flag cm s1)
768	\| Bool.False ->
769	let s0 = add_ticks2 s in
770	Status.set_flags cm s0 new_cy Types.None
771	(Status.get_ov_flag cm s0))
772	\| Types.Inr r' ->
773	let { Types.fst = addr10; Types.snd = addr2' } = r' in
774	let new_cy =
775	Util.ltb
776	(Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
777	(Nat.S (Nat.S (Nat.S Nat.O))))))))
778	(Status.get_arg_8 cm s Bool.False
779	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
780	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
781	(Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
782	ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
783	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
784	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
785	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
786	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
787	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
788	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
789	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
790	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
791	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
792	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
793	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
794	(Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
795	ASM.Ext_indirect, (Vector.VCons (Nat.O,
796	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
797	addr10)))
798	(Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
799	(Nat.S (Nat.S (Nat.S Nat.O))))))))
800	(Status.get_arg_8 cm s Bool.False
801	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
802	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
803	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Data,
804	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
805	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
806	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
807	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
808	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
809	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
810	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
811	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
812	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
813	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
814	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
815	(Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
816	ASM.Ext_indirect, (Vector.VCons (Nat.O,
817	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
818	addr2')))
819	in
820	(match Bool.notb
821	(BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
822	(Nat.S (Nat.S Nat.O))))))))
823	(Status.get_arg_8 cm s Bool.False
824	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
825	(Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
826	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
827	(Vector.VCons ((Nat.S Nat.O), ASM.Registr,
828	(Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty))))
829	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
830	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
831	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
832	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
833	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
834	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
835	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
836	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
837	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
838	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
839	(Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
840	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr,
841	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
842	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
843	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
844	Vector.VEmpty)))))))))))))))))))) addr10))
845	(Status.get_arg_8 cm s Bool.False
846	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
847	Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
848	(Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
849	(Nat.O, ASM.Data, Vector.VEmpty)) (Vector.VCons
850	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
851	(Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
852	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
853	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
854	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
855	(Nat.S (Nat.S Nat.O))))))), ASM.Registr,
856	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
857	(Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S
858	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
859	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
860	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
861	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
862	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
863	ASM.Ext_indirect, (Vector.VCons (Nat.O,
864	ASM.Ext_indirect_dptr,
865	Vector.VEmpty)))))))))))))))))))) addr2'))) with
866	\| Bool.True ->
867	let s0 = add_ticks1 s in
868	let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in
869	Status.set_flags cm s1 new_cy Types.None
870	(Status.get_ov_flag cm s1)
871	\| Bool.False ->
872	let s0 = add_ticks2 s in
873	Status.set_flags cm s0 new_cy Types.None
874	(Status.get_ov_flag cm s0)))
875	\| ASM.DJNZ (addr1, addr2) ->
876	(fun _ ->
877	let { Types.fst = result; Types.snd = flags } =
878	Arithmetic.sub_8_with_carry
879	(Status.get_arg_8 cm s Bool.True
880	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
881	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
882	(Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
883	ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct,
884	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
885	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
886	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
887	(Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
888	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
889	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
890	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
891	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
892	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
893	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
894	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
895	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
896	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
897	Vector.VEmpty)))))))))))))))))))) addr1))
898	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
899	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
900	in
901	let s0 =
902	Status.set_arg_8 cm s
903	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
904	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
905	(Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O,
906	ASM.Direct, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S
907	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
908	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
909	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
910	Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
911	Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
912	ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
913	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
914	Vector.VEmpty)))))))))))))) addr1) result
915	in
916	(match Bool.notb
917	(BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
918	(Nat.S (Nat.S Nat.O)))))))) result
919	(BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
920	(Nat.S (Nat.S Nat.O)))))))))) with
921	\| Bool.True ->
922	let s1 = add_ticks1 s0 in
923	Status.set_program_counter cm s1 (addr_of addr2 s1)
924	\| Bool.False -> let s1 = add_ticks2 s0 in s1))
925	\| ASM.ANL addr ->
926	(fun _ ->
927	let s0 = add_ticks1 s in
928	(match addr with
929	\| Types.Inl l ->
930	(match l with
931	\| Types.Inl l' ->
932	let { Types.fst = addr1; Types.snd = addr2 } = l' in
933	let and_val =
934	BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
935	(Nat.S (Nat.S (Nat.S Nat.O))))))))
936	(Status.get_arg_8 cm s0 Bool.True
937	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
938	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
939	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
940	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
941	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
942	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
943	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
944	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
945	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
946	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
947	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
948	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
949	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
950	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
951	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
952	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
953	ASM.Ext_indirect, (Vector.VCons (Nat.O,
954	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
955	addr1))
956	(Status.get_arg_8 cm s0 Bool.True
957	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
958	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
959	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
960	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
961	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
962	ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
963	(Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty))))))))
964	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
965	(Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
966	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
967	(Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
968	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
969	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
970	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
971	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
972	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
973	(Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S
974	(Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
975	((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons
976	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
977	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
978	addr2))
979	in
980	Status.set_arg_8 cm s0
981	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
982	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
983	(Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty))
984	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
985	Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
986	(Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
987	((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
988	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
989	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
990	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
991	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
992	Vector.VEmpty)))))))))))))) addr1) and_val
993	\| Types.Inr r ->
994	let { Types.fst = addr1; Types.snd = addr2 } = r in
995	let and_val =
996	BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
997	(Nat.S (Nat.S (Nat.S Nat.O))))))))
998	(Status.get_arg_8 cm s0 Bool.True
999	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1000	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1001	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct,
1002	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1003	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1004	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1005	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1006	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1007	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1008	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1009	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1010	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1011	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1012	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1013	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1014	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1015	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1016	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1017	addr1))
1018	(Status.get_arg_8 cm s0 Bool.True
1019	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1020	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1021	(Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S
1022	Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1023	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1024	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1025	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1026	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1027	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1028	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1029	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1030	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1031	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1032	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1033	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1034	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1035	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1036	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1037	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1038	addr2))
1039	in
1040	Status.set_arg_8 cm s0
1041	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1042	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1043	(Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1044	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1045	Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1046	(Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
1047	((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1048	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1049	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1050	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1051	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1052	Vector.VEmpty)))))))))))))) addr1) and_val)
1053	\| Types.Inr r ->
1054	let { Types.fst = addr1; Types.snd = addr2 } = r in
1055	let and_val =
1056	Bool.andb (Status.get_cy_flag cm s0)
1057	(Status.get_arg_1 cm s0
1058	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1059	Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O),
1060	ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1061	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1062	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1063	(Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1064	Bool.True)
1065	in
1066	Status.set_flags cm s0 and_val Types.None
1067	(Status.get_ov_flag cm s0)))
1068	\| ASM.ORL addr ->
1069	(fun _ ->
1070	let s0 = add_ticks1 s in
1071	(match addr with
1072	\| Types.Inl l ->
1073	(match l with
1074	\| Types.Inl l' ->
1075	let { Types.fst = addr1; Types.snd = addr2 } = l' in
1076	let or_val =
1077	BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1078	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1079	(Status.get_arg_8 cm s0 Bool.True
1080	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1081	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1082	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1083	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1084	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1085	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1086	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1087	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1088	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1089	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1090	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1091	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1092	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1093	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1094	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1095	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1096	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1097	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1098	addr1))
1099	(Status.get_arg_8 cm s0 Bool.True
1100	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1101	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
1102	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
1103	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1104	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1105	ASM.Data, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1106	(Vector.VCons (Nat.O, ASM.Indirect,
1107	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S
1108	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1109	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1110	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1111	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1112	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1113	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1114	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1115	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1116	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1117	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1118	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1119	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1120	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1121	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1122	addr2))
1123	in
1124	Status.set_arg_8 cm s0
1125	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1126	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1127	(Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty))
1128	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1129	Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1130	(Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
1131	((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1132	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1133	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1134	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1135	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1136	Vector.VEmpty)))))))))))))) addr1) or_val
1137	\| Types.Inr r ->
1138	let { Types.fst = addr1; Types.snd = addr2 } = r in
1139	let or_val =
1140	BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1141	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1142	(Status.get_arg_8 cm s0 Bool.True
1143	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1144	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1145	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct,
1146	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1147	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1148	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1149	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1150	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1151	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1152	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1153	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1154	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1155	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1156	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1157	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1158	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1159	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1160	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1161	addr1))
1162	(Status.get_arg_8 cm s0 Bool.True
1163	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1164	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1165	(Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S
1166	Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1167	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1168	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1169	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1170	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1171	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1172	(Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1173	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1174	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1175	(Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1176	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1177	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1178	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1179	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1180	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1181	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1182	addr2))
1183	in
1184	Status.set_arg_8 cm s0
1185	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1186	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1187	(Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1188	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1189	Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1190	(Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
1191	((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1192	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1193	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1194	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1195	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1196	Vector.VEmpty)))))))))))))) addr1) or_val)
1197	\| Types.Inr r ->
1198	let { Types.fst = addr1; Types.snd = addr2 } = r in
1199	let or_val =
1200	Bool.orb (Status.get_cy_flag cm s0)
1201	(Status.get_arg_1 cm s0
1202	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1203	Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O),
1204	ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1205	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1206	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1207	(Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1208	Bool.True)
1209	in
1210	Status.set_flags cm s0 or_val Types.None (Status.get_ov_flag cm s0)))
1211	\| ASM.XRL addr ->
1212	(fun _ ->
1213	let s0 = add_ticks1 s in
1214	(match addr with
1215	\| Types.Inl l' ->
1216	let { Types.fst = addr1; Types.snd = addr2 } = l' in
1217	let xor_val =
1218	BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1219	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1220	(Status.get_arg_8 cm s0 Bool.True
1221	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1222	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1223	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1224	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1225	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1226	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1227	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1228	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1229	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1230	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1231	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1232	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1233	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1234	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1235	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1236	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1237	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1238	addr1))
1239	(Status.get_arg_8 cm s0 Bool.True
1240	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1241	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1242	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
1243	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data, (Vector.VCons
1244	((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S
1245	Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
1246	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1247	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1248	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1249	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1250	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1251	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1252	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1253	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1254	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1255	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1256	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1257	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1258	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1259	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1260	addr2))
1261	in
1262	Status.set_arg_8 cm s0
1263	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1264	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1265	(Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1266	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1267	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1268	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1269	Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1270	Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1271	ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1272	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1273	Vector.VEmpty)))))))))))))) addr1) xor_val
1274	\| Types.Inr r ->
1275	let { Types.fst = addr1; Types.snd = addr2 } = r in
1276	let xor_val =
1277	BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1278	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1279	(Status.get_arg_8 cm s0 Bool.True
1280	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1281	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1282	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct,
1283	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1284	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1285	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1286	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1287	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1288	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1289	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1290	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1291	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1292	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1293	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1294	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1295	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1296	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1297	addr1))
1298	(Status.get_arg_8 cm s0 Bool.True
1299	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1300	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1301	(Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
1302	ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1303	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1304	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1305	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1306	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1307	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1308	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1309	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1310	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1311	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1312	(Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1313	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1314	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1315	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1316	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1317	addr2))
1318	in
1319	Status.set_arg_8 cm s0
1320	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1321	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1322	(Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S
1323	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1324	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1325	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1326	Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1327	Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1328	ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1329	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1330	Vector.VEmpty)))))))))))))) addr1) xor_val))
1331	\| ASM.CLR addr ->
1332	(fun _ ->
1333	(match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
1334	((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
1335	Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr,
1336	Vector.VEmpty)))))) addr with
1337	\| ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1338	\| ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1339	\| ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1340	\| ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1341	\| ASM.ACC_A ->
1342	(fun _ ->
1343	let s0 = add_ticks1 s in
1344	Status.set_arg_8 cm s0 ASM.ACC_A
1345	(BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1346	(Nat.S (Nat.S Nat.O))))))))))
1347	\| ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1348	\| ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1349	\| ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1350	\| ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1351	\| ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1352	\| ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1353	\| ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1354	\| ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1355	\| ASM.CARRY ->
1356	(fun _ ->
1357	let s0 = add_ticks1 s in
1358	Status.set_arg_1 cm s0 ASM.CARRY Bool.False)
1359	\| ASM.BIT_ADDR b ->
1360	(fun _ ->
1361	let s0 = add_ticks1 s in
1362	Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.False)
1363	\| ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1364	\| ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1365	\| ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1366	\| ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1367	\| ASM.CPL addr ->
1368	(fun _ ->
1369	(match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
1370	((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
1371	Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr,
1372	Vector.VEmpty)))))) addr with
1373	\| ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1374	\| ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1375	\| ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1376	\| ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1377	\| ASM.ACC_A ->
1378	(fun _ ->
1379	let s0 = add_ticks1 s in
1380	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1381	let new_acc =
1382	BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1383	(Nat.S (Nat.S Nat.O)))))))) old_acc
1384	in
1385	Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1386	\| ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1387	\| ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1388	\| ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1389	\| ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1390	\| ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1391	\| ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1392	\| ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1393	\| ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1394	\| ASM.CARRY ->
1395	(fun _ ->
1396	let s0 = add_ticks1 s in
1397	let old_cy_flag = Status.get_arg_1 cm s0 ASM.CARRY Bool.True in
1398	let new_cy_flag = Bool.notb old_cy_flag in
1399	Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag)
1400	\| ASM.BIT_ADDR b ->
1401	(fun _ ->
1402	let s0 = add_ticks1 s in
1403	let old_bit = Status.get_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.True
1404	in
1405	let new_bit = Bool.notb old_bit in
1406	Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) new_bit)
1407	\| ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1408	\| ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1409	\| ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1410	\| ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1411	\| ASM.RL x ->
1412	(fun _ ->
1413	let s0 = add_ticks1 s in
1414	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1415	let new_acc =
1416	Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1417	(Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc
1418	in
1419	Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1420	\| ASM.RLC x ->
1421	(fun _ ->
1422	let s0 = add_ticks1 s in
1423	let old_cy_flag = Status.get_cy_flag cm s0 in
1424	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1425	let new_cy_flag =
1426	Vector.get_index' Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1427	(Nat.S Nat.O))))))) old_acc
1428	in
1429	let new_acc =
1430	Vector.shift_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1431	(Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc old_cy_flag
1432	in
1433	let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in
1434	Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc)
1435	\| ASM.RR x ->
1436	(fun _ ->
1437	let s0 = add_ticks1 s in
1438	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1439	let new_acc =
1440	Vector.rotate_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1441	(Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc
1442	in
1443	Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1444	\| ASM.RRC x ->
1445	(fun _ ->
1446	let s0 = add_ticks1 s in
1447	let old_cy_flag = Status.get_cy_flag cm s0 in
1448	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1449	let new_cy_flag =
1450	Vector.get_index' (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1451	Nat.O))))))) Nat.O old_acc
1452	in
1453	let new_acc =
1454	Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455	Nat.O))))))) (Nat.S Nat.O) old_acc old_cy_flag
1456	in
1457	let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in
1458	Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc)
1459	\| ASM.SWAP x ->
1460	(fun _ ->
1461	let s0 = add_ticks1 s in
1462	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1463	let { Types.fst = nu; Types.snd = nl } =
1464	Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1465	(Nat.S (Nat.S Nat.O)))) old_acc
1466	in
1467	let new_acc =
1468	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1469	(Nat.S (Nat.S Nat.O)))) nl nu
1470	in
1471	Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1472	\| ASM.MOV addr ->
1473	(fun _ ->
1474	let s0 = add_ticks1 s in
1475	(match addr with
1476	\| Types.Inl l ->
1477	(match l with
1478	\| Types.Inl l' ->
1479	(match l' with
1480	\| Types.Inl l'' ->
1481	(match l'' with
1482	\| Types.Inl l''' ->
1483	(match l''' with
1484	\| Types.Inl l'''' ->
1485	let { Types.fst = addr1; Types.snd = addr2 } = l'''' in
1486	Status.set_arg_8 cm s0
1487	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
1488	Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1489	Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1490	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1491	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1492	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1493	Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S
1494	(Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1495	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1496	ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1497	ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
1498	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1499	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))
1500	addr1)
1501	(Status.get_arg_8 cm s0 Bool.False
1502	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
1503	(Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S
1504	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1505	Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S
1506	(Nat.S Nat.O))), ASM.Registr, (Vector.VCons
1507	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
1508	((Nat.S Nat.O), ASM.Indirect, (Vector.VCons
1509	(Nat.O, ASM.Data, Vector.VEmpty))))))))
1510	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1512	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1513	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1514	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1515	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1516	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1517	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1518	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1519	Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S
1520	(Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data,
1521	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1522	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1523	Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1524	Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1525	ASM.Ext_indirect_dptr,
1526	Vector.VEmpty)))))))))))))))))))) addr2))
1527	\| Types.Inr r'''' ->
1528	let { Types.fst = addr1; Types.snd = addr2 } = r'''' in
1529	Status.set_arg_8 cm s0
1530	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
1531	(Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1532	(Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O),
1533	ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
1534	Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S
1535	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1536	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1537	(Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1538	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1539	Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S
1540	(Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons
1541	((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1542	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1543	(Nat.O, ASM.Ext_indirect_dptr,
1544	Vector.VEmpty)))))))))))))) addr1)
1545	(Status.get_arg_8 cm s0 Bool.False
1546	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
1547	(Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1548	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
1549	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
1550	(Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1551	(Vector.VCons (Nat.O, ASM.Data,
1552	Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S
1553	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1554	Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1555	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1556	Nat.O)))))))), ASM.Indirect, (Vector.VCons
1557	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1558	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1559	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1560	ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1561	(Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1562	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1563	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1564	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
1565	((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons
1566	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1567	(Nat.O, ASM.Ext_indirect_dptr,
1568	Vector.VEmpty)))))))))))))))))))) addr2)))
1569	\| Types.Inr r''' ->
1570	let { Types.fst = addr1; Types.snd = addr2 } = r''' in
1571	Status.set_arg_8 cm s0
1572	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
1573	Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1574	Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct,
1575	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1576	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1577	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1578	Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S
1579	(Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
1580	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1581	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1582	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1583	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1584	Vector.VEmpty)))))))))))))) addr1)
1585	(Status.get_arg_8 cm s0 Bool.False
1586	(ASM.subaddressing_modeel__o__mk_subaddressing_mode
1587	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1588	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1589	Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1590	(Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S
1591	(Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
1592	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
1593	((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O,
1594	ASM.Data, Vector.VEmpty)))))))))) (Vector.VCons
1595	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596	(Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
1597	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1598	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1599	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1600	(Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1601	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1602	(Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S
1603	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1604	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1605	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1606	(Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
1607	(Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1608	Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1609	ASM.Ext_indirect_dptr,
1610	Vector.VEmpty)))))))))))))))))))) addr2)))
1611	\| Types.Inr r'' ->
1612	let { Types.fst = addr1; Types.snd = addr2 } = r'' in
1613	Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1)
1614	\| Types.Inr r ->
1615	let { Types.fst = addr1; Types.snd = addr2 } = r in
1616	Status.set_arg_1 cm s0
1617	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1618	(Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Carry,
1619	Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr,
1620	(Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1)
1621	(Status.get_arg_1 cm s0
1622	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1623	(Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
1624	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1625	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
1626	ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
1627	Vector.VEmpty)))))) addr2) Bool.False))
1628	\| Types.Inr r ->
1629	let { Types.fst = addr1; Types.snd = addr2 } = r in
1630	Status.set_arg_1 cm s0
1631	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1632	Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))
1633	(Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons
1634	(Nat.O, ASM.Carry, Vector.VEmpty)))) addr1)
1635	(Status.get_arg_1 cm s0
1636	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1637	(Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Carry,
1638	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1639	ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1640	(Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1641	Bool.False)))
1642	\| ASM.MOVX addr ->
1643	(fun _ ->
1644	let s0 = add_ticks1 s in
1645	(match addr with
1646	\| Types.Inl l ->
1647	let { Types.fst = addr1; Types.snd = addr2 } = l in
1648	Status.set_arg_8 cm s0
1649	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1650	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1651	(Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1652	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1653	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1654	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1655	Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1656	Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1657	ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1658	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1659	Vector.VEmpty)))))))))))))) addr1)
1660	(Status.get_arg_8 cm s0 Bool.False
1661	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1662	Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1663	(Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
1664	ASM.Ext_indirect, (Vector.VCons (Nat.O,
1665	ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons
1666	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1667	(Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1668	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1669	Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S
1670	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1671	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1672	Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1673	(Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S
1674	(Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
1675	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
1676	((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1677	Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1678	ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1679	addr2))
1680	\| Types.Inr r ->
1681	let { Types.fst = addr1; Types.snd = addr2 } = r in
1682	Status.set_arg_8 cm s0
1683	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
1684	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1685	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1686	(Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons
1687	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1688	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1689	Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1690	(Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
1691	(Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1692	Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
1693	ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1694	Vector.VEmpty)))))))))))))) addr1)
1695	(Status.get_arg_8 cm s0 Bool.False
1696	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1697	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1698	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1699	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1700	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1701	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1702	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1703	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1704	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1705	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1706	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1707	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1708	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1709	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1710	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1711	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1712	Vector.VEmpty)))))))))))))))))))) addr2))))
1713	\| ASM.SETB b ->
1714	(fun _ ->
1715	let s0 = add_ticks1 s in
1716	Status.set_arg_1 cm s0
1717	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
1718	(Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Carry,
1719	(Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))
1720	(Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O,
1721	ASM.Carry, Vector.VEmpty)))) b) Bool.False)
1722	\| ASM.PUSH addr ->
1723	(fun _ ->
1724	let s0 = add_ticks1 s in
1725	let new_sp =
1726	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1727	(Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_SP)
1728	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1729	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
1730	in
1731	let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1732	Status.write_at_stack_pointer cm s1
1733	(Status.get_arg_8 cm s1 Bool.False
1734	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1735	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1736	Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1737	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1738	(Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1739	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1740	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1741	(Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1742	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1743	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1744	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1745	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1746	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
1747	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1748	(Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1749	addr)))
1750	\| ASM.POP addr ->
1751	(fun _ ->
1752	let s0 = add_ticks1 s in
1753	let contents = Status.read_at_stack_pointer cm s0 in
1754	let { Types.fst = new_sp; Types.snd = flags } =
1755	Arithmetic.sub_8_with_carry
1756	(Status.get_8051_sfr cm s0 Status.SFR_SP)
1757	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1758	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1759	in
1760	let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1761	Status.set_arg_8 cm s1
1762	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1763	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1764	(Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1765	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
1766	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1767	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1768	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1769	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1770	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1771	ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) contents)
1772	\| ASM.XCH (addr1, addr2) ->
1773	(fun _ ->
1774	let s0 = add_ticks1 s in
1775	let old_addr =
1776	Status.get_arg_8 cm s0 Bool.False
1777	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
1778	Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1779	(Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1780	ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1781	(Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty))))))
1782	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1783	(Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1784	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1785	ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1786	(Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1787	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1788	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1789	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1790	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1791	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
1792	(Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1793	(Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1794	addr2)
1795	in
1796	let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1797	let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A old_addr in
1798	Status.set_arg_8 cm s1
1799	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
1800	Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1801	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons
1802	((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
1803	Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1804	(Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S
1805	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1806	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1807	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1808	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1809	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1810	ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) old_acc)
1811	\| ASM.XCHD (addr1, addr2) ->
1812	(fun _ ->
1813	let s0 = add_ticks1 s in
1814	let { Types.fst = acc_nu; Types.snd = acc_nl } =
1815	Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1816	(Nat.S (Nat.S Nat.O))))
1817	(Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
1818	in
1819	let { Types.fst = arg_nu; Types.snd = arg_nl } =
1820	Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1821	(Nat.S (Nat.S Nat.O))))
1822	(Status.get_arg_8 cm s0 Bool.False
1823	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1824	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1825	Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Indirect,
1826	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1827	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
1828	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1829	(Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
1830	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1831	Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1832	(Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
1833	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1834	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1835	ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1836	ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1837	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1838	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1839	Vector.VEmpty)))))))))))))))))))) addr2))
1840	in
1841	let new_acc =
1842	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1843	(Nat.S (Nat.S Nat.O)))) acc_nu arg_nl
1844	in
1845	let new_arg =
1846	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1847	(Nat.S (Nat.S Nat.O)))) arg_nu acc_nl
1848	in
1849	let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in
1850	Status.set_arg_8 cm s1
1851	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1852	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1853	(Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1854	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
1855	((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1856	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1857	(Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1858	(Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1859	((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1860	ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) new_arg)
1861	\| ASM.RET ->
1862	(fun _ ->
1863	let s0 = add_ticks1 s in
1864	let high_bits = Status.read_at_stack_pointer cm s0 in
1865	let { Types.fst = new_sp; Types.snd = flags } =
1866	Arithmetic.sub_8_with_carry
1867	(Status.get_8051_sfr cm s0 Status.SFR_SP)
1868	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1869	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1870	in
1871	let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1872	let low_bits = Status.read_at_stack_pointer cm s1 in
1873	let { Types.fst = new_sp0; Types.snd = flags0 } =
1874	Arithmetic.sub_8_with_carry
1875	(Status.get_8051_sfr cm s1 Status.SFR_SP)
1876	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1877	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1878	in
1879	let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
1880	let new_pc =
1881	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1882	(Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1883	(Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
1884	in
1885	Status.set_program_counter cm s2 new_pc)
1886	\| ASM.RETI ->
1887	(fun _ ->
1888	let s0 = add_ticks1 s in
1889	let high_bits = Status.read_at_stack_pointer cm s0 in
1890	let { Types.fst = new_sp; Types.snd = flags } =
1891	Arithmetic.sub_8_with_carry
1892	(Status.get_8051_sfr cm s0 Status.SFR_SP)
1893	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1894	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1895	in
1896	let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1897	let low_bits = Status.read_at_stack_pointer cm s1 in
1898	let { Types.fst = new_sp0; Types.snd = flags0 } =
1899	Arithmetic.sub_8_with_carry
1900	(Status.get_8051_sfr cm s1 Status.SFR_SP)
1901	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1902	(Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1903	in
1904	let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
1905	let new_pc =
1906	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1907	(Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1908	(Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
1909	in
1910	Status.set_program_counter cm s2 new_pc)
1911	\| ASM.NOP -> (fun _ -> let s0 = add_ticks1 s in s0)
1912	\| ASM.JMP x ->
1913	(fun _ ->
1914	let s0 = add_ticks1 s in
1915	let dptr =
1916	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1917	(Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1918	(Nat.S (Nat.S Nat.O))))))))
1919	(Status.get_8051_sfr cm s0 Status.SFR_DPH)
1920	(Status.get_8051_sfr cm s0 Status.SFR_DPL)
1921	in
1922	let big_acc =
1923	Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1924	(Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1925	(Nat.S (Nat.S Nat.O))))))))
1926	(BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1927	(Nat.S Nat.O)))))))))
1928	(Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
1929	in
1930	let jmp_addr =
1931	Arithmetic.add
1932	(Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1933	Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1934	(Nat.S Nat.O))))))))) big_acc dptr
1935	in
1936	let new_pc =
1937	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1938	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1939	Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
1940	in
1941	Status.set_program_counter cm s0 new_pc)) __
1942
1943	(** val execute_1_preinstruction_ok' :
1944	(Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
1945	BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
1946	Status.preStatus Types.sig0 **)
1947	let execute_1_preinstruction_ok' ticks cm addr_of instr s =
1948	let add_ticks1 = fun s0 ->
1949	Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
1950	in
1951	let add_ticks2 = fun s0 ->
1952	Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
1953	in
1954	(match instr with
1955	\| ASM.ADD (addr1, addr2) ->
1956	(fun _ ->
1957	let s0 = add_ticks1 s in
1958	(let { Types.fst = result; Types.snd = flags } =
1959	Arithmetic.add_8_with_carry
1960	(Status.get_arg_8 cm s0 Bool.False
1961	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1962	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1963	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1964	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1965	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1966	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1967	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1968	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1969	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1970	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1971	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1972	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1973	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1974	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1975	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1976	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1977	Vector.VEmpty)))))))))))))))))))) addr1))
1978	(Status.get_arg_8 cm s0 Bool.False
1979	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1980	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1981	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
1982	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
1983	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
1984	Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1985	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1986	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1987	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1988	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1989	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1990	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1991	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1992	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1993	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1994	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1995	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1996	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1997	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1998	Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False
1999	in
2000	(fun _ ->
2001	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2002	let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2003	let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2004	let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2005	Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2006	\| ASM.ADDC (addr1, addr2) ->
2007	(fun _ ->
2008	let s0 = add_ticks1 s in
2009	let old_cy_flag = Status.get_cy_flag cm s0 in
2010	(let { Types.fst = result; Types.snd = flags } =
2011	Arithmetic.add_8_with_carry
2012	(Status.get_arg_8 cm s0 Bool.False
2013	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
2014	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2015	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
2016	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2017	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2018	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2019	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2020	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2021	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2022	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2023	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2024	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2025	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2026	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2027	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2028	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2029	Vector.VEmpty)))))))))))))))))))) addr1))
2030	(Status.get_arg_8 cm s0 Bool.False
2031	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2032	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2033	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2034	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2035	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2036	Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2037	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2038	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2039	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2040	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2041	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2042	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2043	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2044	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2045	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2046	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2047	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2048	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2049	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2050	Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
2051	in
2052	(fun _ ->
2053	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2054	let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2055	let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2056	let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2057	Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2058	\| ASM.SUBB (addr1, addr2) ->
2059	(fun _ ->
2060	let s0 = add_ticks1 s in
2061	let old_cy_flag = Status.get_cy_flag cm s0 in
2062	(let { Types.fst = result; Types.snd = flags } =
2063	Arithmetic.sub_8_with_carry
2064	(Status.get_arg_8 cm s0 Bool.False
2065	(ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
2066	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2067	(Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
2068	Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2069	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2070	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2071	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2072	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2073	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2074	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2075	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2076	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2077	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2078	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2079	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2080	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2081	Vector.VEmpty)))))))))))))))))))) addr1))
2082	(Status.get_arg_8 cm s0 Bool.False
2083	(ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2084	(Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2085	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2086	((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2087	((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2088	Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2089	Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2090	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2091	ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2092	(Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2093	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2094	(Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2095	(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2096	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2097	ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2098	Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2099	Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2100	ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2101	(Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2102	Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
2103	in
2104	(fun _ ->
2105	let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2106	let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2107	let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2108	let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2109	Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2110	\| ASM.INC addr ->
2111	(fun _ ->
2112	(match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
2113	(Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2114	ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2115	ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2116	ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
2117	(Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with
2118	\| ASM.DIRECT d ->
2119	(fun _ _ ->
2120	let s' = add_ticks1 s in
2121	let result =
2122	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2123	(Nat.S Nat.O))))))))
2124	(Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d))
2125	(Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
2126	(Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
2127	in
2128	Status.set_arg_8 cm s' (ASM.DIRECT d) result)
2129	\| ASM.INDIRECT i ->
2130	(fun _ _ ->
2131	let s' = add_ticks1 s in
2132	let result =
2133	Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2134	(Nat.S Nat.O)))