proposition: Lemma MoveM_isTotal {Σ : finType} D (n : nat) : isTotal (@MoveM Σ D n).
proof: Proof. induction n; cbn. - eexists. now auto with nocore TMdb. - destruct IHn as [c IH]. eexists. eapply TerminatesIn_monotone. { now auto with nocore TMdb. } intros ? ? ?. repeat eexists. { apply Nat.le_refl. } { eapply H. } intros. apply Nat.le_refl. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString