proposition: Theorem reduction : CFPP ⪯ CFP.
proof: Proof. exists (fun '(R, a) => (G R a)). intros [R a]. intuition; cbn in *. - destruct H as (A & HR & HA & H). exists (sigma a A). split. + eapply reduction_full; eauto. + eauto. - destruct H as (x & Hx & H). eapply reduction_full in Hx as (A & HR & HA & H1). exists A. subst; eauto. Qed.
imports: Setoid Morphisms List Arith Lia Undecidability.CFG.CFP Undecidability.CFG.CFG Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions