X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fload_write.ma;h=a5fae5375e8f52197421f35ffddded2e7e5e6fdf;hb=9e291b4d0a99118cd0a1c5540ef00c25ca37a56d;hp=9ed17612937cc471557f52548be5ecd28b27b49b;hpb=19b6e9b68fa0403461aff44e77a08e0e4eb84840;p=helm.git

diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index 9ed176129..a5fae5375 100644
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/load_write/".
-
-(*include "/media/VIRTUOSO/freescale/model.ma".*)
 include "freescale/model.ma".
 
 (* errori possibili nel fetch *)
@@ -263,10 +260,12 @@ definition filtered_inc_w16 ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
  get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
 
-let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
+definition filtered_plus_w16 := \lambda m:mcu_type.
+let rec filtered_plus_w16  (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
  match n with
   [ O ⇒ w
-  | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
+  | S n' ⇒ filtered_plus_w16 t s (filtered_inc_w16 m t s w) n' ]
+in filtered_plus_w16.
 
 (* 
    errore1: non esiste traduzione ILL_OP
@@ -350,8 +349,8 @@ definition writebit_to ≝
 definition writew_to ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
  opt_map ?? (memory_filter_write m t s addr (w16h writew))
-  (λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
-    (λtmps'.Some ? (pair ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
+  (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
+    (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
 
 (* ausiliari per definire i tipi e la lettura/scrittura *)