X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus.ma;h=9462c455b8a2da7ba87da795f9ddeb6b085ef941;hb=a79bf6edc13daaea8135ca71fdc92e02e229f030;hp=deaf39aad0c1a058ff4bccb91965062122cec051;hpb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
index deaf39aad..9462c455b 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
@@ -93,18 +93,7 @@ nlet rec forall_memory_ranged
                  (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
   ].
 
-ndefinition eq_clk ≝
-λm:mcu_type.λc1,c2:option (aux_clk_type m).
- match c1 with
-  [ None ⇒ match c2 with
-   [ None ⇒ true | Some _ ⇒ false ]
-  | Some c1' ⇒ match c2 with
-   [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
-                               (eq_op m (snd5T … c1') (snd5T … c2')) ⊗
-                               (eq_im m (thd5T … c1') (thd5T … c2')) ⊗
-                               (eq_b8 (fth5T … c1') (fth5T … c2')) ⊗
-                               (eq_w16 (fft5T … c1') (fft5T … c2')) ]
-  ].
+ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_op m) (eq_im m) eq_b8 eq_w16).
 
 (* generalizzazione del confronto fra stati *)
 ndefinition eq_anystatus ≝