proposition: Lemma ReadCurrentSymbols_Step_Terminates st : projT1 (ReadCurrentSymbols_Step st) ↓ ReadCurrentSymbols_Step_T.
proof: Proof. destruct st as [readSymbols i]. eapply TerminatesIn_monotone. { unfold ReadCurrentSymbols_Step. now auto with nocore TMdb. } { intros tin k. intros [ (tps1&tps2&tp&HCons&Hk) | (tps&HNil&Hk) ]. { unfold ReadCurrentSymbols_Step_steps_cons in Hk. exists (IsCons_steps), (2 + GoToCurrent_steps tp + ReadCurrent_steps + GoToNext_steps tp). repeat split; try lia. intros tmid ymid (HIsCons_cons&HIsCons_nil). specialize HIsCons_cons with (1 := HCons) as (HIsCons&->). exists (GoToCurrent_steps tp), (1 + ReadCurrent_steps + GoToNext_steps tp). (repeat split); [hnf; eauto|lia|]. intros tmid0 ymid0 HGoToCurrent. cbn in HGoToCurrent. specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent&->). exists (ReadCurrent_steps), (GoToNext_steps tp). repeat split; try lia. intros tmid1 ymid1 HReadCurrent. cbn in HReadCurrent. specialize HReadCurrent with (1 := HGoToCurrent) as (HReadCurrent&->). hnf. eauto. } { unfold ReadCurrentSymbols_Step_steps_nil in Hk. exists (IsCons_steps), 0. repeat split; try lia. intros tmid ymid (HIsCons_cons&HIsCons_nil). specialize HIsCons_nil with (1 := HNil) as (HIsNil&->). reflexivity. } } 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)