X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmatch.ma;h=ed4142fa327eeda0f8c9f9bce81a5303df955cf0;hb=b31ab31a99065295b91003a0df95dec817cee5de;hp=ff31367f72edfd37d0d0438ca41c27feed5dbfb1;hpb=cdcfe9f97936f02dab1970ebf3911940bf0a4e29;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma
index ff31367f7..ed4142fa3 100644
--- a/matita/matita/lib/turing/multi_universal/match.ma
+++ b/matita/matita/lib/turing/multi_universal/match.ma
@@ -14,7 +14,7 @@
 
 include "turing/multi_universal/compare.ma".
 include "turing/multi_universal/par_test.ma".
-
+include "turing/multi_universal/moves_2.ma".
 
 definition Rtc_multi_true ≝ 
   λalpha,test,n,i.λt1,t2:Vector ? (S n).
@@ -71,111 +71,223 @@ cases (acc_sem_inject … Hin (sem_test_null alpha) int)
     #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ] 
 qed.
 
-lemma comp_list: ∀S:DeqSet. ∀l1,l2:list S.∀is_endc. ∃l,tl1,tl2. 
-  l1 = l@tl1 ∧ l2 = l@tl2 ∧ (∀c.c ∈ l = true → is_endc c = false) ∧
-  ∀a,tla. tl1 = a::tla → 
-  is_endc a = true ∨ (is_endc a = false ∧∀b,tlb.tl2 = b::tlb → a≠b).
-#S #l1 #l2 #is_endc elim l1 in l2;
-[ #l2 %{[ ]} %{[ ]} %{l2} normalize %
-  [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) ]
-| #x #l3 #IH cases (true_or_false (is_endc x)) #Hendcx
-  [ #l %{[ ]} %{(x::l3)} %{l} normalize
-    % [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) >Hendcx % % ]
-  | *
-    [ %{[ ]} %{(x::l3)} %{[ ]} normalize %
-      [ % [ % // | #c #H destruct (H) ]
-      | #a #tla #H destruct (H) cases (is_endc a)
-        [ % % | %2 % // #b #tlb #H destruct (H) ]
-      ]
-    | #y #l4 cases (true_or_false (x==y)) #Hxy
-      [ lapply (\P Hxy) -Hxy #Hxy destruct (Hxy)  
-        cases (IH l4) -IH #l * #tl1 * #tl2 * * * #Hl3 #Hl4 #Hl #IH
-        %{(y::l)} %{tl1} %{tl2} normalize
-        % [ % [ % // 
-              | #c cases (true_or_false (c==y)) #Hcy >Hcy normalize
-                [ >(\P Hcy) //
-                | @Hl ]
-              ]
-          | #a #tla #Htl1 @(IH … Htl1) ]
-      | %{[ ]} %{(x::l3)} %{(y::l4)} normalize %
-        [ % [ % // | #c #H destruct (H) ]
-        | #a #tla #H destruct (H) cases (is_endc a)
-          [ % % | %2 % // #b #tlb #H destruct (H) @(\Pf Hxy) ]
-        ]
-      ]
-    ]
-  ]
-]
-qed.
-
-definition match_test ≝ λsrc,dst.λsig:DeqSet.λn,is_endc.λv:Vector ? n.
+definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n.
   match (nth src (option sig) v (None ?)) with 
   [ None ⇒  false 
-  | Some x ⇒  notb ((is_endc x) ∨ (nth dst (DeqOption sig) v (None ?) == None ?))]. 
+  | Some x ⇒  notb (nth dst (DeqOption sig) v (None ?) == None ?) ].
 
-definition match_step ≝ λsrc,dst,sig,n,is_startc,is_endc.
-  compare src dst sig n is_endc ·
-     (ifTM ?? (partest sig n (match_test src dst sig ? is_endc))
+definition mmove_states ≝ initN 2.
+
+definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_mmove ≝ 
+ λi,sig,n,D.
+ λp:mmove_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
+ | S _ ⇒ 〈mmove1,null_action sig n〉 ].
+
+definition mmove ≝ 
+  λi,sig,n,D.
+  mk_mTM sig n mmove_states (trans_mmove i sig n D) 
+    mmove0 (λq.q == mmove1).
+    
+definition Rm_multi ≝ 
+  λalpha,n,i,D.λt1,t2:Vector ? (S n).
+  t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
+   
+lemma sem_move_multi :
+  ∀alpha,n,i,D.i ≤ n → 
+  mmove i alpha n D ⊨ Rm_multi alpha n i D.
+#alpha #n #i #D #Hin #int %{2}
+%{(mk_mconfig ? mmove_states n mmove1 ?)} 
+[| %
+ [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f %
+ | whd >tape_move_multi_def
+   <(change_vec_same … (ctapes …) i (niltape ?))
+   >pmap_change <tape_move_multi_def >tape_move_null_action % ] ]
+ qed.
+  
+definition rewind ≝ λsrc,dst,sig,n.
+  parmove src dst sig n L · mmove src sig n R · mmove dst sig n R.
+
+definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+  (∀x,x0,xs,rs.
+    nth src ? int (niltape ?) = midtape sig (xs@[x0]) x rs → 
+    ∀ls0,y,y0,target,rs0.|xs| = |target| → 
+    nth dst ? int (niltape ?) = midtape sig (target@y0::ls0) y rs0 → 
+    outt = change_vec ?? 
+           (change_vec ?? int (midtape sig [] x0 (reverse ? xs@x::rs)) src)
+           (midtape sig ls0 y0 (reverse ? target@y::rs0)) dst).
+           
+theorem accRealize_to_Realize :
+  ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
+  M ⊨ [ acc: Rtrue, Rfalse ] →  M ⊨ Rtrue ∪ Rfalse.
+#sig #n #M #Rtrue #Rfalse #acc #HR #t
+cases (HR t) #k * #outc * * #Hloop
+#Htrue #Hfalse %{k} %{outc} % // 
+cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase
+[ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ]
+qed. 
+           
+lemma sem_rewind : ∀src,dst,sig,n.
+  src ≠ dst → src < S n → dst < S n → 
+  rewind src dst sig n ⊨ R_rewind src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst
+@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) ?)
+[| @(sem_seq_app sig n ????? (sem_move_r_multi …) (sem_move_r_multi …)) //
+ @le_S_S_to_le // ]
+#ta #tb * #tc * * #Htc #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb
+#x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst
+>(Htc ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in Htd;
+[|>Hmidta_dst //
+|>length_append >length_append >Hlen % ] * #_
+[ whd in ⊢ (%→?); * #x1 * #x2 * *
+  >change_vec_commute in ⊢ (%→?); // >nth_change_vec //
+  cases (reverse sig (xs@[x0])@x::rs)
+  [|#z #zs] normalize in ⊢ (%→?); #H destruct (H)
+| whd in ⊢ (%→?); * #_ #Htb >Htb -Htb FAIL
+  
+   normalize in ⊢ (%→?);
+    (sem_parmove_step src dst sig n R Hneq Hsrc Hdst))
+    (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
+      (sem_seq … 
+        (sem_parmoveL ???? Hneq Hsrc Hdst) 
+        (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
+      (sem_nop …)))
+  
+
+definition match_step ≝ λsrc,dst,sig,n.
+  compare src dst sig n ·
+     (ifTM ?? (partest sig n (match_test src dst sig ?))
       (single_finalTM ??
-        (parmove src dst sig n L is_startc · (inject_TM ? (move_r ?) n dst)))
+        (rewind src dst sig n · (inject_TM ? (move_r ?) n dst)))
       (nop …)
       partest1).
       
 definition R_match_step_false ≝ 
-  λsrc,dst,sig,n,is_endc.λint,outt: Vector (tape sig) (S n).
-  ∀ls,x,xs,end,rs.
-  nth src ? int (niltape ?) = midtape sig ls x (xs@end::rs) →
-  (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → is_endc end = true →
-   ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨
+  λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+  ∀ls,x,xs.
+  nth src ? int (niltape ?) = midtape sig ls x xs →
+  ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨
     (∃ls0,rs0,xs0. nth dst ? int (niltape ?) = midtape sig ls0 x rs0 ∧
       xs = rs0@xs0 ∧
       current sig (nth dst (tape sig) outt (niltape sig)) = None ?) ∨
     (∃ls0,rs0. 
      nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧
-     ∀rsj,c. 
-     rs0 = c::rsj →
+     (* ∀rsj,c. 
+     rs0 = c::rsj → *)
      outt = change_vec ??
-            (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rs) src)
-            (midtape sig (reverse ? xs@x::ls0) c rsj) dst).
+            (change_vec ?? int (mk_tape sig (reverse ? xs@x::ls) (None ?) [ ]) src)
+            (mk_tape sig (reverse ? xs@x::ls0) (option_hd ? rs0) (tail ? rs0)) dst).
 
+(*definition R_match_step_true ≝ 
+  λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+  ∀s,rs.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → 
+  current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
+  (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →  
+   outt = change_vec ?? int 
+          (tape_move_mono … (nth dst ? int (niltape ?)) (〈Some ? s1,R〉)) dst) ∧  
+  (∀ls,x,xs,ci,rs,ls0,rs0. 
+    nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
+    nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
+    rs0 ≠ [] ∧
+    ∀cj,rs1.rs0 = cj::rs1 → 
+    ci ≠ cj →
+    (outt = change_vec ?? int 
+        (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst)). 
+*)
 definition R_match_step_true ≝ 
-  λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
+  λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
   ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → 
-  current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
-  (is_startc s = true → 
-   (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
-   (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →  
+  ∃s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 ∧
+  (left ? (nth src ? int (niltape ?)) = [ ] → 
+   (s ≠ s1 →  
     outt = change_vec ?? int 
-          (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧  
-   (∀ls,x,xs,ci,rs,ls0,rs0. 
-     nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
-     nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
-     (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → 
-     is_endc ci = false ∧ rs0 ≠ [] ∧
-     ∀cj,rs1.rs0 = cj::rs1 → 
-      ci ≠ cj →
-      (outt = change_vec ?? int 
-          (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))). 
-           
+          (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst) ∧
+   (∀xs,ci,rs,ls0,rs0. 
+    nth src ? int (niltape ?) = midtape sig [] s (xs@ci::rs) →
+    nth dst ? int (niltape ?) = midtape sig ls0 s (xs@rs0) →
+    rs0 ≠ [] ∧
+    ∀cj,rs1.rs0 = cj::rs1 → 
+    ci ≠ cj →
+    (outt = change_vec ?? int 
+        (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst))). 
+         
 lemma sem_match_step :
-  ∀src,dst,sig,n,is_startc,is_endc.src ≠ dst → src < S n → dst < S n → 
-  match_step src dst sig n is_startc is_endc ⊨ 
+  ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → 
+  match_step src dst sig n ⊨ 
     [ inr ?? (inr ?? (inl … (inr ?? start_nop))) : 
-      R_match_step_true src dst sig n is_startc is_endc, 
-      R_match_step_false src dst sig n is_endc ].
-#src #dst #sig #n #is_startc #is_endc #Hneq #Hsrc #Hdst 
-@(acc_sem_seq_app sig n … (sem_compare src dst sig n is_endc Hneq Hsrc Hdst)
-    (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ? is_endc))
+      R_match_step_true src dst sig n, 
+      R_match_step_false src dst sig n ].
+#src #dst #sig #n #Hneq #Hsrc #Hdst 
+@(acc_sem_seq_app sig n … (sem_compare src dst sig n Hneq Hsrc Hdst)
+    (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
       (sem_seq … 
-        (sem_parmoveL ???? is_startc Hneq Hsrc Hdst) 
+        (sem_parmoveL ???? Hneq Hsrc Hdst) 
         (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
       (sem_nop …)))
-[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * #Htest #Htd >Htd -Htd
- * #te * #Hte #Htb whd 
- #s #Hcurta_src % 
- [ lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) 
+[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * #Htest
+ * #te * #Hte #Htb #s #Hcurta_src whd
+ cut (∃s1.current sig (nth dst (tape sig) ta (niltape sig))=Some sig s1)
+ [ lapply Hcomp1 -Hcomp1 
+   lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
+   cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
+   [ #Hcurta_dst #Hcomp1 >Hcomp1 in Htest; // *
+     change with (vec_map ?????) in match (current_chars ???); whd in ⊢ (??%?→?);
+     <(nth_vec_map ?? (current ?) src ? ta (niltape ?))      
+     <(nth_vec_map ?? (current ?) dst ? ta (niltape ?))
+     >Hcurta_src >Hcurta_dst whd in ⊢ (??%?→?); #H destruct (H)
+   | #s1 #_ #_ %{s1} % ] ]
+ * #s1 #Hcurta_dst %{s1} % // #Hleftta %
+ [ #Hneqss1 -Hcomp2 cut (tc = ta) 
+   [@Hcomp1 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //] 
+    #H destruct (H) -Hcomp1 cut (td = ta)
+    [ cases Htest -Htest // ] #Htdta destruct (Htdta)
+    cases Hte -Hte #Hte #_
+    cases (current_to_midtape … Hcurta_src) #ls * #rs #Hmidta_src
+    cases (current_to_midtape … Hcurta_dst) #ls0 * #rs0 #Hmidta_dst
+    >Hmidta_src in Hleftta; normalize in ⊢ (%→?); #Hls destruct (Hls)
+    >(Hte s [ ] rs Hmidta_src ls0 s1 [ ] rs0 (refl ??) Hmidta_dst) in Htb;
+    * whd in ⊢ (%→?);
+    mid
+    
+      in Htb;
+    cut (te = ta) 
+    [ cases Htest -Htest #Htest #Htdta <Htdta @Hte %1 >Htdta @Hcurta_src %{s} % //] 
+    -Hte #H destruct (H) %
+    [cases Htb * #_ #Hmove #Hmove1 @(eq_vec … (niltape … ))
+     #i #Hi cases (decidable_eq_nat i dst) #Hidst
+      [ >Hidst >nth_change_vec // cases (current_to_midtape … Hcurta_dst)
+        #ls * #rs #Hta_mid >(Hmove … Hta_mid) >Hta_mid cases rs //
+      | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ]
+    | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src
+      >Hcurta_src in Htest; whd in ⊢ (??%?→?);
+      cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq // 
+    ]
+   <(nth_vec_map ?? (current ?) dst ? tc (niltape ?))   
+    >Hcurta_src normalize
+   lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) 
    cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
-   [| #c #_ % #Hfalse destruct (Hfalse) ]
+   [| #s1 #Hcurta_dst %
+     [ % #Hfalse destruct (Hfalse)
+     | #s1' #Hs1 destruct (Hs1) #Hneqss1 -Hcomp2 
+       cut (tc = ta) 
+       [@Hcomp1 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //] 
+       #H destruct (H) -Hcomp1 cases Hte -Hte #_ #Hte
+       cut (te = ta) [ cases Htest -Htest #Htest #Htdta <Htdta @Hte %1 %{s} % //] -Hte #H destruct (H) %
+       [cases Htb * #_ #Hmove #Hmove1 @(eq_vec … (niltape … ))
+        #i #Hi cases (decidable_eq_nat i dst) #Hidst
+         [ >Hidst >nth_change_vec // cases (current_to_midtape … Hcurta_dst)
+           #ls * #rs #Hta_mid >(Hmove … Hta_mid) >Hta_mid cases rs //
+         | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ]
+       | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src
+         >Hcurta_src in Htest; whd in ⊢ (??%?→?);
+         cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq // 
+       ]
+     
+      ]
    #Hcurta_dst >Hcomp1 in Htest; [| %2 %2 //]
    whd in ⊢ (??%?→?); change with (current ? (niltape ?)) in match (None ?);
     <nth_vec_map >Hcurta_src whd in ⊢ (??%?→?); <nth_vec_map
@@ -579,4 +691,110 @@ lapply (sem_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc
     ]
   ]
 ]
+qed.
+
+definition Pre_match_m ≝ 
+  λsrc,sig,n,is_startc,is_endc.λt: Vector (tape sig) (S n).
+  ∃start,xs,end.
+  nth src (tape sig) t (niltape sig) = midtape ? [] start (xs@[end]) ∧
+  is_startc start = true ∧
+  (∀c.c ∈ (xs@[end]) = true → is_startc c = false) ∧
+  (∀c.c ∈ (start::xs) = true → is_endc c = false) ∧
+  is_endc end = true.
+  
+lemma terminate_match_m :
+  ∀src,dst,sig,n,is_startc,is_endc,t.
+  src ≠ dst → src < S n → dst < S n → 
+  Pre_match_m src sig n is_startc is_endc t → 
+  match_m src dst sig n is_startc is_endc ↓ t.
+#src #dst #sig #n #is_startc #is_endc #t #Hneq #Hsrc #Hdst * #start * #xs * #end
+* * * * #Hmid_src #Hstart #Hnotstart #Hnotend #Hend
+@(terminate_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc Hdst)) //
+<(change_vec_same … t dst (niltape ?))
+lapply (refl ? (nth dst (tape sig) t (niltape ?))) 
+cases (nth dst (tape sig) t (niltape ?)) in ⊢ (???%→?);
+[ #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+  >Hmid_src #HR cases (HR ? (refl ??)) -HR
+  >nth_change_vec // >Htape_dst normalize in ⊢ (%→?);
+  * #H @False_ind @H %
+| #x0 #xs0 #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+  >Hmid_src #HR cases (HR ? (refl ??)) -HR
+  >nth_change_vec // >Htape_dst normalize in ⊢ (%→?);
+  * #H @False_ind @H %
+| #x0 #xs0 #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+  >Hmid_src #HR cases (HR ? (refl ??)) -HR
+  >nth_change_vec // >Htape_dst normalize in ⊢ (%→?);
+  * #H @False_ind @H %
+| #ls #s #rs lapply s -s lapply ls -ls lapply Hmid_src lapply t -t elim rs
+  [#t #Hmid_src #ls #s #Hmid_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+   >Hmid_src >nth_change_vec // >Hmid_dst #HR cases (HR ? (refl ??)) -HR #_
+   #HR cases (HR Hstart Hnotstart)
+   cases (true_or_false (start == s)) #Hs
+   [ lapply (\P Hs) -Hs #Hs <Hs #_ #Htrue
+     cut (∃ci,xs1.xs@[end] = ci::xs1)
+     [ cases xs
+       [ %{end} %{[]} %
+       | #x1 #xs1 %{x1} %{(xs1@[end])} % ] ] * #ci * #xs1 #Hxs
+     >Hxs in Htrue; #Htrue
+     cases (Htrue [ ] start [ ] ? xs1 ? [ ] (refl ??) (refl ??) ?)
+     [ * #_ * #H @False_ind @H % ]
+     #c0 #Hc0 @Hnotend >(memb_single … Hc0) @memb_hd
+   | lapply (\Pf Hs) -Hs #Hs #Htrue #_
+     cases (Htrue ? (refl ??) Hs) -Htrue #Ht1 #_ %
+     #t2 whd in ⊢ (%→?); #HR cases (HR start ?)
+     [ >Ht1 >nth_change_vec // normalize in ⊢ (%→?); * #H @False_ind @H %
+     | >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
+       >nth_change_vec_neq [|@sym_not_eq //] >Hmid_src % ]
+   ]
+  |#r0 #rs0 #IH #t #Hmid_src #ls #s #Hmid_dst % #t1 whd in ⊢ (%→?);
+   >nth_change_vec_neq [|@sym_not_eq //] >Hmid_src
+   #Htrue cases (Htrue ? (refl ??)) -Htrue #_ #Htrue
+   <(change_vec_same … t1 dst (niltape ?))
+   cases (Htrue Hstart Hnotstart) -Htrue
+   cases (true_or_false (start == s)) #Hs
+   [ lapply (\P Hs) -Hs #Hs <Hs #_ #Htrue
+    cut (∃ls0,xs0,ci,rs,rs0.
+      nth src ? t (niltape ?) = midtape sig [ ] start (xs0@ci::rs) ∧
+      nth dst ? t (niltape ?) = midtape sig ls0 s (xs0@rs0) ∧
+      (is_endc ci = true ∨ (is_endc ci = false ∧ (∀b,tlb.rs0 = b::tlb → ci ≠ b))))
+    [cases (comp_list ? (xs@[end]) (r0::rs0) is_endc) #xs0 * #xs1 * #xs2
+      * * * #Hxs #Hrs #Hxs0notend #Hcomp >Hrs
+      cut (∃y,ys. xs1 = y::ys)
+      [ lapply Hxs0notend lapply Hxs lapply xs0 elim xs
+        [ *
+          [ normalize #Hxs1 <Hxs1 #_ %{end} %{[]} %
+          | #z #zs normalize in ⊢ (%→?); #H destruct (H) #H
+            lapply (H ? (memb_hd …)) -H >Hend #H1 destruct (H1)
+          ]
+        | #y #ys #IH0 * 
+          [ normalize in ⊢ (%→?); #Hxs1 <Hxs1 #_ %{y} %{(ys@[end])} %
+          | #z #zs normalize in ⊢ (%→?); #H destruct (H) #Hmemb
+            @(IH0 ? e0 ?) #c #Hc @Hmemb @memb_cons // ] ] ] * #y * #ys #Hxs1
+      >Hxs1 in Hxs; #Hxs >Hmid_src >Hmid_dst >Hxs >Hrs
+      %{ls} %{xs0} %{y} %{ys} %{xs2}
+      % [ % // | @Hcomp // ] ]
+    * #ls0 * #xs0 * #ci * #rs * #rs0 * * #Hmid_src' #Hmid_dst' #Hcomp
+    <Hmid_src in Htrue; >nth_change_vec // >Hs #Htrue destruct (Hs)
+    lapply (Htrue ??????? Hmid_src' Hmid_dst' ?) -Htrue
+    [ #c0 #Hc0 @Hnotend cases (orb_true_l … Hc0) -Hc0 #Hc0
+      [ whd in ⊢ (??%?); >Hc0 %
+      | @memb_cons >Hmid_src in Hmid_src'; #Hmid_src' destruct (Hmid_src')
+        lapply e0 -e0 @(list_elim_left … rs)
+        [ #e0 destruct (e0) lapply (append_l1_injective_r ?????? e0) //
+        | #x1 #xs1 #_ >append_cons in ⊢ (???%→?);
+          <associative_append #e0 lapply (append_l1_injective_r ?????? e0) //
+          #e1 >e1 @memb_append_l1 @memb_append_l1 // ] ]
+    | * * #Hciendc cases rs0 in Hcomp;
+      [ #_ * #H @False_ind @H %
+      | #r1 #rs1 * [ >Hciendc #H destruct (H) ]
+        * #_ #Hcomp lapply (Hcomp ?? (refl ??)) -Hcomp #Hcomp #_ #Htrue
+        cases (Htrue ?? (refl ??) Hcomp) #Ht1 #_ >Ht1 @(IH ?? (s::ls) r0)
+        [ >nth_change_vec_neq [|@sym_not_eq //]
+          >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
+        | >nth_change_vec // >Hmid_dst % ] ] ]
+  | >Hmid_dst >nth_change_vec // lapply (\Pf Hs) -Hs #Hs #Htrue #_
+    cases (Htrue ? (refl ??) Hs) #Ht1 #_ >Ht1 @(IH ?? (s::ls) r0)
+    [ >nth_change_vec_neq [|@sym_not_eq //]
+      >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
+    | >nth_change_vec // ] ] ] ]
 qed.
\ No newline at end of file