[ 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.