proposition: Theorem PCPX_iff_dPCP P : PCPX P <-> dPCP P.
proof: Proof. split. - intros (A & H1 & H2 & H3); exists (tau1 A). rewrite H3 at 2; apply PCPX_derivable. exists A; auto. - intros (u & Hu). apply derivable_PCPX in Hu. destruct Hu as (A & H1 & H2 & H3 & H4). exists A; subst; auto. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions