proposition: Lemma MoveToSymbol_steps_local_end t : (forall x, List.In x (tape_local t) -> stop x = false) -> MoveToSymbol_steps stop f t <= 4 + 4 * length (tape_local t).
proof: Proof. remember (tape_local t) as tr eqn:Ht. induction tr in t,Ht |-*;intros Hhalt. all: specialize (tape_local_nil t) as Hcur. - rewrite MoveToSymbol_steps_equation. destruct Hcur as [-> _]. all:easy. - rewrite <- Ht in Hcur. destruct (current t) eqn:Hcur'. 2:{ exfalso. destruct Hcur as [? H']. now discriminate H'. } rewrite MoveToSymbol_steps_equation. rewrite Hcur'. rewrite Hhalt. 2:{ destruct t;inv Hcur'. inv Ht. now trivial with list. } apply Nat.add_le_mono_l. etransitivity. { apply IHtr. - cbn. rewrite tape_local_move_right'. symmetry in Ht. erewrite tape_local_right;eauto. - intros. eapply Hhalt. eauto with list. } 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)