proposition: Lemma Shift_TerminatesIn (s : sig) : projT1 (Shift s) ↓ (fun tin k => Shift_steps (tape_local tin[@Fin0]) <= k).
proof: Proof. eapply TerminatesIn_monotone. { apply StateWhile_TerminatesIn. - intros ?s. eapply RealiseIn_Realise. apply Shift_Step_Sem. - intros ?s. eapply RealiseIn_TerminatesIn. apply Shift_Step_Sem. } { revert s. apply StateWhileCoInduction; intros s; intros. exists 3. split; [reflexivity|]. intros [ s' | [] ]; intros; cbn in *. - destruct (current tin[@Fin0]) eqn:E. + destruct (f e) eqn:Ee; destruct H as [H H']; inv H'. destruct tin[@Fin0] eqn:E'; cbn in *; inv E. rewrite Ee in HT. rename l into ls, l0 into rs. TMSimp. simpl_tape. eexists. split; [reflexivity|]. lia. + destruct H. congruence. - destruct (current tin[@Fin0]) eqn:E. + destruct (f e) eqn:Ee; destruct H as [H H']; inv H'. destruct tin[@Fin0] eqn:E'; cbn in *; inv E. rename l into ls, l0 into rs. rewrite Ee in *. lia. + apply tape_local_nil in E. rewrite E in *. TMSimp. 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)