Certificate for #7039 ⟨a, b, c | ab=1, bbcca=c⟩

Completion settings:

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

Axiom: ab=1.

Defines rule #3.

Referenced by [5], [6], [9], [10], [24], [25], [28].

Axiom: bbcca=c.

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

Axiom: cb=d.

Referenced by [6], [7], [11].

Axiom: adbb=e.

Referenced by [17], [21], [22], [23], [24].

Overlap of [1] ab=1 with [2] bbcca=c:

Critical pair: ac=bcca.

Flip LHS and RHS.

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

Overlap of [2] bbcca=c with [1] ab=1:

Critical pair: bbcc=cb.

Reduce RHS:

Referenced by [8].

Overlap of [3] cb=d with [2] bbcca=c:

Critical pair: cc=dbcca.

Reduce RHS:

Referenced by [8], [13].

Simplify [6] bbcc=d.

Reduce LHS:

Referenced by [9], [14].

Overlap of [1] ab=1 with [8] bbdac=d:

Critical pair: ad=bdac.

Flip LHS and RHS.

Referenced by [10], [11], [13], [14], [15].

Overlap of [1] ab=1 with [9] bdac=ad:

Critical pair: aad=dac.

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [9] bdac=ad with [3] cb=d:

Critical pair: bdad=adb.

Defines rule #9.

Referenced by [19], [21], [22], [23], [25], [26].

Overlap of [2] bbcca=c with [5] bcca=ac:

Critical pair: bac=c.

Referenced by [18].

Overlap of [5] bcca=ac with [7] cc=dac:

Critical pair: bdaca=ac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [18].

Overlap of [8] bbdac=d with [9] bdac=ad:

Critical pair: bad=d.

Defines rule #8.

Referenced by [17], [18], [20], [27].

Overlap of [9] bdac=ad with [10] dac=aad:

Critical pair: baad=ad.

Referenced by [19].

Overlap of [10] dac=aad with [13] ac=ada:

Critical pair: dada=aad.

Flip LHS and RHS.

Defines rule #10.

Referenced by [19], [24], [28].

Overlap of [14] bad=d with [4] adbb=e:

Critical pair: be=dbb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [25].

Simplify [12] bac=c.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Simplify [15] baad=ad.

Reduce LHS:

Referenced by [20], [21], [23].

Overlap of [14] bad=d with [19] adba=ad:

Critical pair: bad=dba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [26], [29].

Overlap of [4] adbb=e with [11] bdad=adb:

Critical pair: adbadb=edad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [29].

Overlap of [11] bdad=adb with [4] adbb=e:

Critical pair: bde=adbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [11] bdad=adb with [19] adba=ad:

Critical pair: bdad=adbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [16] aad=dada with [4] adbb=e:

Critical pair: ae=dadabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [25], [26], [27], [28], [29].

Overlap of [11] bdad=adb with [24] dadb=ae:

Critical pair: bae=adbb.

Reduce RHS:

Defines rule #11.

Overlap of [11] bdad=adb with [24] dadb=ae:

Critical pair: bdaae=adbadb.

Reduce RHS:

Defines rule #14.

Overlap of [14] bad=d with [24] dadb=ae:

Critical pair: baae=dadb.

Reduce RHS:

Defines rule #13.

Overlap of [16] aad=dada with [24] dadb=ae:

Critical pair: aaae=dadaadb.

Reduce RHS:

Defines rule #15.

Overlap of [21] edad=addb with [24] dadb=ae:

Critical pair: edaae=addbadb.

Reduce RHS:

Defines rule #12.