proposition: Lemma Realise_total n (F : Type) (pM : { M : TM n & state M -> F }) R k : pM ⊨ R /\ projT1 pM ↓ (fun _ i => k <= i) <-> pM ⊨c(k) R.
proof: Proof. split. - intros (HR & Ht) t. edestruct (Ht t k); [reflexivity|eauto]. - intros H. split. + intros t i cout Hc. destruct (H t) as (? & ? & ?). replace cout with x. * eassumption. * unfold loopM in *. eapply loop_injective; eauto. + intros t i Hi. edestruct (H t) as (? & ? & ?). exists x. eapply loop_monotone; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM