Certificate for #1877 ⟨a, b, c | aba=bc, cac=1⟩

Completion settings:

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

Axiom: aba=bc.

Referenced by [5], [6].

Axiom: cac=1.

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

Overlap of [2] cac=1 with [2] cac=1:

Critical pair: ca=ac.

Defines rule #1.

Referenced by [4], [6].

Overlap of [2] cac=1 with [3] ca=ac:

Critical pair: acc=1.

Defines rule #2.

Referenced by [5].

Overlap of [1] aba=bc with [4] acc=1:

Critical pair: ab=bccc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [3] ca=ac with [1] aba=bc:

Critical pair: cbc=acba.

Flip LHS and RHS.

Referenced by [7].

Overlap of [2] cac=1 with [6] acba=cbc:

Critical pair: ccbc=ba.

Flip LHS and RHS.

Defines rule #3.