Require Import List.

From Undecidability.Shared.Libs.DLW
  Require Import utils.

Require Import Undecidability.Synthetic.Undecidability.

Require Import Undecidability.TM.TM.

From Undecidability.TM
  Require Import TM SBTM Reductions.HaltTM_1_to_HaltSBTM Reductions.HaltSBTM_to_HaltSBTMu.

From Undecidability.StringRewriting
  Require Import SR HaltSBTMu_to_SRH SRH_to_SR.

From Undecidability.PCP
  Require Import PCP.

From Undecidability.PCP.Reductions
     Require Import SR_to_MPCP MPCP_to_PCP PCP_to_PCPb PCPb_iff_iPCPb.

Import ReductionChainNotations UndecidabilityNotations.

Lemma HaltTM_1_chain_iPCPb :
  HaltTM 1 ⪯ HaltSBTM /\
  HaltSBTM ⪯ HaltSBTMu /\
  HaltSBTMu ⪯ SRH /\
  SRH ⪯ SR /\
  SR ⪯ MPCP /\
  MPCP ⪯ PCP /\
  PCP ⪯ PCPb /\
  PCPb ⪯ iPCPb.
Proof.
  repeat eapply conj.
  + apply HaltTM_1_to_HaltSBTM.reduction.
  + apply HaltSBTM_to_HaltSBTMu.reduction.
  + apply HaltSBTMu_to_SRH.reduction.
  + apply SRH_to_SR.reduction.
  + apply SR_to_MPCP.reduction.
  + apply MPCP_to_PCP.reduction.
  + apply PCP_to_PCPb.reduction.
  + apply PCPb_iff_iPCPb.reductionLR.
Qed.

Lemma HaltTM_1_to_PCP : HaltTM 1 ⪯ PCP.
Proof.
  repeat (eapply reduces_transitive; [eapply HaltTM_1_chain_iPCPb | try eapply reduces_reflexive]).
Qed.

Lemma HaltTM_1_to_PCPb : HaltTM 1 ⪯ PCPb.
Proof.
  repeat (eapply reduces_transitive; [eapply HaltTM_1_chain_iPCPb | try eapply reduces_reflexive]).
Qed.

Lemma HaltTM_1_to_iPCPb : HaltTM 1 ⪯ iPCPb.
Proof.
  repeat (eapply reduces_transitive; [eapply HaltTM_1_chain_iPCPb | try eapply reduces_reflexive]).
Qed.