+definition R_restart_tape ≝ λi,n.λint,outt:Vector (tape FSUnialpha) (S n).
+ ∀t.t = nth i ? int (niltape ?) →
+ outt = change_vec ?? int
+ (mk_tape ? [ ] (option_hd ? (list_of_tape ? t)) (tail ? (list_of_tape ? t))) i.
+
+lemma sem_restart_tape : ∀i,n.i < S n → restart_tape i n ⊨ R_restart_tape i n.
+#i #n #Hleq
+@(sem_seq_app ??????? (sem_move_multi ? n i L ?)
+ (sem_seq ?????? (sem_inject ???? i ? (sem_move_to_end_l ?))
+ (sem_move_multi ? n i R ?))) [1,2,3:@le_S_S_to_le //]
+#ta #tb * #tc * whd in ⊢ (%→?); #Htc
+* #td * * * #Htd1 #Htd2 #Htd3
+whd in ⊢ (%→?); #Htb *
+[ #Hta_i <Hta_i in Htc; whd in ⊢ (???(????%?)→?); #Htc
+ cut (td = tc)
+ [ <(change_vec_same … tc … i … (niltape ?))
+ @(eq_vec_change_vec … (niltape ?))
+ [ @Htd1 >Htc >nth_change_vec //
+ | @Htd3 ] ]
+ (* >Htc in Htd1; >nth_change_vec // *) -Htd1 -Htd2 -Htd3
+ #Htd >Htd in Htb; >Htc >change_vec_change_vec >nth_change_vec //
+ #Htb >Htb %
+| #r0 #rs0 #Hta_i <Hta_i in Htc; whd in ⊢ (???(????%?)→?); #Htc
+ cut (td = tc)
+ [ <(change_vec_same … tc … i … (niltape ?))
+ @(eq_vec_change_vec … (niltape ?))
+ [ @Htd1 >Htc >nth_change_vec //
+ | @Htd3 ] ]
+ (* >Htc in Htd1; >nth_change_vec // *) -Htd1 -Htd2 -Htd3
+ #Htd >Htd in Htb; >Htc >change_vec_change_vec >nth_change_vec //
+ #Htb >Htb %
+| #l0 #ls0 #Hta_i <Hta_i in Htc; whd in ⊢ (???(????%?)→?); #Htc
+ cut (td = change_vec ?? tc (mk_tape ? [ ] (None ?) (reverse ? ls0@[l0])) i)
+ [ <(change_vec_same … tc … i … (niltape ?))
+ @(eq_vec_change_vec … (niltape ?))
+ [ @Htd2 >Htc >nth_change_vec //
+ | #j #Hij >nth_change_vec_neq // @Htd3 // ]]
+ #Htd >Htd in Htb; >Htc >change_vec_change_vec >change_vec_change_vec
+ >nth_change_vec // #Htb >Htb <(reverse_reverse ? ls0) in ⊢ (???%);
+ cases (reverse ? ls0)
+ [ %
+ | #l1 #ls1 >reverse_cons
+ >(?: list_of_tape ? (rightof ? l0 (reverse ? ls1@[l1])) =
+ l1::ls1@[l0])
+ [|change with (reverse ??@?) in ⊢ (??%?);
+ whd in match (left ??); >reverse_cons >reverse_append
+ whd in ⊢ (??%?); @eq_f >reverse_reverse normalize >append_nil % ] % ]
+| *
+ [ #c #rs #Hta_i <Hta_i in Htc; whd in ⊢ (???(????%?)→?); #Htc
+ cut (td = tc)
+ [ <(change_vec_same … tc … i … (niltape ?))
+ @(eq_vec_change_vec … (niltape ?))
+ [ @Htd1 >Htc >nth_change_vec //
+ | @Htd3 ] ]
+ (* >Htc in Htd1; >nth_change_vec // *) -Htd1 -Htd2 -Htd3
+ #Htd >Htd in Htb; >Htc >change_vec_change_vec >nth_change_vec //
+ #Htb >Htb %
+ | #l0 #ls0 #c #rs #Hta_i <Hta_i in Htc; whd in ⊢ (???(????%?)→?); #Htc
+ cut (td = change_vec ?? tc (mk_tape ? [ ] (None ?) (reverse ? ls0@l0::c::rs)) i)
+ [ @(eq_vec_change_vec … (niltape ?))
+ [ @Htd2 >Htc >nth_change_vec //
+ | @Htd3 ] ]
+ #Htd >Htd in Htb; >Htc >change_vec_change_vec >change_vec_change_vec
+ >nth_change_vec // #Htb >Htb <(reverse_reverse ? ls0) in ⊢ (???%);
+ cases (reverse ? ls0)
+ [ %
+ | #l1 #ls1 >reverse_cons
+ >(?: list_of_tape ? (midtape ? (l0::reverse ? ls1@[l1]) c rs) =
+ l1::ls1@l0::c::rs)
+ [|change with (reverse ??@?) in ⊢ (??%?);
+ whd in match (left ??); >reverse_cons >reverse_append
+ whd in ⊢ (??%?); @eq_f >reverse_reverse normalize
+ >associative_append % ] % ]
+ ]
+]
+qed.