New version of freescale:

[helm.git] / helm / software / matita / library / freescale / multivm.ma

diff --git a/helm/software/matita/library/freescale/multivm.ma b/helm/software/matita/library/freescale/multivm.ma
index 2e63c2054a26a598983e7131da91c76ea6733a47..b78efba70dad77b5371bac1bf15e873ccffefe5b 100644 (file)
--- 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.