mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / status / status_base.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma b/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma
old mode 100755 (executable)
new mode 100644 (file)
index b6d394c..b7e3ea4
--- a/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma
@@ -33,20 +33,20 @@ include "emulator/opcodes/pseudo.ma".
 
 (* descrittore del click = stato di avanzamento dell'esecuzione *)
 (* 1) None = istruzione eseguita, attesa del fetch *)
-(* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *)
-ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
+(* 2) Some cur_clk,clks,pseudo,mode,cur_pc = fetch eseguito *)
+ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T nat nat (aux_pseudo_type m) (aux_im_type m) word16.
 
 nlemma clk_is_comparable : mcu_type → comparable.
  #m; @ (aux_clk_type m)
-  ##[ napply (zeroc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (forallc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (eqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (eqc_to_eq (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (eq_to_eqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (neqc_to_neq (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (neq_to_neqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (decidable_c (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
-  ##| napply (symmetric_eqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable))
+  ##[ napply (zeroc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (forallc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (eqc_to_eq (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (eq_to_eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (neqc_to_neq (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (neq_to_neqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (decidable_c (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
+  ##| napply (symmetric_eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
   ##]
 nqed.