Editing Knuth–Bendix completion algorithm (section)

==== A terminating example ====
Consider the monoid: 
:<math> \langle x, y \mid x^3 = y^3 = (xy)^3 = 1 \rangle </math>.  
We use the [[shortlex order]]. This is an infinite monoid but nevertheless, the Knuth–Bendix algorithm is able to solve the word problem.

Our beginning three reductions are therefore
{{NumBlk|:|<math> x^3 \rightarrow 1 </math>|{{EquationRef|1}}}} 
{{NumBlk|:|<math> y^3 \rightarrow 1 </math>|{{EquationRef|2}}}}

{{NumBlk|:|<math> (xy)^3 \rightarrow 1 </math>.|{{EquationRef|3}}}}

A suffix of <math>x^3</math> (namely <math>x</math>) is a prefix of <math>(xy)^3=xyxyxy</math>, so consider the word <math> x^3yxyxy </math>.  Reducing using ({{EquationNote|1}}), we get <math> yxyxy </math>.  Reducing using ({{EquationNote|3}}), we get <math> x^2 </math>.  Hence, we get <math> yxyxy = x^2 </math>, giving the reduction rule

{{NumBlk|:|<math> yxyxy \rightarrow x^2 </math>.|{{EquationRef|4}}}}

Similarly, using <math> xyxyxy^3 </math> and reducing using ({{EquationNote|2}}) and ({{EquationNote|3}}), we get <math> xyxyx = y^2 </math>.  Hence the reduction

{{NumBlk|:|<math> xyxyx \rightarrow y^2 </math>.|{{EquationRef|5}}}}

Both of these rules obsolete ({{EquationNote|3}}), so we remove it.

Next, consider <math> x^3yxyx </math> by overlapping ({{EquationNote|1}}) and ({{EquationNote|5}}). Reducing we get <math> yxyx = x^2y^2 </math>, so we add the rule

{{NumBlk|:|<math> yxyx \rightarrow x^2y^2</math>.|{{EquationRef|6}}}}
Considering <math> xyxyx^3 </math> by overlapping ({{EquationNote|1}}) and ({{EquationNote|5}}), we get <math> xyxy = y^2x^2 </math>, so we add the rule

{{NumBlk|:|<math> y^2x^2 \rightarrow xyxy </math>.|{{EquationRef|7}}}}
These obsolete rules ({{EquationNote|4}}) and ({{EquationNote|5}}), so we remove them.

Now, we are left with the rewriting system
{{NumBlk|:|<math> x^3 \rightarrow 1 </math>|({{EquationNote|1}})|RawN=.}}
{{NumBlk|:|<math> y^3 \rightarrow 1 </math>|({{EquationNote|2}})|RawN=.}}

{{NumBlk|:|<math> yxyx \rightarrow x^2y^2 </math>|({{EquationNote|6}})|RawN=.}}
{{NumBlk|:|<math> y^2 x^2 \rightarrow xyxy </math>.|({{EquationNote|7}})|RawN=.}}

Checking the overlaps of these rules, we find no potential failures of confluence.  Therefore, we have a confluent rewriting system, and the algorithm terminates successfully.