Certificate for #2796 ⟨a, b, c | abc=b, caca=1⟩

Completion settings:

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

Axiom: abc=b.

Defines rule #1.

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

Axiom: caca=1.

Defines rule #4.

Referenced by [3], [4].

Overlap of [1] abc=b with [2] caca=1:

Critical pair: ab=baca.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

Overlap of [2] caca=1 with [1] abc=b:

Critical pair: cacb=bc.

Defines rule #5.

Overlap of [3] baca=ab with [1] abc=b:

Critical pair: bacb=abbc.

Defines rule #3.