proposition: Lemma Loop_Terminates q : projT1 (Loop q) ↓ Loop_T q.
proof: Proof. eapply TerminatesIn_monotone. { unfold Loop. now auto with nocore TMdb. } { revert q. apply StateWhileCoInduction; intros q; intros. destruct HT as (T&kn&outc&HLoop&HEncT&Hk). rewrite Loop_steps_eq in Hk. unfold Step_T, Step_Rel. destruct (halt q) eqn:E; cbn in *. - exists 0. split; auto. intros ymid tmid HStep. specialize HStep with (1 := HEncT) as (HStep&->). auto. - destruct kn as [ | kn']; cbn in *. + unfold haltConf in HLoop. cbn in HLoop. rewrite E in HLoop. congruence. + unfold haltConf in HLoop. cbn in HLoop. rewrite E in HLoop. destruct (trans (q, current_chars T)) as [q' acts] eqn:E2. exists (Step_steps q T). repeat split. eauto. intros ymid tmid HStep. specialize HStep with (1 := HEncT). assert (step (mk_mconfig q T) = mk_mconfig q' (doAct_multi T acts)) as Hstep. { unfold step. cbn. rewrite E2. reflexivity. } rewrite Hstep in HStep. destruct HStep as (HStep&->). exists (Loop_steps q' (doAct_multi T acts) kn'). repeat split; auto. hnf. do 3 eexists. repeat split. 2: eauto. rewrite <- Hstep. all: now eauto. } Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)