source: Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma @ 1098

Last change on this file since 1098 was 1098, checked in by campbell, 8 years ago

Merge branch with trunk

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