proposition: Lemma MoveM_Realise {Σ : finType} D (n : nat) : @MoveM Σ D n ⊨ MoveL_rel D n.
proof: Proof. induction n; unfold MoveL_rel; cbn. - eapply Realise_monotone. { now auto with nocore TMdb. } intros t ([], t') ->. rewrite (destruct_tape t). reflexivity. - eapply Realise_monotone. { eapply Seq_Realise. { eassumption. } { now auto with nocore TMdb. } } intros t ([], t') ?; cbn in *. TMSimp. reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString