Certificate for #1984 ⟨a, b, c | abc=ba, ccb=1⟩

Completion settings:

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

Axiom: abc=ba.

Referenced by [4].

Axiom: ccb=1.

Defines rule #1.

Referenced by [5], [9], [11].

Axiom: ab=d.

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

Overlap of [1] abc=ba with [3] ab=d:

Critical pair: dc=ba.

Flip LHS and RHS.

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

Overlap of [2] ccb=1 with [4] ba=dc:

Critical pair: ccdc=a.

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [3] ab=d with [4] ba=dc:

Critical pair: adc=da.

Reduce LHS:

Reduce RHS:

Referenced by [9].

Overlap of [4] ba=dc with [3] ab=d:

Critical pair: bd=dcb.

Defines rule #5.

Overlap of [3] ab=d with [5] a=ccdc:

Critical pair: ccdcb=d.

Defines rule #4.

Overlap of [6] ccdcdc=dccdc with [2] ccb=1:

Critical pair: ccdcd=dccdccb.

Reduce RHS:

Defines rule #3.

Overlap of [4] ba=dc with [5] a=ccdc:

Critical pair: bccdc=dc.

Referenced by [11].

Overlap of [10] bccdc=dc with [2] ccb=1:

Critical pair: bccd=dccb.

Reduce RHS:

Defines rule #6.