proposition: Lemma L_recognisable_halt {X} `{encodable X} (p : X -> Prop) : L_recognisable p -> p ⪯ converges.
proof: Proof. intros. eapply L_recognisable'_recognisable in H0 as (f & H_f). now exists (fun x0 => f (enc x0)). Qed.
imports: Undecidability.L(Computability.MuRec) Undecidability.L.Datatypes(LNat LOptions LProd) Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.L.Datatypes.List(List_basics List_nat) Datatypes