proposition: Corollary MoveToSymbol_steps_midtape_end tl c tr : (forall x, List.In x (c::tr) -> stop x = false) -> MoveToSymbol_steps stop f (midtape tl c tr) <= 8 + 4 * length tr.
proof: Proof. intros. rewrite MoveToSymbol_steps_local_end. 2:easy. cbn. nia. 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)