proposition: Corollary MoveToSymbol_L_steps_moveleft ls ls' x m rs : stop x = true -> MoveToSymbol_L_steps stop f (tape_move_left' (ls ++ x :: ls') m rs) <= 4 + 4 * length ls.
proof: Proof. intros HStop. destruct ls as [ | s s'] eqn:E; cbn. - rewrite MoveToSymbol_L_steps_equation. cbn. rewrite HStop; cbn. lia. - rewrite MoveToSymbol_L_steps_midtape; auto. lia. 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)