(* operatore Most Significant Bit *)
ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
+ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
(* operatore Least Significant Bit *)
ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
+ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
(* operatore rotazione destra con carry *)
ndefinition rcr_w24 ≝
[ true ⇒ succ_w24 (not_w24 w)
| false ⇒ not_w24 (pred_w24 w) ].
+(* operatore abs *)
+ndefinition abs_w24 ≝
+λw:word24.match getMSB_w24 w with
+ [ true ⇒ compl_w24 w | false ⇒ w ].
+
(* operatore x in [inf,sup] o in sup],[inf *)
ndefinition inrange_w24 ≝
λx,inf,sup:word24.