Hans Zantema raised the question: Does the one-rule string rewriting system 00II - III000 terminate? Two successful termination proofs have been given by Nachum Dershowitz: One by minimal counterexample, and the other, by a forward closure argument. We give a different, more constructive, termination proof, following Zantema's original proof attempt, and using Bellegarde/Lescanne's transformation order method to verify a subtle transformation step.
Ulrike Peiker, Martin Griebl