Require Import Undecidability.Synthetic.Definitions.
Require Import Undecidability.SemiUnification.SemiU. Require Import Undecidability.StackMachines.SSM. Require Import Undecidability.StackMachines.SMN. Require Import Undecidability.CounterMachines.CM1. Require Import Undecidability.MinskyMachines.MM2. Require Import Undecidability.StackMachines.BSM. Require Import Undecidability.PCP.PCP. Require Import Undecidability.TM.TM.
Require Undecidability.SemiUnification.Reductions.RU2SemiU_to_SemiU.
Require Undecidability.SemiUnification.Reductions.SSemiU_to_RU2SemiU.
Require Undecidability.SemiUnification.Reductions.CSSM_UB_to_SSemiU.
Require Undecidability.StackMachines.Reductions.SMNdl_UB_to_CSSM_UB.
Require Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.
Require Undecidability.CounterMachines.Reductions.MM2_HALTING_to_CM1_HALT.
Require Undecidability.MinskyMachines.Reductions.BSM_HALTING_to_MM2_HALTING.
Require Undecidability.StackMachines.Reductions.iPCPb_to_BSM_HALTING.
Require Undecidability.PCP.Reductions.HaltTM_1_to_iPCPb.
Theorem HaltTM_1_chain_SemiU :
HaltTM 1 ⪯ iPCPb /\
iPCPb ⪯ BSM_HALTING /\
BSM_HALTING ⪯ MM2_HALTING /\
MM2_HALTING ⪯ CM1_HALT /\
CM1_HALT ⪯ SMNdl_UB /\
SMNdl_UB ⪯ CSSM_UB /\
CSSM_UB ⪯ SSemiU /\
SSemiU ⪯ RU2SemiU /\
RU2SemiU ⪯ SemiU.
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.
Require Import Undecidability.SemiUnification.SemiU. Require Import Undecidability.StackMachines.SSM. Require Import Undecidability.StackMachines.SMN. Require Import Undecidability.CounterMachines.CM1. Require Import Undecidability.MinskyMachines.MM2. Require Import Undecidability.StackMachines.BSM. Require Import Undecidability.PCP.PCP. Require Import Undecidability.TM.TM.
Require Undecidability.SemiUnification.Reductions.RU2SemiU_to_SemiU.
Require Undecidability.SemiUnification.Reductions.SSemiU_to_RU2SemiU.
Require Undecidability.SemiUnification.Reductions.CSSM_UB_to_SSemiU.
Require Undecidability.StackMachines.Reductions.SMNdl_UB_to_CSSM_UB.
Require Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.
Require Undecidability.CounterMachines.Reductions.MM2_HALTING_to_CM1_HALT.
Require Undecidability.MinskyMachines.Reductions.BSM_HALTING_to_MM2_HALTING.
Require Undecidability.StackMachines.Reductions.iPCPb_to_BSM_HALTING.
Require Undecidability.PCP.Reductions.HaltTM_1_to_iPCPb.
Theorem HaltTM_1_chain_SemiU :
HaltTM 1 ⪯ iPCPb /\
iPCPb ⪯ BSM_HALTING /\
BSM_HALTING ⪯ MM2_HALTING /\
MM2_HALTING ⪯ CM1_HALT /\
CM1_HALT ⪯ SMNdl_UB /\
SMNdl_UB ⪯ CSSM_UB /\
CSSM_UB ⪯ SSemiU /\
SSemiU ⪯ RU2SemiU /\
RU2SemiU ⪯ SemiU.
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.