Certificate for #4868 ⟨a, b | abbabaab=aab⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with c < a < b
• Auxiliary generators:
  1. abbaba=c

Axiom: abbabaab=aab.

Referenced by [3].

Axiom: abbaba=c.

Defines rule #4.

Referenced by [3], [4], [5], [6], [7].

Overlap of [1] abbabaab=aab with [2] abbaba=c:

Critical pair: cab=aab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6].

Overlap of [2] abbaba=c with [2] abbaba=c:

Critical pair: abbabc=cbbaba.

Defines rule #3.

Referenced by [5], [7].

Overlap of [2] abbaba=c with [3] aab=cab:

Critical pair: abbabcab=cab.

Reduce LHS:

Defines rule #6.

Overlap of [3] aab=cab with [2] abbaba=c:

Critical pair: ac=cabbaba.

Reduce RHS:

Defines rule #1.

Referenced by [7].

Overlap of [2] abbaba=c with [6] ac=cc:

Critical pair: abbabcc=cc.

Reduce LHS:

Defines rule #5.