proposition: Theorem reduction : PCP ⪯ CFPP.
proof: Proof. exists (fun P => (gamma P, fresh (sym P))). intros P. split; intros. - destruct H as (A & Hi & He & H). exists (gamma A). repeat split. + eapply gamma_mono. now rewrite gamma_invol. + destruct A; cbn in *; congruence. + eapply tau_eq_iff. * intros F % (sym_mono (P := P)) % fresh_spec; now try eapply F. * eauto. - destruct H as (B & Hi & He & H). exists (gamma B). repeat split. + now eapply gamma_mono. + destruct B; cbn in *; congruence. + eapply tau_eq_iff with (a := fresh (sym P)). * intros F % (sym_mono (P := P)) % fresh_spec. ** now eapply F. ** now eapply gamma_mono. * rewrite gamma_invol. eassumption. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions