X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fmultivm.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fmultivm.ma;h=b78efba70dad77b5371bac1bf15e873ccffefe5b;hb=7845d9d0221d94418beecf3d7c3aed3efb2af7fc;hp=2e63c2054a26a598983e7131da91c76ea6733a47;hpb=25be562c5436746df8d892449a9ff98755c37e9f;p=helm.git

diff --git a/helm/software/matita/library/freescale/multivm.ma b/helm/software/matita/library/freescale/multivm.ma
index 2e63c2054..b78efba70 100644
--- a/helm/software/matita/library/freescale/multivm.ma
+++ b/helm/software/matita/library/freescale/multivm.ma
@@ -944,7 +944,7 @@ definition execute_SBC ≝
  execute_SBC_SUB_aux m t s i cur_pc true
  (λA_op.λM_op.λC_op.match plus_b8 A_op (compl_b8 M_op) false with
   [ pair resb resc ⇒ match C_op with
-   [ true ⇒ plus_b8 resb 〈xF,xF〉 resc
+   [ true ⇒ plus_b8 resb 〈xF,xF〉 false
    | false ⇒ pair ?? resb resc ]]).
 
 (* C = 1 *)
@@ -1304,14 +1304,12 @@ definition tick ≝
 (* ESECUZIONE *)
 (* ********** *)
 
-definition execute := \lambda m:mcu_type.
-let rec execute  (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
+let rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
  match s with
   [ TickERR s' error ⇒ TickERR ? s' error
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
-  | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute t (tick m t s') n' ]
-  ]
-in execute.
+  | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
+  ].
 
 lemma breakpoint:
  ∀m,u,s,n1,n2. execute m u s (n1 + n2) = execute m u (execute m u s n1) n2.