proposition: Lemma GoToNext_Terminates : projT1 GoToNext ↓ GoToNext_T.
proof: Proof. eapply TerminatesIn_monotone. { unfold GoToNext. now auto with nocore TMdb. } { intros tin k (tps1&tps2&tp&HCons&Hk). hnf in HCons. unfold GoToNext_steps in Hk. exists (GoToNext_steps' tp), 2. repeat split. 2: lia. 2: intros _ _ _; reflexivity. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp. { destruct tps2 as [ | tp' tps2']; cbn in *. - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity. - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity. } { destruct tps2 as [ | tp' tps2']; cbn in *. - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))). rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. cbn. lia. - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))). rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. cbn. lia. } { destruct tps2 as [ | tp' tps2']; cbn in *. - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity. - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity. } { destruct tps2 as [ | tp' tps2']; cbn in *. - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. cbn. lia. - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. cbn. lia. } } 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)