(* operatore < *)
ndefinition lt_w16 ≝
-λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with
- [ true ⇒ true
- | false ⇒ match gt_b8 (w16h w1) (w16h w2) with
- [ true ⇒ false
- | false ⇒ lt_b8 (w16l w1) (w16l w2) ]].
+λw1,w2:word16.
+ (lt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (lt_b8 (w16l w1) (w16l w2))).
(* operatore ≤ *)
-ndefinition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2).
+ndefinition le_w16 ≝
+λw1,w2:word16.
+ (lt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (le_b8 (w16l w1) (w16l w2))).
(* operatore > *)
-ndefinition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2).
+ndefinition gt_w16 ≝
+λw1,w2:word16.
+ (gt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (gt_b8 (w16l w1) (w16l w2))).
(* operatore ≥ *)
-ndefinition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2).
+ndefinition ge_w16 ≝
+λw1,w2:word16.
+ (gt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (ge_b8 (w16l w1) (w16l w2))).
(* operatore and *)
ndefinition and_w16 ≝
(* operatore x in [inf,sup] *)
ndefinition inrange_w16 ≝
-λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
+λx,inf,sup:word16.(le_w16 inf x) ⊗ (le_w16 x sup).
(* iteratore sulle word *)
ndefinition forall_w16 ≝