| HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
(λmem.Some ? (set_mem_desc ? t s mem))
| HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
| HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
(λmem.Some ? (set_mem_desc ? t s mem))
| HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)