proposition: Lemma MoveToSymbol_steps_local t r1 sym r2 : tape_local t = r1 ++ sym :: r2 -> stop sym = true -> MoveToSymbol_steps stop f t <= 4 + 4 * length r1.
proof: Proof. revert t sym r2. induction r1; intros t sym r2 HEnc HStop; cbn -[plus mult] in *. - destruct t; cbn in HEnc; inv HEnc. rewrite MoveToSymbol_steps_equation. cbn. rewrite HStop. cbn. lia. - destruct t; cbn in HEnc; try congruence. inv HEnc. rewrite MoveToSymbol_steps_equation. cbn. destruct (stop a). + lia. + apply Nat.add_le_mono_l. replace (4 * S (|r1|)) with (4 + 4 * |r1|) by lia. eapply IHr1; eauto. cbn. now simpl_tape. 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)