From 31790e8f6fa051f710f41e4c17d67701874ba331 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Sat, 19 Oct 2013 10:25:00 +0000
Subject: [PATCH] Slowly porting to an enriched tape alphabet

---
 .../lib/turing/multi_to_mono/shift_trace.ma   | 148 ++++++++++--------
 .../turing/multi_to_mono/shift_trace_aux.ma   |  47 +++---
 .../turing/multi_to_mono/trace_alphabet.ma    |  61 ++++----
 3 files changed, 144 insertions(+), 112 deletions(-)

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 9ff88de28..016648770 100644
--- a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
+++ b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
@@ -24,7 +24,7 @@ axiom regular_tail: ∀sig,n,l,i.
   regular_i sig n l i → regular_i sig n (tail ? l) i.
   
 axiom regular_extend: ∀sig,n,l,i.
-   regular_i sig n l i → regular_i sig n (l@[all_blank sig n]) i.
+   regular_i sig n l i → regular_i sig n (l@[all_blanks sig n]) i.
 
 axiom all_blank_after_blank: ∀sig,n,l1,b,l2,i. 
   nth i ? (vec … b) (blank ?) = blank ? → 
@@ -32,7 +32,7 @@ axiom all_blank_after_blank: ∀sig,n,l1,b,l2,i.
    
 lemma regular_trace_extl:  ∀sig,n,a,ls,rs,i.
   regular_trace sig n a ls rs i → 
-    regular_trace sig n a (ls@[all_blank sig n]) rs i.
+    regular_trace sig n a (ls@[all_blanks sig n]) rs i.
 #sig #n #a #ls #rs #i *
   [* #H1 #H2 % % // @(regular_extend … H1)
   |* #H1 #H2 %2 % // @(regular_extend … H1)
@@ -41,7 +41,7 @@ qed.
 
 lemma regular_cons_hd_rs: ∀sig,n.∀a:multi_sig sig n.∀ls,rs1,rs2,i.
   regular_trace sig n a ls (rs1@rs2) i → 
-    regular_trace sig n a ls (rs1@((hd ? rs2 (all_blank …))::(tail ? rs2))) i.
+    regular_trace sig n a ls (rs1@((hd ? rs2 (all_blanks …))::(tail ? rs2))) i.
 #sig #n #a #ls #rs1 #rs2 #i cases rs2 [2: #b #tl #H @H] 
 *[* #H1 >append_nil #H2 %1 % 
    [@H1 | whd in match (hd ???); @(regular_extend … rs1) //]
@@ -69,7 +69,7 @@ qed.
    improve semantics *)
    
 definition move_to_blank_L ≝ λsig,n,i.
-  (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
+  (move_until ? L (not_blank sig n i)) · extend ? (all_blanks sig n).
 
 (*
 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
@@ -85,7 +85,7 @@ definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
 
 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
 (current ? t1 = None ? → 
-  t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
+  t2 = midtape (multi_sig sig n) (left ? t1) (all_blanks …) (right ? t1)) ∧
 ∀ls,a,rs.
   t1 = midtape (multi_sig sig n) ls a rs → 
   regular_i sig n (a::ls) i →
@@ -93,9 +93,9 @@ definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
   (∃b,ls1,ls2.
     (regular_i sig n (ls1@b::ls2) i) ∧ 
     (∀j. j ≠ i → regular_trace … 
-      (hd ? (ls1@b::ls2) (all_blank …)) (tail ? (ls1@b::ls2)) rs j) ∧ 
-    (no_blank sig n i b = false) ∧ 
-    (hd (multi_sig sig n) (ls1@[b]) (all_blank …) = a) ∧ (* not implied by the next fact *)
+      (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)) ∧
     t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
 
@@ -103,7 +103,7 @@ theorem sem_move_to_blank_L: ∀sig,n,i.
   move_to_blank_L sig n i  ⊨ R_move_to_blank_L sig n i.
 #sig #n #i 
 @(sem_seq_app ?????? 
-  (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
+  (ssem_move_until_L ? (not_blank sig n i)) (sem_extend ? (all_blanks sig n)))
 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
   [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
   |#ls #a #rs #Htin #Hreg #Hreg2 -Ht1a cases (Ht1b … Htin)
@@ -122,11 +122,11 @@ theorem sem_move_to_blank_L: ∀sig,n,i.
       ]
     |* #b * #lss * * #H1 #H2 #Ht1 -Ht1b >Ht1 in Ht2a; 
      whd in match (left ??); whd in match (right ??); #Hout
-     %{(all_blank …)} %{(lss@[b])} %{[]}
+     %{(all_blanks …)} %{(lss@[b])} %{[]}
      %[%[%[%[%[<H2 @regular_extend // 
               |<H2 #j #jneqi whd in match (hd ???); whd in match (tail ??); 
                @regular_trace_extl @Hreg2 //]
-            |whd in match (no_blank ????); >blank_all_blank //]
+            |whd in match (not_blank ????); >blank_all_blanks //]
           |<H2 //]
         |#j #lejn <H2 @sym_eq @to_blank_i_ext]
       |>reverse_append >reverse_single @Hout normalize // 
@@ -138,9 +138,9 @@ qed.
 (******************************************************************************)
    
 definition shift_i_L ≝ λsig,n,i.
-   ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
+   ncombf_r (multi_sig …) (shift_i sig n i) (all_blanks sig n) ·
    mti sig n i · 
-   extend ? (all_blank sig n).
+   extend ? (all_blanks sig n).
    
 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
     (∀a,ls,rs. 
@@ -155,13 +155,13 @@ definition R_shift_i_L ≝ λsig,n,i,t1,t2.
         (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
         shift_l sig n i (a::rs) (rss@[b]) ∧
         t2 = midtape (multi_sig sig n) 
-          ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
+          ((reverse ? (rss@[b]))@ls) (all_blanks sig n) [ ]))).
 
 definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
   (∀a,ls,rs. 
    t1 = midtape ? ls a rs  → 
    ∃rs1,b,rs2,rss.
-      b = hd ? rs2 (all_blank sig n) ∧
+      b = hd ? rs2 (all_blanks sig n) ∧
       nth i ? (vec … b) (blank ?) = (blank ?) ∧
       rs = rs1@rs2 ∧ 
       (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
@@ -171,12 +171,12 @@ definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i  ⊨ R_shift_i_L sig n i.
 #sig #n #i 
 @(sem_seq_app ?????? 
-  (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
+  (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blanks sig n))
    (sem_seq ????? (ssem_mti sig n i) 
-    (sem_extend ? (all_blank sig n))))
+    (sem_extend ? (all_blanks sig n))))
 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
 #a #ls #rs cases rs
-  [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]} 
+  [#Htin %2 %{(shift_i sig n i a (all_blanks sig n))} %{[ ]} 
    %[%[#x @False_ind | @daemon]
     |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1 
      lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1; 
@@ -200,7 +200,7 @@ theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i  ⊨ R_shift_i_L sig n i.
       ]
     |* #b * #rss * * #H1 #H2 
      #Ht2 %2
-     %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
+     %{(shift_i sig n i b (all_blanks sig n))} %{(shift_i sig n i a a1::rss)}
      %[%[@H1 |@daemon ]
       |>Ht2 in Htout1; #Htout >Htout //
        whd in match (left ??); whd in match (right ??);
@@ -221,53 +221,80 @@ theorem sem_shift_i_L_new: ∀sig,n,i.
    %{rs1} %{b} %{(b::rs2)} %{(a1::rss)} 
    %[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
   |* #b * #rss * * #H1 #H2 #Ht2
-   %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])} 
-   %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
+   %{rs} %{(all_blanks sig n)} %{[]} %{(rss@[b])} 
+   %[%[%[%[%[//|@blank_all_blanks]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
   ]
 qed.
    
 
 (*******************************************************************************
-The following machine implements a full move of for a trace: we reach the left 
-border, shift the i-th trace and come back to the head position. *)  
+The following machine implements a full move for a trace: we reach the left 
+border, shift the i-th trace and come back to the head position. 
+The head may hold additional information A, so we suppose that the tape alphabet
+is the disjoint sum between A and the alphabet sig of the multi tape machine. *) 
+
+definition TA ≝ λA,sig. FinSum A sig.
+definition MTA ≝ λA,sig,n.multi_sig (TA A sig) n.
+
+definition is_head ≝ λA,sig.λc:sig_ext (TA A sig).
+  match c with
+  [ None ⇒ false
+  | Some a ⇒ match a with 
+     [ inl _ ⇒ true
+     | inr _ ⇒ false]].
+
+definition is_sig ≝ λA,sig.λc:sig_ext (TA A sig).
+  match c with
+  [ None ⇒ false
+  | Some a ⇒ match a with 
+     [ inl _ ⇒ false
+     | inr _ ⇒ true]].
 
-(* this exclude the possibility that traces do not overlap: the head must 
-remain inside all traces *)
+definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) n.
+  ¬(is_head A sig (nth n ? (vec … c) (blank ?))).
+  
+definition no_head_in ≝ λA,sig,n,l. 
+  ∀x. mem ? x (trace (TA A sig) 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.
+*)
 
-definition mtiL ≝ λsig,n,i.
-   move_to_blank_L sig n i · 
-   shift_i_L sig n i ·
-   move_until ? L (no_head sig n). 
+definition mtiL ≝ λA,sig,n,i.
+   move_to_blank_L (TA A sig) n i · 
+   shift_i_L (TA A sig) n i ·
+   move_until ? L (not_head A sig n). 
    
-definition Rmtil ≝ λsig,n,i,t1,t2.
+definition Rmtil ≝ λA,sig,n,i,t1,t2.
   ∀ls,a,rs. 
-   t1 = midtape (multi_sig sig n) ls a rs → 
-   nth n ? (vec … a) (blank ?) = head ? →  
-   (∀i.regular_trace sig n a ls rs i) → 
+   t1 = midtape (MTA A sig 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) → 
    (* next: we cannot be on rightof on trace i *)
    (nth i ? (vec … a) (blank ?) = (blank ?) 
-     → nth i ? (vec … (hd ? rs (all_blank …))) (blank ?) ≠ (blank ?)) →
+     → nth i ? (vec … (hd ? rs (all_blanks …))) (blank ?) ≠ (blank ?)) →
    no_head_in … ls →   
    no_head_in … rs  → 
    (∃ls1,a1,rs1.
-     t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
+     t2 = midtape (MTA A sig 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).
 
-theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i  ⊨ Rmtil sig n i.
-#sig #n #i #lt_in
+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
 @(sem_seq_app ?????? 
   (sem_move_to_blank_L … )
    (sem_seq ????? (sem_shift_i_L_new …)
-    (ssem_move_until_L ? (no_head sig n))))
+    (ssem_move_until_L ? (not_head A sig n))))
 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
 (* we start looking into Rmitl *)
 #ls #a #rs #Htin (* tin is a midtape *)
-#Hhead #Hreg #no_rightof #Hnohead_ls #Hnohead_rs 
-cut (regular_i sig n (a::ls) i)
+#Hheada #Hreg #no_rightof #Hnohead_ls #Hnohead_rs 
+cut (regular_i ? 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 *)
@@ -299,11 +326,10 @@ lapply (Htout … Ht2) -Htout -Ht2 *
   [(* the current character on trace i holds the head-mark.
       The case is absurd, since b0 is the head of rs2, that is a sublist of rs, 
       and the head-mark is not in rs *)
-   * #H3 @False_ind @(absurd (nth n ? (vec … b0) (blank sig) = head ?)) 
-     [@(\P ?) @injective_notb @H3 ]
-   @Hnohead_rs >H2 >trace_append @mem_append_l2 
+   * #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 (no_head ???); 
+    [whd in match (hd ???); #H >H in H3; whd in match (not_head ????); 
      >all_blank_n normalize -H #H destruct (H); @False_ind
     |#c #r #H4 %1 >H4 //
     ]
@@ -312,43 +338,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 sig n j (reverse (multi_sig sig n) rs1@b::ls2) = 
-      trace sig n j (ls10@a1::ls20))
+      trace ? n j (reverse (multi_sig (TA A sig) n) rs1@b::ls2) = 
+      trace ? 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
      <(trace_def …  (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ] 
    #Htracej
-   cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) = 
-        trace sig n i (ls10@a1::ls20))
+   cut (trace ? n i (reverse (multi_sig (TA A sig) n) (rs1@[b0])@ls2) = 
+        trace ? n i (ls10@a1::ls20))
     [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0]) 
-     cut (trace sig n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
+     cut (trace ? n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
      lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
      >reverse_map >map_append <trace_def <Hls20 % 
     ] 
    #Htracei
    cut (∀j. j ≠ i →
-      (trace sig n j (reverse (multi_sig sig n) rs11) = trace sig n j ls10) ∧ 
-      (trace sig n j (ls1@b::ls2) = trace sig n j (a1::ls20)))
+      (trace ? n j (reverse (MTA A sig n) rs11) = trace ? n j ls10) ∧ 
+      (trace ? n j (ls1@b::ls2) = trace ? 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 sig n i (b0::reverse ? rs11) = trace sig n i (ls10@[a1])) ∧ 
-      (trace sig n i (ls1@ls2) = trace sig n i ls20))
+  cut ((trace ? n i (b0::reverse ? rs11) = trace ? n i (ls10@[a1])) ∧ 
+      (trace ? n i (ls1@ls2) = trace ? 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 sig n j (reverse (multi_sig sig n) ls10@rs2) = trace sig n j rs)
-    [#j #jneqi @(injective_append_l … (trace sig n j (reverse ? ls1)))
+    trace ? n j (reverse (MTA A sig n) ls10@rs2) = trace ? n j rs)
+    [#j #jneqi @(injective_append_l … (trace ? 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 (multi_sig sig n) rs2)}
+   %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (MTA A sig n) rs2)}
    %[%[%[%[%[@Htout
     |#j cases (decidable_eq_nat j i)
       [#eqji >eqji (* by cases wether a1 is blank *)
@@ -371,7 +397,7 @@ lapply (Htout … Ht2) -Htout -Ht2 *
      whd in match (to_blank_i ????); <(proj2 … H3)
      @daemon ]
     |>reverse_cons >associative_append  
-     cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon] 
+     cut (to_blank_i ? n i rs = to_blank_i ? 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
@@ -380,14 +406,14 @@ lapply (Htout … Ht2) -Htout -Ht2 *
     ]
   |(*we do not find the head: this is absurd *)
    * #b1 * #lss * * #H2 @False_ind 
-   cut (∀x0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) → x0 ≠ head ?)
+   cut (∀x0. mem ? x0 (trace ? n n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
      [@daemon] -H2 #H2
-   lapply (trace_shift_neq sig n i n … lt_in … Hrss)
+   lapply (trace_shift_neq ? n i n … lt_in … Hrss)
      [@lt_to_not_eq @lt_in | // ] 
    #H3 @(absurd 
-        (nth n ? (vec … (hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
+        (is_head  … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … n))) (blank ?)) = true))
      [>Hhead //
-     |@H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def 
+     |@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 
       >reverse_reverse >associative_append <map_append @mem_append_l2
       cases ls1 [%1 % |#x #ll %1 %]
diff --git a/matita/matita/lib/turing/multi_to_mono/shift_trace_aux.ma b/matita/matita/lib/turing/multi_to_mono/shift_trace_aux.ma
index 3574d6471..d1cd65dda 100644
--- a/matita/matita/lib/turing/multi_to_mono/shift_trace_aux.ma
+++ b/matita/matita/lib/turing/multi_to_mono/shift_trace_aux.ma
@@ -4,10 +4,12 @@ include "turing/multi_to_mono/trace_alphabet.ma".
 
 (* a machine that shift the i trace r starting from the bord of the trace *)
 
+(* (λc.¬(nth i ? (vec … c) (blank ?))==blank ?)) *)
 (* vec is a coercion. Why should I insert it? *)
 definition mti_step ≝ λsig:FinSet.λn,i.
-  ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
-     (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
+  ifTM (multi_sig sig n) (test_char ? (not_blank sig n i))
+     (single_finalTM … 
+       (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blanks sig n)))
      (nop ?) tc_true.
       
 definition Rmti_step_true ≝ 
@@ -18,7 +20,7 @@ definition Rmti_step_true ≝
        t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
      (∃ls.
        t1 = midtape ? ls b [] ∧
-       t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
+       t2 = rightof ? (shift_i sig n i b (all_blanks sig n)) ls)).
 
 (* 〈combf0,all_blank sig n〉 *)
 definition Rmti_step_false ≝ 
@@ -31,9 +33,9 @@ lemma sem_mti_step :
   mti_step sig n i  ⊨ 
     [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
 #sig #n #i
-@(acc_sem_if_app (multi_sig sig n) ?????????? 
-     (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n)) 
-     (sem_nop (multi_sig sig n)))
+@(acc_sem_if_app (multi_sig sig n) … (sem_test_char …) 
+  (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blanks sig n)) 
+  (sem_nop (multi_sig sig n)))
   [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
    #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
    #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
@@ -58,23 +60,22 @@ definition mti ≝
 
 axiom daemon: ∀P:Prop.P.
 
-definition R_mti ≝ 
-  λsig,n,i,t1,t2.
-    (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
-    (∀a,ls,rs. 
-      t1 = midtape (multi_sig sig n) ls a rs → 
-      (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
-      ((∃rs1,b,rs2,rss.
-        rs = rs1@b::rs2 ∧ 
-        nth i ? (vec … b) (blank ?) = (blank ?) ∧
-        (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
-        shift_l sig n i (a::rs1) rss ∧
-        t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
-      (∃b,rss. 
-        (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
-        shift_l sig n i (a::rs) (rss@[b]) ∧
-        t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n)) 
-         ((reverse ? rss)@ls)))).  
+definition R_mti ≝ λsig,n,i,t1,t2.
+  (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
+  (∀a,ls,rs. 
+    t1 = midtape (multi_sig sig n) ls a rs → 
+    (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
+    ((∃rs1,b,rs2,rss.
+      rs = rs1@b::rs2 ∧ 
+      nth i ? (vec … b) (blank ?) = (blank ?) ∧
+      (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
+      shift_l sig n i (a::rs1) rss ∧
+      t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
+    (∃b,rss. 
+      (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
+      shift_l sig n i (a::rs) (rss@[b]) ∧
+      t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blanks sig n)) 
+       ((reverse ? rss)@ls)))).  
 
 lemma sem_mti:
   ∀sig,n,i.
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 bb1e54e63..2c162745f 100644
--- a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
+++ b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
@@ -4,38 +4,42 @@ simulating a multi-tape machine, and a library of functions operating on them *)
 include "basics/vector_finset.ma".
 
 (* a multi_sig characheter is composed by n+1 sub-characters: n for each tape 
-of a multitape machine, and an additional one to mark the position of the head. 
-We extend the tape alphabet with two new symbols true and false. 
-false is used to pad shorter tapes, and true to mark the head of the tape *)
+of a multitape machine.  
+We extend the tape alphabet with a special symbol None to pad shorter tapes.
+For the moment, the actual content of the tape alphabet is left unspecifed, 
+but we shall need characters to store states and moves of the multitape 
+machines and to mark the head position *)
 
-definition sig_ext ≝ λsig. FinSum FinBool sig.
-definition blank : ∀sig.sig_ext sig ≝ λsig. inl … false.
-definition head : ∀sig.sig_ext sig ≝ λsig. inl … true.
+definition sig_ext ≝ λsig. FinOption sig.
+definition blank : ∀sig.sig_ext sig ≝ λsig. None sig.
+
+(* definition head : ∀sig.sig_ext sig ≝ λsig. inl … true. *)
 
 definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
 
 (* a character containing blank characters in each trace *)
-let rec all_blank sig n on n : multi_sig sig n ≝ 
+let rec all_blanks sig n on n : multi_sig sig n ≝ 
   match n with
   [ O ⇒ Vector_of_list ? []
-  | S m ⇒ vec_cons ? (blank ?) m (all_blank sig m)
+  | S m ⇒ vec_cons ? (blank ?) m (all_blanks sig m)
   ].
 
-lemma blank_all_blank: ∀sig,n,i.
-  nth i ? (vec … (all_blank sig n)) (blank sig) = blank ?.
+lemma blank_all_blanks: ∀sig,n,i.
+  nth i ? (vec … (all_blanks sig n)) (blank sig) = blank ?.
 #sig #n elim n normalize [#i >nth_nil // |#m #Hind #i cases i // #j @Hind ]
 qed.
 
 lemma all_blank_n: ∀sig,n.
-  nth n ? (vec … (all_blank sig n)) (blank sig) = blank ?.
-#sig #n @blank_all_blank 
+  nth n ? (vec … (all_blanks sig n)) (blank sig) = blank ?.
+#sig #n @blank_all_blanks 
 qed.
 
 (* boolen test functions *)
 
-definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
+definition not_blank ≝ λsig,n,i.λc:multi_sig sig n.
   ¬(nth i ? (vec … c) (blank ?))==blank ?.
 
+(*
 definition no_head ≝ λsig,n.λc:multi_sig sig n.
   ¬((nth n ? (vec … c) (blank ?))==head ?).
     
@@ -48,7 +52,7 @@ qed.
 lemma no_head_false: ∀sig,n,a. 
   nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
 #sig #n #a #H normalize >H //  
-qed.
+qed. *)
 
 (**************************** extract the i-th trace **************************)
 definition trace ≝ λsig,n,i,l. 
@@ -60,8 +64,8 @@ lemma trace_def : ∀sig,n,i,l.
 
 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 % 
+    nth i ? (hd ? l (all_blanks … )) (blank ?).
+#sig #n #i #l elim l // normalize >blank_all_blanks % 
 qed.
  
 lemma tail_trace:  ∀sig,n,i,l. 
@@ -88,19 +92,20 @@ qed.
 
 lemma nth_trace : ∀sig,n,i,j,l.
   nth j ? (trace sig n i l) (blank ?) = 
-    nth i ? (nth j ? l (all_blank sig n)) (blank ?).
+    nth i ? (nth j ? l (all_blanks sig n)) (blank ?).
 #sig #n #i #j elim j
-  [#l cases l normalize // >blank_all_blank //
+  [#l cases l normalize // >blank_all_blanks //
   |-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
    cases l 
-    [normalize >nth_nil >nth_nil >blank_all_blank //
+    [normalize >nth_nil >nth_nil >blank_all_blanks //
     |#a #tl normalize @Hind]
   ]
 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).
@@ -178,9 +183,9 @@ asserts that v1 is obtained from v2 by shifting_left the i-trace *)
 
 definition shift_l ≝ λsig,n,i,v1,v2.  (* multi_sig sig n *) 
   |v1| = |v2| ∧ 
-  ∀j.nth j ? v2 (all_blank sig n) = 
-      change_vec ? n (nth j ? v1 (all_blank sig n)) 
-        (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
+  ∀j.nth j ? v2 (all_blanks sig n) = 
+      change_vec ? n (nth j ? v1 (all_blanks sig n)) 
+        (nth i ? (vec … (nth (S j) ? v1 (all_blanks sig n))) (blank ?)) i.
 
 (* supposing (shift_l … i v1 v2), the i-th trace of v2 is equal to the tail of
 the i-th trace of v1, plus a trailing blank *)
@@ -193,8 +198,8 @@ lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
     |#b #tl #_ normalize >length_append >length_trace normalize //
     ]
   |#j >nth_trace >Hnth >nth_change_vec // >tail_trace 
-   cut (trace ? n i [all_blank sig n] = [blank sig]) 
-     [normalize >blank_all_blank //] 
+   cut (trace ? n i [all_blanks sig n] = [blank sig]) 
+     [normalize >blank_all_blanks //] 
    #Hcut <Hcut <trace_append >nth_trace 
    <nth_extended //
   ]
@@ -250,16 +255,16 @@ 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.
 
 lemma to_blank_i_ext : ∀sig,n,i,l.
-  to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
+  to_blank_i sig n i l = to_blank_i sig n i (l@[all_blanks …]).
 #sig #n #i #l elim l
-  [@sym_eq @to_blank_cons_b @blank_all_blank
+  [@sym_eq @to_blank_cons_b @blank_all_blanks
   |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
   ]
 qed. 
   
 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
   to_blank_i sig n i (l1@l2) = 
-    to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
+    to_blank_i … i (l1@(hd … l2 (all_blanks …))::tail … l2).
 #sig #n #i #l1 #l2 cases l2
   [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext 
   |#a #tl % 
-- 
2.39.2