proposition: Theorem BPCP_ksatis R : ~ PCPb R <-> ksatis (¬ F R).
proof: Proof. split. - intros H % (BPCP_satis R). now apply ksatis_satis. - intros (D & M & u & rho & H) H' % (BPCP_kvalid R (ff:=falsity_on)). apply (H u), (H' D M u). apply M. Qed.
imports: Undecidability.PCP(PCP Util.PCP_facts) Undecidability.FOL(Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Syntax.Facts) Undecidability.FOL.Semantics.Kripke(FragmentCore FragmentSoundness FragmentToTarski) Undecidability.FOL(FOL) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts MoreReducibilityFacts) Undecidability.PCP.Reductions.PCPb_iff_dPCPb Undecidability.FOL.Reductions.PCPb_to_FOL Undecidability(Shared.ListAutomation)