proposition: Lemma DoActions_Realise : DoActions ⊨ DoActions_Rel.
proof: Proof. clear pM F. unfold DoActions. destruct (finMin_opt n) as [ i | ] eqn:E; swap 1 2. { eapply Realise_monotone. { now auto with nocore TMdb. } { intros tin ([], tout) H. intros tps HL HStart. cbn in *. intros. TMSimp. unfold atStart in HStart. TMSimp. apply finMin_opt_None in E as ->. destruct tps; cbn in *; inv HL. hnf. cbn. reflexivity. } } { eapply Realise_monotone. { now auto with nocore TMdb. } { intros tin ([], tout) H. intros tps HL HStart. TMSimp. rename H0 into HLoop_Nil, H1 into HLoop_Cons. clear HLoop_Cons. pose proof finMin_opt_Some E as (n'&E'). apply finMin_opt_Some_val in E. subst. destruct tps as [ | tp tps]; cbn in *. inv HL. specialize (HLoop_Nil nil tps tp). spec_assert HLoop_Nil by now rewrite E. spec_assert HLoop_Nil by auto. spec_assert HLoop_Nil. { cbn. unfold atStart in HStart. TMSimp. hnf. f_equal. now rewrite map_app, <- app_assoc. } rewrite (Vector.eta acts) in *. assumption. } } 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)