into which instead eats the symbol on its right. (In this phase the string rewrite system no longer simulates a Turing machine, since that cannot remove cells from the tape.) After all symbols are gone, we have reached the terminal string . A decision procedure for the word problem would then also yield a procedure for deciding whether the given Turing machine terminates when started in a particular total state , by testing whether and belong to the same congruence class with respect to this string rewrite system. Technically, we have the following: Lemma. Let be a deterministic Turing machine and be the string rewrite system implementing , as described above. Then will halt when started from the total state encoded as if and only if (that is to say, if and only if and are Thue congruent for ). That if halts when started from is immediate from the construction of (simply running until it halts constructs a proof of ), but also allows the Turing machine to take steps backwards. Here it becomes relevant that is deterministic, because then the forward steps are all unique; in a walk from to the last backward step must be followed by its counterpart as a forward step, so these two cancel, and by induction all backward steps can be eliminated from such a walk. Hence if does not halt when started from , i.e., if we do not have , then we also do not have . Therefore deciding tells us the answer to the halting problem for . An apparent limitation of this argument is that in order to produce a semigroup with undecidable word problem, one must first have a concrete example of a Turing machine for which the halting problem is undecidable, but the various Turing machines figuring in the proof of the undecidability of the general halting problem all have as component a hypothetical Turing machine solving the halting problem, so none of those machines can actually exist; all that proves is that there is some Turing machine for which the decision problem is undecidable. However, that there is some Turing machine with undecidable halting problem means that the halting problem for a universal Turing machine is undecidable (since that can simulate any Turing machine), and concrete examples of universal Turing machines have been constructed. Connections with other notions A semi-Thue system is also a term-rewriting system—one