proposition: Lemma L_enumerable_halt {X} `{encodable X} (p : X -> Prop) : L_decidable (X := X * X) (fun '(x,y) => x = y) -> L_enumerable p -> p ⪯ converges.
proof: Proof. intros (d & [c_d] & H_d) (f & [c_f] & H_f). edestruct L_enumerable_recognisable with (p := p) (d := fun x y => d (x,y)) (f := f); eauto. - extract. - intros. specialize (H_d (x,y)). destruct (d (x,y)); intuition (auto with bool). - now exists (fun x0 => L.app x (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