proposition: Lemma DoAction_Terminates (d : option move) (a : option sig * move) : projT1 (DoAction d a) ↓ DoAction_T d a.
proof: Proof. unfold DoAction. destruct a as [ [ w | ] m]; cbn in *. { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } { intros tin k. intros (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. exists (DoWrite_steps d tps1 tps2), DoMove_steps. repeat split; try lia. { hnf. do 3 eexists. repeat split; eauto. } } } { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } { intros tin k. intros (tps1&tps2&tp&HDir&HCons&Hk). cbn 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)