Certificate for #2572 ⟨a, b | abaaab=baab⟩

Completion settings:

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

Axiom: abaaab=baab.

Referenced by [3].

Axiom: aba=c.

Defines rule #2.

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

Overlap of [1] abaaab=baab with [2] aba=c:

Critical pair: caab=baab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [5], [6].

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

Critical pair: abc=cba.

Defines rule #1.

Overlap of [2] aba=c with [3] baab=caab:

Critical pair: acaab=cab.

Defines rule #10.

Referenced by [10], [11].

Overlap of [3] baab=caab with [2] aba=c:

Critical pair: bac=caaba.

Reduce RHS:

Defines rule #4.

Referenced by [7], [8], [10].

Overlap of [2] aba=c with [6] bac=cac:

Critical pair: acac=cc.

Defines rule #6.

Referenced by [8], [9], [11].

Overlap of [6] bac=cac with [7] acac=cc:

Critical pair: bcc=cacac.

Reduce RHS:

Defines rule #3.

Overlap of [7] acac=cc with [7] acac=cc:

Critical pair: accc=ccac.

Defines rule #5.

Overlap of [6] bac=cac with [5] acaab=cab:

Critical pair: bcab=cacaab.

Reduce RHS:

Defines rule #7.

Overlap of [7] acac=cc with [5] acaab=cab:

Critical pair: accab=ccaab.

Defines rule #9.