proposition: Lemma DoActions_Terminates : projT1 DoActions ↓ DoActions_T.
proof: Proof. clear pM F. unfold DoActions. unfold DoActions_T, DoActions_steps. destruct (finMin_opt n) as [ i | ] eqn:Ei. { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } { intros tin k. intros (tps&HL&HStart&Hk). hnf in HStart. TMSimp. destruct tps as [ | tp tps]; cbn in *. { exfalso. clear acts Hk. destruct n; cbn in *; congruence. } exists 1, (DoActions_Loop_steps_cons i [] tps tp). repeat split; try lia. intros tmid () H. hnf. left. TMSimp. exists nil, tps, tp. cbn. rewrite (finMin_opt_Some_val Ei). repeat split; auto. hnf. now simpl_list. } } { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } now intros tin k (?&?&?&H). } 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)