proposition: Lemma MoveToStart_Terminates : projT1 MoveToStart ↓ MoveToStart_T.
proof: Proof. eapply TerminatesIn_monotone. { unfold MoveToStart. now auto with nocore TMdb. } { intros tin k (tps&HNil&Hk). hnf in HNil. TMSimp. rewrite MoveToSymbol_L_steps_midtape; cbn; auto. simpl_list. cbn. rewrite <- Hk. rewrite removelast_length. unfold MoveToStart_steps. lia. } Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)