Certificate for #3601 ⟨a, b | aababbaaab=a⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1
• Auxiliary generators:
  1. ababb=c

Axiom: aababbaaab=a.

Referenced by [3].

Axiom: ababb=c.

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

Overlap of [1] aababbaaab=a with [2] ababb=c:

Critical pair: acaaab=a.

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

Overlap of [3] acaaab=a with [2] ababb=c:

Critical pair: acaac=aabb.

Flip LHS and RHS.

Referenced by [5], [8].

Overlap of [3] acaaab=a with [4] aabb=acaac:

Critical pair: acaacaac=ab.

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [2] ababb=c with [5] ab=acaacaac:

Critical pair: acaacaacabb=c.

Reduce LHS:

Defines rule #9.

Referenced by [12], [13].

Overlap of [3] acaaab=a with [5] ab=acaacaac:

Critical pair: acaaacaacaac=a.

Defines rule #2.

Referenced by [9], [10], [11], [12], [13].

Overlap of [4] aabb=acaac with [5] ab=acaacaac:

Critical pair: aacaacaacb=acaac.

Defines rule #6.

Referenced by [10], [11].

Overlap of [7] acaaacaacaac=a with [7] acaaacaacaac=a:

Critical pair: acaaacaacaa=aaaacaacaac.

Flip LHS and RHS.

Defines rule #1.

Overlap of [7] acaaacaacaac=a with [8] aacaacaacb=acaac:

Critical pair: acaaacacaac=aaacb.

Flip LHS and RHS.

Defines rule #4.

Overlap of [7] acaaacaacaac=a with [8] aacaacaacb=acaac:

Critical pair: acaaacaacacaac=aaacaacb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [7] acaaacaacaac=a with [6] acaacaacacaacaacb=c:

Critical pair: acaaacac=aaacacaacaacb.

Flip LHS and RHS.

Defines rule #7.

Overlap of [7] acaaacaacaac=a with [6] acaacaacacaacaacb=c:

Critical pair: acaaacaacac=aaacaacacaacaacb.

Flip LHS and RHS.

Defines rule #8.