Certificate for #4527 ⟨a, b | aaababba=baa⟩

Completion settings:

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

Axiom: aaababba=baa.

Referenced by [4].

Axiom: babb=c.

Defines rule #10.

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

Axiom: caa=d.

Defines rule #4.

Referenced by [6], [7], [8], [9], [10], [11].

Overlap of [1] aaababba=baa with [2] babb=c:

Critical pair: aaaca=baa.

Flip LHS and RHS.

Defines rule #7.

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

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

Critical pair: babc=cabb.

Defines rule #9.

Overlap of [2] babb=c with [4] baa=aaaca:

Critical pair: babaaaca=caa.

Reduce LHS:

Reduce RHS:

Defines rule #2.

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

Overlap of [3] caa=d with [6] aaadadca=d:

Critical pair: cd=dadadca.

Defines rule #3.

Overlap of [3] caa=d with [6] aaadadca=d:

Critical pair: cad=daadadca.

Defines rule #5.

Overlap of [4] baa=aaaca with [6] aaadadca=d:

Critical pair: bd=aaacaadadca.

Reduce RHS:

Defines rule #6.

Overlap of [4] baa=aaaca with [6] aaadadca=d:

Critical pair: bad=aaacaaadadca.

Reduce RHS:

Defines rule #8.

Overlap of [6] aaadadca=d with [3] caa=d:

Critical pair: aaadadd=da.

Defines rule #1.