proposition: Corollary ToSingleTape_Terminates' : projT1 pM ↓ M_T -> projT1 ToSingleTape ↓ ToSingleTape_T'.
proof: Proof. intros HTerm. eapply TerminatesIn_monotone. { apply ToSingleTape_Terminates. } { intros tin k (T&kn&HEncT&HT&Hk). hnf. hnf in HTerm. specialize (HTerm _ _ HT) as (oconf&HLoop). do 3 eexists. repeat split; eauto. } 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)