Certificate for #4459 ⟨a, b, c | aba=1, bccb=c⟩

Completion settings:

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

Axiom: aba=1.

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

Axiom: bccb=c.

Referenced by [5], [6].

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

Critical pair: ab=ba.

Defines rule #1.

Referenced by [4], [6].

Overlap of [1] aba=1 with [3] ab=ba:

Critical pair: baa=1.

Defines rule #2.

Referenced by [5].

Overlap of [2] bccb=c with [4] baa=1:

Critical pair: bcc=caa.

Flip LHS and RHS.

Defines rule #3.

Overlap of [3] ab=ba with [2] bccb=c:

Critical pair: ac=baccb.

Flip LHS and RHS.

Referenced by [7].

Overlap of [1] aba=1 with [6] baccb=ac:

Critical pair: aac=ccb.

Flip LHS and RHS.

Defines rule #4.