X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fturing.ma;h=9b2d8437c32605d0604dbefb8fde2d37368ff72b;hb=1e74e10d6d177c8afe14f20f050812f68aa2b530;hp=7e9c708d0bda3a345b39122a191446a54a0704f5;hpb=3f37ee83ce3c43f34d38729d192e72510f998a53;p=helm.git

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index 7e9c708d0..9b2d8437c 100644
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -32,11 +32,19 @@ qed.
 definition current_chars ≝ λsig.λn.λtapes.
   vec_map ?? (current sig) (S n) tapes.
 
+lemma nth_current_chars : ∀sig,n,tapes,i.
+  nth i ? (current_chars sig n tapes) (None ?) 
+   = current sig (nth i ? tapes (niltape sig)).
+#sig #n #tapes #i >(nth_vec_map … (current sig) i (S n)) %
+qed.
+
 definition tape_move_multi ≝ 
   λsig,n,ts,mvs.
-  pmap_vec ??? (tape_move sig) ? 
-    (pmap_vec ??? (tape_write sig) n ts (vec_map ?? (λx.\fst x) ? mvs))
-        (vec_map ?? (λx.\snd x) ? mvs).
+  pmap_vec ??? (tape_move_mono sig) n ts mvs.
+  
+lemma tape_move_multi_def : ∀sig,n,ts,mvs.
+  tape_move_multi sig n ts mvs = pmap_vec ??? (tape_move_mono sig) n ts mvs.
+// qed.
 
 definition step ≝ λsig.λn.λM:mTM sig n.λc:mconfig sig (states ?? M) n.
   let 〈news,mvs〉 ≝ trans sig n M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in