X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fturing.ma;h=dc0a43e755968a27ea32aaea3deb2fa84548a03d;hb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;hp=4cf3ebaf17a99ed3fe6e0d0333e1db2456794bbe;hpb=b31ab31a99065295b91003a0df95dec817cee5de;p=helm.git

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index 4cf3ebaf1..dc0a43e75 100644
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -1,3 +1,4 @@
+include "basics/core_notation/fintersects_2.ma".
 include "turing/mono.ma".
 include "basics/vectors.ma".
 
@@ -31,7 +32,13 @@ 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_mono sig) n ts mvs.