Certificate for #1811 ⟨a, b, c | aba=ab, bac=1⟩

Completion settings:

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

Axiom: aba=ab.

Referenced by [4].

Axiom: bac=1.

Referenced by [7], [9].

Axiom: ab=d.

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

Simplify [1] aba=ab.

Reduce RHS:

Referenced by [5].

Overlap of [4] aba=d with [3] ab=d:

Critical pair: da=d.

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

Overlap of [5] da=d with [3] ab=d:

Critical pair: dd=db.

Flip LHS and RHS.

Defines rule #1.

Overlap of [3] ab=d with [2] bac=1:

Critical pair: a=dac.

Reduce RHS:

Defines rule #5.

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

Overlap of [3] ab=d with [7] a=dc:

Critical pair: dcb=d.

Defines rule #3.

Overlap of [2] bac=1 with [7] a=dc:

Critical pair: bdcc=1.

Defines rule #4.

Overlap of [5] da=d with [7] a=dc:

Critical pair: ddc=d.

Defines rule #2.