+
+(* ************************************** *)
+(* raccordo di tutte le possibili letture *)
+(* ************************************** *)
+
+(* addr+=2 *)
+ndefinition aux_inc_addr2 ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))).
+
+ndefinition IP2022_multi_mode_load_auxb ≝
+λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* NO: solo word *)
+ | MODE_INHADDR ⇒ None ?
+(* NO: solo word *)
+ | MODE_INHADDRpp ⇒ None ?
+
+(* IMM3 *)
+ | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc)
+(* IMM8 *)
+ | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s)
+ (λb.Some ? (triple … s b cur_pc))
+(* NO: solo lettura word *)
+ | MODE_IMM13 _ ⇒ None ?
+
+(* NO: solo word *)
+ | MODE_FR0_and_W ⇒ None ?
+(* NO: solo word *)
+ | MODE_FR1_and_W ⇒ None ?
+(* NO: solo word *)
+ | MODE_W_and_FR0 ⇒ None ?
+(* NO: solo word *)
+ | MODE_W_and_FR1 ⇒ None ?
+
+(* [FRn] *)
+ | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s o)
+ (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
+(* [FRn] *)
+ | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s o)
+ (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
+ ].
+
+ndefinition IP2022_multi_mode_load_auxw ≝
+λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* [ADDR] *)
+ | MODE_INHADDR ⇒ opt_map … (mode_ADDR_load t s)
+ (λw.Some ? (triple … s w cur_pc))
+(* [ADDR], ADDR+=2 *)
+ | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_load t s)
+ (λw.Some ? (triple … (aux_inc_addr2 t s) w cur_pc))
+
+(* NO: solo lettura byte *)
+ | MODE_IMM3 _ ⇒ None ?
+(* NO: solo lettura byte *)
+ | MODE_IMM8 ⇒ None ?
+(* IMM13 *)
+ | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s)
+ (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc))
+
+(* FR, W → FR *)
+ | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s)
+ (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
+(* FR, W → FR *)
+ | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s)
+ (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
+(* W, FR → W *)
+ | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s)
+ (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
+(* W, FR → W *)
+ | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s)
+ (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
+
+(* NO: solo byte *)
+ | MODE_FR0n _ ⇒ None ?
+(* NO: solo byte *)
+ | MODE_FR1n _ ⇒ None ?
+ ].
+
+(* **************************************** *)
+(* raccordo di tutte le possibili scritture *)
+(* **************************************** *)
+
+ndefinition IP2022_multi_mode_write_auxb ≝
+λt.λs:any_status IP2022 t.λcur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* NO: solo word *)
+ | MODE_INHADDR ⇒ None ?
+(* NO: solo word *)
+ | MODE_INHADDRpp ⇒ None ?
+
+(* NO: solo lettura byte *)
+ | MODE_IMM3 _ ⇒ None ?
+(* NO: solo lettura byte *)
+ | MODE_IMM8 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM13 _ ⇒ None ?
+
+(* FR, W → FR *)
+ | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s flag writeb)
+ (λs'.Some ? (pair … s' cur_pc))
+(* FR, W → FR *)
+ | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s flag writeb)
+ (λs'.Some ? (pair … s' cur_pc))
+(* W, FR → W *)
+ | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
+(* W, FR → W *)
+ | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
+
+(* [FRn] *)
+ | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
+ (λs'.Some ? (pair … s' cur_pc))
+(* [FRn] *)
+ | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
+ (λs'.Some ? (pair … s' cur_pc))
+ ].
+
+ndefinition IP2022_multi_mode_write_auxw ≝
+λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* [ADDR] *)
+ | MODE_INHADDR ⇒ opt_map … (mode_ADDR_write t s writew)
+ (λs'.Some ? (pair … s' cur_pc))
+(* [ADDR], ADDR+=2 *)
+ | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_write t s writew)
+ (λs'.Some ? (pair … (aux_inc_addr2 t s') cur_pc))
+
+(* NO: solo lettura byte *)
+ | MODE_IMM3 _ ⇒ None ?
+(* NO: solo lettura byte *)
+ | MODE_IMM8 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM13 _ ⇒ None ?
+
+(* NO: solo byte *)
+ | MODE_FR0_and_W ⇒ None ?
+(* NO: solo byte *)
+ | MODE_FR1_and_W ⇒ None ?
+(* NO: solo byte *)
+ | MODE_W_and_FR0 ⇒ None ?
+(* NO: solo byte *)
+ | MODE_W_and_FR1 ⇒ None ?
+
+(* NO: solo byte *)
+ | MODE_FR0n _ ⇒ None ?
+(* NO: solo byte *)
+ | MODE_FR1n _ ⇒ None ?
+ ].