include "arithmetics/nat.ma". include "basics/jmeq.ma". include "ASM/String.ma". include "ASM/ASM.ma". include "utilities/Compare.ma". (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps not further back in the translation chain. *) inductive OpAccs: Type[0] ≝ Mul: OpAccs | Divu: OpAccs | Modu: OpAccs. inductive Op1: Type[0] ≝ Cmpl: Op1 | Inc: Op1. inductive Op2: Type[0] ≝ Add: Op2 | Addc: Op2 | Sub: Op2 | And: Op2 | Or: Op2 | Xor: Op2. (* dpm: maybe useless? *) inductive Register: Type[0] ≝ Register00: Register | Register01: Register | Register02: Register | Register03: Register | Register04: Register | Register05: Register | Register06: Register | Register07: Register | Register10: Register | Register11: Register | Register12: Register | Register13: Register | Register14: Register | Register15: Register | Register16: Register | Register17: Register | Register20: Register | Register21: Register | Register22: Register | Register23: Register | Register24: Register | Register25: Register | Register26: Register | Register27: Register | Register30: Register | Register31: Register | Register32: Register | Register33: Register | Register34: Register | Register35: Register | Register36: Register | Register37: Register | RegisterA: Register | RegisterB: Register | RegisterDPL: Register | RegisterDPH: Register. definition nat_of_register: Register → nat ≝ λr: Register. match r with [ Register00 ⇒ 0 | Register01 ⇒ 1 | Register02 ⇒ 2 | Register03 ⇒ 3 | Register04 ⇒ 4 | Register05 ⇒ 5 | Register06 ⇒ 6 | Register07 ⇒ 7 | Register10 ⇒ 8 | Register11 ⇒ 9 | Register12 ⇒ 10 | Register13 ⇒ 11 | Register14 ⇒ 12 | Register15 ⇒ 13 | Register16 ⇒ 14 | Register17 ⇒ 15 | Register20 ⇒ 16 | Register21 ⇒ 17 | Register22 ⇒ 18 | Register23 ⇒ 19 | Register24 ⇒ 20 | Register25 ⇒ 21 | Register26 ⇒ 22 | Register27 ⇒ 23 | Register30 ⇒ 24 | Register31 ⇒ 25 | Register32 ⇒ 26 | Register33 ⇒ 27 | Register34 ⇒ 28 | Register35 ⇒ 29 | Register36 ⇒ 30 | Register37 ⇒ 31 | RegisterA ⇒ 32 | RegisterB ⇒ 33 | RegisterDPL ⇒ 34 | RegisterDPH ⇒ 35 ]. definition compare_register: Register → Register → Compare ≝ λr, s: Register. let r_as_nat ≝ nat_of_register r in let s_as_nat ≝ nat_of_register s in match eqb r_as_nat s_as_nat with [ true ⇒ Compare_Equal | false ⇒ match ltb r_as_nat s_as_nat with [ true ⇒ Compare_Less | false ⇒ Compare_Greater ] ]. definition eq_register: Register → Register → bool ≝ λr, s: Register. let r_as_nat ≝ nat_of_register r in let s_as_nat ≝ nat_of_register s in eqb r_as_nat s_as_nat. axiom print_register: Register → String. (* dpm: registers for stack manipulation *) definition RegisterSST ≝ Register03. definition RegisterST0 ≝ Register04. definition RegisterST1 ≝ Register05. definition RegisterSPL ≝ Register06. definition RegisterSPH ≝ Register07. definition register_address: Register → [[ acc_a; direct; register ]] ≝ λr: Register. match r with [ Register00 ⇒ REGISTER [[ false; false; false ]] | Register01 ⇒ REGISTER [[ false; false; true ]] | Register02 ⇒ REGISTER [[ false; true; false ]] | Register03 ⇒ REGISTER [[ false; true; true ]] | Register04 ⇒ REGISTER [[ true; false; false ]] | Register05 ⇒ REGISTER [[ true; false; true ]] | Register06 ⇒ REGISTER [[ true; true; false ]] | Register07 ⇒ REGISTER [[ true; true; true ]] | RegisterA ⇒ ACC_A | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240) | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82) | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83) | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) ]. [*: normalize @ I ] qed. definition registers: list Register ≝ [ Register00; Register01; Register02; Register03; Register04; Register05; Register06; Register07; RegisterA; RegisterB; RegisterDPL; RegisterDPH; Register10; Register11; Register12; Register13; Register14; Register15; Register16; Register17; Register20; Register21; Register22; Register23; Register24; Register25; Register26; Register27; Register30; Register31; Register32; Register33; Register34; Register35; Register36; Register37; RegisterSST; RegisterST0; RegisterST1; RegisterSPL; RegisterSPH ]. definition forbidden_registers: list Register ≝ [ RegisterSST; RegisterST0; RegisterST1; RegisterSPL; RegisterSPH ]. record RegisterMap: Type[0] ≝ { register_00_value: option Byte; register_01_value: option Byte; register_02_value: option Byte; register_03_value: option Byte; register_04_value: option Byte; register_05_value: option Byte; register_06_value: option Byte; register_07_value: option Byte; register_10_value: option Byte; register_11_value: option Byte; register_12_value: option Byte; register_13_value: option Byte; register_14_value: option Byte; register_15_value: option Byte; register_16_value: option Byte; register_17_value: option Byte; register_20_value: option Byte; register_21_value: option Byte; register_22_value: option Byte; register_23_value: option Byte; register_24_value: option Byte; register_25_value: option Byte; register_26_value: option Byte; register_27_value: option Byte; register_30_value: option Byte; register_31_value: option Byte; register_32_value: option Byte; register_33_value: option Byte; register_34_value: option Byte; register_35_value: option Byte; register_36_value: option Byte; register_37_value: option Byte; register_A_value: option Byte; register_B_value: option Byte; register_DPL_value: option Byte; register_DPH_value: option Byte }. definition initialize_register_map: RegisterMap ≝ mk_RegisterMap (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?) (None ?). definition lookup_register_map: Register → RegisterMap → option Byte ≝ λr: Register. λm: RegisterMap. match r with [ Register00 ⇒ register_00_value m | Register01 ⇒ register_01_value m | Register02 ⇒ register_02_value m | Register03 ⇒ register_03_value m | Register04 ⇒ register_04_value m | Register05 ⇒ register_05_value m | Register06 ⇒ register_06_value m | Register07 ⇒ register_07_value m | Register10 ⇒ register_10_value m | Register11 ⇒ register_11_value m | Register12 ⇒ register_12_value m | Register13 ⇒ register_13_value m | Register14 ⇒ register_14_value m | Register15 ⇒ register_15_value m | Register16 ⇒ register_16_value m | Register17 ⇒ register_17_value m | Register20 ⇒ register_20_value m | Register21 ⇒ register_21_value m | Register22 ⇒ register_22_value m | Register23 ⇒ register_23_value m | Register24 ⇒ register_24_value m | Register25 ⇒ register_25_value m | Register26 ⇒ register_26_value m | Register27 ⇒ register_27_value m | Register30 ⇒ register_30_value m | Register31 ⇒ register_31_value m | Register32 ⇒ register_32_value m | Register33 ⇒ register_33_value m | Register34 ⇒ register_34_value m | Register35 ⇒ register_35_value m | Register36 ⇒ register_36_value m | Register37 ⇒ register_37_value m | RegisterA ⇒ register_A_value m | RegisterB ⇒ register_B_value m | RegisterDPL ⇒ register_DPL_value m | RegisterDPH ⇒ register_DPH_value m ]. definition update_register_00: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap (Some ? b) old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_01: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value (Some ? b) old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_02: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value (Some ? b) old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_03: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value (Some ? b) old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_04: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value (Some ? b) old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_05: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value (Some ? b) old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_06: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value (Some ? b) old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_07: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value (Some ? b) old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_10: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value (Some ? b) old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_11: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value (Some ? b) old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_12: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value (Some ? b) old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_13: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value (Some ? b) old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_14: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value (Some ? b) old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_15: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value (Some ? b) old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_16: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value (Some ? b) old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_17: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value (Some ? b) old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_20: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value (Some ? b) old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_21: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value (Some ? b) old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_22: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value (Some ? b) old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_23: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value (Some ? b) old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_24: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value (Some ? b) old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_25: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value (Some ? b) old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_26: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value (Some ? b) old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_27: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value (Some ? b) old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_30: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value (Some ? b) old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_31: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value (Some ? b) old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_32: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value (Some ? b) old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_33: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value (Some ? b) old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_34: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value (Some ? b) old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_35: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value (Some ? b) old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_36: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value (Some ? b) old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_37: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value (Some ? b) old_register_A_value old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_A: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value (Some ? b) old_register_B_value old_register_DPL_value old_register_DPH_value. definition update_register_B: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value (Some ? b) old_register_DPL_value old_register_DPH_value. definition update_register_DPL: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value (Some ? b) old_register_DPH_value. definition update_register_DPH: Byte → RegisterMap → RegisterMap ≝ λb: Byte. λm: RegisterMap. let old_register_00_value ≝ register_00_value m in let old_register_01_value ≝ register_01_value m in let old_register_02_value ≝ register_02_value m in let old_register_03_value ≝ register_03_value m in let old_register_04_value ≝ register_04_value m in let old_register_05_value ≝ register_05_value m in let old_register_06_value ≝ register_06_value m in let old_register_07_value ≝ register_07_value m in let old_register_10_value ≝ register_01_value m in let old_register_11_value ≝ register_01_value m in let old_register_12_value ≝ register_02_value m in let old_register_13_value ≝ register_03_value m in let old_register_14_value ≝ register_04_value m in let old_register_15_value ≝ register_05_value m in let old_register_16_value ≝ register_06_value m in let old_register_17_value ≝ register_07_value m in let old_register_20_value ≝ register_01_value m in let old_register_21_value ≝ register_02_value m in let old_register_22_value ≝ register_02_value m in let old_register_23_value ≝ register_03_value m in let old_register_24_value ≝ register_04_value m in let old_register_25_value ≝ register_05_value m in let old_register_26_value ≝ register_06_value m in let old_register_27_value ≝ register_07_value m in let old_register_30_value ≝ register_01_value m in let old_register_31_value ≝ register_02_value m in let old_register_32_value ≝ register_02_value m in let old_register_33_value ≝ register_03_value m in let old_register_34_value ≝ register_04_value m in let old_register_35_value ≝ register_05_value m in let old_register_36_value ≝ register_06_value m in let old_register_37_value ≝ register_07_value m in let old_register_A_value ≝ register_A_value m in let old_register_B_value ≝ register_B_value m in let old_register_DPL_value ≝ register_DPL_value m in let old_register_DPH_value ≝ register_DPH_value m in mk_RegisterMap old_register_00_value old_register_01_value old_register_02_value old_register_03_value old_register_04_value old_register_05_value old_register_06_value old_register_07_value old_register_10_value old_register_11_value old_register_12_value old_register_13_value old_register_14_value old_register_15_value old_register_16_value old_register_17_value old_register_20_value old_register_21_value old_register_22_value old_register_23_value old_register_24_value old_register_25_value old_register_26_value old_register_27_value old_register_30_value old_register_31_value old_register_32_value old_register_33_value old_register_34_value old_register_35_value old_register_36_value old_register_37_value old_register_A_value old_register_B_value old_register_DPL_value (Some ? b). definition update_register_map: Register → Byte → RegisterMap → RegisterMap ≝ λr: Register. λb: Byte. λm: RegisterMap. match r with [ Register00 ⇒ update_register_00 b m | Register01 ⇒ update_register_01 b m | Register02 ⇒ update_register_02 b m | Register03 ⇒ update_register_03 b m | Register04 ⇒ update_register_04 b m | Register05 ⇒ update_register_05 b m | Register06 ⇒ update_register_06 b m | Register07 ⇒ update_register_07 b m | Register10 ⇒ update_register_10 b m | Register11 ⇒ update_register_11 b m | Register12 ⇒ update_register_12 b m | Register13 ⇒ update_register_13 b m | Register14 ⇒ update_register_14 b m | Register15 ⇒ update_register_15 b m | Register16 ⇒ update_register_16 b m | Register17 ⇒ update_register_17 b m | Register20 ⇒ update_register_20 b m | Register21 ⇒ update_register_21 b m | Register22 ⇒ update_register_22 b m | Register23 ⇒ update_register_23 b m | Register24 ⇒ update_register_24 b m | Register25 ⇒ update_register_25 b m | Register26 ⇒ update_register_26 b m | Register27 ⇒ update_register_27 b m | Register30 ⇒ update_register_30 b m | Register31 ⇒ update_register_31 b m | Register32 ⇒ update_register_32 b m | Register33 ⇒ update_register_33 b m | Register34 ⇒ update_register_34 b m | Register35 ⇒ update_register_35 b m | Register36 ⇒ update_register_36 b m | Register37 ⇒ update_register_37 b m | RegisterA ⇒ update_register_A b m | RegisterB ⇒ update_register_B b m | RegisterDPL ⇒ update_register_DPL b m | RegisterDPH ⇒ update_register_DPH b m ]. record Eval: Type[0] ≝ { opaccs: OpAccs → Byte → Byte → option Byte; op1: Op1 → Byte → Byte; op2: Bit → Op2 → Byte → Byte → (Byte × Bit) }. axiom opaccs_implementation: OpAccs → Byte → Byte → option Byte. axiom op1_implementation: Op1 → Byte → Byte. axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit). definition eval: Eval ≝ mk_Eval opaccs_implementation op1_implementation op2_implementation.