proposition: Lemma DoActions_Step_Realise (i : Fin.t n) : DoActions_Step i ⊨ DoActions_Step_Rel i.
proof: Proof. eapply Realise_monotone. { unfold DoActions_Step. now auto with nocore TMdb. } { intros tin (yout, tout) H; split. { intros tps1 tps2 tp HL1 HL2 HCons. TMSimp. destruct H; TMSimp; swap 1 2. { specialize H with (1 := HCons) as (_&?). congruence. } rename H into HIsCons, H0 into HGoToCurrent, H3 into HDoAct, H4 into HDoActs_Step. specialize HIsCons with (1 := HCons) as (HIsCons&_). specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent1&->). apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2. specialize HDoAct with (1 := eq_refl) (2 := HGoToCurrent1). specialize HDoActs_Step with (1 := HDoAct). destruct tps2 as [ | tp' tps2']; (destruct ymid0; auto; try easy). - split; auto. cbn in *. unshelve epose proof @finSucc_opt_None n i _ as ->. lia. reflexivity. - split; auto. cbn in *. unshelve epose proof @finSucc_opt_Some n i _ as (i'&->). lia. reflexivity. } { intros tps HNil. destruct H; TMSimp. { specialize H1 with (1 := HNil) as (_&?). congruence. } now specialize H2 with (1 := HNil) as (HIsNil&_). } } 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)