Require Import Prelim Reductions PCP String_rewriting Single_TM.
Require Import SR_MPCP Halt_SR SR_RSR RSR_PCP Halt_MPCP MPCP_PCP.

Theorem Halt_MPCP_PCP_reduction : red HaltD PCPD.
Proof.
  apply red_trans with (q:= MPCPD).
  apply reduction_halt_mpcp. apply reduction_mpcp_pcp.
Qed.

Theorem Halt_SR_RSR_PCP_reduction : red HaltD PCPD.
Proof. apply red_trans with (q:=RSR). apply red_trans with (q:=SR).
         apply reduction_halt_sr. apply reduction_sr_restricted_sr.
         apply reduction_restricted_sr_pcp.
Qed.

Theorem Halt_SR_MPCP_PCP_reduction : red HaltD PCPD.
Proof.
    apply red_trans with (q:= MPCPD). apply red_trans with (q:= SR).
    apply reduction_halt_sr. apply reduction_sr_mpcp. apply reduction_mpcp_pcp.
Qed.

Corollary PCP_undecidability : undecidable PCPD.
Proof.
  apply Halt_SR_MPCP_PCP_reduction.
Qed.