Certificate for #5167 ⟨a, b | aababaa=aaba⟩

Completion settings:

• Reduction order:
  • Right-to-left shortlex with b < c < a
• Auxiliary generators:
  1. aaba=c

Axiom: aababaa=aaba.

Referenced by [3].

Axiom: aaba=c.

Defines rule #4.

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

Simplify [1] aababaa=aaba.

Reduce RHS:

Referenced by [4].

Overlap of [3] aababaa=c with [2] aaba=c:

Critical pair: cbaa=c.

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

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

Critical pair: aabc=caba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7].

Overlap of [4] cbaa=c with [2] aaba=c:

Critical pair: cbc=cba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [8].

Overlap of [4] cbaa=c with [2] aaba=c:

Critical pair: cbac=caba.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Overlap of [4] cbaa=c with [6] cba=cbc:

Critical pair: cbca=c.

Defines rule #5.