source: Deliverables/D4.2-4.3/ASM/I8051.ma @ 491

Last change on this file since 491 was 491, checked in by mulligan, 8 years ago

Initial commit of (part)-formalisation of LIN intermediate language.

File size: 134.7 KB
Line 
1include "arithmetics/nat.ma".
2
3include "cerco/String.ma".
4include "cerco/ASM.ma".
5include "cerco-intermediate-languages/utilities/Compare.ma".
6
7(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
8        not further back in the translation chain.                            *)
9inductive OpAccs: Type[0] ≝
10  Mul: OpAccs
11| Divu: OpAccs
12| Modu: OpAccs.
13
14inductive Op1: Type[0] ≝
15  Cmpl: Op1
16| Inc: Op1.
17
18inductive Op2: Type[0] ≝
19  Add: Op2
20| Addc: Op2
21| Sub: Op2
22| And: Op2
23| Or: Op2
24| Xor: Op2.
25
26(* dpm: maybe useless? *)
27inductive Register: Type[0] ≝
28  Register00: Register
29| Register01: Register
30| Register02: Register
31| Register03: Register
32| Register04: Register
33| Register05: Register
34| Register06: Register
35| Register07: Register
36| Register10: Register
37| Register11: Register
38| Register12: Register
39| Register13: Register
40| Register14: Register
41| Register15: Register
42| Register16: Register
43| Register17: Register
44| Register20: Register
45| Register21: Register
46| Register22: Register
47| Register23: Register
48| Register24: Register
49| Register25: Register
50| Register26: Register
51| Register27: Register
52| Register30: Register
53| Register31: Register
54| Register32: Register
55| Register33: Register
56| Register34: Register
57| Register35: Register
58| Register36: Register
59| Register37: Register
60| RegisterA: Register
61| RegisterB: Register
62| RegisterDPL: Register
63| RegisterDPH: Register.
64
65definition nat_of_register: Register → nat ≝
66  λr: Register.
67  match r with
68  [ Register00 ⇒ 0
69  | Register01 ⇒ 1
70  | Register02 ⇒ 2
71  | Register03 ⇒ 3
72  | Register04 ⇒ 4
73  | Register05 ⇒ 5
74  | Register06 ⇒ 6
75  | Register07 ⇒ 7
76  | Register10 ⇒ 8
77  | Register11 ⇒ 9
78  | Register12 ⇒ 10
79  | Register13 ⇒ 11
80  | Register14 ⇒ 12
81  | Register15 ⇒ 13
82  | Register16 ⇒ 14
83  | Register17 ⇒ 15
84  | Register20 ⇒ 16
85  | Register21 ⇒ 17
86  | Register22 ⇒ 18
87  | Register23 ⇒ 19
88  | Register24 ⇒ 20
89  | Register25 ⇒ 21
90  | Register26 ⇒ 22
91  | Register27 ⇒ 23
92  | Register30 ⇒ 24
93  | Register31 ⇒ 25
94  | Register32 ⇒ 26
95  | Register33 ⇒ 27
96  | Register34 ⇒ 28
97  | Register35 ⇒ 29
98  | Register36 ⇒ 30
99  | Register37 ⇒ 31
100  | RegisterA ⇒ 32
101  | RegisterB ⇒ 33
102  | RegisterDPL ⇒ 34
103  | RegisterDPH ⇒ 35
104  ].
105
106definition compare_register: Register → Register → Compare ≝
107  λr, s: Register.
108    let r_as_nat ≝ nat_of_register r in
109    let s_as_nat ≝ nat_of_register s in
110      if eqb r_as_nat s_as_nat then
111        Compare_Equal
112      else if ltb r_as_nat s_as_nat then
113        Compare_Less
114      else
115        Compare_Greater.
116
117definition eq_register: Register → Register → bool ≝
118  λr, s: Register.
119  let r_as_nat ≝ nat_of_register r in
120  let s_as_nat ≝ nat_of_register s in
121    eqb r_as_nat s_as_nat.
122
123axiom print_register: Register → String.
124
125(* dpm: registers for stack manipulation *)
126definition RegisterSST ≝ Register03.
127definition RegisterST0 ≝ Register04.
128definition RegisterST1 ≝ Register05.
129definition RegisterSPL ≝ Register06.
130definition RegisterSPH ≝ Register07.
131
132definition register_address: Register → addressing_mode ≝
133  λr: Register.
134    match r with
135    [ Register00 ⇒ REGISTER [[ false; false; false ]]
136    | Register01 ⇒ REGISTER [[ false; false; true ]]
137    | Register02 ⇒ REGISTER [[ false; true; false ]]
138    | Register03 ⇒ REGISTER [[ false; true; true ]]
139    | Register04 ⇒ REGISTER [[ true; false; false ]]
140    | Register05 ⇒ REGISTER [[ true; false; true ]]
141    | Register06 ⇒ REGISTER [[ true; true; false ]]
142    | Register07 ⇒ REGISTER [[ true; true; true ]]
143    | RegisterA ⇒ ACC_A
144    | RegisterB ⇒ ACC_B
145    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
146    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
147    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
148    ].
149   
150definition registers: list Register ≝
151  [ Register00; Register01; Register02; Register03;
152    Register04; Register05; Register06; Register07;
153    RegisterA; RegisterB; RegisterDPL; RegisterDPH;
154    Register10; Register11; Register12; Register13;
155    Register14; Register15; Register16; Register17;
156    Register20; Register21; Register22; Register23;
157    Register24; Register25; Register26; Register27;
158    Register30; Register31; Register32; Register33;
159    Register34; Register35; Register36; Register37;
160    RegisterSST; RegisterST0; RegisterST1;
161    RegisterSPL; RegisterSPH ].
162   
163definition forbidden_registers: list Register ≝
164  [ RegisterSST; RegisterST0; RegisterST1;
165    RegisterSPL; RegisterSPH ].
166   
167record RegisterMap: Type[0] ≝
168{
169  register_00_value: option Byte;
170  register_01_value: option Byte;
171  register_02_value: option Byte;
172  register_03_value: option Byte;
173  register_04_value: option Byte;
174  register_05_value: option Byte;
175  register_06_value: option Byte;
176  register_07_value: option Byte;
177  register_10_value: option Byte;
178  register_11_value: option Byte;
179  register_12_value: option Byte;
180  register_13_value: option Byte;
181  register_14_value: option Byte;
182  register_15_value: option Byte;
183  register_16_value: option Byte;
184  register_17_value: option Byte;
185  register_20_value: option Byte;
186  register_21_value: option Byte;
187  register_22_value: option Byte;
188  register_23_value: option Byte;
189  register_24_value: option Byte;
190  register_25_value: option Byte;
191  register_26_value: option Byte;
192  register_27_value: option Byte;
193  register_30_value: option Byte;
194  register_31_value: option Byte;
195  register_32_value: option Byte;
196  register_33_value: option Byte;
197  register_34_value: option Byte;
198  register_35_value: option Byte;
199  register_36_value: option Byte;
200  register_37_value: option Byte;
201  register_A_value: option Byte;
202  register_B_value: option Byte;
203  register_DPL_value: option Byte;
204  register_DPH_value: option Byte
205}.
206
207definition initialize_register_map: RegisterMap ≝
208  mk_RegisterMap (None ?) (None ?) (None ?) (None ?)
209                 (None ?) (None ?) (None ?) (None ?)
210                 (None ?) (None ?) (None ?) (None ?)
211                 (None ?) (None ?) (None ?) (None ?)
212                 (None ?) (None ?) (None ?) (None ?)
213                 (None ?) (None ?) (None ?) (None ?)
214                 (None ?) (None ?) (None ?) (None ?)
215                 (None ?) (None ?) (None ?) (None ?)
216                 (None ?) (None ?) (None ?) (None ?).
217                 
218definition lookup_register_map: Register → RegisterMap → option Byte ≝
219  λr: Register.
220  λm: RegisterMap.
221  match r with
222  [ Register00 ⇒ register_00_value m
223  | Register01 ⇒ register_01_value m
224  | Register02 ⇒ register_02_value m
225  | Register03 ⇒ register_03_value m
226  | Register04 ⇒ register_04_value m
227  | Register05 ⇒ register_05_value m
228  | Register06 ⇒ register_06_value m
229  | Register07 ⇒ register_07_value m
230  | Register10 ⇒ register_10_value m
231  | Register11 ⇒ register_11_value m
232  | Register12 ⇒ register_12_value m
233  | Register13 ⇒ register_13_value m
234  | Register14 ⇒ register_14_value m
235  | Register15 ⇒ register_15_value m
236  | Register16 ⇒ register_16_value m
237  | Register17 ⇒ register_17_value m
238  | Register20 ⇒ register_20_value m
239  | Register21 ⇒ register_21_value m
240  | Register22 ⇒ register_22_value m
241  | Register23 ⇒ register_23_value m
242  | Register24 ⇒ register_24_value m
243  | Register25 ⇒ register_25_value m
244  | Register26 ⇒ register_26_value m
245  | Register27 ⇒ register_27_value m
246  | Register30 ⇒ register_30_value m
247  | Register31 ⇒ register_31_value m
248  | Register32 ⇒ register_32_value m
249  | Register33 ⇒ register_33_value m
250  | Register34 ⇒ register_34_value m
251  | Register35 ⇒ register_35_value m
252  | Register36 ⇒ register_36_value m
253  | Register37 ⇒ register_37_value m
254  | RegisterA ⇒ register_A_value m
255  | RegisterB ⇒ register_B_value m
256  | RegisterDPL ⇒ register_DPL_value m
257  | RegisterDPH ⇒ register_DPH_value m
258  ].
259 
260definition update_register_00: Byte → RegisterMap → RegisterMap ≝
261  λb: Byte.
262  λm: RegisterMap.
263  let old_register_00_value ≝ register_00_value m in
264  let old_register_01_value ≝ register_01_value m in
265  let old_register_02_value ≝ register_02_value m in
266  let old_register_03_value ≝ register_03_value m in
267  let old_register_04_value ≝ register_04_value m in
268  let old_register_05_value ≝ register_05_value m in
269  let old_register_06_value ≝ register_06_value m in
270  let old_register_07_value ≝ register_07_value m in
271  let old_register_10_value ≝ register_01_value m in
272  let old_register_11_value ≝ register_01_value m in
273  let old_register_12_value ≝ register_02_value m in
274  let old_register_13_value ≝ register_03_value m in
275  let old_register_14_value ≝ register_04_value m in
276  let old_register_15_value ≝ register_05_value m in
277  let old_register_16_value ≝ register_06_value m in
278  let old_register_17_value ≝ register_07_value m in
279  let old_register_20_value ≝ register_01_value m in
280  let old_register_21_value ≝ register_02_value m in
281  let old_register_22_value ≝ register_02_value m in
282  let old_register_23_value ≝ register_03_value m in
283  let old_register_24_value ≝ register_04_value m in
284  let old_register_25_value ≝ register_05_value m in
285  let old_register_26_value ≝ register_06_value m in
286  let old_register_27_value ≝ register_07_value m in
287  let old_register_30_value ≝ register_01_value m in
288  let old_register_31_value ≝ register_02_value m in
289  let old_register_32_value ≝ register_02_value m in
290  let old_register_33_value ≝ register_03_value m in
291  let old_register_34_value ≝ register_04_value m in
292  let old_register_35_value ≝ register_05_value m in
293  let old_register_36_value ≝ register_06_value m in
294  let old_register_37_value ≝ register_07_value m in
295  let old_register_A_value ≝ register_A_value m in
296  let old_register_B_value ≝ register_B_value m in
297  let old_register_DPL_value ≝ register_DPL_value m in
298  let old_register_DPH_value ≝ register_DPH_value m in
299    mk_RegisterMap (Some ? b)
300                   old_register_01_value
301                   old_register_02_value
302                   old_register_03_value
303                   old_register_04_value
304                   old_register_05_value
305                   old_register_06_value
306                   old_register_07_value
307                   old_register_10_value
308                   old_register_11_value
309                   old_register_12_value
310                   old_register_13_value
311                   old_register_14_value
312                   old_register_15_value
313                   old_register_16_value
314                   old_register_17_value
315                   old_register_20_value
316                   old_register_21_value
317                   old_register_22_value
318                   old_register_23_value
319                   old_register_24_value
320                   old_register_25_value
321                   old_register_26_value
322                   old_register_27_value
323                   old_register_30_value
324                   old_register_31_value
325                   old_register_32_value
326                   old_register_33_value
327                   old_register_34_value
328                   old_register_35_value
329                   old_register_36_value
330                   old_register_37_value
331                   old_register_A_value
332                   old_register_B_value
333                   old_register_DPL_value
334                   old_register_DPH_value.
335
336definition update_register_01: Byte → RegisterMap → RegisterMap ≝
337  λb: Byte.
338  λm: RegisterMap.
339  let old_register_00_value ≝ register_00_value m in
340  let old_register_01_value ≝ register_01_value m in
341  let old_register_02_value ≝ register_02_value m in
342  let old_register_03_value ≝ register_03_value m in
343  let old_register_04_value ≝ register_04_value m in
344  let old_register_05_value ≝ register_05_value m in
345  let old_register_06_value ≝ register_06_value m in
346  let old_register_07_value ≝ register_07_value m in
347  let old_register_10_value ≝ register_01_value m in
348  let old_register_11_value ≝ register_01_value m in
349  let old_register_12_value ≝ register_02_value m in
350  let old_register_13_value ≝ register_03_value m in
351  let old_register_14_value ≝ register_04_value m in
352  let old_register_15_value ≝ register_05_value m in
353  let old_register_16_value ≝ register_06_value m in
354  let old_register_17_value ≝ register_07_value m in
355  let old_register_20_value ≝ register_01_value m in
356  let old_register_21_value ≝ register_02_value m in
357  let old_register_22_value ≝ register_02_value m in
358  let old_register_23_value ≝ register_03_value m in
359  let old_register_24_value ≝ register_04_value m in
360  let old_register_25_value ≝ register_05_value m in
361  let old_register_26_value ≝ register_06_value m in
362  let old_register_27_value ≝ register_07_value m in
363  let old_register_30_value ≝ register_01_value m in
364  let old_register_31_value ≝ register_02_value m in
365  let old_register_32_value ≝ register_02_value m in
366  let old_register_33_value ≝ register_03_value m in
367  let old_register_34_value ≝ register_04_value m in
368  let old_register_35_value ≝ register_05_value m in
369  let old_register_36_value ≝ register_06_value m in
370  let old_register_37_value ≝ register_07_value m in
371  let old_register_A_value ≝ register_A_value m in
372  let old_register_B_value ≝ register_B_value m in
373  let old_register_DPL_value ≝ register_DPL_value m in
374  let old_register_DPH_value ≝ register_DPH_value m in
375    mk_RegisterMap old_register_00_value
376                   (Some ? b)
377                   old_register_02_value
378                   old_register_03_value
379                   old_register_04_value
380                   old_register_05_value
381                   old_register_06_value
382                   old_register_07_value
383                   old_register_10_value
384                   old_register_11_value
385                   old_register_12_value
386                   old_register_13_value
387                   old_register_14_value
388                   old_register_15_value
389                   old_register_16_value
390                   old_register_17_value
391                   old_register_20_value
392                   old_register_21_value
393                   old_register_22_value
394                   old_register_23_value
395                   old_register_24_value
396                   old_register_25_value
397                   old_register_26_value
398                   old_register_27_value
399                   old_register_30_value
400                   old_register_31_value
401                   old_register_32_value
402                   old_register_33_value
403                   old_register_34_value
404                   old_register_35_value
405                   old_register_36_value
406                   old_register_37_value
407                   old_register_A_value
408                   old_register_B_value
409                   old_register_DPL_value
410                   old_register_DPH_value.
411
412definition update_register_02: Byte → RegisterMap → RegisterMap ≝
413  λb: Byte.
414  λm: RegisterMap.
415  let old_register_00_value ≝ register_00_value m in
416  let old_register_01_value ≝ register_01_value m in
417  let old_register_02_value ≝ register_02_value m in
418  let old_register_03_value ≝ register_03_value m in
419  let old_register_04_value ≝ register_04_value m in
420  let old_register_05_value ≝ register_05_value m in
421  let old_register_06_value ≝ register_06_value m in
422  let old_register_07_value ≝ register_07_value m in
423  let old_register_10_value ≝ register_01_value m in
424  let old_register_11_value ≝ register_01_value m in
425  let old_register_12_value ≝ register_02_value m in
426  let old_register_13_value ≝ register_03_value m in
427  let old_register_14_value ≝ register_04_value m in
428  let old_register_15_value ≝ register_05_value m in
429  let old_register_16_value ≝ register_06_value m in
430  let old_register_17_value ≝ register_07_value m in
431  let old_register_20_value ≝ register_01_value m in
432  let old_register_21_value ≝ register_02_value m in
433  let old_register_22_value ≝ register_02_value m in
434  let old_register_23_value ≝ register_03_value m in
435  let old_register_24_value ≝ register_04_value m in
436  let old_register_25_value ≝ register_05_value m in
437  let old_register_26_value ≝ register_06_value m in
438  let old_register_27_value ≝ register_07_value m in
439  let old_register_30_value ≝ register_01_value m in
440  let old_register_31_value ≝ register_02_value m in
441  let old_register_32_value ≝ register_02_value m in
442  let old_register_33_value ≝ register_03_value m in
443  let old_register_34_value ≝ register_04_value m in
444  let old_register_35_value ≝ register_05_value m in
445  let old_register_36_value ≝ register_06_value m in
446  let old_register_37_value ≝ register_07_value m in
447  let old_register_A_value ≝ register_A_value m in
448  let old_register_B_value ≝ register_B_value m in
449  let old_register_DPL_value ≝ register_DPL_value m in
450  let old_register_DPH_value ≝ register_DPH_value m in
451    mk_RegisterMap old_register_00_value
452                   old_register_01_value
453                   (Some ? b)
454                   old_register_03_value
455                   old_register_04_value
456                   old_register_05_value
457                   old_register_06_value
458                   old_register_07_value
459                   old_register_10_value
460                   old_register_11_value
461                   old_register_12_value
462                   old_register_13_value
463                   old_register_14_value
464                   old_register_15_value
465                   old_register_16_value
466                   old_register_17_value
467                   old_register_20_value
468                   old_register_21_value
469                   old_register_22_value
470                   old_register_23_value
471                   old_register_24_value
472                   old_register_25_value
473                   old_register_26_value
474                   old_register_27_value
475                   old_register_30_value
476                   old_register_31_value
477                   old_register_32_value
478                   old_register_33_value
479                   old_register_34_value
480                   old_register_35_value
481                   old_register_36_value
482                   old_register_37_value
483                   old_register_A_value
484                   old_register_B_value
485                   old_register_DPL_value
486                   old_register_DPH_value.
487
488definition update_register_03: Byte → RegisterMap → RegisterMap ≝
489  λb: Byte.
490  λm: RegisterMap.
491  let old_register_00_value ≝ register_00_value m in
492  let old_register_01_value ≝ register_01_value m in
493  let old_register_02_value ≝ register_02_value m in
494  let old_register_03_value ≝ register_03_value m in
495  let old_register_04_value ≝ register_04_value m in
496  let old_register_05_value ≝ register_05_value m in
497  let old_register_06_value ≝ register_06_value m in
498  let old_register_07_value ≝ register_07_value m in
499  let old_register_10_value ≝ register_01_value m in
500  let old_register_11_value ≝ register_01_value m in
501  let old_register_12_value ≝ register_02_value m in
502  let old_register_13_value ≝ register_03_value m in
503  let old_register_14_value ≝ register_04_value m in
504  let old_register_15_value ≝ register_05_value m in
505  let old_register_16_value ≝ register_06_value m in
506  let old_register_17_value ≝ register_07_value m in
507  let old_register_20_value ≝ register_01_value m in
508  let old_register_21_value ≝ register_02_value m in
509  let old_register_22_value ≝ register_02_value m in
510  let old_register_23_value ≝ register_03_value m in
511  let old_register_24_value ≝ register_04_value m in
512  let old_register_25_value ≝ register_05_value m in
513  let old_register_26_value ≝ register_06_value m in
514  let old_register_27_value ≝ register_07_value m in
515  let old_register_30_value ≝ register_01_value m in
516  let old_register_31_value ≝ register_02_value m in
517  let old_register_32_value ≝ register_02_value m in
518  let old_register_33_value ≝ register_03_value m in
519  let old_register_34_value ≝ register_04_value m in
520  let old_register_35_value ≝ register_05_value m in
521  let old_register_36_value ≝ register_06_value m in
522  let old_register_37_value ≝ register_07_value m in
523  let old_register_A_value ≝ register_A_value m in
524  let old_register_B_value ≝ register_B_value m in
525  let old_register_DPL_value ≝ register_DPL_value m in
526  let old_register_DPH_value ≝ register_DPH_value m in
527    mk_RegisterMap old_register_00_value
528                   old_register_01_value
529                   old_register_02_value
530                   (Some ? b)
531                   old_register_04_value
532                   old_register_05_value
533                   old_register_06_value
534                   old_register_07_value
535                   old_register_10_value
536                   old_register_11_value
537                   old_register_12_value
538                   old_register_13_value
539                   old_register_14_value
540                   old_register_15_value
541                   old_register_16_value
542                   old_register_17_value
543                   old_register_20_value
544                   old_register_21_value
545                   old_register_22_value
546                   old_register_23_value
547                   old_register_24_value
548                   old_register_25_value
549                   old_register_26_value
550                   old_register_27_value
551                   old_register_30_value
552                   old_register_31_value
553                   old_register_32_value
554                   old_register_33_value
555                   old_register_34_value
556                   old_register_35_value
557                   old_register_36_value
558                   old_register_37_value
559                   old_register_A_value
560                   old_register_B_value
561                   old_register_DPL_value
562                   old_register_DPH_value.
563
564definition update_register_04: Byte → RegisterMap → RegisterMap ≝
565  λb: Byte.
566  λm: RegisterMap.
567  let old_register_00_value ≝ register_00_value m in
568  let old_register_01_value ≝ register_01_value m in
569  let old_register_02_value ≝ register_02_value m in
570  let old_register_03_value ≝ register_03_value m in
571  let old_register_04_value ≝ register_04_value m in
572  let old_register_05_value ≝ register_05_value m in
573  let old_register_06_value ≝ register_06_value m in
574  let old_register_07_value ≝ register_07_value m in
575  let old_register_10_value ≝ register_01_value m in
576  let old_register_11_value ≝ register_01_value m in
577  let old_register_12_value ≝ register_02_value m in
578  let old_register_13_value ≝ register_03_value m in
579  let old_register_14_value ≝ register_04_value m in
580  let old_register_15_value ≝ register_05_value m in
581  let old_register_16_value ≝ register_06_value m in
582  let old_register_17_value ≝ register_07_value m in
583  let old_register_20_value ≝ register_01_value m in
584  let old_register_21_value ≝ register_02_value m in
585  let old_register_22_value ≝ register_02_value m in
586  let old_register_23_value ≝ register_03_value m in
587  let old_register_24_value ≝ register_04_value m in
588  let old_register_25_value ≝ register_05_value m in
589  let old_register_26_value ≝ register_06_value m in
590  let old_register_27_value ≝ register_07_value m in
591  let old_register_30_value ≝ register_01_value m in
592  let old_register_31_value ≝ register_02_value m in
593  let old_register_32_value ≝ register_02_value m in
594  let old_register_33_value ≝ register_03_value m in
595  let old_register_34_value ≝ register_04_value m in
596  let old_register_35_value ≝ register_05_value m in
597  let old_register_36_value ≝ register_06_value m in
598  let old_register_37_value ≝ register_07_value m in
599  let old_register_A_value ≝ register_A_value m in
600  let old_register_B_value ≝ register_B_value m in
601  let old_register_DPL_value ≝ register_DPL_value m in
602  let old_register_DPH_value ≝ register_DPH_value m in
603    mk_RegisterMap old_register_00_value
604                   old_register_01_value
605                   old_register_02_value
606                   old_register_03_value
607                   (Some ? b)
608                   old_register_05_value
609                   old_register_06_value
610                   old_register_07_value
611                   old_register_10_value
612                   old_register_11_value
613                   old_register_12_value
614                   old_register_13_value
615                   old_register_14_value
616                   old_register_15_value
617                   old_register_16_value
618                   old_register_17_value
619                   old_register_20_value
620                   old_register_21_value
621                   old_register_22_value
622                   old_register_23_value
623                   old_register_24_value
624                   old_register_25_value
625                   old_register_26_value
626                   old_register_27_value
627                   old_register_30_value
628                   old_register_31_value
629                   old_register_32_value
630                   old_register_33_value
631                   old_register_34_value
632                   old_register_35_value
633                   old_register_36_value
634                   old_register_37_value
635                   old_register_A_value
636                   old_register_B_value
637                   old_register_DPL_value
638                   old_register_DPH_value.
639
640definition update_register_05: Byte → RegisterMap → RegisterMap ≝
641  λb: Byte.
642  λm: RegisterMap.
643  let old_register_00_value ≝ register_00_value m in
644  let old_register_01_value ≝ register_01_value m in
645  let old_register_02_value ≝ register_02_value m in
646  let old_register_03_value ≝ register_03_value m in
647  let old_register_04_value ≝ register_04_value m in
648  let old_register_05_value ≝ register_05_value m in
649  let old_register_06_value ≝ register_06_value m in
650  let old_register_07_value ≝ register_07_value m in
651  let old_register_10_value ≝ register_01_value m in
652  let old_register_11_value ≝ register_01_value m in
653  let old_register_12_value ≝ register_02_value m in
654  let old_register_13_value ≝ register_03_value m in
655  let old_register_14_value ≝ register_04_value m in
656  let old_register_15_value ≝ register_05_value m in
657  let old_register_16_value ≝ register_06_value m in
658  let old_register_17_value ≝ register_07_value m in
659  let old_register_20_value ≝ register_01_value m in
660  let old_register_21_value ≝ register_02_value m in
661  let old_register_22_value ≝ register_02_value m in
662  let old_register_23_value ≝ register_03_value m in
663  let old_register_24_value ≝ register_04_value m in
664  let old_register_25_value ≝ register_05_value m in
665  let old_register_26_value ≝ register_06_value m in
666  let old_register_27_value ≝ register_07_value m in
667  let old_register_30_value ≝ register_01_value m in
668  let old_register_31_value ≝ register_02_value m in
669  let old_register_32_value ≝ register_02_value m in
670  let old_register_33_value ≝ register_03_value m in
671  let old_register_34_value ≝ register_04_value m in
672  let old_register_35_value ≝ register_05_value m in
673  let old_register_36_value ≝ register_06_value m in
674  let old_register_37_value ≝ register_07_value m in
675  let old_register_A_value ≝ register_A_value m in
676  let old_register_B_value ≝ register_B_value m in
677  let old_register_DPL_value ≝ register_DPL_value m in
678  let old_register_DPH_value ≝ register_DPH_value m in
679    mk_RegisterMap old_register_00_value
680                   old_register_01_value
681                   old_register_02_value
682                   old_register_03_value
683                   old_register_04_value
684                   (Some ? b)
685                   old_register_06_value
686                   old_register_07_value
687                   old_register_10_value
688                   old_register_11_value
689                   old_register_12_value
690                   old_register_13_value
691                   old_register_14_value
692                   old_register_15_value
693                   old_register_16_value
694                   old_register_17_value
695                   old_register_20_value
696                   old_register_21_value
697                   old_register_22_value
698                   old_register_23_value
699                   old_register_24_value
700                   old_register_25_value
701                   old_register_26_value
702                   old_register_27_value
703                   old_register_30_value
704                   old_register_31_value
705                   old_register_32_value
706                   old_register_33_value
707                   old_register_34_value
708                   old_register_35_value
709                   old_register_36_value
710                   old_register_37_value
711                   old_register_A_value
712                   old_register_B_value
713                   old_register_DPL_value
714                   old_register_DPH_value.
715
716definition update_register_06: Byte → RegisterMap → RegisterMap ≝
717  λb: Byte.
718  λm: RegisterMap.
719  let old_register_00_value ≝ register_00_value m in
720  let old_register_01_value ≝ register_01_value m in
721  let old_register_02_value ≝ register_02_value m in
722  let old_register_03_value ≝ register_03_value m in
723  let old_register_04_value ≝ register_04_value m in
724  let old_register_05_value ≝ register_05_value m in
725  let old_register_06_value ≝ register_06_value m in
726  let old_register_07_value ≝ register_07_value m in
727  let old_register_10_value ≝ register_01_value m in
728  let old_register_11_value ≝ register_01_value m in
729  let old_register_12_value ≝ register_02_value m in
730  let old_register_13_value ≝ register_03_value m in
731  let old_register_14_value ≝ register_04_value m in
732  let old_register_15_value ≝ register_05_value m in
733  let old_register_16_value ≝ register_06_value m in
734  let old_register_17_value ≝ register_07_value m in
735  let old_register_20_value ≝ register_01_value m in
736  let old_register_21_value ≝ register_02_value m in
737  let old_register_22_value ≝ register_02_value m in
738  let old_register_23_value ≝ register_03_value m in
739  let old_register_24_value ≝ register_04_value m in
740  let old_register_25_value ≝ register_05_value m in
741  let old_register_26_value ≝ register_06_value m in
742  let old_register_27_value ≝ register_07_value m in
743  let old_register_30_value ≝ register_01_value m in
744  let old_register_31_value ≝ register_02_value m in
745  let old_register_32_value ≝ register_02_value m in
746  let old_register_33_value ≝ register_03_value m in
747  let old_register_34_value ≝ register_04_value m in
748  let old_register_35_value ≝ register_05_value m in
749  let old_register_36_value ≝ register_06_value m in
750  let old_register_37_value ≝ register_07_value m in
751  let old_register_A_value ≝ register_A_value m in
752  let old_register_B_value ≝ register_B_value m in
753  let old_register_DPL_value ≝ register_DPL_value m in
754  let old_register_DPH_value ≝ register_DPH_value m in
755    mk_RegisterMap old_register_00_value
756                   old_register_01_value
757                   old_register_02_value
758                   old_register_03_value
759                   old_register_04_value
760                   old_register_05_value
761                   (Some ? b)
762                   old_register_07_value
763                   old_register_10_value
764                   old_register_11_value
765                   old_register_12_value
766                   old_register_13_value
767                   old_register_14_value
768                   old_register_15_value
769                   old_register_16_value
770                   old_register_17_value
771                   old_register_20_value
772                   old_register_21_value
773                   old_register_22_value
774                   old_register_23_value
775                   old_register_24_value
776                   old_register_25_value
777                   old_register_26_value
778                   old_register_27_value
779                   old_register_30_value
780                   old_register_31_value
781                   old_register_32_value
782                   old_register_33_value
783                   old_register_34_value
784                   old_register_35_value
785                   old_register_36_value
786                   old_register_37_value
787                   old_register_A_value
788                   old_register_B_value
789                   old_register_DPL_value
790                   old_register_DPH_value.
791
792definition update_register_07: Byte → RegisterMap → RegisterMap ≝
793  λb: Byte.
794  λm: RegisterMap.
795  let old_register_00_value ≝ register_00_value m in
796  let old_register_01_value ≝ register_01_value m in
797  let old_register_02_value ≝ register_02_value m in
798  let old_register_03_value ≝ register_03_value m in
799  let old_register_04_value ≝ register_04_value m in
800  let old_register_05_value ≝ register_05_value m in
801  let old_register_06_value ≝ register_06_value m in
802  let old_register_07_value ≝ register_07_value m in
803  let old_register_10_value ≝ register_01_value m in
804  let old_register_11_value ≝ register_01_value m in
805  let old_register_12_value ≝ register_02_value m in
806  let old_register_13_value ≝ register_03_value m in
807  let old_register_14_value ≝ register_04_value m in
808  let old_register_15_value ≝ register_05_value m in
809  let old_register_16_value ≝ register_06_value m in
810  let old_register_17_value ≝ register_07_value m in
811  let old_register_20_value ≝ register_01_value m in
812  let old_register_21_value ≝ register_02_value m in
813  let old_register_22_value ≝ register_02_value m in
814  let old_register_23_value ≝ register_03_value m in
815  let old_register_24_value ≝ register_04_value m in
816  let old_register_25_value ≝ register_05_value m in
817  let old_register_26_value ≝ register_06_value m in
818  let old_register_27_value ≝ register_07_value m in
819  let old_register_30_value ≝ register_01_value m in
820  let old_register_31_value ≝ register_02_value m in
821  let old_register_32_value ≝ register_02_value m in
822  let old_register_33_value ≝ register_03_value m in
823  let old_register_34_value ≝ register_04_value m in
824  let old_register_35_value ≝ register_05_value m in
825  let old_register_36_value ≝ register_06_value m in
826  let old_register_37_value ≝ register_07_value m in
827  let old_register_A_value ≝ register_A_value m in
828  let old_register_B_value ≝ register_B_value m in
829  let old_register_DPL_value ≝ register_DPL_value m in
830  let old_register_DPH_value ≝ register_DPH_value m in
831    mk_RegisterMap old_register_00_value
832                   old_register_01_value
833                   old_register_02_value
834                   old_register_03_value
835                   old_register_04_value
836                   old_register_05_value
837                   old_register_06_value
838                   (Some ? b)
839                   old_register_10_value
840                   old_register_11_value
841                   old_register_12_value
842                   old_register_13_value
843                   old_register_14_value
844                   old_register_15_value
845                   old_register_16_value
846                   old_register_17_value
847                   old_register_20_value
848                   old_register_21_value
849                   old_register_22_value
850                   old_register_23_value
851                   old_register_24_value
852                   old_register_25_value
853                   old_register_26_value
854                   old_register_27_value
855                   old_register_30_value
856                   old_register_31_value
857                   old_register_32_value
858                   old_register_33_value
859                   old_register_34_value
860                   old_register_35_value
861                   old_register_36_value
862                   old_register_37_value
863                   old_register_A_value
864                   old_register_B_value
865                   old_register_DPL_value
866                   old_register_DPH_value.
867
868definition update_register_10: Byte → RegisterMap → RegisterMap ≝
869  λb: Byte.
870  λm: RegisterMap.
871  let old_register_00_value ≝ register_00_value m in
872  let old_register_01_value ≝ register_01_value m in
873  let old_register_02_value ≝ register_02_value m in
874  let old_register_03_value ≝ register_03_value m in
875  let old_register_04_value ≝ register_04_value m in
876  let old_register_05_value ≝ register_05_value m in
877  let old_register_06_value ≝ register_06_value m in
878  let old_register_07_value ≝ register_07_value m in
879  let old_register_10_value ≝ register_01_value m in
880  let old_register_11_value ≝ register_01_value m in
881  let old_register_12_value ≝ register_02_value m in
882  let old_register_13_value ≝ register_03_value m in
883  let old_register_14_value ≝ register_04_value m in
884  let old_register_15_value ≝ register_05_value m in
885  let old_register_16_value ≝ register_06_value m in
886  let old_register_17_value ≝ register_07_value m in
887  let old_register_20_value ≝ register_01_value m in
888  let old_register_21_value ≝ register_02_value m in
889  let old_register_22_value ≝ register_02_value m in
890  let old_register_23_value ≝ register_03_value m in
891  let old_register_24_value ≝ register_04_value m in
892  let old_register_25_value ≝ register_05_value m in
893  let old_register_26_value ≝ register_06_value m in
894  let old_register_27_value ≝ register_07_value m in
895  let old_register_30_value ≝ register_01_value m in
896  let old_register_31_value ≝ register_02_value m in
897  let old_register_32_value ≝ register_02_value m in
898  let old_register_33_value ≝ register_03_value m in
899  let old_register_34_value ≝ register_04_value m in
900  let old_register_35_value ≝ register_05_value m in
901  let old_register_36_value ≝ register_06_value m in
902  let old_register_37_value ≝ register_07_value m in
903  let old_register_A_value ≝ register_A_value m in
904  let old_register_B_value ≝ register_B_value m in
905  let old_register_DPL_value ≝ register_DPL_value m in
906  let old_register_DPH_value ≝ register_DPH_value m in
907    mk_RegisterMap old_register_00_value
908                   old_register_01_value
909                   old_register_02_value
910                   old_register_03_value
911                   old_register_04_value
912                   old_register_05_value
913                   old_register_06_value
914                   old_register_07_value
915                   (Some ? b)
916                   old_register_11_value
917                   old_register_12_value
918                   old_register_13_value
919                   old_register_14_value
920                   old_register_15_value
921                   old_register_16_value
922                   old_register_17_value
923                   old_register_20_value
924                   old_register_21_value
925                   old_register_22_value
926                   old_register_23_value
927                   old_register_24_value
928                   old_register_25_value
929                   old_register_26_value
930                   old_register_27_value
931                   old_register_30_value
932                   old_register_31_value
933                   old_register_32_value
934                   old_register_33_value
935                   old_register_34_value
936                   old_register_35_value
937                   old_register_36_value
938                   old_register_37_value
939                   old_register_A_value
940                   old_register_B_value
941                   old_register_DPL_value
942                   old_register_DPH_value.
943
944definition update_register_11: Byte → RegisterMap → RegisterMap ≝
945  λb: Byte.
946  λm: RegisterMap.
947  let old_register_00_value ≝ register_00_value m in
948  let old_register_01_value ≝ register_01_value m in
949  let old_register_02_value ≝ register_02_value m in
950  let old_register_03_value ≝ register_03_value m in
951  let old_register_04_value ≝ register_04_value m in
952  let old_register_05_value ≝ register_05_value m in
953  let old_register_06_value ≝ register_06_value m in
954  let old_register_07_value ≝ register_07_value m in
955  let old_register_10_value ≝ register_01_value m in
956  let old_register_11_value ≝ register_01_value m in
957  let old_register_12_value ≝ register_02_value m in
958  let old_register_13_value ≝ register_03_value m in
959  let old_register_14_value ≝ register_04_value m in
960  let old_register_15_value ≝ register_05_value m in
961  let old_register_16_value ≝ register_06_value m in
962  let old_register_17_value ≝ register_07_value m in
963  let old_register_20_value ≝ register_01_value m in
964  let old_register_21_value ≝ register_02_value m in
965  let old_register_22_value ≝ register_02_value m in
966  let old_register_23_value ≝ register_03_value m in
967  let old_register_24_value ≝ register_04_value m in
968  let old_register_25_value ≝ register_05_value m in
969  let old_register_26_value ≝ register_06_value m in
970  let old_register_27_value ≝ register_07_value m in
971  let old_register_30_value ≝ register_01_value m in
972  let old_register_31_value ≝ register_02_value m in
973  let old_register_32_value ≝ register_02_value m in
974  let old_register_33_value ≝ register_03_value m in
975  let old_register_34_value ≝ register_04_value m in
976  let old_register_35_value ≝ register_05_value m in
977  let old_register_36_value ≝ register_06_value m in
978  let old_register_37_value ≝ register_07_value m in
979  let old_register_A_value ≝ register_A_value m in
980  let old_register_B_value ≝ register_B_value m in
981  let old_register_DPL_value ≝ register_DPL_value m in
982  let old_register_DPH_value ≝ register_DPH_value m in
983    mk_RegisterMap old_register_00_value
984                   old_register_01_value
985                   old_register_02_value
986                   old_register_03_value
987                   old_register_04_value
988                   old_register_05_value
989                   old_register_06_value
990                   old_register_07_value
991                   old_register_10_value
992                   (Some ? b)
993                   old_register_12_value
994                   old_register_13_value
995                   old_register_14_value
996                   old_register_15_value
997                   old_register_16_value
998                   old_register_17_value
999                   old_register_20_value
1000                   old_register_21_value
1001                   old_register_22_value
1002                   old_register_23_value
1003                   old_register_24_value
1004                   old_register_25_value
1005                   old_register_26_value
1006                   old_register_27_value
1007                   old_register_30_value
1008                   old_register_31_value
1009                   old_register_32_value
1010                   old_register_33_value
1011                   old_register_34_value
1012                   old_register_35_value
1013                   old_register_36_value
1014                   old_register_37_value
1015                   old_register_A_value
1016                   old_register_B_value
1017                   old_register_DPL_value
1018                   old_register_DPH_value.
1019
1020definition update_register_12: Byte → RegisterMap → RegisterMap ≝
1021  λb: Byte.
1022  λm: RegisterMap.
1023  let old_register_00_value ≝ register_00_value m in
1024  let old_register_01_value ≝ register_01_value m in
1025  let old_register_02_value ≝ register_02_value m in
1026  let old_register_03_value ≝ register_03_value m in
1027  let old_register_04_value ≝ register_04_value m in
1028  let old_register_05_value ≝ register_05_value m in
1029  let old_register_06_value ≝ register_06_value m in
1030  let old_register_07_value ≝ register_07_value m in
1031  let old_register_10_value ≝ register_01_value m in
1032  let old_register_11_value ≝ register_01_value m in
1033  let old_register_12_value ≝ register_02_value m in
1034  let old_register_13_value ≝ register_03_value m in
1035  let old_register_14_value ≝ register_04_value m in
1036  let old_register_15_value ≝ register_05_value m in
1037  let old_register_16_value ≝ register_06_value m in
1038  let old_register_17_value ≝ register_07_value m in
1039  let old_register_20_value ≝ register_01_value m in
1040  let old_register_21_value ≝ register_02_value m in
1041  let old_register_22_value ≝ register_02_value m in
1042  let old_register_23_value ≝ register_03_value m in
1043  let old_register_24_value ≝ register_04_value m in
1044  let old_register_25_value ≝ register_05_value m in
1045  let old_register_26_value ≝ register_06_value m in
1046  let old_register_27_value ≝ register_07_value m in
1047  let old_register_30_value ≝ register_01_value m in
1048  let old_register_31_value ≝ register_02_value m in
1049  let old_register_32_value ≝ register_02_value m in
1050  let old_register_33_value ≝ register_03_value m in
1051  let old_register_34_value ≝ register_04_value m in
1052  let old_register_35_value ≝ register_05_value m in
1053  let old_register_36_value ≝ register_06_value m in
1054  let old_register_37_value ≝ register_07_value m in
1055  let old_register_A_value ≝ register_A_value m in
1056  let old_register_B_value ≝ register_B_value m in
1057  let old_register_DPL_value ≝ register_DPL_value m in
1058  let old_register_DPH_value ≝ register_DPH_value m in
1059    mk_RegisterMap old_register_00_value
1060                   old_register_01_value
1061                   old_register_02_value
1062                   old_register_03_value
1063                   old_register_04_value
1064                   old_register_05_value
1065                   old_register_06_value
1066                   old_register_07_value
1067                   old_register_10_value
1068                   old_register_11_value
1069                   (Some ? b)
1070                   old_register_13_value
1071                   old_register_14_value
1072                   old_register_15_value
1073                   old_register_16_value
1074                   old_register_17_value
1075                   old_register_20_value
1076                   old_register_21_value
1077                   old_register_22_value
1078                   old_register_23_value
1079                   old_register_24_value
1080                   old_register_25_value
1081                   old_register_26_value
1082                   old_register_27_value
1083                   old_register_30_value
1084                   old_register_31_value
1085                   old_register_32_value
1086                   old_register_33_value
1087                   old_register_34_value
1088                   old_register_35_value
1089                   old_register_36_value
1090                   old_register_37_value
1091                   old_register_A_value
1092                   old_register_B_value
1093                   old_register_DPL_value
1094                   old_register_DPH_value.
1095
1096definition update_register_13: Byte → RegisterMap → RegisterMap ≝
1097  λb: Byte.
1098  λm: RegisterMap.
1099  let old_register_00_value ≝ register_00_value m in
1100  let old_register_01_value ≝ register_01_value m in
1101  let old_register_02_value ≝ register_02_value m in
1102  let old_register_03_value ≝ register_03_value m in
1103  let old_register_04_value ≝ register_04_value m in
1104  let old_register_05_value ≝ register_05_value m in
1105  let old_register_06_value ≝ register_06_value m in
1106  let old_register_07_value ≝ register_07_value m in
1107  let old_register_10_value ≝ register_01_value m in
1108  let old_register_11_value ≝ register_01_value m in
1109  let old_register_12_value ≝ register_02_value m in
1110  let old_register_13_value ≝ register_03_value m in
1111  let old_register_14_value ≝ register_04_value m in
1112  let old_register_15_value ≝ register_05_value m in
1113  let old_register_16_value ≝ register_06_value m in
1114  let old_register_17_value ≝ register_07_value m in
1115  let old_register_20_value ≝ register_01_value m in
1116  let old_register_21_value ≝ register_02_value m in
1117  let old_register_22_value ≝ register_02_value m in
1118  let old_register_23_value ≝ register_03_value m in
1119  let old_register_24_value ≝ register_04_value m in
1120  let old_register_25_value ≝ register_05_value m in
1121  let old_register_26_value ≝ register_06_value m in
1122  let old_register_27_value ≝ register_07_value m in
1123  let old_register_30_value ≝ register_01_value m in
1124  let old_register_31_value ≝ register_02_value m in
1125  let old_register_32_value ≝ register_02_value m in
1126  let old_register_33_value ≝ register_03_value m in
1127  let old_register_34_value ≝ register_04_value m in
1128  let old_register_35_value ≝ register_05_value m in
1129  let old_register_36_value ≝ register_06_value m in
1130  let old_register_37_value ≝ register_07_value m in
1131  let old_register_A_value ≝ register_A_value m in
1132  let old_register_B_value ≝ register_B_value m in
1133  let old_register_DPL_value ≝ register_DPL_value m in
1134  let old_register_DPH_value ≝ register_DPH_value m in
1135    mk_RegisterMap old_register_00_value
1136                   old_register_01_value
1137                   old_register_02_value
1138                   old_register_03_value
1139                   old_register_04_value
1140                   old_register_05_value
1141                   old_register_06_value
1142                   old_register_07_value
1143                   old_register_10_value
1144                   old_register_11_value
1145                   old_register_12_value
1146                   (Some ? b)
1147                   old_register_14_value
1148                   old_register_15_value
1149                   old_register_16_value
1150                   old_register_17_value
1151                   old_register_20_value
1152                   old_register_21_value
1153                   old_register_22_value
1154                   old_register_23_value
1155                   old_register_24_value
1156                   old_register_25_value
1157                   old_register_26_value
1158                   old_register_27_value
1159                   old_register_30_value
1160                   old_register_31_value
1161                   old_register_32_value
1162                   old_register_33_value
1163                   old_register_34_value
1164                   old_register_35_value
1165                   old_register_36_value
1166                   old_register_37_value
1167                   old_register_A_value
1168                   old_register_B_value
1169                   old_register_DPL_value
1170                   old_register_DPH_value.
1171
1172definition update_register_14: Byte → RegisterMap → RegisterMap ≝
1173  λb: Byte.
1174  λm: RegisterMap.
1175  let old_register_00_value ≝ register_00_value m in
1176  let old_register_01_value ≝ register_01_value m in
1177  let old_register_02_value ≝ register_02_value m in
1178  let old_register_03_value ≝ register_03_value m in
1179  let old_register_04_value ≝ register_04_value m in
1180  let old_register_05_value ≝ register_05_value m in
1181  let old_register_06_value ≝ register_06_value m in
1182  let old_register_07_value ≝ register_07_value m in
1183  let old_register_10_value ≝ register_01_value m in
1184  let old_register_11_value ≝ register_01_value m in
1185  let old_register_12_value ≝ register_02_value m in
1186  let old_register_13_value ≝ register_03_value m in
1187  let old_register_14_value ≝ register_04_value m in
1188  let old_register_15_value ≝ register_05_value m in
1189  let old_register_16_value ≝ register_06_value m in
1190  let old_register_17_value ≝ register_07_value m in
1191  let old_register_20_value ≝ register_01_value m in
1192  let old_register_21_value ≝ register_02_value m in
1193  let old_register_22_value ≝ register_02_value m in
1194  let old_register_23_value ≝ register_03_value m in
1195  let old_register_24_value ≝ register_04_value m in
1196  let old_register_25_value ≝ register_05_value m in
1197  let old_register_26_value ≝ register_06_value m in
1198  let old_register_27_value ≝ register_07_value m in
1199  let old_register_30_value ≝ register_01_value m in
1200  let old_register_31_value ≝ register_02_value m in
1201  let old_register_32_value ≝ register_02_value m in
1202  let old_register_33_value ≝ register_03_value m in
1203  let old_register_34_value ≝ register_04_value m in
1204  let old_register_35_value ≝ register_05_value m in
1205  let old_register_36_value ≝ register_06_value m in
1206  let old_register_37_value ≝ register_07_value m in
1207  let old_register_A_value ≝ register_A_value m in
1208  let old_register_B_value ≝ register_B_value m in
1209  let old_register_DPL_value ≝ register_DPL_value m in
1210  let old_register_DPH_value ≝ register_DPH_value m in
1211    mk_RegisterMap old_register_00_value
1212                   old_register_01_value
1213                   old_register_02_value
1214                   old_register_03_value
1215                   old_register_04_value
1216                   old_register_05_value
1217                   old_register_06_value
1218                   old_register_07_value
1219                   old_register_10_value
1220                   old_register_11_value
1221                   old_register_12_value
1222                   old_register_13_value
1223                   (Some ? b)
1224                   old_register_15_value
1225                   old_register_16_value
1226                   old_register_17_value
1227                   old_register_20_value
1228                   old_register_21_value
1229                   old_register_22_value
1230                   old_register_23_value
1231                   old_register_24_value
1232                   old_register_25_value
1233                   old_register_26_value
1234                   old_register_27_value
1235                   old_register_30_value
1236                   old_register_31_value
1237                   old_register_32_value
1238                   old_register_33_value
1239                   old_register_34_value
1240                   old_register_35_value
1241                   old_register_36_value
1242                   old_register_37_value
1243                   old_register_A_value
1244                   old_register_B_value
1245                   old_register_DPL_value
1246                   old_register_DPH_value.
1247
1248definition update_register_15: Byte → RegisterMap → RegisterMap ≝
1249  λb: Byte.
1250  λm: RegisterMap.
1251  let old_register_00_value ≝ register_00_value m in
1252  let old_register_01_value ≝ register_01_value m in
1253  let old_register_02_value ≝ register_02_value m in
1254  let old_register_03_value ≝ register_03_value m in
1255  let old_register_04_value ≝ register_04_value m in
1256  let old_register_05_value ≝ register_05_value m in
1257  let old_register_06_value ≝ register_06_value m in
1258  let old_register_07_value ≝ register_07_value m in
1259  let old_register_10_value ≝ register_01_value m in
1260  let old_register_11_value ≝ register_01_value m in
1261  let old_register_12_value ≝ register_02_value m in
1262  let old_register_13_value ≝ register_03_value m in
1263  let old_register_14_value ≝ register_04_value m in
1264  let old_register_15_value ≝ register_05_value m in
1265  let old_register_16_value ≝ register_06_value m in
1266  let old_register_17_value ≝ register_07_value m in
1267  let old_register_20_value ≝ register_01_value m in
1268  let old_register_21_value ≝ register_02_value m in
1269  let old_register_22_value ≝ register_02_value m in
1270  let old_register_23_value ≝ register_03_value m in
1271  let old_register_24_value ≝ register_04_value m in
1272  let old_register_25_value ≝ register_05_value m in
1273  let old_register_26_value ≝ register_06_value m in
1274  let old_register_27_value ≝ register_07_value m in
1275  let old_register_30_value ≝ register_01_value m in
1276  let old_register_31_value ≝ register_02_value m in
1277  let old_register_32_value ≝ register_02_value m in
1278  let old_register_33_value ≝ register_03_value m in
1279  let old_register_34_value ≝ register_04_value m in
1280  let old_register_35_value ≝ register_05_value m in
1281  let old_register_36_value ≝ register_06_value m in
1282  let old_register_37_value ≝ register_07_value m in
1283  let old_register_A_value ≝ register_A_value m in
1284  let old_register_B_value ≝ register_B_value m in
1285  let old_register_DPL_value ≝ register_DPL_value m in
1286  let old_register_DPH_value ≝ register_DPH_value m in
1287    mk_RegisterMap old_register_00_value
1288                   old_register_01_value
1289                   old_register_02_value
1290                   old_register_03_value
1291                   old_register_04_value
1292                   old_register_05_value
1293                   old_register_06_value
1294                   old_register_07_value
1295                   old_register_10_value
1296                   old_register_11_value
1297                   old_register_12_value
1298                   old_register_13_value
1299                   old_register_14_value
1300                   (Some ? b)
1301                   old_register_16_value
1302                   old_register_17_value
1303                   old_register_20_value
1304                   old_register_21_value
1305                   old_register_22_value
1306                   old_register_23_value
1307                   old_register_24_value
1308                   old_register_25_value
1309                   old_register_26_value
1310                   old_register_27_value
1311                   old_register_30_value
1312                   old_register_31_value
1313                   old_register_32_value
1314                   old_register_33_value
1315                   old_register_34_value
1316                   old_register_35_value
1317                   old_register_36_value
1318                   old_register_37_value
1319                   old_register_A_value
1320                   old_register_B_value
1321                   old_register_DPL_value
1322                   old_register_DPH_value.
1323
1324definition update_register_16: Byte → RegisterMap → RegisterMap ≝
1325  λb: Byte.
1326  λm: RegisterMap.
1327  let old_register_00_value ≝ register_00_value m in
1328  let old_register_01_value ≝ register_01_value m in
1329  let old_register_02_value ≝ register_02_value m in
1330  let old_register_03_value ≝ register_03_value m in
1331  let old_register_04_value ≝ register_04_value m in
1332  let old_register_05_value ≝ register_05_value m in
1333  let old_register_06_value ≝ register_06_value m in
1334  let old_register_07_value ≝ register_07_value m in
1335  let old_register_10_value ≝ register_01_value m in
1336  let old_register_11_value ≝ register_01_value m in
1337  let old_register_12_value ≝ register_02_value m in
1338  let old_register_13_value ≝ register_03_value m in
1339  let old_register_14_value ≝ register_04_value m in
1340  let old_register_15_value ≝ register_05_value m in
1341  let old_register_16_value ≝ register_06_value m in
1342  let old_register_17_value ≝ register_07_value m in
1343  let old_register_20_value ≝ register_01_value m in
1344  let old_register_21_value ≝ register_02_value m in
1345  let old_register_22_value ≝ register_02_value m in
1346  let old_register_23_value ≝ register_03_value m in
1347  let old_register_24_value ≝ register_04_value m in
1348  let old_register_25_value ≝ register_05_value m in
1349  let old_register_26_value ≝ register_06_value m in
1350  let old_register_27_value ≝ register_07_value m in
1351  let old_register_30_value ≝ register_01_value m in
1352  let old_register_31_value ≝ register_02_value m in
1353  let old_register_32_value ≝ register_02_value m in
1354  let old_register_33_value ≝ register_03_value m in
1355  let old_register_34_value ≝ register_04_value m in
1356  let old_register_35_value ≝ register_05_value m in
1357  let old_register_36_value ≝ register_06_value m in
1358  let old_register_37_value ≝ register_07_value m in
1359  let old_register_A_value ≝ register_A_value m in
1360  let old_register_B_value ≝ register_B_value m in
1361  let old_register_DPL_value ≝ register_DPL_value m in
1362  let old_register_DPH_value ≝ register_DPH_value m in
1363    mk_RegisterMap old_register_00_value
1364                   old_register_01_value
1365                   old_register_02_value
1366                   old_register_03_value
1367                   old_register_04_value
1368                   old_register_05_value
1369                   old_register_06_value
1370                   old_register_07_value
1371                   old_register_10_value
1372                   old_register_11_value
1373                   old_register_12_value
1374                   old_register_13_value
1375                   old_register_14_value
1376                   old_register_15_value
1377                   (Some ? b)
1378                   old_register_17_value
1379                   old_register_20_value
1380                   old_register_21_value
1381                   old_register_22_value
1382                   old_register_23_value
1383                   old_register_24_value
1384                   old_register_25_value
1385                   old_register_26_value
1386                   old_register_27_value
1387                   old_register_30_value
1388                   old_register_31_value
1389                   old_register_32_value
1390                   old_register_33_value
1391                   old_register_34_value
1392                   old_register_35_value
1393                   old_register_36_value
1394                   old_register_37_value
1395                   old_register_A_value
1396                   old_register_B_value
1397                   old_register_DPL_value
1398                   old_register_DPH_value.
1399
1400definition update_register_17: Byte → RegisterMap → RegisterMap ≝
1401  λb: Byte.
1402  λm: RegisterMap.
1403  let old_register_00_value ≝ register_00_value m in
1404  let old_register_01_value ≝ register_01_value m in
1405  let old_register_02_value ≝ register_02_value m in
1406  let old_register_03_value ≝ register_03_value m in
1407  let old_register_04_value ≝ register_04_value m in
1408  let old_register_05_value ≝ register_05_value m in
1409  let old_register_06_value ≝ register_06_value m in
1410  let old_register_07_value ≝ register_07_value m in
1411  let old_register_10_value ≝ register_01_value m in
1412  let old_register_11_value ≝ register_01_value m in
1413  let old_register_12_value ≝ register_02_value m in
1414  let old_register_13_value ≝ register_03_value m in
1415  let old_register_14_value ≝ register_04_value m in
1416  let old_register_15_value ≝ register_05_value m in
1417  let old_register_16_value ≝ register_06_value m in
1418  let old_register_17_value ≝ register_07_value m in
1419  let old_register_20_value ≝ register_01_value m in
1420  let old_register_21_value ≝ register_02_value m in
1421  let old_register_22_value ≝ register_02_value m in
1422  let old_register_23_value ≝ register_03_value m in
1423  let old_register_24_value ≝ register_04_value m in
1424  let old_register_25_value ≝ register_05_value m in
1425  let old_register_26_value ≝ register_06_value m in
1426  let old_register_27_value ≝ register_07_value m in
1427  let old_register_30_value ≝ register_01_value m in
1428  let old_register_31_value ≝ register_02_value m in
1429  let old_register_32_value ≝ register_02_value m in
1430  let old_register_33_value ≝ register_03_value m in
1431  let old_register_34_value ≝ register_04_value m in
1432  let old_register_35_value ≝ register_05_value m in
1433  let old_register_36_value ≝ register_06_value m in
1434  let old_register_37_value ≝ register_07_value m in
1435  let old_register_A_value ≝ register_A_value m in
1436  let old_register_B_value ≝ register_B_value m in
1437  let old_register_DPL_value ≝ register_DPL_value m in
1438  let old_register_DPH_value ≝ register_DPH_value m in
1439    mk_RegisterMap old_register_00_value
1440                   old_register_01_value
1441                   old_register_02_value
1442                   old_register_03_value
1443                   old_register_04_value
1444                   old_register_05_value
1445                   old_register_06_value
1446                   old_register_07_value
1447                   old_register_10_value
1448                   old_register_11_value
1449                   old_register_12_value
1450                   old_register_13_value
1451                   old_register_14_value
1452                   old_register_15_value
1453                   old_register_16_value
1454                   (Some ? b)
1455                   old_register_20_value
1456                   old_register_21_value
1457                   old_register_22_value
1458                   old_register_23_value
1459                   old_register_24_value
1460                   old_register_25_value
1461                   old_register_26_value
1462                   old_register_27_value
1463                   old_register_30_value
1464                   old_register_31_value
1465                   old_register_32_value
1466                   old_register_33_value
1467                   old_register_34_value
1468                   old_register_35_value
1469                   old_register_36_value
1470                   old_register_37_value
1471                   old_register_A_value
1472                   old_register_B_value
1473                   old_register_DPL_value
1474                   old_register_DPH_value.
1475
1476definition update_register_20: Byte → RegisterMap → RegisterMap ≝
1477  λb: Byte.
1478  λm: RegisterMap.
1479  let old_register_00_value ≝ register_00_value m in
1480  let old_register_01_value ≝ register_01_value m in
1481  let old_register_02_value ≝ register_02_value m in
1482  let old_register_03_value ≝ register_03_value m in
1483  let old_register_04_value ≝ register_04_value m in
1484  let old_register_05_value ≝ register_05_value m in
1485  let old_register_06_value ≝ register_06_value m in
1486  let old_register_07_value ≝ register_07_value m in
1487  let old_register_10_value ≝ register_01_value m in
1488  let old_register_11_value ≝ register_01_value m in
1489  let old_register_12_value ≝ register_02_value m in
1490  let old_register_13_value ≝ register_03_value m in
1491  let old_register_14_value ≝ register_04_value m in
1492  let old_register_15_value ≝ register_05_value m in
1493  let old_register_16_value ≝ register_06_value m in
1494  let old_register_17_value ≝ register_07_value m in
1495  let old_register_20_value ≝ register_01_value m in
1496  let old_register_21_value ≝ register_02_value m in
1497  let old_register_22_value ≝ register_02_value m in
1498  let old_register_23_value ≝ register_03_value m in
1499  let old_register_24_value ≝ register_04_value m in
1500  let old_register_25_value ≝ register_05_value m in
1501  let old_register_26_value ≝ register_06_value m in
1502  let old_register_27_value ≝ register_07_value m in
1503  let old_register_30_value ≝ register_01_value m in
1504  let old_register_31_value ≝ register_02_value m in
1505  let old_register_32_value ≝ register_02_value m in
1506  let old_register_33_value ≝ register_03_value m in
1507  let old_register_34_value ≝ register_04_value m in
1508  let old_register_35_value ≝ register_05_value m in
1509  let old_register_36_value ≝ register_06_value m in
1510  let old_register_37_value ≝ register_07_value m in
1511  let old_register_A_value ≝ register_A_value m in
1512  let old_register_B_value ≝ register_B_value m in
1513  let old_register_DPL_value ≝ register_DPL_value m in
1514  let old_register_DPH_value ≝ register_DPH_value m in
1515    mk_RegisterMap old_register_00_value
1516                   old_register_01_value
1517                   old_register_02_value
1518                   old_register_03_value
1519                   old_register_04_value
1520                   old_register_05_value
1521                   old_register_06_value
1522                   old_register_07_value
1523                   old_register_10_value
1524                   old_register_11_value
1525                   old_register_12_value
1526                   old_register_13_value
1527                   old_register_14_value
1528                   old_register_15_value
1529                   old_register_16_value
1530                   old_register_17_value
1531                   (Some ? b)
1532                   old_register_21_value
1533                   old_register_22_value
1534                   old_register_23_value
1535                   old_register_24_value
1536                   old_register_25_value
1537                   old_register_26_value
1538                   old_register_27_value
1539                   old_register_30_value
1540                   old_register_31_value
1541                   old_register_32_value
1542                   old_register_33_value
1543                   old_register_34_value
1544                   old_register_35_value
1545                   old_register_36_value
1546                   old_register_37_value
1547                   old_register_A_value
1548                   old_register_B_value
1549                   old_register_DPL_value
1550                   old_register_DPH_value.
1551
1552definition update_register_21: Byte → RegisterMap → RegisterMap ≝
1553  λb: Byte.
1554  λm: RegisterMap.
1555  let old_register_00_value ≝ register_00_value m in
1556  let old_register_01_value ≝ register_01_value m in
1557  let old_register_02_value ≝ register_02_value m in
1558  let old_register_03_value ≝ register_03_value m in
1559  let old_register_04_value ≝ register_04_value m in
1560  let old_register_05_value ≝ register_05_value m in
1561  let old_register_06_value ≝ register_06_value m in
1562  let old_register_07_value ≝ register_07_value m in
1563  let old_register_10_value ≝ register_01_value m in
1564  let old_register_11_value ≝ register_01_value m in
1565  let old_register_12_value ≝ register_02_value m in
1566  let old_register_13_value ≝ register_03_value m in
1567  let old_register_14_value ≝ register_04_value m in
1568  let old_register_15_value ≝ register_05_value m in
1569  let old_register_16_value ≝ register_06_value m in
1570  let old_register_17_value ≝ register_07_value m in
1571  let old_register_20_value ≝ register_01_value m in
1572  let old_register_21_value ≝ register_02_value m in
1573  let old_register_22_value ≝ register_02_value m in
1574  let old_register_23_value ≝ register_03_value m in
1575  let old_register_24_value ≝ register_04_value m in
1576  let old_register_25_value ≝ register_05_value m in
1577  let old_register_26_value ≝ register_06_value m in
1578  let old_register_27_value ≝ register_07_value m in
1579  let old_register_30_value ≝ register_01_value m in
1580  let old_register_31_value ≝ register_02_value m in
1581  let old_register_32_value ≝ register_02_value m in
1582  let old_register_33_value ≝ register_03_value m in
1583  let old_register_34_value ≝ register_04_value m in
1584  let old_register_35_value ≝ register_05_value m in
1585  let old_register_36_value ≝ register_06_value m in
1586  let old_register_37_value ≝ register_07_value m in
1587  let old_register_A_value ≝ register_A_value m in
1588  let old_register_B_value ≝ register_B_value m in
1589  let old_register_DPL_value ≝ register_DPL_value m in
1590  let old_register_DPH_value ≝ register_DPH_value m in
1591    mk_RegisterMap old_register_00_value
1592                   old_register_01_value
1593                   old_register_02_value
1594                   old_register_03_value
1595                   old_register_04_value
1596                   old_register_05_value
1597                   old_register_06_value
1598                   old_register_07_value
1599                   old_register_10_value
1600                   old_register_11_value
1601                   old_register_12_value
1602                   old_register_13_value
1603                   old_register_14_value
1604                   old_register_15_value
1605                   old_register_16_value
1606                   old_register_17_value
1607                   old_register_20_value
1608                   (Some ? b)
1609                   old_register_22_value
1610                   old_register_23_value
1611                   old_register_24_value
1612                   old_register_25_value
1613                   old_register_26_value
1614                   old_register_27_value
1615                   old_register_30_value
1616                   old_register_31_value
1617                   old_register_32_value
1618                   old_register_33_value
1619                   old_register_34_value
1620                   old_register_35_value
1621                   old_register_36_value
1622                   old_register_37_value
1623                   old_register_A_value
1624                   old_register_B_value
1625                   old_register_DPL_value
1626                   old_register_DPH_value.
1627
1628definition update_register_22: Byte → RegisterMap → RegisterMap ≝
1629  λb: Byte.
1630  λm: RegisterMap.
1631  let old_register_00_value ≝ register_00_value m in
1632  let old_register_01_value ≝ register_01_value m in
1633  let old_register_02_value ≝ register_02_value m in
1634  let old_register_03_value ≝ register_03_value m in
1635  let old_register_04_value ≝ register_04_value m in
1636  let old_register_05_value ≝ register_05_value m in
1637  let old_register_06_value ≝ register_06_value m in
1638  let old_register_07_value ≝ register_07_value m in
1639  let old_register_10_value ≝ register_01_value m in
1640  let old_register_11_value ≝ register_01_value m in
1641  let old_register_12_value ≝ register_02_value m in
1642  let old_register_13_value ≝ register_03_value m in
1643  let old_register_14_value ≝ register_04_value m in
1644  let old_register_15_value ≝ register_05_value m in
1645  let old_register_16_value ≝ register_06_value m in
1646  let old_register_17_value ≝ register_07_value m in
1647  let old_register_20_value ≝ register_01_value m in
1648  let old_register_21_value ≝ register_02_value m in
1649  let old_register_22_value ≝ register_02_value m in
1650  let old_register_23_value ≝ register_03_value m in
1651  let old_register_24_value ≝ register_04_value m in
1652  let old_register_25_value ≝ register_05_value m in
1653  let old_register_26_value ≝ register_06_value m in
1654  let old_register_27_value ≝ register_07_value m in
1655  let old_register_30_value ≝ register_01_value m in
1656  let old_register_31_value ≝ register_02_value m in
1657  let old_register_32_value ≝ register_02_value m in
1658  let old_register_33_value ≝ register_03_value m in
1659  let old_register_34_value ≝ register_04_value m in
1660  let old_register_35_value ≝ register_05_value m in
1661  let old_register_36_value ≝ register_06_value m in
1662  let old_register_37_value ≝ register_07_value m in
1663  let old_register_A_value ≝ register_A_value m in
1664  let old_register_B_value ≝ register_B_value m in
1665  let old_register_DPL_value ≝ register_DPL_value m in
1666  let old_register_DPH_value ≝ register_DPH_value m in
1667    mk_RegisterMap old_register_00_value
1668                   old_register_01_value
1669                   old_register_02_value
1670                   old_register_03_value
1671                   old_register_04_value
1672                   old_register_05_value
1673                   old_register_06_value
1674                   old_register_07_value
1675                   old_register_10_value
1676                   old_register_11_value
1677                   old_register_12_value
1678                   old_register_13_value
1679                   old_register_14_value
1680                   old_register_15_value
1681                   old_register_16_value
1682                   old_register_17_value
1683                   old_register_20_value
1684                   old_register_21_value
1685                   (Some ? b)
1686                   old_register_23_value
1687                   old_register_24_value
1688                   old_register_25_value
1689                   old_register_26_value
1690                   old_register_27_value
1691                   old_register_30_value
1692                   old_register_31_value
1693                   old_register_32_value
1694                   old_register_33_value
1695                   old_register_34_value
1696                   old_register_35_value
1697                   old_register_36_value
1698                   old_register_37_value
1699                   old_register_A_value
1700                   old_register_B_value
1701                   old_register_DPL_value
1702                   old_register_DPH_value.
1703                   
1704definition update_register_23: Byte → RegisterMap → RegisterMap ≝
1705  λb: Byte.
1706  λm: RegisterMap.
1707  let old_register_00_value ≝ register_00_value m in
1708  let old_register_01_value ≝ register_01_value m in
1709  let old_register_02_value ≝ register_02_value m in
1710  let old_register_03_value ≝ register_03_value m in
1711  let old_register_04_value ≝ register_04_value m in
1712  let old_register_05_value ≝ register_05_value m in
1713  let old_register_06_value ≝ register_06_value m in
1714  let old_register_07_value ≝ register_07_value m in
1715  let old_register_10_value ≝ register_01_value m in
1716  let old_register_11_value ≝ register_01_value m in
1717  let old_register_12_value ≝ register_02_value m in
1718  let old_register_13_value ≝ register_03_value m in
1719  let old_register_14_value ≝ register_04_value m in
1720  let old_register_15_value ≝ register_05_value m in
1721  let old_register_16_value ≝ register_06_value m in
1722  let old_register_17_value ≝ register_07_value m in
1723  let old_register_20_value ≝ register_01_value m in
1724  let old_register_21_value ≝ register_02_value m in
1725  let old_register_22_value ≝ register_02_value m in
1726  let old_register_23_value ≝ register_03_value m in
1727  let old_register_24_value ≝ register_04_value m in
1728  let old_register_25_value ≝ register_05_value m in
1729  let old_register_26_value ≝ register_06_value m in
1730  let old_register_27_value ≝ register_07_value m in
1731  let old_register_30_value ≝ register_01_value m in
1732  let old_register_31_value ≝ register_02_value m in
1733  let old_register_32_value ≝ register_02_value m in
1734  let old_register_33_value ≝ register_03_value m in
1735  let old_register_34_value ≝ register_04_value m in
1736  let old_register_35_value ≝ register_05_value m in
1737  let old_register_36_value ≝ register_06_value m in
1738  let old_register_37_value ≝ register_07_value m in
1739  let old_register_A_value ≝ register_A_value m in
1740  let old_register_B_value ≝ register_B_value m in
1741  let old_register_DPL_value ≝ register_DPL_value m in
1742  let old_register_DPH_value ≝ register_DPH_value m in
1743    mk_RegisterMap old_register_00_value
1744                   old_register_01_value
1745                   old_register_02_value
1746                   old_register_03_value
1747                   old_register_04_value
1748                   old_register_05_value
1749                   old_register_06_value
1750                   old_register_07_value
1751                   old_register_10_value
1752                   old_register_11_value
1753                   old_register_12_value
1754                   old_register_13_value
1755                   old_register_14_value
1756                   old_register_15_value
1757                   old_register_16_value
1758                   old_register_17_value
1759                   old_register_20_value
1760                   old_register_21_value
1761                   old_register_22_value
1762                   (Some ? b)
1763                   old_register_24_value
1764                   old_register_25_value
1765                   old_register_26_value
1766                   old_register_27_value
1767                   old_register_30_value
1768                   old_register_31_value
1769                   old_register_32_value
1770                   old_register_33_value
1771                   old_register_34_value
1772                   old_register_35_value
1773                   old_register_36_value
1774                   old_register_37_value
1775                   old_register_A_value
1776                   old_register_B_value
1777                   old_register_DPL_value
1778                   old_register_DPH_value.
1779                   
1780definition update_register_24: Byte → RegisterMap → RegisterMap ≝
1781  λb: Byte.
1782  λm: RegisterMap.
1783  let old_register_00_value ≝ register_00_value m in
1784  let old_register_01_value ≝ register_01_value m in
1785  let old_register_02_value ≝ register_02_value m in
1786  let old_register_03_value ≝ register_03_value m in
1787  let old_register_04_value ≝ register_04_value m in
1788  let old_register_05_value ≝ register_05_value m in
1789  let old_register_06_value ≝ register_06_value m in
1790  let old_register_07_value ≝ register_07_value m in
1791  let old_register_10_value ≝ register_01_value m in
1792  let old_register_11_value ≝ register_01_value m in
1793  let old_register_12_value ≝ register_02_value m in
1794  let old_register_13_value ≝ register_03_value m in
1795  let old_register_14_value ≝ register_04_value m in
1796  let old_register_15_value ≝ register_05_value m in
1797  let old_register_16_value ≝ register_06_value m in
1798  let old_register_17_value ≝ register_07_value m in
1799  let old_register_20_value ≝ register_01_value m in
1800  let old_register_21_value ≝ register_02_value m in
1801  let old_register_22_value ≝ register_02_value m in
1802  let old_register_23_value ≝ register_03_value m in
1803  let old_register_24_value ≝ register_04_value m in
1804  let old_register_25_value ≝ register_05_value m in
1805  let old_register_26_value ≝ register_06_value m in
1806  let old_register_27_value ≝ register_07_value m in
1807  let old_register_30_value ≝ register_01_value m in
1808  let old_register_31_value ≝ register_02_value m in
1809  let old_register_32_value ≝ register_02_value m in
1810  let old_register_33_value ≝ register_03_value m in
1811  let old_register_34_value ≝ register_04_value m in
1812  let old_register_35_value ≝ register_05_value m in
1813  let old_register_36_value ≝ register_06_value m in
1814  let old_register_37_value ≝ register_07_value m in
1815  let old_register_A_value ≝ register_A_value m in
1816  let old_register_B_value ≝ register_B_value m in
1817  let old_register_DPL_value ≝ register_DPL_value m in
1818  let old_register_DPH_value ≝ register_DPH_value m in
1819    mk_RegisterMap old_register_00_value
1820                   old_register_01_value
1821                   old_register_02_value
1822                   old_register_03_value
1823                   old_register_04_value
1824                   old_register_05_value
1825                   old_register_06_value
1826                   old_register_07_value
1827                   old_register_10_value
1828                   old_register_11_value
1829                   old_register_12_value
1830                   old_register_13_value
1831                   old_register_14_value
1832                   old_register_15_value
1833                   old_register_16_value
1834                   old_register_17_value
1835                   old_register_20_value
1836                   old_register_21_value
1837                   old_register_22_value
1838                   old_register_23_value
1839                   (Some ? b)
1840                   old_register_25_value
1841                   old_register_26_value
1842                   old_register_27_value
1843                   old_register_30_value
1844                   old_register_31_value
1845                   old_register_32_value
1846                   old_register_33_value
1847                   old_register_34_value
1848                   old_register_35_value
1849                   old_register_36_value
1850                   old_register_37_value
1851                   old_register_A_value
1852                   old_register_B_value
1853                   old_register_DPL_value
1854                   old_register_DPH_value.
1855
1856definition update_register_25: Byte → RegisterMap → RegisterMap ≝
1857  λb: Byte.
1858  λm: RegisterMap.
1859  let old_register_00_value ≝ register_00_value m in
1860  let old_register_01_value ≝ register_01_value m in
1861  let old_register_02_value ≝ register_02_value m in
1862  let old_register_03_value ≝ register_03_value m in
1863  let old_register_04_value ≝ register_04_value m in
1864  let old_register_05_value ≝ register_05_value m in
1865  let old_register_06_value ≝ register_06_value m in
1866  let old_register_07_value ≝ register_07_value m in
1867  let old_register_10_value ≝ register_01_value m in
1868  let old_register_11_value ≝ register_01_value m in
1869  let old_register_12_value ≝ register_02_value m in
1870  let old_register_13_value ≝ register_03_value m in
1871  let old_register_14_value ≝ register_04_value m in
1872  let old_register_15_value ≝ register_05_value m in
1873  let old_register_16_value ≝ register_06_value m in
1874  let old_register_17_value ≝ register_07_value m in
1875  let old_register_20_value ≝ register_01_value m in
1876  let old_register_21_value ≝ register_02_value m in
1877  let old_register_22_value ≝ register_02_value m in
1878  let old_register_23_value ≝ register_03_value m in
1879  let old_register_24_value ≝ register_04_value m in
1880  let old_register_25_value ≝ register_05_value m in
1881  let old_register_26_value ≝ register_06_value m in
1882  let old_register_27_value ≝ register_07_value m in
1883  let old_register_30_value ≝ register_01_value m in
1884  let old_register_31_value ≝ register_02_value m in
1885  let old_register_32_value ≝ register_02_value m in
1886  let old_register_33_value ≝ register_03_value m in
1887  let old_register_34_value ≝ register_04_value m in
1888  let old_register_35_value ≝ register_05_value m in
1889  let old_register_36_value ≝ register_06_value m in
1890  let old_register_37_value ≝ register_07_value m in
1891  let old_register_A_value ≝ register_A_value m in
1892  let old_register_B_value ≝ register_B_value m in
1893  let old_register_DPL_value ≝ register_DPL_value m in
1894  let old_register_DPH_value ≝ register_DPH_value m in
1895    mk_RegisterMap old_register_00_value
1896                   old_register_01_value
1897                   old_register_02_value
1898                   old_register_03_value
1899                   old_register_04_value
1900                   old_register_05_value
1901                   old_register_06_value
1902                   old_register_07_value
1903                   old_register_10_value
1904                   old_register_11_value
1905                   old_register_12_value
1906                   old_register_13_value
1907                   old_register_14_value
1908                   old_register_15_value
1909                   old_register_16_value
1910                   old_register_17_value
1911                   old_register_20_value
1912                   old_register_21_value
1913                   old_register_22_value
1914                   old_register_23_value
1915                   old_register_24_value
1916                   (Some ? b)
1917                   old_register_26_value
1918                   old_register_27_value
1919                   old_register_30_value
1920                   old_register_31_value
1921                   old_register_32_value
1922                   old_register_33_value
1923                   old_register_34_value
1924                   old_register_35_value
1925                   old_register_36_value
1926                   old_register_37_value
1927                   old_register_A_value
1928                   old_register_B_value
1929                   old_register_DPL_value
1930                   old_register_DPH_value.
1931
1932definition update_register_26: Byte → RegisterMap → RegisterMap ≝
1933  λb: Byte.
1934  λm: RegisterMap.
1935  let old_register_00_value ≝ register_00_value m in
1936  let old_register_01_value ≝ register_01_value m in
1937  let old_register_02_value ≝ register_02_value m in
1938  let old_register_03_value ≝ register_03_value m in
1939  let old_register_04_value ≝ register_04_value m in
1940  let old_register_05_value ≝ register_05_value m in
1941  let old_register_06_value ≝ register_06_value m in
1942  let old_register_07_value ≝ register_07_value m in
1943  let old_register_10_value ≝ register_01_value m in
1944  let old_register_11_value ≝ register_01_value m in
1945  let old_register_12_value ≝ register_02_value m in
1946  let old_register_13_value ≝ register_03_value m in
1947  let old_register_14_value ≝ register_04_value m in
1948  let old_register_15_value ≝ register_05_value m in
1949  let old_register_16_value ≝ register_06_value m in
1950  let old_register_17_value ≝ register_07_value m in
1951  let old_register_20_value ≝ register_01_value m in
1952  let old_register_21_value ≝ register_02_value m in
1953  let old_register_22_value ≝ register_02_value m in
1954  let old_register_23_value ≝ register_03_value m in
1955  let old_register_24_value ≝ register_04_value m in
1956  let old_register_25_value ≝ register_05_value m in
1957  let old_register_26_value ≝ register_06_value m in
1958  let old_register_27_value ≝ register_07_value m in
1959  let old_register_30_value ≝ register_01_value m in
1960  let old_register_31_value ≝ register_02_value m in
1961  let old_register_32_value ≝ register_02_value m in
1962  let old_register_33_value ≝ register_03_value m in
1963  let old_register_34_value ≝ register_04_value m in
1964  let old_register_35_value ≝ register_05_value m in
1965  let old_register_36_value ≝ register_06_value m in
1966  let old_register_37_value ≝ register_07_value m in
1967  let old_register_A_value ≝ register_A_value m in
1968  let old_register_B_value ≝ register_B_value m in
1969  let old_register_DPL_value ≝ register_DPL_value m in
1970  let old_register_DPH_value ≝ register_DPH_value m in
1971    mk_RegisterMap old_register_00_value
1972                   old_register_01_value
1973                   old_register_02_value
1974                   old_register_03_value
1975                   old_register_04_value
1976                   old_register_05_value
1977                   old_register_06_value
1978                   old_register_07_value
1979                   old_register_10_value
1980                   old_register_11_value
1981                   old_register_12_value
1982                   old_register_13_value
1983                   old_register_14_value
1984                   old_register_15_value
1985                   old_register_16_value
1986                   old_register_17_value
1987                   old_register_20_value
1988                   old_register_21_value
1989                   old_register_22_value
1990                   old_register_23_value
1991                   old_register_24_value
1992                   old_register_25_value
1993                   (Some ? b)
1994                   old_register_27_value
1995                   old_register_30_value
1996                   old_register_31_value
1997                   old_register_32_value
1998                   old_register_33_value
1999                   old_register_34_value
2000                   old_register_35_value
2001                   old_register_36_value
2002                   old_register_37_value
2003                   old_register_A_value
2004                   old_register_B_value
2005                   old_register_DPL_value
2006                   old_register_DPH_value.
2007
2008definition update_register_27: Byte → RegisterMap → RegisterMap ≝
2009  λb: Byte.
2010  λm: RegisterMap.
2011  let old_register_00_value ≝ register_00_value m in
2012  let old_register_01_value ≝ register_01_value m in
2013  let old_register_02_value ≝ register_02_value m in
2014  let old_register_03_value ≝ register_03_value m in
2015  let old_register_04_value ≝ register_04_value m in
2016  let old_register_05_value ≝ register_05_value m in
2017  let old_register_06_value ≝ register_06_value m in
2018  let old_register_07_value ≝ register_07_value m in
2019  let old_register_10_value ≝ register_01_value m in
2020  let old_register_11_value ≝ register_01_value m in
2021  let old_register_12_value ≝ register_02_value m in
2022  let old_register_13_value ≝ register_03_value m in
2023  let old_register_14_value ≝ register_04_value m in
2024  let old_register_15_value ≝ register_05_value m in
2025  let old_register_16_value ≝ register_06_value m in
2026  let old_register_17_value ≝ register_07_value m in
2027  let old_register_20_value ≝ register_01_value m in
2028  let old_register_21_value ≝ register_02_value m in
2029  let old_register_22_value ≝ register_02_value m in
2030  let old_register_23_value ≝ register_03_value m in
2031  let old_register_24_value ≝ register_04_value m in
2032  let old_register_25_value ≝ register_05_value m in
2033  let old_register_26_value ≝ register_06_value m in
2034  let old_register_27_value ≝ register_07_value m in
2035  let old_register_30_value ≝ register_01_value m in
2036  let old_register_31_value ≝ register_02_value m in
2037  let old_register_32_value ≝ register_02_value m in
2038  let old_register_33_value ≝ register_03_value m in
2039  let old_register_34_value ≝ register_04_value m in
2040  let old_register_35_value ≝ register_05_value m in
2041  let old_register_36_value ≝ register_06_value m in
2042  let old_register_37_value ≝ register_07_value m in
2043  let old_register_A_value ≝ register_A_value m in
2044  let old_register_B_value ≝ register_B_value m in
2045  let old_register_DPL_value ≝ register_DPL_value m in
2046  let old_register_DPH_value ≝ register_DPH_value m in
2047    mk_RegisterMap old_register_00_value
2048                   old_register_01_value
2049                   old_register_02_value
2050                   old_register_03_value
2051                   old_register_04_value
2052                   old_register_05_value
2053                   old_register_06_value
2054                   old_register_07_value
2055                   old_register_10_value
2056                   old_register_11_value
2057                   old_register_12_value
2058                   old_register_13_value
2059                   old_register_14_value
2060                   old_register_15_value
2061                   old_register_16_value
2062                   old_register_17_value
2063                   old_register_20_value
2064                   old_register_21_value
2065                   old_register_22_value
2066                   old_register_23_value
2067                   old_register_24_value
2068                   old_register_25_value
2069                   old_register_26_value
2070                   (Some ? b)
2071                   old_register_30_value
2072                   old_register_31_value
2073                   old_register_32_value
2074                   old_register_33_value
2075                   old_register_34_value
2076                   old_register_35_value
2077                   old_register_36_value
2078                   old_register_37_value
2079                   old_register_A_value
2080                   old_register_B_value
2081                   old_register_DPL_value
2082                   old_register_DPH_value.
2083
2084definition update_register_30: Byte → RegisterMap → RegisterMap ≝
2085  λb: Byte.
2086  λm: RegisterMap.
2087  let old_register_00_value ≝ register_00_value m in
2088  let old_register_01_value ≝ register_01_value m in
2089  let old_register_02_value ≝ register_02_value m in
2090  let old_register_03_value ≝ register_03_value m in
2091  let old_register_04_value ≝ register_04_value m in
2092  let old_register_05_value ≝ register_05_value m in
2093  let old_register_06_value ≝ register_06_value m in
2094  let old_register_07_value ≝ register_07_value m in
2095  let old_register_10_value ≝ register_01_value m in
2096  let old_register_11_value ≝ register_01_value m in
2097  let old_register_12_value ≝ register_02_value m in
2098  let old_register_13_value ≝ register_03_value m in
2099  let old_register_14_value ≝ register_04_value m in
2100  let old_register_15_value ≝ register_05_value m in
2101  let old_register_16_value ≝ register_06_value m in
2102  let old_register_17_value ≝ register_07_value m in
2103  let old_register_20_value ≝ register_01_value m in
2104  let old_register_21_value ≝ register_02_value m in
2105  let old_register_22_value ≝ register_02_value m in
2106  let old_register_23_value ≝ register_03_value m in
2107  let old_register_24_value ≝ register_04_value m in
2108  let old_register_25_value ≝ register_05_value m in
2109  let old_register_26_value ≝ register_06_value m in
2110  let old_register_27_value ≝ register_07_value m in
2111  let old_register_30_value ≝ register_01_value m in
2112  let old_register_31_value ≝ register_02_value m in
2113  let old_register_32_value ≝ register_02_value m in
2114  let old_register_33_value ≝ register_03_value m in
2115  let old_register_34_value ≝ register_04_value m in
2116  let old_register_35_value ≝ register_05_value m in
2117  let old_register_36_value ≝ register_06_value m in
2118  let old_register_37_value ≝ register_07_value m in
2119  let old_register_A_value ≝ register_A_value m in
2120  let old_register_B_value ≝ register_B_value m in
2121  let old_register_DPL_value ≝ register_DPL_value m in
2122  let old_register_DPH_value ≝ register_DPH_value m in
2123    mk_RegisterMap old_register_00_value
2124                   old_register_01_value
2125                   old_register_02_value
2126                   old_register_03_value
2127                   old_register_04_value
2128                   old_register_05_value
2129                   old_register_06_value
2130                   old_register_07_value
2131                   old_register_10_value
2132                   old_register_11_value
2133                   old_register_12_value
2134                   old_register_13_value
2135                   old_register_14_value
2136                   old_register_15_value
2137                   old_register_16_value
2138                   old_register_17_value
2139                   old_register_20_value
2140                   old_register_21_value
2141                   old_register_22_value
2142                   old_register_23_value
2143                   old_register_24_value
2144                   old_register_25_value
2145                   old_register_26_value
2146                   old_register_27_value
2147                   (Some ? b)
2148                   old_register_31_value
2149                   old_register_32_value
2150                   old_register_33_value
2151                   old_register_34_value
2152                   old_register_35_value
2153                   old_register_36_value
2154                   old_register_37_value
2155                   old_register_A_value
2156                   old_register_B_value
2157                   old_register_DPL_value
2158                   old_register_DPH_value.
2159
2160definition update_register_31: Byte → RegisterMap → RegisterMap ≝
2161  λb: Byte.
2162  λm: RegisterMap.
2163  let old_register_00_value ≝ register_00_value m in
2164  let old_register_01_value ≝ register_01_value m in
2165  let old_register_02_value ≝ register_02_value m in
2166  let old_register_03_value ≝ register_03_value m in
2167  let old_register_04_value ≝ register_04_value m in
2168  let old_register_05_value ≝ register_05_value m in
2169  let old_register_06_value ≝ register_06_value m in
2170  let old_register_07_value ≝ register_07_value m in
2171  let old_register_10_value ≝ register_01_value m in
2172  let old_register_11_value ≝ register_01_value m in
2173  let old_register_12_value ≝ register_02_value m in
2174  let old_register_13_value ≝ register_03_value m in
2175  let old_register_14_value ≝ register_04_value m in
2176  let old_register_15_value ≝ register_05_value m in
2177  let old_register_16_value ≝ register_06_value m in
2178  let old_register_17_value ≝ register_07_value m in
2179  let old_register_20_value ≝ register_01_value m in
2180  let old_register_21_value ≝ register_02_value m in
2181  let old_register_22_value ≝ register_02_value m in
2182  let old_register_23_value ≝ register_03_value m in
2183  let old_register_24_value ≝ register_04_value m in
2184  let old_register_25_value ≝ register_05_value m in
2185  let old_register_26_value ≝ register_06_value m in
2186  let old_register_27_value ≝ register_07_value m in
2187  let old_register_30_value ≝ register_01_value m in
2188  let old_register_31_value ≝ register_02_value m in
2189  let old_register_32_value ≝ register_02_value m in
2190  let old_register_33_value ≝ register_03_value m in
2191  let old_register_34_value ≝ register_04_value m in
2192  let old_register_35_value ≝ register_05_value m in
2193  let old_register_36_value ≝ register_06_value m in
2194  let old_register_37_value ≝ register_07_value m in
2195  let old_register_A_value ≝ register_A_value m in
2196  let old_register_B_value ≝ register_B_value m in
2197  let old_register_DPL_value ≝ register_DPL_value m in
2198  let old_register_DPH_value ≝ register_DPH_value m in
2199    mk_RegisterMap old_register_00_value
2200                   old_register_01_value
2201                   old_register_02_value
2202                   old_register_03_value
2203                   old_register_04_value
2204                   old_register_05_value
2205                   old_register_06_value
2206                   old_register_07_value
2207                   old_register_10_value
2208                   old_register_11_value
2209                   old_register_12_value
2210                   old_register_13_value
2211                   old_register_14_value
2212                   old_register_15_value
2213                   old_register_16_value
2214                   old_register_17_value
2215                   old_register_20_value
2216                   old_register_21_value
2217                   old_register_22_value
2218                   old_register_23_value
2219                   old_register_24_value
2220                   old_register_25_value
2221                   old_register_26_value
2222                   old_register_27_value
2223                   old_register_30_value
2224                   (Some ? b)
2225                   old_register_32_value
2226                   old_register_33_value
2227                   old_register_34_value
2228                   old_register_35_value
2229                   old_register_36_value
2230                   old_register_37_value
2231                   old_register_A_value
2232                   old_register_B_value
2233                   old_register_DPL_value
2234                   old_register_DPH_value.
2235
2236definition update_register_32: Byte → RegisterMap → RegisterMap ≝
2237  λb: Byte.
2238  λm: RegisterMap.
2239  let old_register_00_value ≝ register_00_value m in
2240  let old_register_01_value ≝ register_01_value m in
2241  let old_register_02_value ≝ register_02_value m in
2242  let old_register_03_value ≝ register_03_value m in
2243  let old_register_04_value ≝ register_04_value m in
2244  let old_register_05_value ≝ register_05_value m in
2245  let old_register_06_value ≝ register_06_value m in
2246  let old_register_07_value ≝ register_07_value m in
2247  let old_register_10_value ≝ register_01_value m in
2248  let old_register_11_value ≝ register_01_value m in
2249  let old_register_12_value ≝ register_02_value m in
2250  let old_register_13_value ≝ register_03_value m in
2251  let old_register_14_value ≝ register_04_value m in
2252  let old_register_15_value ≝ register_05_value m in
2253  let old_register_16_value ≝ register_06_value m in
2254  let old_register_17_value ≝ register_07_value m in
2255  let old_register_20_value ≝ register_01_value m in
2256  let old_register_21_value ≝ register_02_value m in
2257  let old_register_22_value ≝ register_02_value m in
2258  let old_register_23_value ≝ register_03_value m in
2259  let old_register_24_value ≝ register_04_value m in
2260  let old_register_25_value ≝ register_05_value m in
2261  let old_register_26_value ≝ register_06_value m in
2262  let old_register_27_value ≝ register_07_value m in
2263  let old_register_30_value ≝ register_01_value m in
2264  let old_register_31_value ≝ register_02_value m in
2265  let old_register_32_value ≝ register_02_value m in
2266  let old_register_33_value ≝ register_03_value m in
2267  let old_register_34_value ≝ register_04_value m in
2268  let old_register_35_value ≝ register_05_value m in
2269  let old_register_36_value ≝ register_06_value m in
2270  let old_register_37_value ≝ register_07_value m in
2271  let old_register_A_value ≝ register_A_value m in
2272  let old_register_B_value ≝ register_B_value m in
2273  let old_register_DPL_value ≝ register_DPL_value m in
2274  let old_register_DPH_value ≝ register_DPH_value m in
2275    mk_RegisterMap old_register_00_value
2276                   old_register_01_value
2277                   old_register_02_value
2278                   old_register_03_value
2279                   old_register_04_value
2280                   old_register_05_value
2281                   old_register_06_value
2282                   old_register_07_value
2283                   old_register_10_value
2284                   old_register_11_value
2285                   old_register_12_value
2286                   old_register_13_value
2287                   old_register_14_value
2288                   old_register_15_value
2289                   old_register_16_value
2290                   old_register_17_value
2291                   old_register_20_value
2292                   old_register_21_value
2293                   old_register_22_value
2294                   old_register_23_value
2295                   old_register_24_value
2296                   old_register_25_value
2297                   old_register_26_value
2298                   old_register_27_value
2299                   old_register_30_value
2300                   old_register_31_value
2301                   (Some ? b)
2302                   old_register_33_value
2303                   old_register_34_value
2304                   old_register_35_value
2305                   old_register_36_value
2306                   old_register_37_value
2307                   old_register_A_value
2308                   old_register_B_value
2309                   old_register_DPL_value
2310                   old_register_DPH_value.
2311
2312definition update_register_33: Byte → RegisterMap → RegisterMap ≝
2313  λb: Byte.
2314  λm: RegisterMap.
2315  let old_register_00_value ≝ register_00_value m in
2316  let old_register_01_value ≝ register_01_value m in
2317  let old_register_02_value ≝ register_02_value m in
2318  let old_register_03_value ≝ register_03_value m in
2319  let old_register_04_value ≝ register_04_value m in
2320  let old_register_05_value ≝ register_05_value m in
2321  let old_register_06_value ≝ register_06_value m in
2322  let old_register_07_value ≝ register_07_value m in
2323  let old_register_10_value ≝ register_01_value m in
2324  let old_register_11_value ≝ register_01_value m in
2325  let old_register_12_value ≝ register_02_value m in
2326  let old_register_13_value ≝ register_03_value m in
2327  let old_register_14_value ≝ register_04_value m in
2328  let old_register_15_value ≝ register_05_value m in
2329  let old_register_16_value ≝ register_06_value m in
2330  let old_register_17_value ≝ register_07_value m in
2331  let old_register_20_value ≝ register_01_value m in
2332  let old_register_21_value ≝ register_02_value m in
2333  let old_register_22_value ≝ register_02_value m in
2334  let old_register_23_value ≝ register_03_value m in
2335  let old_register_24_value ≝ register_04_value m in
2336  let old_register_25_value ≝ register_05_value m in
2337  let old_register_26_value ≝ register_06_value m in
2338  let old_register_27_value ≝ register_07_value m in
2339  let old_register_30_value ≝ register_01_value m in
2340  let old_register_31_value ≝ register_02_value m in
2341  let old_register_32_value ≝ register_02_value m in
2342  let old_register_33_value ≝ register_03_value m in
2343  let old_register_34_value ≝ register_04_value m in
2344  let old_register_35_value ≝ register_05_value m in
2345  let old_register_36_value ≝ register_06_value m in
2346  let old_register_37_value ≝ register_07_value m in
2347  let old_register_A_value ≝ register_A_value m in
2348  let old_register_B_value ≝ register_B_value m in
2349  let old_register_DPL_value ≝ register_DPL_value m in
2350  let old_register_DPH_value ≝ register_DPH_value m in
2351    mk_RegisterMap old_register_00_value
2352                   old_register_01_value
2353                   old_register_02_value
2354                   old_register_03_value
2355                   old_register_04_value
2356                   old_register_05_value
2357                   old_register_06_value
2358                   old_register_07_value
2359                   old_register_10_value
2360                   old_register_11_value
2361                   old_register_12_value
2362                   old_register_13_value
2363                   old_register_14_value
2364                   old_register_15_value
2365                   old_register_16_value
2366                   old_register_17_value
2367                   old_register_20_value
2368                   old_register_21_value
2369                   old_register_22_value
2370                   old_register_23_value
2371                   old_register_24_value
2372                   old_register_25_value
2373                   old_register_26_value
2374                   old_register_27_value
2375                   old_register_30_value
2376                   old_register_31_value
2377                   old_register_32_value
2378                   (Some ? b)
2379                   old_register_34_value
2380                   old_register_35_value
2381                   old_register_36_value
2382                   old_register_37_value
2383                   old_register_A_value
2384                   old_register_B_value
2385                   old_register_DPL_value
2386                   old_register_DPH_value.
2387
2388definition update_register_34: Byte → RegisterMap → RegisterMap ≝
2389  λb: Byte.
2390  λm: RegisterMap.
2391  let old_register_00_value ≝ register_00_value m in
2392  let old_register_01_value ≝ register_01_value m in
2393  let old_register_02_value ≝ register_02_value m in
2394  let old_register_03_value ≝ register_03_value m in
2395  let old_register_04_value ≝ register_04_value m in
2396  let old_register_05_value ≝ register_05_value m in
2397  let old_register_06_value ≝ register_06_value m in
2398  let old_register_07_value ≝ register_07_value m in
2399  let old_register_10_value ≝ register_01_value m in
2400  let old_register_11_value ≝ register_01_value m in
2401  let old_register_12_value ≝ register_02_value m in
2402  let old_register_13_value ≝ register_03_value m in
2403  let old_register_14_value ≝ register_04_value m in
2404  let old_register_15_value ≝ register_05_value m in
2405  let old_register_16_value ≝ register_06_value m in
2406  let old_register_17_value ≝ register_07_value m in
2407  let old_register_20_value ≝ register_01_value m in
2408  let old_register_21_value ≝ register_02_value m in
2409  let old_register_22_value ≝ register_02_value m in
2410  let old_register_23_value ≝ register_03_value m in
2411  let old_register_24_value ≝ register_04_value m in
2412  let old_register_25_value ≝ register_05_value m in
2413  let old_register_26_value ≝ register_06_value m in
2414  let old_register_27_value ≝ register_07_value m in
2415  let old_register_30_value ≝ register_01_value m in
2416  let old_register_31_value ≝ register_02_value m in
2417  let old_register_32_value ≝ register_02_value m in
2418  let old_register_33_value ≝ register_03_value m in
2419  let old_register_34_value ≝ register_04_value m in
2420  let old_register_35_value ≝ register_05_value m in
2421  let old_register_36_value ≝ register_06_value m in
2422  let old_register_37_value ≝ register_07_value m in
2423  let old_register_A_value ≝ register_A_value m in
2424  let old_register_B_value ≝ register_B_value m in
2425  let old_register_DPL_value ≝ register_DPL_value m in
2426  let old_register_DPH_value ≝ register_DPH_value m in
2427    mk_RegisterMap old_register_00_value
2428                   old_register_01_value
2429                   old_register_02_value
2430                   old_register_03_value
2431                   old_register_04_value
2432                   old_register_05_value
2433                   old_register_06_value
2434                   old_register_07_value
2435                   old_register_10_value
2436                   old_register_11_value
2437                   old_register_12_value
2438                   old_register_13_value
2439                   old_register_14_value
2440                   old_register_15_value
2441                   old_register_16_value
2442                   old_register_17_value
2443                   old_register_20_value
2444                   old_register_21_value
2445                   old_register_22_value
2446                   old_register_23_value
2447                   old_register_24_value
2448                   old_register_25_value
2449                   old_register_26_value
2450                   old_register_27_value
2451                   old_register_30_value
2452                   old_register_31_value
2453                   old_register_32_value
2454                   old_register_33_value
2455                   (Some ? b)
2456                   old_register_35_value
2457                   old_register_36_value
2458                   old_register_37_value
2459                   old_register_A_value
2460                   old_register_B_value
2461                   old_register_DPL_value
2462                   old_register_DPH_value.
2463
2464definition update_register_35: Byte → RegisterMap → RegisterMap ≝
2465  λb: Byte.
2466  λm: RegisterMap.
2467  let old_register_00_value ≝ register_00_value m in
2468  let old_register_01_value ≝ register_01_value m in
2469  let old_register_02_value ≝ register_02_value m in
2470  let old_register_03_value ≝ register_03_value m in
2471  let old_register_04_value ≝ register_04_value m in
2472  let old_register_05_value ≝ register_05_value m in
2473  let old_register_06_value ≝ register_06_value m in
2474  let old_register_07_value ≝ register_07_value m in
2475  let old_register_10_value ≝ register_01_value m in
2476  let old_register_11_value ≝ register_01_value m in
2477  let old_register_12_value ≝ register_02_value m in
2478  let old_register_13_value ≝ register_03_value m in
2479  let old_register_14_value ≝ register_04_value m in
2480  let old_register_15_value ≝ register_05_value m in
2481  let old_register_16_value ≝ register_06_value m in
2482  let old_register_17_value ≝ register_07_value m in
2483  let old_register_20_value ≝ register_01_value m in
2484  let old_register_21_value ≝ register_02_value m in
2485  let old_register_22_value ≝ register_02_value m in
2486  let old_register_23_value ≝ register_03_value m in
2487  let old_register_24_value ≝ register_04_value m in
2488  let old_register_25_value ≝ register_05_value m in
2489  let old_register_26_value ≝ register_06_value m in
2490  let old_register_27_value ≝ register_07_value m in
2491  let old_register_30_value ≝ register_01_value m in
2492  let old_register_31_value ≝ register_02_value m in
2493  let old_register_32_value ≝ register_02_value m in
2494  let old_register_33_value ≝ register_03_value m in
2495  let old_register_34_value ≝ register_04_value m in
2496  let old_register_35_value ≝ register_05_value m in
2497  let old_register_36_value ≝ register_06_value m in
2498  let old_register_37_value ≝ register_07_value m in
2499  let old_register_A_value ≝ register_A_value m in
2500  let old_register_B_value ≝ register_B_value m in
2501  let old_register_DPL_value ≝ register_DPL_value m in
2502  let old_register_DPH_value ≝ register_DPH_value m in
2503    mk_RegisterMap old_register_00_value
2504                   old_register_01_value
2505                   old_register_02_value
2506                   old_register_03_value
2507                   old_register_04_value
2508                   old_register_05_value
2509                   old_register_06_value
2510                   old_register_07_value
2511                   old_register_10_value
2512                   old_register_11_value
2513                   old_register_12_value
2514                   old_register_13_value
2515                   old_register_14_value
2516                   old_register_15_value
2517                   old_register_16_value
2518                   old_register_17_value
2519                   old_register_20_value
2520                   old_register_21_value
2521                   old_register_22_value
2522                   old_register_23_value
2523                   old_register_24_value
2524                   old_register_25_value
2525                   old_register_26_value
2526                   old_register_27_value
2527                   old_register_30_value
2528                   old_register_31_value
2529                   old_register_32_value
2530                   old_register_33_value
2531                   old_register_34_value
2532                   (Some ? b)
2533                   old_register_36_value
2534                   old_register_37_value
2535                   old_register_A_value
2536                   old_register_B_value
2537                   old_register_DPL_value
2538                   old_register_DPH_value.
2539
2540definition update_register_36: Byte → RegisterMap → RegisterMap ≝
2541  λb: Byte.
2542  λm: RegisterMap.
2543  let old_register_00_value ≝ register_00_value m in
2544  let old_register_01_value ≝ register_01_value m in
2545  let old_register_02_value ≝ register_02_value m in
2546  let old_register_03_value ≝ register_03_value m in
2547  let old_register_04_value ≝ register_04_value m in
2548  let old_register_05_value ≝ register_05_value m in
2549  let old_register_06_value ≝ register_06_value m in
2550  let old_register_07_value ≝ register_07_value m in
2551  let old_register_10_value ≝ register_01_value m in
2552  let old_register_11_value ≝ register_01_value m in
2553  let old_register_12_value ≝ register_02_value m in
2554  let old_register_13_value ≝ register_03_value m in
2555  let old_register_14_value ≝ register_04_value m in
2556  let old_register_15_value ≝ register_05_value m in
2557  let old_register_16_value ≝ register_06_value m in
2558  let old_register_17_value ≝ register_07_value m in
2559  let old_register_20_value ≝ register_01_value m in
2560  let old_register_21_value ≝ register_02_value m in
2561  let old_register_22_value ≝ register_02_value m in
2562  let old_register_23_value ≝ register_03_value m in
2563  let old_register_24_value ≝ register_04_value m in
2564  let old_register_25_value ≝ register_05_value m in
2565  let old_register_26_value ≝ register_06_value m in
2566  let old_register_27_value ≝ register_07_value m in
2567  let old_register_30_value ≝ register_01_value m in
2568  let old_register_31_value ≝ register_02_value m in
2569  let old_register_32_value ≝ register_02_value m in
2570  let old_register_33_value ≝ register_03_value m in
2571  let old_register_34_value ≝ register_04_value m in
2572  let old_register_35_value ≝ register_05_value m in
2573  let old_register_36_value ≝ register_06_value m in
2574  let old_register_37_value ≝ register_07_value m in
2575  let old_register_A_value ≝ register_A_value m in
2576  let old_register_B_value ≝ register_B_value m in
2577  let old_register_DPL_value ≝ register_DPL_value m in
2578  let old_register_DPH_value ≝ register_DPH_value m in
2579    mk_RegisterMap old_register_00_value
2580                   old_register_01_value
2581                   old_register_02_value
2582                   old_register_03_value
2583                   old_register_04_value
2584                   old_register_05_value
2585                   old_register_06_value
2586                   old_register_07_value
2587                   old_register_10_value
2588                   old_register_11_value
2589                   old_register_12_value
2590                   old_register_13_value
2591                   old_register_14_value
2592                   old_register_15_value
2593                   old_register_16_value
2594                   old_register_17_value
2595                   old_register_20_value
2596                   old_register_21_value
2597                   old_register_22_value
2598                   old_register_23_value
2599                   old_register_24_value
2600                   old_register_25_value
2601                   old_register_26_value
2602                   old_register_27_value
2603                   old_register_30_value
2604                   old_register_31_value
2605                   old_register_32_value
2606                   old_register_33_value
2607                   old_register_34_value
2608                   old_register_35_value
2609                   (Some ? b)
2610                   old_register_37_value
2611                   old_register_A_value
2612                   old_register_B_value
2613                   old_register_DPL_value
2614                   old_register_DPH_value.
2615
2616definition update_register_37: Byte → RegisterMap → RegisterMap ≝
2617  λb: Byte.
2618  λm: RegisterMap.
2619  let old_register_00_value ≝ register_00_value m in
2620  let old_register_01_value ≝ register_01_value m in
2621  let old_register_02_value ≝ register_02_value m in
2622  let old_register_03_value ≝ register_03_value m in
2623  let old_register_04_value ≝ register_04_value m in
2624  let old_register_05_value ≝ register_05_value m in
2625  let old_register_06_value ≝ register_06_value m in
2626  let old_register_07_value ≝ register_07_value m in
2627  let old_register_10_value ≝ register_01_value m in
2628  let old_register_11_value ≝ register_01_value m in
2629  let old_register_12_value ≝ register_02_value m in
2630  let old_register_13_value ≝ register_03_value m in
2631  let old_register_14_value ≝ register_04_value m in
2632  let old_register_15_value ≝ register_05_value m in
2633  let old_register_16_value ≝ register_06_value m in
2634  let old_register_17_value ≝ register_07_value m in
2635  let old_register_20_value ≝ register_01_value m in
2636  let old_register_21_value ≝ register_02_value m in
2637  let old_register_22_value ≝ register_02_value m in
2638  let old_register_23_value ≝ register_03_value m in
2639  let old_register_24_value ≝ register_04_value m in
2640  let old_register_25_value ≝ register_05_value m in
2641  let old_register_26_value ≝ register_06_value m in
2642  let old_register_27_value ≝ register_07_value m in
2643  let old_register_30_value ≝ register_01_value m in
2644  let old_register_31_value ≝ register_02_value m in
2645  let old_register_32_value ≝ register_02_value m in
2646  let old_register_33_value ≝ register_03_value m in
2647  let old_register_34_value ≝ register_04_value m in
2648  let old_register_35_value ≝ register_05_value m in
2649  let old_register_36_value ≝ register_06_value m in
2650  let old_register_37_value ≝ register_07_value m in
2651  let old_register_A_value ≝ register_A_value m in
2652  let old_register_B_value ≝ register_B_value m in
2653  let old_register_DPL_value ≝ register_DPL_value m in
2654  let old_register_DPH_value ≝ register_DPH_value m in
2655    mk_RegisterMap old_register_00_value
2656                   old_register_01_value
2657                   old_register_02_value
2658                   old_register_03_value
2659                   old_register_04_value
2660                   old_register_05_value
2661                   old_register_06_value
2662                   old_register_07_value
2663                   old_register_10_value
2664                   old_register_11_value
2665                   old_register_12_value
2666                   old_register_13_value
2667                   old_register_14_value
2668                   old_register_15_value
2669                   old_register_16_value
2670                   old_register_17_value
2671                   old_register_20_value
2672                   old_register_21_value
2673                   old_register_22_value
2674                   old_register_23_value
2675                   old_register_24_value
2676                   old_register_25_value
2677                   old_register_26_value
2678                   old_register_27_value
2679                   old_register_30_value
2680                   old_register_31_value
2681                   old_register_32_value
2682                   old_register_33_value
2683                   old_register_34_value
2684                   old_register_35_value
2685                   old_register_36_value
2686                   (Some ? b)
2687                   old_register_A_value
2688                   old_register_B_value
2689                   old_register_DPL_value
2690                   old_register_DPH_value.
2691
2692definition update_register_A: Byte → RegisterMap → RegisterMap ≝
2693  λb: Byte.
2694  λm: RegisterMap.
2695  let old_register_00_value ≝ register_00_value m in
2696  let old_register_01_value ≝ register_01_value m in
2697  let old_register_02_value ≝ register_02_value m in
2698  let old_register_03_value ≝ register_03_value m in
2699  let old_register_04_value ≝ register_04_value m in
2700  let old_register_05_value ≝ register_05_value m in
2701  let old_register_06_value ≝ register_06_value m in
2702  let old_register_07_value ≝ register_07_value m in
2703  let old_register_10_value ≝ register_01_value m in
2704  let old_register_11_value ≝ register_01_value m in
2705  let old_register_12_value ≝ register_02_value m in
2706  let old_register_13_value ≝ register_03_value m in
2707  let old_register_14_value ≝ register_04_value m in
2708  let old_register_15_value ≝ register_05_value m in
2709  let old_register_16_value ≝ register_06_value m in
2710  let old_register_17_value ≝ register_07_value m in
2711  let old_register_20_value ≝ register_01_value m in
2712  let old_register_21_value ≝ register_02_value m in
2713  let old_register_22_value ≝ register_02_value m in
2714  let old_register_23_value ≝ register_03_value m in
2715  let old_register_24_value ≝ register_04_value m in
2716  let old_register_25_value ≝ register_05_value m in
2717  let old_register_26_value ≝ register_06_value m in
2718  let old_register_27_value ≝ register_07_value m in
2719  let old_register_30_value ≝ register_01_value m in
2720  let old_register_31_value ≝ register_02_value m in
2721  let old_register_32_value ≝ register_02_value m in
2722  let old_register_33_value ≝ register_03_value m in
2723  let old_register_34_value ≝ register_04_value m in
2724  let old_register_35_value ≝ register_05_value m in
2725  let old_register_36_value ≝ register_06_value m in
2726  let old_register_37_value ≝ register_07_value m in
2727  let old_register_A_value ≝ register_A_value m in
2728  let old_register_B_value ≝ register_B_value m in
2729  let old_register_DPL_value ≝ register_DPL_value m in
2730  let old_register_DPH_value ≝ register_DPH_value m in
2731    mk_RegisterMap old_register_00_value
2732                   old_register_01_value
2733                   old_register_02_value
2734                   old_register_03_value
2735                   old_register_04_value
2736                   old_register_05_value
2737                   old_register_06_value
2738                   old_register_07_value
2739                   old_register_10_value
2740                   old_register_11_value
2741                   old_register_12_value
2742                   old_register_13_value
2743                   old_register_14_value
2744                   old_register_15_value
2745                   old_register_16_value
2746                   old_register_17_value
2747                   old_register_20_value
2748                   old_register_21_value
2749                   old_register_22_value
2750                   old_register_23_value
2751                   old_register_24_value
2752                   old_register_25_value
2753                   old_register_26_value
2754                   old_register_27_value
2755                   old_register_30_value
2756                   old_register_31_value
2757                   old_register_32_value
2758                   old_register_33_value
2759                   old_register_34_value
2760                   old_register_35_value
2761                   old_register_36_value
2762                   old_register_37_value
2763                   (Some ? b)
2764                   old_register_B_value
2765                   old_register_DPL_value
2766                   old_register_DPH_value.
2767
2768definition update_register_B: Byte → RegisterMap → RegisterMap ≝
2769  λb: Byte.
2770  λm: RegisterMap.
2771  let old_register_00_value ≝ register_00_value m in
2772  let old_register_01_value ≝ register_01_value m in
2773  let old_register_02_value ≝ register_02_value m in
2774  let old_register_03_value ≝ register_03_value m in
2775  let old_register_04_value ≝ register_04_value m in
2776  let old_register_05_value ≝ register_05_value m in
2777  let old_register_06_value ≝ register_06_value m in
2778  let old_register_07_value ≝ register_07_value m in
2779  let old_register_10_value ≝ register_01_value m in
2780  let old_register_11_value ≝ register_01_value m in
2781  let old_register_12_value ≝ register_02_value m in
2782  let old_register_13_value ≝ register_03_value m in
2783  let old_register_14_value ≝ register_04_value m in
2784  let old_register_15_value ≝ register_05_value m in
2785  let old_register_16_value ≝ register_06_value m in
2786  let old_register_17_value ≝ register_07_value m in
2787  let old_register_20_value ≝ register_01_value m in
2788  let old_register_21_value ≝ register_02_value m in
2789  let old_register_22_value ≝ register_02_value m in
2790  let old_register_23_value ≝ register_03_value m in
2791  let old_register_24_value ≝ register_04_value m in
2792  let old_register_25_value ≝ register_05_value m in
2793  let old_register_26_value ≝ register_06_value m in
2794  let old_register_27_value ≝ register_07_value m in
2795  let old_register_30_value ≝ register_01_value m in
2796  let old_register_31_value ≝ register_02_value m in
2797  let old_register_32_value ≝ register_02_value m in
2798  let old_register_33_value ≝ register_03_value m in
2799  let old_register_34_value ≝ register_04_value m in
2800  let old_register_35_value ≝ register_05_value m in
2801  let old_register_36_value ≝ register_06_value m in
2802  let old_register_37_value ≝ register_07_value m in
2803  let old_register_A_value ≝ register_A_value m in
2804  let old_register_B_value ≝ register_B_value m in
2805  let old_register_DPL_value ≝ register_DPL_value m in
2806  let old_register_DPH_value ≝ register_DPH_value m in
2807    mk_RegisterMap old_register_00_value
2808                   old_register_01_value
2809                   old_register_02_value
2810                   old_register_03_value
2811                   old_register_04_value
2812                   old_register_05_value
2813                   old_register_06_value
2814                   old_register_07_value
2815                   old_register_10_value
2816                   old_register_11_value
2817                   old_register_12_value
2818                   old_register_13_value
2819                   old_register_14_value
2820                   old_register_15_value
2821                   old_register_16_value
2822                   old_register_17_value
2823                   old_register_20_value
2824                   old_register_21_value
2825                   old_register_22_value
2826                   old_register_23_value
2827                   old_register_24_value
2828                   old_register_25_value
2829                   old_register_26_value
2830                   old_register_27_value
2831                   old_register_30_value
2832                   old_register_31_value
2833                   old_register_32_value
2834                   old_register_33_value
2835                   old_register_34_value
2836                   old_register_35_value
2837                   old_register_36_value
2838                   old_register_37_value
2839                   old_register_A_value
2840                   (Some ? b)
2841                   old_register_DPL_value
2842                   old_register_DPH_value.
2843
2844definition update_register_DPL: Byte → RegisterMap → RegisterMap ≝
2845  λb: Byte.
2846  λm: RegisterMap.
2847  let old_register_00_value ≝ register_00_value m in
2848  let old_register_01_value ≝ register_01_value m in
2849  let old_register_02_value ≝ register_02_value m in
2850  let old_register_03_value ≝ register_03_value m in
2851  let old_register_04_value ≝ register_04_value m in
2852  let old_register_05_value ≝ register_05_value m in
2853  let old_register_06_value ≝ register_06_value m in
2854  let old_register_07_value ≝ register_07_value m in
2855  let old_register_10_value ≝ register_01_value m in
2856  let old_register_11_value ≝ register_01_value m in
2857  let old_register_12_value ≝ register_02_value m in
2858  let old_register_13_value ≝ register_03_value m in
2859  let old_register_14_value ≝ register_04_value m in
2860  let old_register_15_value ≝ register_05_value m in
2861  let old_register_16_value ≝ register_06_value m in
2862  let old_register_17_value ≝ register_07_value m in
2863  let old_register_20_value ≝ register_01_value m in
2864  let old_register_21_value ≝ register_02_value m in
2865  let old_register_22_value ≝ register_02_value m in
2866  let old_register_23_value ≝ register_03_value m in
2867  let old_register_24_value ≝ register_04_value m in
2868  let old_register_25_value ≝ register_05_value m in
2869  let old_register_26_value ≝ register_06_value m in
2870  let old_register_27_value ≝ register_07_value m in
2871  let old_register_30_value ≝ register_01_value m in
2872  let old_register_31_value ≝ register_02_value m in
2873  let old_register_32_value ≝ register_02_value m in
2874  let old_register_33_value ≝ register_03_value m in
2875  let old_register_34_value ≝ register_04_value m in
2876  let old_register_35_value ≝ register_05_value m in
2877  let old_register_36_value ≝ register_06_value m in
2878  let old_register_37_value ≝ register_07_value m in
2879  let old_register_A_value ≝ register_A_value m in
2880  let old_register_B_value ≝ register_B_value m in
2881  let old_register_DPL_value ≝ register_DPL_value m in
2882  let old_register_DPH_value ≝ register_DPH_value m in
2883    mk_RegisterMap old_register_00_value
2884                   old_register_01_value
2885                   old_register_02_value
2886                   old_register_03_value
2887                   old_register_04_value
2888                   old_register_05_value
2889                   old_register_06_value
2890                   old_register_07_value
2891                   old_register_10_value
2892                   old_register_11_value
2893                   old_register_12_value
2894                   old_register_13_value
2895                   old_register_14_value
2896                   old_register_15_value
2897                   old_register_16_value
2898                   old_register_17_value
2899                   old_register_20_value
2900                   old_register_21_value
2901                   old_register_22_value
2902                   old_register_23_value
2903                   old_register_24_value
2904                   old_register_25_value
2905                   old_register_26_value
2906                   old_register_27_value
2907                   old_register_30_value
2908                   old_register_31_value
2909                   old_register_32_value
2910                   old_register_33_value
2911                   old_register_34_value
2912                   old_register_35_value
2913                   old_register_36_value
2914                   old_register_37_value
2915                   old_register_A_value
2916                   old_register_B_value
2917                   (Some ? b)
2918                   old_register_DPH_value.
2919
2920definition update_register_DPH: Byte → RegisterMap → RegisterMap ≝
2921  λb: Byte.
2922  λm: RegisterMap.
2923  let old_register_00_value ≝ register_00_value m in
2924  let old_register_01_value ≝ register_01_value m in
2925  let old_register_02_value ≝ register_02_value m in
2926  let old_register_03_value ≝ register_03_value m in
2927  let old_register_04_value ≝ register_04_value m in
2928  let old_register_05_value ≝ register_05_value m in
2929  let old_register_06_value ≝ register_06_value m in
2930  let old_register_07_value ≝ register_07_value m in
2931  let old_register_10_value ≝ register_01_value m in
2932  let old_register_11_value ≝ register_01_value m in
2933  let old_register_12_value ≝ register_02_value m in
2934  let old_register_13_value ≝ register_03_value m in
2935  let old_register_14_value ≝ register_04_value m in
2936  let old_register_15_value ≝ register_05_value m in
2937  let old_register_16_value ≝ register_06_value m in
2938  let old_register_17_value ≝ register_07_value m in
2939  let old_register_20_value ≝ register_01_value m in
2940  let old_register_21_value ≝ register_02_value m in
2941  let old_register_22_value ≝ register_02_value m in
2942  let old_register_23_value ≝ register_03_value m in
2943  let old_register_24_value ≝ register_04_value m in
2944  let old_register_25_value ≝ register_05_value m in
2945  let old_register_26_value ≝ register_06_value m in
2946  let old_register_27_value ≝ register_07_value m in
2947  let old_register_30_value ≝ register_01_value m in
2948  let old_register_31_value ≝ register_02_value m in
2949  let old_register_32_value ≝ register_02_value m in
2950  let old_register_33_value ≝ register_03_value m in
2951  let old_register_34_value ≝ register_04_value m in
2952  let old_register_35_value ≝ register_05_value m in
2953  let old_register_36_value ≝ register_06_value m in
2954  let old_register_37_value ≝ register_07_value m in
2955  let old_register_A_value ≝ register_A_value m in
2956  let old_register_B_value ≝ register_B_value m in
2957  let old_register_DPL_value ≝ register_DPL_value m in
2958  let old_register_DPH_value ≝ register_DPH_value m in
2959    mk_RegisterMap old_register_00_value
2960                   old_register_01_value
2961                   old_register_02_value
2962                   old_register_03_value
2963                   old_register_04_value
2964                   old_register_05_value
2965                   old_register_06_value
2966                   old_register_07_value
2967                   old_register_10_value
2968                   old_register_11_value
2969                   old_register_12_value
2970                   old_register_13_value
2971                   old_register_14_value
2972                   old_register_15_value
2973                   old_register_16_value
2974                   old_register_17_value
2975                   old_register_20_value
2976                   old_register_21_value
2977                   old_register_22_value
2978                   old_register_23_value
2979                   old_register_24_value
2980                   old_register_25_value
2981                   old_register_26_value
2982                   old_register_27_value
2983                   old_register_30_value
2984                   old_register_31_value
2985                   old_register_32_value
2986                   old_register_33_value
2987                   old_register_34_value
2988                   old_register_35_value
2989                   old_register_36_value
2990                   old_register_37_value
2991                   old_register_A_value
2992                   old_register_B_value
2993                   old_register_DPL_value
2994                   (Some ? b).
2995
2996definition update_register_map: Register → Byte → RegisterMap → RegisterMap ≝
2997  λr: Register.
2998  λb: Byte.
2999  λm: RegisterMap.
3000  match r with
3001  [ Register00 ⇒ update_register_00 b m
3002  | Register01 ⇒ update_register_01 b m
3003  | Register02 ⇒ update_register_02 b m
3004  | Register03 ⇒ update_register_03 b m
3005  | Register04 ⇒ update_register_04 b m
3006  | Register05 ⇒ update_register_05 b m
3007  | Register06 ⇒ update_register_06 b m
3008  | Register07 ⇒ update_register_07 b m
3009  | Register10 ⇒ update_register_10 b m
3010  | Register11 ⇒ update_register_11 b m
3011  | Register12 ⇒ update_register_12 b m
3012  | Register13 ⇒ update_register_13 b m
3013  | Register14 ⇒ update_register_14 b m
3014  | Register15 ⇒ update_register_15 b m
3015  | Register16 ⇒ update_register_16 b m
3016  | Register17 ⇒ update_register_17 b m
3017  | Register20 ⇒ update_register_20 b m
3018  | Register21 ⇒ update_register_21 b m
3019  | Register22 ⇒ update_register_22 b m
3020  | Register23 ⇒ update_register_23 b m
3021  | Register24 ⇒ update_register_24 b m
3022  | Register25 ⇒ update_register_25 b m
3023  | Register26 ⇒ update_register_26 b m
3024  | Register27 ⇒ update_register_27 b m
3025  | Register30 ⇒ update_register_30 b m
3026  | Register31 ⇒ update_register_31 b m
3027  | Register32 ⇒ update_register_32 b m
3028  | Register33 ⇒ update_register_33 b m
3029  | Register34 ⇒ update_register_34 b m
3030  | Register35 ⇒ update_register_35 b m
3031  | Register36 ⇒ update_register_36 b m
3032  | Register37 ⇒ update_register_37 b m
3033  | RegisterA ⇒ update_register_A b m
3034  | RegisterB ⇒ update_register_B b m
3035  | RegisterDPL ⇒ update_register_DPL b m
3036  | RegisterDPH ⇒ update_register_DPH b m
3037  ].
3038 
3039record Eval: Type[0] ≝
3040{
3041  opaccs: OpAccs → Byte → Byte → option Byte;
3042  op1: Op1 → Byte → Byte;
3043  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
3044}.
3045
3046axiom opaccs_implementation: OpAccs → Byte → Byte → option Byte.
3047axiom op1_implementation: Op1 → Byte → Byte.
3048axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
3049
3050definition eval: Eval ≝
3051  mk_Eval opaccs_implementation
3052          op1_implementation
3053          op2_implementation.
Note: See TracBrowser for help on using the repository browser.