source: src/ASM/I8051.ma @ 1187

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

fixed build.ma

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