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