almost there

[helm.git] / matita / matita / lib / turing / multi_to_mono / trace_alphabet.ma

diff --git a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
index 86db474004cabf4888ba8fd262036b1ea20147d8..bb1e54e638d7df7fa9a9098af50927963c1b2efa 100644 (file)
--- a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
+++ b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
@@ -57,6 +57,12 @@ definition trace ≝ λsig,n,i,l.
 lemma trace_def : ∀sig,n,i,l. 
   trace sig n i l = map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
 // qed.
+
+lemma hd_trace:  ∀sig,n,i,l. 
+  hd ? (trace sig n i l) (blank ?) = 
+    nth i ? (hd ? l (all_blank … )) (blank ?).
+#sig #n #i #l elim l // normalize >blank_all_blank % 
+qed.
  
 lemma tail_trace:  ∀sig,n,i,l. 
   tail ? (trace sig n i l) = trace sig n i (tail ? l).
@@ -95,6 +101,7 @@ qed.
 definition no_head_in ≝ λsig,n,l. 
   ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
 
+
 (* some lemmas over lists, to be moved *)
 lemma injective_append_l: ∀A,l. injective ?? (append A l).
 #A #l elim l 
@@ -212,6 +219,12 @@ let rec to_blank sig l on l ≝
   | cons a tl ⇒ 
       if a == blank sig then [ ] else a::(to_blank sig tl)]. 
       
+let rec after_blank sig l on l ≝
+  match l with
+  [ nil ⇒  [ ]
+  | cons a tl ⇒ 
+      if a == blank sig then (a::tl) else (after_blank sig tl)]. 
+      
 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
 
 lemma to_blank_i_def : ∀sig,n,i,l.