proposition: Lemma DoActions_Step_Terminates (i : Fin.t n) : projT1 (DoActions_Step i) ↓ DoActions_Step_T i.
proof: Proof. eapply TerminatesIn_monotone. { unfold DoActions_Step. now auto with nocore TMdb. } { intros tin k [ (tps1&tps2&tp&HL1&HL2&HCons&Hk) | (tps&HNil&Hk) ]. { unfold DoActions_Step_steps_cons in Hk. exists (IsCons_steps), (2 + GoToCurrent_steps tp + DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2 + GoToNext_steps (doAct tp acts[@i])). repeat split; try lia. intros tmid ymid (HIsCons_cons&_). specialize HIsCons_cons with (1 := HCons) as (HIsCons&->). exists (GoToCurrent_steps tp), (1 + DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2 + GoToNext_steps (doAct tp acts[@i])). repeat split; try lia. { hnf. eauto. } intros tmid0 ymid0 HGoToCurrent. cbn in HGoToCurrent. specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent&->). exists (DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2), (GoToNext_steps (doAct tp acts[@i])). repeat split; try lia. { hnf. eauto 6. } intros tmid1 ymid1 HDoAction. cbn in HDoAction. specialize HDoAction with (1 := eq_refl) (2 := HGoToCurrent). { hnf. eauto. } } { unfold DoActions_Step_steps_nil in Hk. exists IsCons_steps, 0. repeat split; try lia. intros tmid ymid (_&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)