proposition: Lemma reduction : HaltTM 1 ⪯ PCP.
proof: Proof. apply (reduces_transitive HaltTM_1_to_SR.reduction). apply (reduces_transitive SR_to_MPCP.reduction). exact MPCP_to_PCP.reduction. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.PCP.PCP Undecidability.PCP.Reductions.SR_to_MPCP Undecidability.PCP.Reductions.MPCP_to_PCP