Certificate for #3818 ⟨a, b | abbabbaaab=b⟩

Completion settings:

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

Axiom: abbabbaaab=b.

Referenced by [3].

Axiom: bba=c.

Defines rule #8.

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

Overlap of [1] abbabbaaab=b with [2] bba=c:

Critical pair: acbbaaab=b.

Reduce LHS:

Defines rule #6.

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

Overlap of [2] bba=c with [3] accaab=b:

Critical pair: bbb=cccaab.

Defines rule #9.

Referenced by [8].

Overlap of [3] accaab=b with [2] bba=c:

Critical pair: accaac=bba.

Reduce RHS:

Defines rule #3.

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

Overlap of [5] accaac=c with [3] accaab=b:

Critical pair: accab=ccaab.

Defines rule #5.

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

Critical pair: accac=ccaac.

Defines rule #2.

Referenced by [9], [10].

Overlap of [4] bbb=cccaab with [2] bba=c:

Critical pair: bc=cccaaba.

Defines rule #7.

Overlap of [7] accac=ccaac with [3] accaab=b:

Critical pair: accb=ccaaccaab.

Reduce RHS:

Defines rule #4.

Overlap of [7] accac=ccaac with [5] accaac=c:

Critical pair: accc=ccaaccaac.

Reduce RHS:

Defines rule #1.