proposition: Lemma HaltTM_1_chain_iPCPb : HaltTM 1 ⪯ SBTM_HALT /\ SBTM_HALT ⪯ SR /\ SR ⪯ MPCP /\ MPCP ⪯ PCP /\ PCP ⪯ PCPb /\ PCPb ⪯ iPCPb.
proof: Proof. repeat eapply conj. + apply HaltTM_1_to_SBTM_HALT.reduction. + apply SBTM_HALT_to_SR.reduction. + apply SR_to_MPCP.reduction. + apply MPCP_to_PCP.reduction. + apply PCP_to_PCPb.reduction. + apply PCPb_iff_iPCPb.reductionLR. Qed.
imports: List Undecidability.Shared.Libs.DLW(utils) Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.StringRewriting(SR) Undecidability.PCP(PCP) Undecidability.TM(SBTM)