proposition: Lemma SSTS01_undec : undecidable SSTS01.
proof: Proof. apply (undecidability_from_reducibility MM2_ZERO_HALTING_undec). apply MM2_ZERO_HALTING_to_SSTS01.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.StringRewriting.SSTS Undecidability.MinskyMachines.MM2_undec