From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 24 Oct 2013 06:48:13 +0000 (+0000)
Subject: many changes
X-Git-Tag: make_still_working~1072
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8712a9a43384e0f437e8ea97fd66c8ea4da7bcfe;p=helm.git

many changes
---

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 1e5fa3d2e..c1559702a 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -41,6 +41,26 @@ lemma sem_write_strong : ∀alpha,c.Realize ? (write alpha c) (R_write_strong al
   [|% [% |cases t normalize // ] ]
 qed. 
 
+(***************************** replace a with f a *****************************)
+
+definition writef ≝ λalpha,f.
+  mk_TM alpha write_states
+  (λp.let 〈q,a〉 ≝ p in
+    match pi1 … q with 
+    [ O ⇒ 〈wr1,Some ? (f a),N〉
+    | S _ ⇒ 〈wr1,None ?,N〉 ])
+  wr0 (λx.x == wr1).
+
+definition R_writef ≝ λalpha,f,t1,t2.
+  ∀c. current ? t1 = c  →
+  t2 = midtape alpha (left ? t1) (f c) (right ? t1).
+  
+lemma sem_writef : ∀alpha,f.
+  writef alpha f  ⊨ R_writef alpha f.
+#alpha #f #t @(ex_intro … 2) @ex_intro
+  [|% [% |cases t normalize // ] ]
+qed. 
+
 (******************** moves the head one step to the right ********************)
 
 definition move_states ≝ initN 2.
diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index e670c2635..393fa2af9 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -79,7 +79,53 @@ qed.
 
 inductive move : Type[0] ≝
   | L : move | R : move | N : move.
+  
+(*************************** turning moves into a DeqSet **********************)
+
+definition move_eq ≝ λm1,m2:move.
+  match m1 with
+  [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
+  |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
+  |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
+
+lemma move_eq_true:∀m1,m2.
+  move_eq m1 m2 = true ↔ m1 = m2.
+*
+  [* normalize [% #_ % |2,3: % #H destruct ]
+  |* normalize [1,3: % #H destruct |% #_ % ]
+  |* normalize [1,2: % #H destruct |% #_ % ]
+qed.
+
+definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
+
+unification hint 0 ≔ ;
+    X ≟ DeqMove
+(* ---------------------------------------- *) ⊢ 
+    move ≡ carr X.
+
+unification hint  0 ≔ m1,m2; 
+    X ≟ DeqMove
+(* ---------------------------------------- *) ⊢ 
+    move_eq m1 m2 ≡ eqb X m1 m2.
+
+
+(************************ turning DeqMove into a FinSet ***********************)
+
+definition move_enum ≝ [L;R;N].
+
+lemma move_enum_unique: uniqueb ? [L;R;N] = true.
+// qed.
+
+lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
+* // qed.
+
+definition FinMove ≝ 
+  mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
 
+unification hint  0 ≔ ; 
+    X ≟ FinMove
+(* ---------------------------------------- *) ⊢ 
+    move ≡ FinSetcarr X.
 (********************************** machine ***********************************)
 
 record TM (sig:FinSet): Type[1] ≝ 
diff --git a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
index 496b84c5f..dae4aa6af 100644
--- a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
+++ b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
@@ -3,18 +3,81 @@
 include "turing/multi_to_mono/exec_trace_move.ma".
 (* include "turing/turing.ma". *)
 
-let rec exec_moves sig n i on i : TM (multi_sig sig n) ≝
+(**************************** Vector Operations *******************************)
+
+let rec resize A (l:list A) i d on i ≝
+  match i with 
+  [ O ⇒ [ ]
+  | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
+  ].
+
+lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
+#A #l #i lapply l -l elim i 
+  [#l #d % 
+  |#m #Hind #l cases l 
+    [#d normalize @eq_f @Hind
+    |#a #tl #d normalize @eq_f @Hind
+    ]
+  ]
+qed.
+
+lemma resize_id : ∀A,n,l,d. |l| = n → 
+  resize A l n d = l.
+#A #n elim n 
+  [#l #d #H >(lenght_to_nil … H) //
+  |#m #Hind * #d normalize 
+    [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
+  ]
+qed.
+
+definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
+#A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
+qed.
+
+axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
+  nth i ? (resize_vec A n v j d) d = nth i ? v d.
+  
+lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d. 
+  resize_vec A n v n d = v.
+#A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
+qed.
+
+definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
+  mk_Vector A 1 [a] (refl ??).
+  
+definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
+#A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
+>length_append >(len A n v) //
+qed.
+
+lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
+  a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
+// qed.
+
+axiom nth_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. 
+  nth n ? (vec_cons_right A a n v) d = a.
+(*
+#A #a #n elim n 
+  [#v #d >(vector_nil … v) //
+  |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);    
+   whd in match (vec_cons_right ????);  
+*)
+
+lemma get_moves_cons_right: ∀Q,sig,n,q,moves,a.
+  get_moves Q sig (S n)
+    (vec_cons_right ? (Some ? (inl ?? 〈q,moves〉)) (S n) a) = moves.
+#Q #sig #n #q #moves #a whd in ⊢(??%?); >nth_cons_right //
+qed.
+    
+axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. 
+  resize_vec ? (S n) (vec_cons_right A a n v) n d = v.
+  
+let rec exec_moves Q sig n i on i : TM (MTA (HC Q n) sig (S n)) ≝
   match i with 
   [ O ⇒ nop ? (* exec_move_i sig n 0 *)
-  | S j ⇒ seq ? (exec_moves sig n j) (exec_move_i sig n j) 
+  | S j ⇒ seq ? (exec_moves Q sig n j) (exec_move_i Q sig n j) 
   ].
-     
-axiom get_moves : ∀sig,n.∀a:multi_sig sig n.∀i.Vector DeqMove i.
 
-axiom get_moves_cons: ∀sig,n,a,j.j < n → 
- get_moves sig n a (S j) = 
- vec_cons ? (get_move ? n a j) j (get_moves sig n a j).
- 
 definition a_moves ≝ 
   λsig,n.λactions: Vector ((option sig) × move) n. 
   vec_map ?? (snd ??) n actions.
@@ -35,6 +98,20 @@ definition tape_writem ≝
   λsig,n,ts,chars.
   pmap_vec ??? (tape_write sig) n ts chars.
 
+(*
+let rec i_moves a i on i : Vector move i ≝
+  match i with 
+  [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
+  | S j ⇒ vec_cons ? (nth j ? a N) j (i_moves a j)
+  ]. *)
+
+definition vec_moves ≝ λQ,sig,n,a,i. 
+  resize_vec … (get_moves Q sig n a) i N.
+
+axiom vec_moves_cons: ∀Q,sig,n,a,j.j < n → 
+ vec_moves Q sig n a (S j) = 
+ vec_cons ? (get_move Q ? n a j) j (vec_moves Q sig n a j).
+
 (*
 axiom actions_commute : ∀sig,n,ts,actions.
   tape_moves sig n (tape_writem ?? ts (a_chars … actions)) (a_moves … actions) = 
@@ -43,21 +120,22 @@ axiom actions_commute : ∀sig,n,ts,actions.
 (* devo rafforzare la semantica, dicendo che i tape non toccati
 dalle moves non cambiano *)
 
-definition R_exec_moves ≝ λsig,n,i,t1,t2.
+
+definition R_exec_moves ≝ λQ,sig,n,i,t1,t2.
 ∀a,ls,rs. 
   t1 = midtape ? ls a rs → 
-  (∀i.regular_trace sig n a ls rs i) → 
-  nth n ? (vec … a) (blank ?) = head ? → 
+  (∀i.regular_trace (TA (HC Q n) sig) (S n) a ls rs i) → 
+  is_head ?? (nth n ? (vec … a) (blank ?)) = true →  
   no_head_in … ls →
   no_head_in … rs →
   ∃ls1,a1,rs1. 
-   t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
-   (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
-   readback sig n ls1 (vec … a1) rs1 i = 
-     tape_moves ?? (readback sig n ls (vec … a) rs i) (get_moves sig n a i) ∧
+   t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
+   (∀i.regular_trace (TA (HC Q n) sig) (S n) a1 ls1 rs1 i) ∧
+   readback ? (S n) ls1 (vec … a1) rs1 i = 
+     tape_moves ?? (readback ? (S n) ls (vec … a) rs i) (vec_moves Q sig n a i) ∧
    (∀j. i ≤ j → j ≤ n →  
-    rb_trace_i sig n ls1 (vec … a1) rs1 j = 
-      rb_trace_i sig n ls (vec … a) rs j).
+    rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = 
+      rb_trace_i ? (S n) ls (vec … a) rs j).
      
 (* alias id "Realize_to_Realize" = 
   "cic:/matita/turing/mono/Realize_to_Realize.def(13)". *)
@@ -74,30 +152,30 @@ lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j →
   ]
 qed.
 
-lemma sem_exec_moves: ∀sig,n,i. i < n → 
-  exec_moves sig n i ⊨ R_exec_moves sig n i.
-#sig #n #i elim i 
+lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n → 
+  exec_moves Q sig n i ⊨ R_exec_moves Q sig n i.
+#Q #sig #n #i elim i 
   [#_ @(Realize_to_Realize … (sem_nop …))
    #t1 #t2 #H #a #ls #rs #Ht1 #Hreg #H1 #H2 #H3 
    %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| %]|//]
   |#j #Hind #lttj lapply (lt_to_le … lttj) #ltj
-   @(sem_seq_app … (Hind ltj) (sem_exec_move_i … ltj)) -Hind
+   @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind
    #int #outt * #t1 * #H1 #H2
    #a #ls #rs #Hint #H3 #H4 #H5 #H6
    lapply (H1 … Hint H3 H4 H5 H6)
    * #ls1 * #a1 * #rs1 * * * #H7 #H8 #H9 #H10
    lapply (reg_inv … (H8 n) ? H4 H5 H6)
-    [@H10 [@lt_to_le @ltj |@le_n]]
+    [@H10 [@ltj |@le_n]]
    -H3 -H4 -H5 -H6 * * #H3 #H4 #H5
    lapply (H2 … H7 H8 H3 H4 H5)
    * #ls2 * #a2 * #rs2 * * * #Houtt #Hregout #Hrboutt #Hrbid
    %{ls2} %{a2} %{rs2} 
-   cut (∀i. get_move sig n a i = get_move sig n a1 i)
+   cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i)
      [@daemon] #aa1
    %[%[%[@Houtt|@Hregout]
-      |whd in ⊢ (??%?); @Vector_eq >(get_moves_cons … ltj)
+      |whd in ⊢ (??%?); @Vector_eq >(vec_moves_cons … lttj)
        >tape_moves_def >pmap_vec_cons @eq_f2
-        [<H10 [>aa1 @Hrboutt |@lt_to_le @ltj |@le_n]
+        [<H10 [>aa1 @Hrboutt |@ltj |@le_n]
         |<tape_moves_def <H9 (* mitico *) @eq_f 
          @(eq_vec … (niltape ?)) #i #ltij 
          >(nth_readback … ltij) >(nth_readback … ltij) @Hrbid 
diff --git a/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma b/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma
index dc75bc627..0fdfa86b8 100644
--- a/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma
+++ b/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma
@@ -1,7 +1,6 @@
 (* include "turing/auxiliary_machines.ma". *)
 
 include "turing/multi_to_mono/shift_trace.ma".
-include "turing/multi_universal/normalTM.ma". (* for DeqMove *)
 
 (******************************************************************************)
 
@@ -65,18 +64,18 @@ lemma sem_mtestR: ∀sig,test.
 qed.
 
 definition guarded_M ≝ λsig,n,i,M.
-  (ifTM ? (test_char ? (no_blank sig n i))
+  (ifTM ? (test_char ? (not_blank sig n i))
    M
-   (ifTM ? (mtestR ? (no_blank sig n i))
+   (ifTM ? (mtestR ? (not_blank sig n i))
     M
     (nop ?) (mtestR_acc …)) tc_true).
     
 definition R_guarded_M ≝ λsig,n,i,RM,t1,t2. 
   ∀ls,a,rs. t1 = midtape ? ls a rs → 
-   (no_blank sig n i a = false → 
-     no_blank sig n i (hd ? rs (all_blank …)) = false → t1=t2) ∧
-   (no_blank sig n i a = true ∨
-     no_blank sig n i (hd ? rs (all_blank …)) = true → RM t1 t2).
+   (not_blank sig n i a = false → 
+     not_blank sig n i (hd ? rs (all_blanks …)) = false → t1=t2) ∧
+   (not_blank sig n i a = true ∨
+     not_blank sig n i (hd ? rs (all_blanks …)) = true → RM t1 t2).
 
 lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
    guarded_M sig n i M ⊨ R_guarded_M sig n i RM.
@@ -98,7 +97,7 @@ lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
       [#Ht1 * #t2 * * #_ #Ht2 lapply (Ht2 … Ht1) -Ht2 #Ht2
        whd in ⊢ (%→?); #Htout % [//] * 
         [>Ha [#H destruct (H)| >Ht1 %] 
-        |whd in ⊢ (??%?→?); >blank_all_blank whd in ⊢ (??%?→?);
+        |whd in ⊢ (??%?→?); >blank_all_blanks whd in ⊢ (??%?→?);
          #H destruct (H)
         ]
       |#c #rs1 #Ht1 * #t2 * * #Ht2 #_ lapply (Ht2 … Ht1) -Ht2 * 
@@ -112,9 +111,11 @@ lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
   ]
 qed.
 
-definition move_R_i ≝ λsig,n,i. guarded_M sig n i (mtiL sig n i).
+definition move_R_i ≝ λA,sig,n,i. 
+  guarded_M ? (S n) i (mtiL A sig n i).
 
-definition Rmove_R_i ≝ λsig,n,i. R_guarded_M sig n i (Rmtil sig n i).
+definition Rmove_R_i ≝ λA,sig,n,i. 
+  R_guarded_M ? (S n) i (Rmtil A sig n i).
 
 
 (*************************** readback of the tape *****************************)
@@ -149,63 +150,63 @@ lemma orb_false_l: ∀b1,b2:bool.
 * * normalize /2/ qed.
 
 lemma no_blank_true_to_not_blank: ∀sig,n,a,i. 
-  (no_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
+  (not_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
 #sig #n #a #i #H @(not_to_not … (eqnot_to_noteq … false H))
 -H #H normalize >H % 
 qed.
 
-lemma rb_move_R : ∀sig,n,ls,a,rs,outt,i.
-  (∀i.regular_trace sig n a ls rs i) → 
-  nth n ? (vec … a) (blank ?) = head ? → 
+lemma rb_move_R : ∀A,sig,n,ls,a,rs,outt,i.
+  (∀i.regular_trace (TA A sig) (S n) a ls rs i) → 
+  is_head ?? (nth n ? (vec … a) (blank ?)) = true → 
   no_head_in … ls →
   no_head_in … rs →
   Rmove_R_i … i (midtape ? ls a rs) outt → 
   ∃ls1,a1,rs1. 
    outt = midtape ? ls1 a1 rs1 ∧
-   (∀i.regular_trace sig n a1 ls1 rs1 i) ∧ 
-   rb_trace_i sig n ls1 (vec … a1) rs1 i = 
-     tape_move ? (rb_trace_i sig n ls (vec … a) rs i) R ∧
-   ∀j. j ≤n → j ≠ i → 
-    rb_trace_i sig n ls1 (vec … a1) rs1 j = 
-      rb_trace_i sig n ls (vec … a) rs j.
-#sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
+   (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧ 
+   rb_trace_i ? (S n) ls1 (vec … a1) rs1 i = 
+     tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
+   ∀j. j ≤ n → j ≠ i → 
+    rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = 
+      rb_trace_i ? (S n) ls (vec … a) rs j.
+#A #sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
 lapply (Hmove … (refl …)) -Hmove * #HMove1 #HMove2
-cases (true_or_false (no_blank sig n i a ∨ 
-        no_blank sig n i (hd (multi_sig sig n) rs (all_blank sig n))))
+cases (true_or_false (not_blank ? (S n) i a ∨ 
+        not_blank ? (S n) i (hd ? rs (all_blanks ? (S n)))))
   [2: #Hcase cases (orb_false_l … Hcase) -Hcase #Hb1 #Hb2 
    lapply (HMove1 … Hb1 Hb2) #Hout %{ls} %{a} %{rs}
    %[%[%[@sym_eq @Hout |@Hreg]
       |>rb_trace_i_def
-       cut (nth i ? (vec … a) (blank ?) = blank sig)
+       cut (nth i ? (vec … a) (blank ?) = blank ?)
         [@(\P ?) @injective_notb @Hb1] #Ha >Ha
        >rb_trace_def whd in match (opt_cur ??);
-       cut (to_blank sig (trace sig n i rs) = [])
+       cut (to_blank ? (trace ? (S n) i rs) = [])
         [@daemon] #Hrs >Hrs 
-       cases (to_blank sig (trace sig n i ls)) // 
+       cases (to_blank ? (trace ? (S n) i ls)) // 
       ]
     |//]
   |-HMove1 #Hb 
    lapply(HMove2 (orb_true_l … Hb) … (refl …) Hha Hreg ? Hhls Hhrs) -HMove2 
-    [#Hb1 lapply Hb -Hb  whd in match (no_blank sig n i a);
+    [#Hb1 lapply Hb -Hb  whd in match (not_blank ? (S n) i a);
      >Hb1 #H @no_blank_true_to_not_blank @H] 
    * #ls1 * #a1 * #rs1 * * * * * #H1 #H2 #H3 #H4 #H5 #H6
    %{ls1} %{a1} %{rs1} 
    %[%[%[@H1|@H2]
       |(* either a is blank or not *)
-       cases (true_or_false (no_blank sig n i a)) #Hba
+       cases (true_or_false (not_blank ? (S n) i a)) #Hba
         [(* a not blank *) 
          >rb_trace_i_def >rb_trace_def <to_blank_i_def >H5 >to_blank_cons_nb
           [2: @no_blank_true_to_not_blank //]        
          lapply H6 -H6 #Hrs >(rb_trace_i_def … rs i) >rb_trace_def 
          <(to_blank_i_def … rs) <Hrs
-         cut (opt_cur sig (nth i ? (vec … a) (blank sig)) =
-              Some ? (nth i ? (vec … a) (blank sig))) [@daemon] #Ha >Ha
+         cut (opt_cur ? (nth i ? (vec … a) (blank ?)) =
+              Some ? (nth i ? (vec … a) (blank ?))) [@daemon] #Ha >Ha
          (* either a1 is blank or not *)
-         cases (true_or_false (no_blank sig n i a1)) #Hba1
-          [cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) =
-                Some ? (nth i ? (vec … a1) (blank sig))) [@daemon] #Ha1 >Ha1
+         cases (true_or_false (not_blank ? (S n) i a1)) #Hba1
+          [cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
+                Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] #Ha1 >Ha1
            >to_blank_cons_nb [%|@(\Pf ?) @injective_notb @Hba1]
-          |cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) = None ?) [@daemon] 
+          |cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) = None ?) [@daemon] 
            #Ha1 >Ha1 
            cut (to_blank_i … i (a1::rs1) = [ ]) [@daemon] #Ha1rs1 >Ha1rs1
            cut (to_blank_i … i rs1 = [ ]) [@daemon] #Hrs1 <to_blank_i_def >Hrs1 %
@@ -214,43 +215,43 @@ cases (true_or_false (no_blank sig n i a ∨
          >rb_trace_i_def >rb_trace_def <(to_blank_i_def … rs) <H6 >H5
          cut (to_blank_i … i (a::ls) = [ ]) [@daemon] #Hals >Hals
          cut (to_blank_i … i ls = [ ]) [@daemon] #Hls <(to_blank_i_def … ls) >Hls
-         cut (opt_cur sig (nth i ? (vec … a) (blank sig)) = None ?) [@daemon] #Ha >Ha
+         cut (opt_cur ? (nth i ? (vec … a) (blank ?)) = None ?) [@daemon] #Ha >Ha
          cut (nth i ? (vec … a1) (blank ?) ≠ blank ?) [@daemon] #Ha1 
          >(to_blank_cons_nb … Ha1)
-         cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) =
-              Some ? (nth i ? (vec … a1) (blank sig))) [@daemon] -Ha1 #Ha1 >Ha1 %
+         cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
+              Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] -Ha1 #Ha1 >Ha1 %
         ]
       ]
     |(* case j ≠ i *)
      #j #Hle #Hneq >rb_trace_i_def >rb_trace_i_def >rb_trace_def >rb_trace_def 
      <(to_blank_i_def … rs) <(to_blank_i_def … rs1) >(H4 j Hle Hneq)
-     cut ((to_blank_i sig n j ls1 = to_blank_i sig n j ls) ∧ 
-          (opt_cur sig (nth j (sig_ext sig) (vec … a1) (blank sig)) =  
-           opt_cur sig (nth j (sig_ext sig) (vec … a) (blank sig))))
-      [@daemon] * #H7 #H8 >H7 >H8 //
+     cut ((to_blank_i ? (S n) j ls1 = to_blank_i ? (S n) j ls) ∧ 
+          (opt_cur ? (nth j ? (vec … a1) (blank ?)) =  
+           opt_cur ? (nth j ? (vec … a) (blank ?))))
+      [@daemon] * #H7 #H8 <to_blank_i_def >H7 >H8 //
     ]
   ]
 qed.
 
-definition Rmove_R_i_rb ≝ λsig,n,i,t1,t2.
+definition Rmove_R_i_rb ≝ λA,sig,n,i,t1,t2.
 ∀ls,a,rs.
   t1 = midtape ? ls a rs →
-  (∀i.regular_trace sig n a ls rs i) → 
-  nth n ? (vec … a) (blank ?) = head ? → 
+  (∀i.regular_trace (TA A sig) (S n) a ls rs i) → 
+  is_head ?? (nth n ? (vec … a) (blank ?)) = true → 
   no_head_in … ls →
   no_head_in … rs →
   ∃ls1,a1,rs1. 
-   t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
-   (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
-   rb_trace_i sig n ls1 (vec … a1) rs1 i = 
-     tape_move ? (rb_trace_i sig n ls (vec … a) rs i) R ∧
-   ∀j. j ≤n → j ≠ i → 
-    rb_trace_i sig n ls1 (vec … a1) rs1 j = 
-      rb_trace_i sig n ls (vec … a) rs j.
-
-lemma sem_move_R_i : ∀sig,n,i.i < n →
-  move_R_i sig n i ⊨ Rmove_R_i_rb sig n i.
-#sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i sig n i))
+   t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
+   (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
+   rb_trace_i ? (S n) ls1 (vec … a1) rs1 i = 
+     tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
+   ∀j. j ≤ n → j ≠ i → 
+    rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = 
+      rb_trace_i ? (S n) ls (vec … a) rs j.
+
+lemma sem_move_R_i : ∀A,sig,n,i.i < n →
+  move_R_i A sig n i ⊨ Rmove_R_i_rb A sig n i.
+#A #sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i A sig n i))
   [#t1 #t2 #H #ls #a #rs #H1 #H2 #H3 #H4 #H5 @rb_move_R // <H1 // 
   |@sem_R_guarded @sem_Rmtil //
   ]
@@ -258,26 +259,26 @@ qed.
   
 (* move_L_i axiomatized *)
 
-axiom move_L_i : ∀sig.∀n,i:nat.TM (multi_sig sig n).
+axiom move_L_i : ∀A,sig.∀n,i:nat.TM (MTA A sig (S n)).
 
-definition Rmove_L_i_rb ≝ λsig,n,i,t1,t2.
+definition Rmove_L_i_rb ≝ λA,sig,n,i,t1,t2.
 ∀ls,a,rs.
   t1 = midtape ? ls a rs →
-  (∀i.regular_trace sig n a ls rs i) → 
-  nth n ? (vec … a) (blank ?) = head ? → 
+  (∀i.regular_trace (TA A sig) (S n) a ls rs i) → 
+  is_head ?? (nth n ? (vec … a) (blank ?)) = true →  
   no_head_in … ls →
   no_head_in … rs →
   ∃ls1,a1,rs1. 
-   t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
-   (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
-   rb_trace_i sig n ls1 (vec … a1) rs1 i = 
-     tape_move ? (rb_trace_i sig n ls (vec … a) rs i) L ∧
-   ∀j. j ≤n → j ≠ i → 
-    rb_trace_i sig n ls1 (vec … a1) rs1 j = 
-      rb_trace_i sig n ls (vec … a) rs j.
+   t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
+   (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
+   rb_trace_i ? (S n) ls1 (vec … a1) rs1 i = 
+     tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) L ∧
+   ∀j. j ≤ n → j ≠ i → 
+    rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = 
+      rb_trace_i ? (S n) ls (vec … a) rs j.
       
-axiom sem_move_L_i : ∀sig,n,i.i < n →
-  move_L_i sig n i ⊨ Rmove_L_i_rb sig n i.
+axiom sem_move_L_i : ∀A,sig,n,i.i < n →
+  move_L_i A sig n i ⊨ Rmove_L_i_rb A sig n i.
   
 (*
 lemma rb_move_L : ∀sig,n,ls,a,rs,outt,i.
@@ -296,54 +297,72 @@ lemma rb_move_L : ∀sig,n,ls,a,rs,outt,i.
 
 (* The following function read a move from  a vector of moves and executes it *)
 
-axiom get_move : ∀sig.∀n.∀a:multi_sig sig n.nat → DeqMove. 
+(* The head character contains a state and a sequence of moves *)
+
+definition HC ≝ λQ,n.FinProd Q (FinVector FinMove n).
 
-definition exec_move_i ≝ λsig,n,i.
-    (ifTM ? (test_char ? (λa. (get_move sig n a i == R)))
-      (move_R_i sig n i)
-      (ifTM ? (test_char ? (λa. (get_move sig n a i == L)))
-        (move_L_i sig n i)
+let rec all_N n on n : FinVector FinMove n ≝ 
+  match n with
+  [ O ⇒ Vector_of_list ? []
+  | S m ⇒ vec_cons ? N m (all_N m)
+  ].
+
+definition get_moves ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).
+  match nth n ? (vec … a) (blank ?) with 
+  [ None ⇒ all_N n
+  | Some x ⇒ match x with 
+    [inl y ⇒ snd ?? y
+    |inr y ⇒ all_N n]].
+    
+definition get_move ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λi.
+  nth i ? (vec … (get_moves Q sig n a)) N.
+
+definition exec_move_i ≝ λQ,sig,n,i.
+    (ifTM ? (test_char ? (λa. (get_move Q sig n a i == R)))
+      (move_R_i (HC Q n) sig n i)
+      (ifTM ? (test_char ? (λa. (get_move Q sig n a i == L)))
+        (move_L_i (HC Q n) sig n i)
         (nop ?) tc_true) tc_true).
-        
-definition R_exec_move_i ≝ λsig,n,i,t1,t2.
+
+definition R_exec_move_i ≝ λQ,sig,n,i,t1,t2.
 ∀a,ls,rs. 
-  t1 = midtape ? ls a rs → 
-  (∀i.regular_trace sig n a ls rs i) → 
-  nth n ? (vec … a) (blank ?) = head ? → 
+  t1 = midtape (MTA (HC Q n) sig (S n)) ls a rs → 
+  (∀i.regular_trace ? (S n) a ls rs i) →
+  is_head ?? (nth n ? (vec … a) (blank ?)) = true →   
   no_head_in … ls →
   no_head_in … rs →
   ∃ls1,a1,rs1. 
-   t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
-   (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
-   rb_trace_i sig n ls1 (vec … a1) rs1 i = 
-     tape_move ? (rb_trace_i sig n ls (vec … a) rs i) (get_move sig n a i) ∧
-   ∀j. j ≤n → j ≠ i → 
-    rb_trace_i sig n ls1 (vec … a1) rs1 j = 
-      rb_trace_i sig n ls (vec … a) rs j.
+   t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
+   (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
+   rb_trace_i ? (S n) ls1 (vec … a1) rs1 i = 
+     tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) (get_move Q sig n a i) ∧
+   ∀j. j ≤ n → j ≠ i → 
+    rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = 
+      rb_trace_i ? (S n) ls (vec … a) rs j.
 
 lemma  tape_move_N: ∀A,t. tape_move A t N = t.
 // qed.
 
-lemma sem_exec_move_i: ∀sig,n,i. i < n →
-  exec_move_i sig n i ⊨ R_exec_move_i sig n i.
-#sig #n #i #ltin
+lemma sem_exec_move_i: ∀Q,sig,n,i. i < n →
+  exec_move_i Q sig n i ⊨ R_exec_move_i Q sig n i.
+#Q #sig #n #i #ltin
 @(sem_if_app … (sem_test_char …)
-  (sem_move_R_i … ltin) 
+  (sem_move_R_i … ltin)
   (sem_if … (sem_test_char …)
     (sem_move_L_i … ltin) (sem_nop ?)))
 #tin #tout #t1 *
   [* * * #c * #Hc #HR #Ht1 #HMR 
    #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
-    >(\P HR) @HMR >Ht1 @Htin
+    >(\P HR) whd in HMR; @HMR >Ht1 @Htin
   |* * #HR #Ht1 >Ht1 *
     [* #t2 * * * #c * #Hc #HL #Ht2 #HML 
      #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
      >(\P HL) @HML >Ht2 @Htin
     |* #t2 * * #HL #Ht2 >Ht2 whd in ⊢ (%→?); #Htout >Htout
      #a #ls #rs #Htin >Htin in HR; #HR >Htin in HL; #HL  
-     cut (get_move sig n a i = N)
+     cut (get_move Q sig n a i = N)
       [lapply (HR a (refl … )) lapply (HL a (refl … ))
-       cases (get_move sig n a i) normalize 
+       cases (get_move Q sig n a i) normalize 
         [#H destruct (H) |#_ #H destruct (H) | //]]
      #HN >HN >tape_move_N #Hreg #_ #_ #_
      %{ls} %{a} %{rs} 
@@ -352,14 +371,14 @@ lemma sem_exec_move_i: ∀sig,n,i. i < n →
   ]
 qed.
 
-axiom reg_inv : ∀sig,n,a,ls,rs,a1,ls1,rs1. 
-  regular_trace sig n a1 ls1 rs1 n →  
-  (rb_trace_i sig n ls1 (vec … a1) rs1 n = 
-      rb_trace_i sig n ls (vec  … n a) rs n) →
-  nth n ? (vec … a) (blank ?) = head ? → 
+axiom reg_inv : ∀A,sig,n,a,ls,rs,a1,ls1,rs1. 
+  regular_trace (TA A sig) (S n) a1 ls1 rs1 n →  
+  (rb_trace_i ? (S n) ls1 (vec … a1) rs1 n = 
+      rb_trace_i ? (S n) ls (vec  …  a) rs n) →
+  is_head ?? (nth n ? (vec … (S n) a) (blank ?)) = true →
   no_head_in … ls →
   no_head_in … rs →
-  nth n ? (vec … a1) (blank ?) = head ? ∧ 
+  is_head ?? (nth n ? (vec … a1) (blank ?)) = true ∧ 
   no_head_in … ls1 ∧ no_head_in … rs1.
 
 
diff --git a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
index 016648770..1e5e36e91 100644
--- a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
+++ b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
@@ -96,7 +96,7 @@ definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
       (hd ? (ls1@b::ls2) (all_blanks …)) (tail ? (ls1@b::ls2)) rs j) ∧ 
     (not_blank sig n i b = false) ∧ 
     (hd (multi_sig sig n) (ls1@[b]) (all_blanks …) = a) ∧ (* not implied by the next fact *)
-    (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
+    (∀j.j < n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
     t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
 
 theorem sem_move_to_blank_L: ∀sig,n,i. 
@@ -250,39 +250,47 @@ definition is_sig ≝ λA,sig.λc:sig_ext (TA A sig).
      [ inl _ ⇒ false
      | inr _ ⇒ true]].
 
-definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) n.
+definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) (S n).
   ¬(is_head A sig (nth n ? (vec … c) (blank ?))).
   
+lemma not_head_all_blanks : ∀A,sig,n. 
+  not_head A sig n (all_blanks … (S n)) = true.
+#A #sig #n whd in ⊢ (??%?); >blank_all_blanks //
+qed.  
+
 definition no_head_in ≝ λA,sig,n,l. 
-  ∀x. mem ? x (trace (TA A sig) n n l) → is_head … x = false.
+  ∀x. mem ? x (trace (TA A sig) (S n) n l) → is_head … x = false.
 
 (*
 lemma not_head_true: ∀A,sig,n,c. not_head A sig n c = true → 
   is_head … (nth n ? (vec … c) (blank ?)) = false.
 *)
 
+lemma hd_nil : ∀A,d. hd A [ ] d = d. 
+// qed.
+
 definition mtiL ≝ λA,sig,n,i.
-   move_to_blank_L (TA A sig) n i · 
-   shift_i_L (TA A sig) n i ·
+   move_to_blank_L (TA A sig) (S n) i · 
+   shift_i_L (TA A sig) (S n) i ·
    move_until ? L (not_head A sig n). 
    
 definition Rmtil ≝ λA,sig,n,i,t1,t2.
   ∀ls,a,rs. 
-   t1 = midtape (MTA A sig n) ls a rs → 
+   t1 = midtape (MTA A sig (S n)) ls a rs → 
    is_head A sig (nth n ? (vec … a) (blank ?)) = true →  
-   (∀i.regular_trace (TA A sig) n a ls rs i) → 
+   (∀i.regular_trace (TA A sig) (S n) a ls rs i) → 
    (* next: we cannot be on rightof on trace i *)
    (nth i ? (vec … a) (blank ?) = (blank ?) 
      → nth i ? (vec … (hd ? rs (all_blanks …))) (blank ?) ≠ (blank ?)) →
    no_head_in … ls →   
    no_head_in … rs  → 
    (∃ls1,a1,rs1.
-     t2 = midtape (MTA A sig n) ls1 a1 rs1 ∧
+     t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
      (∀i.regular_trace … a1 ls1 rs1 i) ∧
-     (∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
-     (∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
-     (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
-     (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
+     (∀j. j ≤ n → j ≠ i → to_blank_i ? (S n) j (a1::ls1) = to_blank_i ? (S n) j (a::ls)) ∧
+     (∀j. j ≤ n → j ≠ i → to_blank_i ? (S n) j rs1 = to_blank_i ? (S n) j rs) ∧
+     (to_blank_i ? (S n) i ls1 = to_blank_i ? (S n) i (a::ls)) ∧
+     (to_blank_i ? (S n) i (a1::rs1)) = to_blank_i ? (S n) i rs).
 
 theorem sem_Rmtil: ∀A,sig,n,i. i < n → mtiL A sig n i  ⊨ Rmtil A sig n i.
 #A #sig #n #i #lt_in
@@ -294,7 +302,7 @@ theorem sem_Rmtil: ∀A,sig,n,i. i < n → mtiL A sig n i  ⊨ Rmtil A sig n i.
 (* we start looking into Rmitl *)
 #ls #a #rs #Htin (* tin is a midtape *)
 #Hheada #Hreg #no_rightof #Hnohead_ls #Hnohead_rs 
-cut (regular_i ? n (a::ls) i)
+cut (regular_i ? (S n) (a::ls) i)
   [cases (Hreg i) * // 
    cases (true_or_false (nth i ? (vec … a) (blank ?) == (blank ?))) #Htest
     [#_ @daemon (* absurd, since hd rs non e' blank *)
@@ -329,8 +337,7 @@ lapply (Htout … Ht2) -Htout -Ht2 *
    * #H3 @False_ind @(absurd (true=false)) [2://] <H3 @sym_eq
    <(notb_notb true) @(eq_f … notb) @Hnohead_rs >H2 >trace_append @mem_append_l2 
    lapply Hb0 cases rs2 
-    [whd in match (hd ???); #H >H in H3; whd in match (not_head ????); 
-     >all_blank_n normalize -H #H destruct (H); @False_ind
+    [>hd_nil #H >H in H3; >not_head_all_blanks #Habs destruct (Habs)
     |#c #r #H4 %1 >H4 //
     ]
   |* 
@@ -338,43 +345,43 @@ lapply (Htout … Ht2) -Htout -Ht2 *
    (* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
    * #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
    cut (∀j.j ≠ i →
-      trace ? n j (reverse (multi_sig (TA A sig) n) rs1@b::ls2) = 
-      trace ? n j (ls10@a1::ls20))
+      trace ? (S n) j (reverse (multi_sig (TA A sig) (S n)) rs1@b::ls2) = 
+      trace ? (S n) j (ls10@a1::ls20))
     [#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
-     lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
+     lapply (trace_shift_neq … (le_S … lt_in) ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
      <(trace_def …  (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ] 
    #Htracej
-   cut (trace ? n i (reverse (multi_sig (TA A sig) n) (rs1@[b0])@ls2) = 
-        trace ? n i (ls10@a1::ls20))
+   cut (trace ? (S n) i (reverse (multi_sig (TA A sig) (S n)) (rs1@[b0])@ls2) = 
+        trace ? (S n) i (ls10@a1::ls20))
     [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0]) 
-     cut (trace ? n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
-     lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
+     cut (trace ? (S n) i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
+     lapply (trace_shift … (le_S … lt_in) … Hrss) [//] whd in match (tail ??); #Htr <Htr
      >reverse_map >map_append <trace_def <Hls20 % 
     ] 
    #Htracei
    cut (∀j. j ≠ i →
-      (trace ? n j (reverse (MTA A sig n) rs11) = trace ? n j ls10) ∧ 
-      (trace ? n j (ls1@b::ls2) = trace ? n j (a1::ls20)))
+      (trace ? (S n) j (reverse (MTA A sig (S n)) rs11) = trace ? (S n) j ls10) ∧ 
+      (trace ? (S n) j (ls1@b::ls2) = trace ? (S n) j (a1::ls20)))
    [@daemon (* si fa 
      #j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
       [lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append 
        >trace_def in ⊢ (%→?); <map_append #H @H  
       | *) ] #H2
-  cut ((trace ? n i (b0::reverse ? rs11) = trace ? n i (ls10@[a1])) ∧ 
-      (trace ? n i (ls1@ls2) = trace ? n i ls20))
+  cut ((trace ? (S n) i (b0::reverse ? rs11) = trace ? (S n) i (ls10@[a1])) ∧ 
+      (trace ? (S n) i (ls1@ls2) = trace ? (S n) i ls20))
    [>H1 in Htracei; >reverse_append >reverse_single >reverse_append 
      >reverse_reverse >associative_append >associative_append
      @daemon
     ] #H3    
   cut (∀j. j ≠ i → 
-    trace ? n j (reverse (MTA A sig n) ls10@rs2) = trace ? n j rs)
-    [#j #jneqi @(injective_append_l … (trace ? n j (reverse ? ls1)))
+    trace ? (S n) j (reverse ? ls10@rs2) = trace ? (S n) j rs)
+    [#j #jneqi @(injective_append_l … (trace ? (S n) j (reverse ? ls1)))
      >map_append >map_append >Hrs1 >H1 >associative_append 
      <map_append <map_append in ⊢ (???%); @eq_f 
      <map_append <map_append @eq_f2 // @sym_eq 
      <(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
      @eq_f @(proj1 … (H2 j jneqi))] #Hrs_j
-   %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (MTA A sig n) rs2)}
+   %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail ? rs2)}
    %[%[%[%[%[@Htout
     |#j cases (decidable_eq_nat j i)
       [#eqji >eqji (* by cases wether a1 is blank *)
@@ -387,17 +394,17 @@ lapply (Htout … Ht2) -Htout -Ht2 *
         |@sym_eq @Hrs_j //
         ]
       ]]
-    |#j #lejn #jneqi <(Hls1 … lejn) 
+    |#j #lejn #jneqi <(Hls1 … (le_S_S … lejn)) 
      >to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
     |#j #lejn #jneqi >reverse_cons >associative_append >Hb0
      <to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f @Hrs_j //]
-    |<(Hls1 i) [2:@lt_to_le //] 
+    |<(Hls1 i) [2:@le_S //] 
      lapply (all_blank_after_blank … reg_ls1_i) 
        [@(\P ?) @daemon] #allb_ls2
      whd in match (to_blank_i ????); <(proj2 … H3)
      @daemon ]
     |>reverse_cons >associative_append  
-     cut (to_blank_i ? n i rs = to_blank_i ? n i (rs11@[b0])) [@daemon] 
+     cut (to_blank_i ? (S n) i rs = to_blank_i ? (S n) i (rs11@[b0])) [@daemon] 
      #Hcut >Hcut >(to_blank_i_chop  … b0 (a1::reverse …ls10)) [2: @Hb0blank]
      >to_blank_i_def >to_blank_i_def @eq_f 
      >trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
@@ -406,12 +413,12 @@ lapply (Htout … Ht2) -Htout -Ht2 *
     ]
   |(*we do not find the head: this is absurd *)
    * #b1 * #lss * * #H2 @False_ind 
-   cut (∀x0. mem ? x0 (trace ? n n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
+   cut (∀x0. mem ? x0 (trace ? (S n) n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
      [@daemon] -H2 #H2
-   lapply (trace_shift_neq ? n i n … lt_in … Hrss)
+   lapply (trace_shift_neq ? (S n) i n … (le_S … lt_in) … Hrss)
      [@lt_to_not_eq @lt_in | // ] 
    #H3 @(absurd 
-        (is_head  … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … n))) (blank ?)) = true))
+        (is_head  … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … (S n)))) (blank ?)) = true))
      [>Hhead //
      |@eqnot_to_noteq @H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def 
       >H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append 
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 2c162745f..52c91909d 100644
--- a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
+++ b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
@@ -252,7 +252,7 @@ lemma to_blank_cons_nb: ∀sig,n,i,a,l.
 qed.
 
 axiom to_blank_hd : ∀sig,n,a,b,l1,l2. 
-  (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
+  (∀i. i < n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
 
 lemma to_blank_i_ext : ∀sig,n,i,l.
   to_blank_i sig n i l = to_blank_i sig n i (l@[all_blanks …]).
diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma
index 6459cedd9..28c3920bc 100644
--- a/matita/matita/lib/turing/multi_universal/normalTM.ma
+++ b/matita/matita/lib/turing/multi_universal/normalTM.ma
@@ -12,51 +12,6 @@
 include "turing/multi_universal/alphabet.ma".
 include "turing/mono.ma".
 
-(************************* turning DeqMove into a DeqSet **********************)
-definition move_eq ≝ λm1,m2:move.
-  match m1 with
-  [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
-  |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
-  |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
-
-lemma move_eq_true:∀m1,m2.
-  move_eq m1 m2 = true ↔ m1 = m2.
-*
-  [* normalize [% #_ % |2,3: % #H destruct ]
-  |* normalize [1,3: % #H destruct |% #_ % ]
-  |* normalize [1,2: % #H destruct |% #_ % ]
-qed.
-
-definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
-
-unification hint 0 ≔ ;
-    X ≟ DeqMove
-(* ---------------------------------------- *) ⊢ 
-    move ≡ carr X.
-
-unification hint  0 ≔ m1,m2; 
-    X ≟ DeqMove
-(* ---------------------------------------- *) ⊢ 
-    move_eq m1 m2 ≡ eqb X m1 m2.
-
-
-(************************ turning DeqMove into a FinSet ***********************)
-definition move_enum ≝ [L;R;N].
-
-lemma move_enum_unique: uniqueb ? [L;R;N] = true.
-// qed.
-
-lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
-* // qed.
-
-definition FinMove ≝ 
-  mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
-
-unification hint  0 ≔ ; 
-    X ≟ FinMove
-(* ---------------------------------------- *) ⊢ 
-    move ≡ FinSetcarr X.
-
 (*************************** normal Turing Machines ***************************)
 
 (* A normal turing machine is just an ordinary machine where: