proposition: Lemma Shift_L_TerminatesIn (s : sig) : projT1 (Shift_L s) ↓ (fun tin k => Shift_steps (tape_local_l tin[@Fin0]) <= k).
proof: Proof. eapply TerminatesIn_monotone. { unfold Shift_L. apply Mirror_Terminates, Shift_TerminatesIn. } { intros tin k Hk. hnf. now simpl_tape in *. } 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)