Undecidability of PCP

Hopcroft: Halt < 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.

Davis: Halt < SR < RSR < PCP

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.

Halt < SR < MPCP < PCP

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.