(* *)
(* ********************************************************************** *)
-include "emulator/read_write/load_write_base.ma".
include "emulator/status/status_getter.ma".
+include "emulator/read_write/load_write_base.ma".
(* lettura da [curpc]: IMM1 *)
ndefinition mode_IMM1_load ≝
(* **************************************** *)
ndefinition Freescale_multi_mode_write_auxb ≝
-λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwriteb:byte8.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* scrive A *)