(λs_tmp.Some ? s_tmp)).
ndefinition Freescale_multi_mode_load_auxb ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* restituisce A *)
].
ndefinition Freescale_multi_mode_load_auxw ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* NO: solo lettura/scrittura byte *)
(* **************************************** *)
ndefinition Freescale_multi_mode_write_auxb ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λflag:aux_mod_type.λ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 *)
].
ndefinition Freescale_multi_mode_write_auxw ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* NO: solo lettura/scrittura byte *)