proposition: Lemma TSR_undec : undecidable TSR.
proof: Proof. apply (undecidability_from_reducibility SBTM_HALT_undec). exact SBTM_HALT_to_TSR.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.StringRewriting.SR Undecidability.TM.SBTM_undec