proposition: Lemma PCPb_iff_iPCPb P : PCPb P <-> iPCPb P.
proof: Proof. split. - intros (A & ? & ? & ?). exists (f P A). repeat split. + now intros ? (? & ? & ? % pos_length) % in_omap_iff. + destruct A as [ | c A ]; try congruence. cbn. assert (c el P) as [n ->] % (el_pos card_eq) by firstorder. congruence. + rewrite itau_tau1, H1, itau_tau2; eauto. - intros (A & ? & ? & ?). exists (g P A). repeat split. + unfold g. intros ? (? & <- & ?) % in_map_iff. eapply nth_In; firstorder. + destruct A; cbn; congruence. + now rewrite tau_itau1, H1, tau_itau2. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions