Certificate for #6154 ⟨a, b, c | aa=1, abaccb=1⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #1.

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

Axiom: abaccb=1.

Referenced by [4].

Axiom: cc=d.

Defines rule #6.

Referenced by [4], [5].

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

Critical pair: abadb=1.

Referenced by [6].

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

Critical pair: cd=dc.

Defines rule #4.

Referenced by [10].

Overlap of [1] aa=1 with [4] abadb=1:

Critical pair: a=badb.

Flip LHS and RHS.

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

Overlap of [6] badb=a with [6] badb=a:

Critical pair: bada=aadb.

Reduce RHS:

Referenced by [8].

Overlap of [7] bada=db with [1] aa=1:

Critical pair: bad=dba.

Defines rule #2.

Referenced by [9], [11].

Overlap of [6] badb=a with [8] bad=dba:

Critical pair: dbab=a.

Defines rule #3.

Referenced by [10].

Overlap of [5] cd=dc with [9] dbab=a:

Critical pair: ca=dcbab.

Flip LHS and RHS.

Referenced by [11].

Overlap of [8] bad=dba with [10] dcbab=ca:

Critical pair: baca=dbacbab.

Flip LHS and RHS.

Referenced by [12].

Overlap of [6] badb=a with [11] dbacbab=baca:

Critical pair: babaca=aacbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.