(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
ndefinition mf_check_update_ranged ≝
λf:word16 → memory_type.λi.λs.λv.
(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
ndefinition mf_check_update_ranged ≝
λf:word16 → memory_type.λi.λs.λv.