Certificate for #6271 ⟨a, b, c | aa=1, bccbbc=1⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #1.

Axiom: bccbbc=1.

Referenced by [5].

Axiom: bc=d.

Defines rule #8.

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

Axiom: cbd=e.

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

Overlap of [2] bccbbc=1 with [3] bc=d:

Critical pair: dcbbc=1.

Reduce LHS:

Defines rule #2.

Referenced by [6], [10], [14], [15], [16].

Overlap of [4] cbd=e with [5] de=1:

Critical pair: cb=ee.

Defines rule #9.

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

Overlap of [3] bc=d with [6] cb=ee:

Critical pair: bee=db.

Flip LHS and RHS.

Defines rule #4.

Referenced by [11].

Overlap of [4] cbd=e with [6] cb=ee:

Critical pair: eed=e.

Referenced by [10], [12].

Overlap of [6] cb=ee with [3] bc=d:

Critical pair: cd=eec.

Flip LHS and RHS.

Referenced by [14].

Overlap of [5] de=1 with [8] eed=e:

Critical pair: de=ed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [11], [13].

Overlap of [10] ed=1 with [7] db=bee:

Critical pair: ebee=b.

Referenced by [12].

Overlap of [11] ebee=b with [8] eed=e:

Critical pair: ebe=bd.

Referenced by [13].

Overlap of [12] ebe=bd with [10] ed=1:

Critical pair: eb=bdd.

Defines rule #5.

Overlap of [5] de=1 with [9] eec=cd:

Critical pair: dcd=ec.

Flip LHS and RHS.

Defines rule #6.

Referenced by [15].

Overlap of [5] de=1 with [14] ec=dcd:

Critical pair: ddcd=c.

Referenced by [16].

Overlap of [15] ddcd=c with [5] de=1:

Critical pair: ddc=ce.

Defines rule #7.