Certificate for #1857 ⟨a, b, c | aba=bb, caa=1⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a < c

Axiom: aba=bb.

Defines rule #1.

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

Axiom: caa=1.

Defines rule #2.

Referenced by [4].

Overlap of [1] aba=bb with [1] aba=bb:

Critical pair: abbb=bbba.

Defines rule #3.

Referenced by [5].

Overlap of [2] caa=1 with [1] aba=bb:

Critical pair: cabb=ba.

Defines rule #4.

Referenced by [5].

Overlap of [4] cabb=ba with [3] abbb=bbba:

Critical pair: cbbba=bab.

Defines rule #5.

Referenced by [6].

Overlap of [5] cbbba=bab with [1] aba=bb:

Critical pair: cbbbbb=babba.

Defines rule #6.