proposition: Lemma semi_decidable_PCPb : semi_decider sdec_PCPb PCPb.
proof: Proof. intros P. unfold sdec_PCPb. split. - intros (A & H1 & H2 & H3). destruct (stack_enum_spec A) as [nA HnA]. exists nA. rewrite HnA. destruct A as [ | c A]; try congruence. eapply andb_true_intro. split. + rewrite subsetb_spec. eapply forallb_forall. intros ? H % H1. unfold my_inb. eapply list_in_decb_iff. 2: eassumption. intros a b. destruct (prod_eqb_spec (list_eqb_spec Bool.eqb_spec) (list_eqb_spec Bool.eqb_spec) a b); firstorder congruence. + eapply blist_eqb_spec. now rewrite tau1'_spec, tau2'_spec. - intros [n Hn]. destruct stack_enum as [A | ] eqn:E; try congruence. exists A. destruct A; try congruence. eapply Bool.andb_true_iff in Hn as [H1 H2]. rewrite subsetb_spec in H1. rewrite tau1'_spec, tau2'_spec in H2. unfold my_inb in H1. rewrite forallb_forall in H1. eapply blist_eqb_spec in H2. repeat eapply conj; try congruence. intros ? ? % H1. eapply list_in_decb_iff. 2: eassumption. intros a_ b_. destruct (prod_eqb_spec (list_eqb_spec Bool.eqb_spec) (list_eqb_spec Bool.eqb_spec) a_ b_); firstorder congruence. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts ListEnumerabilityFacts) Lia Undecidability.L(LProd LBool LNat LOptions) Undecidability.L.Datatypes.List(List_basics List_eqb List_extra List_nat) Undecidability(PCP)