A Noetherian and confluent rewrite system for idempotent semigroups

Let B be a semigroup with the additional relation $$\begin{gathered} xx \Rightarrow x \hfill \\ xyz \Rightarrow xz if x \mathop {CI}\limits_ = z and xy\mathop {CI}\limits_ = z \hfill \\ \end{gathered} $$ B is called aband or anidempotent semigroup 3]. It is shown in this paper that the replacement rules (rewrites) resulting from the axiom of idempotence: $$\forall w \in B.ww = w$$ can be replaced by theNoetherian, confluent, conditional rewrites (i. e. a terminating replacement system having the Church-Rosser-Property): $$\begin{gathered} xx \Rightarrow x \hfill \\ x \Rightarrow xx \hfill \\ \end{gathered} $$ These rewrites are used to obtain a unique normal form for words in B and hence are the basis for a decision procedure for word equality in B. The proof techniques are based uponterm rewriting systems 7] rather than the usual algebraic approach. Alternative and simpler proofs of a result reported earlier by Green and Rees 4] and Gerhardt 6] have been obtained.