source: src/ASM/I8051.ma @ 1089

Last change on this file since 1089 was 1089, checked in by mulligan, 9 years ago

more changes from earlier in the week

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