proposition: Lemma MoveToStart_Realise : MoveToStart ⊨ MoveToStart_Rel.
proof: Proof. eapply Realise_monotone. { unfold MoveToStart. now auto with nocore TMdb. } { intros tin (yout, tout) H. intros tps HNil. unfold atNil, atStart in *. TMSimp. clear. rewrite MoveToSymbol_L_correct_midtape; cbn; auto. - rewrite !map_id; cbv [id]. rewrite map_rev, rev_involutive. f_equal. change [inr (@sigList_nil (sigTape sig)); inl STOP] with (List.map inr [ @sigList_nil (sigTape sig)] ++ [inl STOP]). rewrite app_assoc, <- map_app. f_equal. f_equal. apply encode_list_remove. - intros ? (?&<-&?) % in_map_iff. cbn. reflexivity. } 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)