Certificate for #19155 ⟨a, b | aba=a, bbaabb=b⟩

Completion settings:

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

Axiom: aba=a.

Referenced by [6].

Axiom: bbaabb=b.

Referenced by [4].

Axiom: bb=c.

Referenced by [4], [5].

Overlap of [2] bbaabb=b with [3] bb=c:

Critical pair: caabb=b.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [5], [6].

Overlap of [3] bb=c with [4] b=caac:

Critical pair: caacb=c.

Reduce LHS:

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

Simplify [1] aba=a.

Reduce LHS:

Referenced by [7], [8].

Overlap of [6] acaaca=a with [6] acaaca=a:

Critical pair: acaa=aaca.

Defines rule #2.

Referenced by [8], [11], [13], [14], [16].

Overlap of [6] acaaca=a with [7] acaa=aaca:

Critical pair: aacaca=a.

Defines rule #6.

Referenced by [10], [11], [14].

Overlap of [5] caaccaac=c with [5] caaccaac=c:

Critical pair: caacc=ccaac.

Flip LHS and RHS.

Referenced by [11].

Overlap of [5] caaccaac=c with [8] aacaca=a:

Critical pair: caacca=caca.

Referenced by [12], [16].

Overlap of [7] acaa=aaca with [5] caaccaac=c:

Critical pair: ac=aacaccaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [12], [13].

Overlap of [5] caaccaac=c with [11] aacc=ac:

Critical pair: caaccac=cc.

Reduce LHS:

Defines rule #5.

Referenced by [14], [15].

Overlap of [7] acaa=aaca with [11] aacc=ac:

Critical pair: acac=aacacc.

Flip LHS and RHS.

Defines rule #7.

Overlap of [12] cacac=cc with [7] acaa=aaca:

Critical pair: cacaaca=ccaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [12] cacac=cc with [12] cacac=cc:

Critical pair: cacc=ccac.

Flip LHS and RHS.

Defines rule #4.

Overlap of [5] caaccaac=c with [10] caacca=caca:

Critical pair: cacaac=c.

Reduce LHS:

Defines rule #8.