Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts.
Require Import Undecidability.TM.TM.
Require Import Undecidability.StackMachines.SSM.
Require Undecidability.CounterMachines.Reductions.HaltTM_1_to_CM1_HALT.
Require Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.
Require Undecidability.StackMachines.Reductions.SMNdl_UB_to_CSSM_UB.
Theorem reduction : HaltTM 1 ⪯ CSSM_UB.
Proof.
apply (reduces_transitive HaltTM_1_to_CM1_HALT.reduction).
apply (reduces_transitive CM1_HALT_to_SMNdl_UB.reduction).
exact SMNdl_UB_to_CSSM_UB.reduction.
Qed.
Require Import Undecidability.TM.TM.
Require Import Undecidability.StackMachines.SSM.
Require Undecidability.CounterMachines.Reductions.HaltTM_1_to_CM1_HALT.
Require Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.
Require Undecidability.StackMachines.Reductions.SMNdl_UB_to_CSSM_UB.
Theorem reduction : HaltTM 1 ⪯ CSSM_UB.
Proof.
apply (reduces_transitive HaltTM_1_to_CM1_HALT.reduction).
apply (reduces_transitive CM1_HALT_to_SMNdl_UB.reduction).
exact SMNdl_UB_to_CSSM_UB.reduction.
Qed.