proposition: Lemma MoveToSymbol_Terminates : projT1 MoveToSymbol ↓ (fun tin k => MoveToSymbol_steps (tin[@Fin0]) <= k).
proof: Proof. eapply TerminatesIn_monotone. { apply While_TerminatesIn. all: eapply Realise_total, MoveToSymbol_Step_Sem. } { apply WhileCoInduction; intros. cbn. exists 3. repeat split. - reflexivity. - intros ymid tmid. intros H. destruct ymid as [()| ]; TMSimp. + destruct (current _) eqn:E; TMSimp; auto. * destruct (f e) eqn:Ef; inv H0. rewrite MoveToSymbol_steps_equation in HT. rewrite E, Ef in HT. lia. * rewrite MoveToSymbol_steps_equation in HT. rewrite E in HT. lia. + destruct (current _) eqn:E. * destruct (f e) eqn:Ef; inv H0. rewrite MoveToSymbol_steps_equation in HT. rewrite E, Ef in HT. eexists (MoveToSymbol_steps (doAct _ (Some (g e), Rmove))). cbn. split. -- unfold MoveToSymbol_Step_Fun. rewrite E, Ef. cbn. reflexivity. -- rewrite <- HT. cbn. lia. * congruence. } 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)