(* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
ndefinition mode_DIR2_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (memory_filter_read m t s cur_pc)
(λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
(* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
ndefinition mode_DIR2_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (memory_filter_read m t s cur_pc)
(λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))