Certificate for #5343 ⟨a, b | ababaab=abaa⟩

Completion settings:

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

Axiom: ababaab=abaa.

Referenced by [3].

Axiom: abaa=c.

Defines rule #2.

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

Simplify [1] ababaab=abaa.

Reduce RHS:

Referenced by [4].

Overlap of [3] ababaab=c with [2] abaa=c:

Critical pair: abcb=c.

Defines rule #3.

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

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

Critical pair: abac=cbaa.

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [2] abaa=c with [4] abcb=c:

Critical pair: abac=cbcb.

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [4] abcb=c with [5] cbaa=abac:

Critical pair: ababac=caa.

Defines rule #8.

Referenced by [8], [12].

Overlap of [4] abcb=c with [6] cbcb=abac:

Critical pair: ababac=ccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [10], [11].

Overlap of [6] cbcb=abac with [5] cbaa=abac:

Critical pair: cbabac=abacaa.

Defines rule #9.

Overlap of [8] ccb=caa with [5] cbaa=abac:

Critical pair: cabac=caaaa.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12].

Overlap of [8] ccb=caa with [6] cbcb=abac:

Critical pair: cabac=caacb.

Flip LHS and RHS.

Defines rule #7.

Overlap of [7] ababac=caa with [10] caaaa=cabac:

Critical pair: ababacabac=caaaaaa.

Reduce LHS:

Reduce RHS:

Defines rule #10.