proposition: Lemma RealiseIn_monotone n (F : Type) (pM : pTM F n) (R R' : pRel sig F n) k k' : pM ⊨c(k') R' -> k' <= k -> R' <<=2 R -> pM ⊨c(k) R.
proof: Proof. unfold RealiseIn. intros H1 H2 H3 input. specialize (H1 input) as (outc & H1). exists outc. split. - unfold loopM. eapply loop_monotone; eauto. intuition. - intuition. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM