proposition: Lemma RealiseIn_TerminatesIn n (F : Type) (pM : { M : TM n & state M -> F }) R k : pM ⊨c(k) R -> projT1 pM ↓ (fun tin l => k <= l).
proof: Proof. intros HRel. hnf. intros tin l HSteps. hnf in HRel. specialize (HRel tin) as (outc&HLoop&Rloop). exists outc. eapply loop_monotone; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM