X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword32.ma;h=a5a74faa8803279db711d45b9f6b34763a3c9644;hb=d00e19c7000a00659ffd609ef79675eb0f010659;hp=51bbf1ceddaec04e367ca29d99217afdafaf5991;hpb=417792b30223b5edd4a9194193c7f34514bd0fa3;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index 51bbf1ced..a5a74faa8 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -42,20 +42,27 @@ ndefinition eq_w32 ≝ λdw1,dw2.(eq_w16 (w32h dw1) (w32h dw2)) ⊗ (eq_w16 (w32
 
 (* operatore < *)
 ndefinition lt_w32 ≝
-λdw1,dw2:word32.match lt_w16 (w32h dw1) (w32h dw2) with
- [ true ⇒ true
- | false ⇒ match gt_w16 (w32h dw1) (w32h dw2) with
-  [ true ⇒ false
-  | false ⇒ lt_w16 (w32l dw1) (w32l dw2) ]].
+λdw1,dw2:word32.
+ (lt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (lt_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore ≤ *)
-ndefinition le_w32 ≝ λdw1,dw2:word32.(eq_w32 dw1 dw2) ⊕ (lt_w32 dw1 dw2).
+ndefinition le_w32 ≝
+λdw1,dw2:word32.
+ (lt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (le_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore > *)
-ndefinition gt_w32 ≝ λdw1,dw2:word32.⊖ (le_w32 dw1 dw2).
+ndefinition gt_w32 ≝
+λdw1,dw2:word32.
+ (gt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (gt_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore ≥ *)
-ndefinition ge_w32 ≝ λdw1,dw2:word32.⊖ (lt_w32 dw1 dw2).
+ndefinition ge_w32 ≝
+λdw1,dw2:word32.
+ (gt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (ge_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore and *)
 ndefinition and_w32 ≝
@@ -228,7 +235,7 @@ ndefinition div_w16 ≝
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w32 ≝
-λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup).
+λx,inf,sup:word32.(le_w32 inf x) ⊗ (le_w32 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w32 ≝