From 723514507b1e2e58c0a8c7bcc39c5d1301b910bc Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 14 Jan 2013 10:36:34 +0000
Subject: [PATCH] nth_current_chars

---
 matita/matita/lib/turing/turing.ma | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index 4cf3ebaf1..9b2d8437c 100644
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -31,7 +31,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.
-- 
2.39.2