X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmultivm.ma;h=44dacea60f6f3cfb90d03faa3098019d71f2114e;hb=dc7e826399162e2fde3ddf1f02d5530d6cd11205;hp=40c8c11c760448946082998212e493f8ca21b3ad;hpb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
index 40c8c11c7..44dacea60 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
@@ -15,13 +15,12 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 include "freescale/load_write.ma".
-include "freescale/nat_lemmas.ma".
 
 (* ************************************************ *)
 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
@@ -1306,36 +1305,3 @@ nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
   | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
   ].
-
-nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
- #m; #t; #s; #err; #n;
- ncases n;
- ##[ ##2: #n1 ##]
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
- #m; #t; #s; #susp; #n;
- ncases n;
- ##[ ##2: #n1 ##]
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma breakpoint :
- ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
- #m; #t; #n1;
- nelim n1;
- ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply refl_eq
- ##| ##2: #n3; #H; #n2; #s; ncases s;
-          ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply refl_eq
-          ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply refl_eq
-          ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
-                   nchange with ((execute m t (tick m t x) (n3+n2)) =
-                                 (execute m t (execute m t (tick m t x) n3) n2));
-                   nrewrite > (H n2 (tick m t x));
-                   napply refl_eq
-          ##]
- ##]
-nqed.