proposition: Corollary ToSingleTape_Realise' : pM ⊨ M_R -> ToSingleTape ⊨ ToSingleTape_Rel'.
proof: Proof. intros M_Realise. eapply Realise_monotone. { apply ToSingleTape_Realise. } { intros tin (yout, tout) H. cbn in *. hnf in M_Realise. intros T HEncT. specialize (H _ HEncT) as (c'&k&HLoop&HEncT'&->). specialize (M_Realise _ _ _ HLoop). exists (ctapes c'). auto. } 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)