proposition: Lemma DoAction_Realise (d : option move) (a : option sig * move) : DoAction d a ⊨ DoAction_Rel d a.
proof: Proof. unfold DoAction. destruct a as [[ w | ] m]; cbn. { eapply Realise_monotone. { now auto with nocore TMdb. } intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. TMSimp. rename H into HWrite, H0 into HMove. specialize HWrite with (1 := eq_refl) (2 := HCons). specialize (HMove tps1 tps2 (midtape (left tp) w (right tp))). cbn in *. auto. } { eapply Realise_monotone. { now auto with nocore TMdb. } intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. TMSimp. specialize H with (1 := eq_refl) (2 := HCons). auto. } 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)