proposition: Theorem reduction : PCP ⪯ PCPb.
proof: Proof. exists f. intros B. split. - intros (A & HP & He & H). exists (f A). repeat split. + now eapply f_subset. + destruct A; cbn; congruence. + unfold f, f_c, f_s. setoid_rewrite tau1_f. setoid_rewrite tau2_f. now rewrite H. - intros (A & HP & He & H). exists (g A). repeat split. + eapply f_g_subset; eauto. + destruct A; cbn; congruence. + erewrite tau1_g, tau2_g, H; eauto. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions