source: src/ASM/I8051.ma @ 762

Last change on this file since 762 was 757, checked in by mulligan, 10 years ago

Lots more fixing to get both front and backends using same conventions and types.

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