-definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
- mk_tape B (map ?? f (left ? t))
- (option_map ?? f (current ? t))
- (map ?? f (right ? t)).
-
-definition low ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
- [tape_map ?? bit (ctape ?? c);
- midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
- midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))
- ].
+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) [@daemon]
+ (* >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) [@daemon]
+ (* >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)
+ [@daemon]
+ #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) [@daemon]
+ (* >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)
+ [@daemon]
+ #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.