freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / status.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index 532b996ff3cb6772886ba09f06d89f3263980c71..1354861e2a9858f0ef90c99e85917b6b1b04117b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
@@ -1164,7 +1164,7 @@ ndefinition setweak_irq_flag ≝
 (* ***************** *)
 
 (* confronto registro per registro dell'HC05 *)
-ndefinition eq_alu_HC05 ≝
+ndefinition eq_aluHC05 ≝
 λalu1,alu2:alu_HC05.
  match alu1 with
   [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
@@ -1185,7 +1185,7 @@ ndefinition eq_alu_HC05 ≝
    (eq_bool irqfl1 irqfl2) ]].
 
 (* confronto registro per registro dell'HC08 *)
-ndefinition eq_alu_HC08 ≝
+ndefinition eq_aluHC08 ≝
 λalu1,alu2:alu_HC08.
  match alu1 with
   [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
@@ -1205,7 +1205,7 @@ ndefinition eq_alu_HC08 ≝
    (eq_bool irqfl1 irqfl2) ]].
 
 (* confronto registro per registro dell'RS08 *)
-ndefinition eq_alu_RS08 ≝
+ndefinition eq_aluRS08 ≝
 λalu1,alu2:alu_RS08.
  match alu1 with
   [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
@@ -1252,7 +1252,7 @@ ndefinition eq_clk ≝
   ].
 
 (* generalizzazione del confronto fra stati *)
-ndefinition eq_status ≝
+ndefinition eq_anystatus ≝
 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
  match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
  match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
@@ -1264,7 +1264,7 @@ ndefinition eq_status ≝
    match m with
     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
    bool with
-  [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
+  [ HC05 ⇒ eq_aluHC05 | HC08 ⇒ eq_aluHC08 | HCS08 ⇒ eq_aluHC08 | RS08 ⇒ eq_aluRS08 ]
  alu1 alu2) ⊗
 
  (* 2) confronto della memoria in [inf,inf+n] *)