Certificate for #2384 ⟨a, b, c | aab=a, bccb=1⟩

Completion settings:

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

Axiom: aab=a.

Defines rule #2.

Referenced by [7], [8].

Axiom: bccb=1.

Referenced by [4].

Axiom: cc=d.

Defines rule #5.

Referenced by [4], [5].

Overlap of [2] bccb=1 with [3] cc=d:

Critical pair: bdb=1.

Referenced by [6], [7], [9], [12].

Overlap of [3] cc=d with [3] cc=d:

Critical pair: cd=dc.

Defines rule #4.

Referenced by [10].

Overlap of [4] bdb=1 with [4] bdb=1:

Critical pair: bd=db.

Defines rule #3.

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

Overlap of [1] aab=a with [4] bdb=1:

Critical pair: aa=adb.

Flip LHS and RHS.

Referenced by [8].

Overlap of [1] aab=a with [6] bd=db:

Critical pair: aadb=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [4] bdb=1 with [6] bd=db:

Critical pair: dbb=1.

Defines rule #6.

Referenced by [10].

Overlap of [5] cd=dc with [9] dbb=1:

Critical pair: c=dcbb.

Flip LHS and RHS.

Referenced by [11].

Overlap of [6] bd=db with [10] dcbb=c:

Critical pair: bc=dbcbb.

Flip LHS and RHS.

Referenced by [12].

Overlap of [4] bdb=1 with [11] dbcbb=bc:

Critical pair: bbc=cbb.

Flip LHS and RHS.

Defines rule #7.