- (sem_parmoveL ???? is_startc Hneq Hsrc Hdst)
- (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
- (sem_nop …)))
-[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * * #c * #Hcurtc #Hcend #Htd >Htd -Htd
- #Htb #s #Hcurta_src #Hstart #Hnotstart %
- [ #s1 #Hcurta_dst #Hneqss1
- lapply Htb lapply Hcurtc -Htb -Hcurtc >(?:tc=ta)
- [|@Hcomp1 %2 % % >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) % ]
- #Hcurtc * #te * * #_ #Hte >Hte // whd in ⊢ (%→?); * * #_ #Htbdst #Htbelse %
- [ @(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 >(Htbdst … Hta_mid) >Hta_mid cases rs //
- | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Htbelse @sym_not_eq // ]
- | >Hcurtc in Hcurta_src; #H destruct (H) cases (is_endc s) in Hcend;
- normalize #H destruct (H) // ]
- |#ls #x #xs #ci #rs #ls0 #cj #rs0 #Htasrc_mid #Htadst_mid #Hcicj #Hnotendc
- cases (Hcomp2 … Htasrc_mid Htadst_mid Hnotendc) [ * #H destruct (H) ]
- * #cj' * #rs0' * #Hcjrs0 destruct (Hcjrs0) -Hcomp2 #Hcomp2
- lapply (Hcomp2 (or_intror ?? Hcicj)) -Hcomp2 #Htc
- cases Htb #td * * #Htd #_ >Htasrc_mid in Hcurta_src; normalize in ⊢ (%→?);
- #H destruct (H)
- >(Htd ls ci (reverse ? xs) rs s ??? ls0 cj' (reverse ? xs) s rs0' (refl ??)) //
- [| >Htc >nth_change_vec //
- | #c0 #Hc0 @(Hnotstart c0) >Htasrc_mid
- cases (orb_true_l … Hc0) -Hc0 #Hc0
- [@memb_append_l2 >(\P Hc0) @memb_hd
- |@memb_append_l1 <(reverse_reverse …xs) @memb_reverse //
- ]
- | >Htc >nth_change_vec_neq [|@sym_not_eq // ] @nth_change_vec // ]
- * * #_ #Htbdst #Htbelse %
- [ @(eq_vec … (niltape ?)) #i #Hi cases (decidable_eq_nat i dst) #Hidst
- [ >Hidst >nth_change_vec // >Htadst_mid >(Htbdst ls0 s (xs@cj'::rs0'))
- [ cases xs //
- | >nth_change_vec // ]
- | >nth_change_vec_neq [|@sym_not_eq //]
- <Htbelse [|@sym_not_eq // ]
- >nth_change_vec_neq [|@sym_not_eq //]
- cases (decidable_eq_nat i src) #Hisrc
- [ >Hisrc >nth_change_vec // >Htasrc_mid //
- | >nth_change_vec_neq [|@sym_not_eq //]
- <(Htbelse i) [|@sym_not_eq // ]
- >Htc >nth_change_vec_neq [|@sym_not_eq // ]
- >nth_change_vec_neq [|@sym_not_eq // ] //
- ]
- ]
- | >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // whd in ⊢ (??%?→?);
- #H destruct (H) cases (is_endc c) in Hcend;
- normalize #H destruct (H) // ]
- ]
-|#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb
- whd in ⊢ (%→?); #Hout >Hout >Htb whd
- #ls #c_src #xs #end #rs #Hmid_src #Hnotend #Hend
- lapply (current_to_midtape sig (nth dst ? intape (niltape ?)))
- cases (current … (nth dst ? intape (niltape ?))) in Hcomp1;
- [#Hcomp1 #_ %1 % [% | @Hcomp1 %2 %2 % ]
- |#c_dst cases (true_or_false (c_src == c_dst)) #Hceq
- [#_ #Hmid_dst cases (Hmid_dst c_dst (refl …)) -Hmid_dst
- #ls_dst * #rs_dst #Hmid_dst %2
- cases (comp_list … (xs@end::rs) rs_dst is_endc) #xs1 * #rsi * #rsj * * *
- #Hrs_src #Hrs_dst #Hnotendxs1 #Hneq %{ls_dst} %{rsj} >Hrs_dst in Hmid_dst; #Hmid_dst
- cut (∃r1,rs1.rsi = r1::rs1) [@daemon] * #r1 * #rs1 #Hrs1 >Hrs1 in Hrs_src;
- #Hrs_src >Hrs_src in Hmid_src; #Hmid_src <(\P Hceq) in Hmid_dst; #Hmid_dst
- lapply (Hcomp2 ??????? Hmid_src Hmid_dst ?)
- [ #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @Hnotend @memb_hd | @Hnotendxs1 //]
- | *
- [ * #Hrsj #Hta %
- [ >Hta in Hc; >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- #Hc lapply (Hc ? (refl ??)) #Hendr1
- cut (xs = xs1)
- [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
- -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
- [ * normalize in ⊢ (%→?); //
- #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
- lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
- | #x2 #xs2 #IH *
- [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
- >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
- normalize in ⊢ (%→?); #H destruct (H)
- | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
- #Hnotendc #Hnotendcxs1 @eq_f @IH
- [ @(cons_injective_r … Heq)
- | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @memb_hd
- | @memb_cons @memb_cons // ]
- | #c #Hc @Hnotendcxs1 @memb_cons // ]
- ]
- ]
- | #Hxsxs1 >Hmid_dst >Hxsxs1 % ]
- | #rsj0 #c >Hrsj #Hrsj0 destruct (Hrsj0) ]
- | * #cj * #rs2 * #Hrs2 #Hta lapply (Hta ?)
- [ cases (Hneq … Hrs1) /2/ #H %2 @(H ?? Hrs2) ]
- -Hta #Hta >Hta in Hc; >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // #Hc lapply (Hc ? (refl ??)) #Hendr1
- (* lemmatize this proof *) cut (xs = xs1)
- [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
- -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
- [ * normalize in ⊢ (%→?); //
- #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
- lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
- | #x2 #xs2 #IH *
- [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
- >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
- normalize in ⊢ (%→?); #H destruct (H)
- | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
- #Hnotendc #Hnotendcxs1 @eq_f @IH
- [ @(cons_injective_r … Heq)
- | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @memb_hd
- | @memb_cons @memb_cons // ]
- | #c #Hc @Hnotendcxs1 @memb_cons // ]
- ]
- ]
- | #Hxsxs1 >Hmid_dst >Hxsxs1 % //
- #rsj0 #c #Hcrsj destruct (Hxsxs1 Hrs2 Hcrsj) @eq_f3 //
- @eq_f3 // lapply (append_l2_injective ?????? Hrs_src) //
- #Hendr1 destruct (Hendr1) % ]
+ (sem_rewind_strong ???? Hneq Hsrc Hdst)
+ (sem_move_multi … R ?))
+ (sem_nop …))) [/2/]
+[ #ta #tb #tc * lapply (refl ? (current ? (nth src ? ta (niltape ?))))
+ cases (current ? (nth src ? ta (niltape ?))) in ⊢ (???%→%);
+ [ #Hcurta_src #Hcomp #_ * #td * >Hcomp [| % %2 %]
+ whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >nth_current_chars >Hcurta_src normalize in ⊢ (%→?); #H destruct (H)
+ | #s #Hs lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
+ cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
+ [ #Hcurta_dst #Hcomp #_ * #td * >Hcomp [| %2 %]
+ whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >nth_current_chars >nth_current_chars >Hs >Hcurta_dst
+ normalize in ⊢ (%→?); #H destruct (H)
+ | #s0 #Hs0
+ cases (current_to_midtape … Hs) #ls * #rs #Hmidta_src >Hmidta_src
+ cases (current_to_midtape … Hs0) #ls0 * #rs0 #Hmidta_dst >Hmidta_dst
+ cases (true_or_false (s == s0)) #Hss0
+ [ lapply (\P Hss0) -Hss0 #Hss0 destruct (Hss0)
+ #_ #Hcomp cases (Hcomp ????? (refl ??) (refl ??)) -Hcomp [ *
+ [ * #rs' * #_ #Hcurtc_dst * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >nth_current_chars >nth_current_chars >Hcurtc_dst
+ cases (current ? (nth src …))
+ [normalize in ⊢ (%→?); #H destruct (H)
+ | #x >nth_change_vec [|@Hdst] cases (reverse ? rs0)
+ [ normalize in ⊢ (%→?); #H destruct (H)
+ | #r1 #rs1 normalize in ⊢ (%→?); #H destruct (H) ] ]
+ | * #rs0' * #_ #Hcurtc_src * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >(?:nth src ? (current_chars ?? tc) (None ?) = None ?)
+ [|>nth_current_chars >Hcurtc_src >nth_change_vec_neq
+ [>nth_change_vec [cases (append ???) // | @Hsrc]
+ |@(not_to_not … Hneq) //
+ ]]
+ normalize in ⊢ (%→?); #H destruct (H) ]
+ | * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0
+ #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * * *
+ >Htc >change_vec_commute [|//] >nth_change_vec [|//]
+ >change_vec_commute [|@sym_not_eq //] >nth_change_vec [|//]
+ cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
+ destruct (Hlsalsb) *
+ [ #Hte #_ #_ <(reverse_reverse … ls) in Hte; <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte #_
+ lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
+ >change_vec_commute [|//] >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
+ >Hte whd in ⊢ (%→?); >change_vec_change_vec >nth_change_vec [|//]
+ >reverse_reverse #Htb
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [ ] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst)
+ [ >Htb @eq_f3 // cases (xs@cj::rs0') // ]
+ -Htb #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec [|//]
+ >right_mk_tape [|cases xs [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H)]
+ normalize in match (left ??);
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
+ whd in match (option_cons ???); >Hrs0
+ normalize in ⊢ (?(?%)%); //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte
+ lapply (Hte ci hdb (reverse ? xs@s0::reverse ? tlb) rs'' ?
+ lsb cj hda (reverse ? xs@s0::reverse ? tla) rs0' ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_append >length_append @eq_f @(eq_f ?? S)
+ >H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
+ >length_reverse >length_reverse destruct (Hlen') //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte #_ whd in ⊢ (%→?); #Htb
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0'))) dst)
+ (midtape ? [ ] hdb (reverse sig (reverse sig xs@s0::reverse sig tlb)@ci::rs'')) src)
+ [ >Htb >Hte >nth_change_vec // >change_vec_change_vec >change_vec_commute [|//]
+ >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+ >change_vec_change_vec >change_vec_commute [|//]
+ @eq_f3 // cases (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0') // ]
+ -Htb #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig xs@s0::reverse sig tla))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand whd in match (option_cons ???);
+ >Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse
+ >length_append >commutative_plus in match (|reverse ??| + ?);
+ whd in match (|?::?|); >length_reverse >length_reverse
+ <(length_reverse ? ls) <Hlen' >H1 normalize // ]
+ | #_ #Hte #_ <(reverse_reverse … ls0) in Hte; <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls0|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #Hte
+ lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
+ >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+ >change_vec_change_vec #Hte #_
+ >Hte whd in ⊢ (%→?); >nth_change_vec [|//] >reverse_reverse #Htb
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst)
+ (midtape ? lsb s0 (xs@ci::rs'')) src)
+ [ >Htb >change_vec_change_vec >change_vec_commute [|//]
+ @eq_f3 // <Hrs0 cases rs0 // ]
+ -Htb #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases xs [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ normalize in match (left ??);
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand >Hrs0
+ >length_append normalize >length_append >length_append
+ <(reverse_reverse ? lsa) >H1 normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte
+ lapply (Hte cj hdb (reverse ? xs@s0::reverse ? tlb) rs0' ?
+ lsb ci hda (reverse ? xs@s0::reverse ? tla) rs'' ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_append >length_append @eq_f @(eq_f ?? S)
+ >H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
+ >length_reverse >length_reverse destruct (Hlen') //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte #_ whd in ⊢ (%→?); >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0'))) dst)
+ (midtape ? lsb hda (reverse sig (reverse sig xs@s0::reverse sig tla)@ci::rs'')) src)
+ [ >Htb >change_vec_change_vec >change_vec_commute [|//]
+ >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+ >change_vec_change_vec >change_vec_commute [|//]
+ @eq_f3 // cases (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0') // ]
+ -Htb #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig xs@s0::reverse sig tlb))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand
+ whd in match (option_cons ???);
+ >Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse
+ >length_append >commutative_plus in match (|reverse ??| + ?);
+ whd in match (|?::?|); >length_reverse >length_reverse
+ <(length_reverse ? lsa) >Hlen' >H2 >length_append
+ normalize //
+ ]
+ ]
+ ]
+ | lapply (\Pf Hss0) -Hss0 #Hss0 #Htc cut (tc = ta)
+ [@Htc % % @(not_to_not ??? Hss0) #H destruct (H) %]
+ -Htc #Htc destruct (Htc) #_ * #td * whd in ⊢ (%→?); * #_
+ #Htd destruct (Htd) * #te * * * * >Hmidta_src >Hmidta_dst
+ cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
+ destruct (Hlsalsb)
+ [ <(reverse_reverse … ls) <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 -H1 -H2 #_ #_ normalize in match (reverse ? [ ]); #Hte #_
+ lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte)
+ whd in ⊢ (%→?); >Hmidta_dst #Htb
+ cut (tb = change_vec ?? ta (mk_tape ? (s0::lsa@lsb) (option_hd ? rs0) (tail ? rs0)) dst)
+ [ >Htb cases rs0 // ]
+ -Htb #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
+ >right_mk_tape
+ [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H)] ]
+ normalize in match (left ??); normalize in match (right ??);
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
+ normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons >associative_append #Hte
+ lapply (Hte ???? (refl ??) ? s0 ? (reverse ? tla) ?? (refl ??))
+ [ >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
+ normalize #H destruct (H) // ] #Hte #_ #_ #_
+ whd in ⊢ (%→?); >Hte >change_vec_change_vec >nth_change_vec // #Htb
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig tla)@s0::rs0)) (tail ? (reverse sig (reverse sig tla)@s0::rs0))) dst)
+ (midtape ? [ ] hdb (reverse sig (reverse sig tlb)@s::rs)) src)
+ [ >Htb >change_vec_commute [|//] @eq_f3 // cases (reverse sig (reverse sig tla)@s0::rs0) // ]
+ -Htb #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig tla))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand >length_append
+ >length_reverse >length_reverse <(length_reverse ? ls) <Hlen'
+ >H1 normalize // ]
+ | #_ <(reverse_reverse … ls0) <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls0|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #_ #_ #Hte
+ lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte)
+ whd in ⊢ (%→?); #Htb whd >Hmidta_dst
+ cut (tb = change_vec (tape sig) (S n) ta (mk_tape ? (s0::ls0) (option_hd ? rs0) (tail ? rs0)) dst)
+ [ >Htb >Hmidta_dst cases rs0 // ]
+ -Htb #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
+ >current_mk_tape >right_mk_tape
+ [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H) ]]
+ normalize in ⊢ (??%); <opt_cons_tail_expand
+ normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte #_ #_
+ lapply (Hte s0 hdb (reverse ? tlb) rs0 ?
+ lsb s hda (reverse ? tla) rs ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
+ normalize #H destruct (H) //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte whd in ⊢ (%→?); >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig tlb)@s0::rs0)) (tail ? (reverse sig (reverse sig tlb)@s0::rs0))) dst)
+ (midtape ? lsb hda (reverse sig (reverse sig tla)@s::rs)) src)
+ [ >Htb >change_vec_commute [|//] >change_vec_change_vec
+ @eq_f3 // cases (reverse sig (reverse sig tlb)@s0::rs0) // ]
+ -Htb #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse ? (reverse ? tlb)) [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand >length_append
+ normalize in ⊢ (??%); >length_append >reverse_reverse
+ <(length_reverse ? lsa) >Hlen' >H2 normalize //
+ ]