proposition: Lemma MoveToSymbol_L_Terminates : projT1 MoveToSymbol_L ↓ (fun tin k => MoveToSymbol_L_steps (tin[@Fin0]) <= k).
proof: Proof. eapply TerminatesIn_monotone. - eapply Mirror_Terminates. eapply MoveToSymbol_Terminates. - cbn. intros tin k Hk. rewrite (destruct_tape tin) in *. cbn in *. rewrite <- Hk. unfold mirror_tapes. rewrite MoveToSymbol_steps_mirror. constructor. Qed.
imports: Undecidability(TM.Util.Prelim) Undecidability(TM.Basic.Mono) Undecidability(TM.Combinators.Combinators) Undecidability(TM.Compound.TMTac) Undecidability(TM.Compound.Multi) Coq(FunInd) Coq(Recdef)