proposition: Lemma PCP_compl_undec : undecidable (complement PCP).
proof: Proof. apply (undecidability_from_reducibility complement_SBTM_HALT_undec). apply reduces_complement. eapply reduces_transitive; last apply MPCP_to_PCP.reduction. eapply reduces_transitive; last apply SR_to_MPCP.reduction. Locate SR.SR. eapply reduces_transitive; last apply SBTM_HALT_to_SR.reduction. eapply reduces_reflexive. Qed.
imports: Undecidability.PCP.PCP Undecidability.Synthetic.Undecidability Undecidability.Synthetic.ReducibilityFacts Undecidability.FRACTRAN(FRACTRAN Reductions.MM_FRACTRAN) Undecidability.MinskyMachines(MM Reductions.BSM_MM) Undecidability.StackMachines(BSM Reductions.SBTM_HALT_to_HaltBSM) Undecidability.TM.SBTM_undec