-(* commutation lemma for actions *)
-lemma map_action: ∀t,cout,m.
- tape_move ? (tape_write ? (tape_map FinBool ? bit t)
- (char_to_bit_option (low_char cout))) (char_to_move (low_mv m))
- = tape_map ?? bit (tape_move ? (tape_write ? t cout) m).
-#t #cout #m >map_write >map_move %
-qed.
-
-lemma map_move_mono: ∀t,cout,m.
- tape_move_mono ? (tape_map FinBool ? bit t)
- 〈char_to_bit_option (low_char cout), char_to_move (low_mv m)〉
- = tape_map ?? bit (tape_move_mono ? t 〈cout,m〉).
-@map_action
-qed.
-
-definition R_unistep_high ≝ λM:normalTM.λc:nconfig (no_states M).λt1,t2.
- t1 = low_tapes M c →
- t2 = low_tapes M (step ? M c).
-
-lemma R_unistep_equiv : ∀M,c,t1,t2.
- R_unistep (no_states M) (graph_enum ?? (ntrans M)) (nhalt M) t1 t2 →
- R_unistep_high M c t1 t2.
-#M #c #t1 #t2 #H #Ht1
-lapply (initial_bar ? (nhalt M) (graph_enum ?? (ntrans M)) (nTM_nog ?)) #Htable
-(* tup = current tuple *)
-cut (∃t.t = 〈〈cstate … c,current ? (ctape … c)〉,
- ntrans M 〈cstate … c,current ? (ctape … c)〉〉) [% //] * #tup #Htup
-(* tup is in the graph *)
-cut (mem ? tup (graph_enum ?? (ntrans M)))
- [@memb_to_mem >Htup @(graph_enum_complete … (ntrans M)) %] #Hingraph
-(* tupe target = 〈qout,cout,m〉 *)
-lapply (decomp_target ? (ntrans M 〈cstate … c,current ? (ctape … c)〉))
-* #qout * #cout * #m #Htg >Htg in Htup; #Htup
-(* new config *)
-cut (step FinBool M c = mk_config ?? qout (tape_move ? (tape_write ? (ctape … c) cout) m))
- [>(config_expand … c) whd in ⊢ (??%?); (* >Htg ?? why not?? *)
- cut (trans ? M 〈cstate … c, current ? (ctape … c)〉 = 〈qout,cout,m〉) [<Htg %] #Heq1
- >Heq1 %] #Hstep
-(* new state *)
-cut (cstate ?? (step FinBool M c) = qout) [>Hstep %] #Hnew_state
-(* new tape *)
-cut (ctape ?? (step FinBool M c) = tape_move ? (tape_write ? (ctape … c) cout) m)
- [>Hstep %] #Hnew_tape
-lapply(H (bits_of_state ? (nhalt M) (cstate ?? c))
- (low_char (current ? (ctape ?? c)))
- (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M)))
- ??????)
-[<Htable
- lapply(list_to_table … (nhalt M) …Hingraph) * #ll * #lr #Htable1 %{ll}
- %{(((bits_of_state ? (nhalt M) qout)@[low_char cout;low_mv m])@lr)}
- >Htable1 @eq_f <associative_append @eq_f2 // >Htup
- whd in ⊢ (??%?); @eq_f >associative_append %
-|>Ht1 >obj_low_tapes >map_list_of_tape elim (list_of_tape ??)
- [#b @False_ind | #b #tl #Hind #a * [#Ha >Ha //| @Hind]]
-|@sym_eq @Htable
-|>Ht1 %
-|%{(bits_of_state ? (nhalt M) (cstate ?? c))} %{(low_char (current ? (ctape ?? c)))}
- % [% [% [// | cases (current ??) normalize [|#b] % #Hd destruct (Hd)]
- |>length_map whd in match (length ??); @eq_f //]
- |//]
-|>Ht1 >cfg_low_tapes //] -H #H
-lapply(H (bits_of_state … (nhalt M) qout) (low_char … cout)
- (low_mv … m) tup ? Hingraph)
- [>Htup whd in ⊢ (??%?); @eq_f >associative_append %] -H
-#Ht2 >Ht2 @(eq_vec ? 3 … (niltape ?)) #i #Hi
-cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
- [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
- [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
- [@False_ind /2/
- |>Hi >obj_low_tapes >nth_change_vec //
- >Ht1 >obj_low_tapes >Hstep @map_action
- ]
- |>Hi >cfg_low_tapes >nth_change_vec_neq
- [|% whd in ⊢ (??%?→?); #H destruct (H)]
- >nth_change_vec // >Hnew_state @eq_f @eq_f >Hnew_tape
- @eq_f2 [|2:%] >Ht1 >obj_low_tapes >map_move_mono >low_char_current %
- ]
- |(* program tapes do not change *)
- >Hi >prg_low_tapes
- >nth_change_vec_neq [|% whd in ⊢ (??%?→?); #H destruct (H)]
- >nth_change_vec_neq [|% whd in ⊢ (??%?→?); #H destruct (H)]
- >Ht1 >prg_low_tapes //
+definition restart_tape ≝ λi,n.
+ mmove i FSUnialpha n L ·
+ inject_TM ? (move_to_end FSUnialpha L) n i ·
+ mmove i FSUnialpha n R.
+
+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 % ] % ]