proposition: Theorem reduction : HaltTM 1 ⪯ CSSM_UB.
proof: 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.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.StackMachines.SSM