proposition: Theorem reduction : HaltTM 1 ⪯ SR.
proof: Proof. apply (reduces_transitive HaltTM_1_to_SBTM_HALT.reduction). exact SBTM_HALT_to_SR.reduction. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.StringRewriting.SR