proposition: Theorem HaltTM_1_chain_SemiU : HaltTM 1 ⪯ iPCPb /\ iPCPb ⪯ Halt_BSM /\ Halt_BSM ⪯ MM2_HALTING /\ MM2_HALTING ⪯ CM1_HALT /\ CM1_HALT ⪯ SMNdl_UB /\ SMNdl_UB ⪯ CSSM_UB /\ CSSM_UB ⪯ SSemiU /\ SSemiU ⪯ RU2SemiU /\ RU2SemiU ⪯ SemiU.
proof: Proof. constructor. { exact HaltTM_1_to_iPCPb.reduction. } constructor. { exact iPCPb_to_BSM_HALTING.iPCPb_to_BSM_HALTING. } constructor. { exact BSM_HALTING_to_MM2_HALTING.reduction. } constructor. { exact MM2_HALTING_to_CM1_HALT.reduction. } constructor. { exact CM1_HALT_to_SMNdl_UB.reduction. } constructor. { exact SMNdl_UB_to_CSSM_UB.reduction. } constructor. { exact CSSM_UB_to_SSemiU.reduction. } constructor. { exact SSemiU_to_RU2SemiU.reduction. } exact RU2SemiU_to_SemiU.reduction. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.SemiUnification.SemiU Undecidability.StackMachines.SSM Undecidability.StackMachines.SMN Undecidability.CounterMachines.CM1 Undecidability.MinskyMachines.MM2 Undecidability.StackMachines.BSM Undecidability.PCP.PCP Undecidability.TM.TM