Certificate for #4109 ⟨a, b | aababaaab=ab⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a

Axiom: aababaaab=ab.

Defines rule #3.

Referenced by [2], [3].

Overlap of [1] aababaaab=ab with [1] aababaaab=ab:

Critical pair: aababaab=ababaaab.

Defines rule #2.

Referenced by [3].

Overlap of [2] aababaab=ababaaab with [1] aababaaab=ab:

Critical pair: aababab=ababaaababaaab.

Reduce RHS:

Defines rule #1.