proposition: Lemma enumerable_PCP : enumerable dPCPb.
proof: Proof. pose proof enumerable_derivable. assert (enumerable (X := (stack bool * (string bool * string bool))) (fun '(C, (s, t)) => s = t)). { eapply dec_count_enum. - eapply decidable_iff. econstructor. intros (? & ? & ?). exact _. - eapply enum_enumT. econstructor. exact _. } unshelve epose proof (enumerable_conj _ _ _ _ H H0). - eapply discrete_iff. econstructor. exact _. - eapply projection in H1 as [f]. exists f. unfold enumerator in *. intros x. rewrite <- H1. intuition. + destruct H2 as [u]. exists (u,u). eauto. + destruct H2 as [[u v] [? ->]]. exists v. eauto. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)