proposition: Theorem reduction : MPCPb ⪯ (HSC_PRV Argument.ΓPCP).
proof: Proof. exists (fun '((v, w), P) => (Argument.PCPf ((v, w) :: P) v w)). intros [[v w] P]. constructor. - exact Argument.ΓPCP_soundness. - exact Argument.ΓPCP_completeness. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP Undecidability.Synthetic.Definitions