Certificate for #3285 ⟨a, b | abbabaabaab=1⟩

Completion settings:

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

Axiom: abbabaabaab=1.

Referenced by [4].

Axiom: aba=c.

Defines rule #18.

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

Axiom: cb=d.

Defines rule #2.

Referenced by [5], [6], [7], [11], [12], [13], [21], [25].

Overlap of [1] abbabaabaab=1 with [2] aba=c:

Critical pair: abbcabaab=1.

Reduce LHS:

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

Overlap of [2] aba=c with [2] aba=c:

Critical pair: abc=cba.

Reduce RHS:

Defines rule #11.

Referenced by [6], [7], [8], [10], [14], [28], [32].

Overlap of [2] aba=c with [5] abc=da:

Critical pair: abda=cbc.

Reduce RHS:

Defines rule #23.

Referenced by [10].

Overlap of [5] abc=da with [3] cb=d:

Critical pair: abd=dab.

Flip LHS and RHS.

Defines rule #21.

Referenced by [8].

Overlap of [7] dab=abd with [5] abc=da:

Critical pair: dda=abdc.

Defines rule #15.

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

Critical pair: abbcc=bccab.

Referenced by [10], [12].

Overlap of [4] abbccab=1 with [5] abc=da:

Critical pair: abbccda=c.

Reduce LHS:

Referenced by [11].

Overlap of [3] cb=d with [10] bccdc=c:

Critical pair: cc=dccdc.

Flip LHS and RHS.

Referenced by [15].

Overlap of [4] abbccab=1 with [9] abbcc=bccab:

Critical pair: bccabab=1.

Reduce LHS:

Defines rule #5.

Referenced by [13], [14], [16], [17], [21], [23], [26].

Overlap of [3] cb=d with [12] bccd=1:

Critical pair: c=dccd.

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [16], [18], [19], [24].

Overlap of [5] abc=da with [12] bccd=1:

Critical pair: a=dacd.

Flip LHS and RHS.

Defines rule #13.

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

Overlap of [11] dccdc=cc with [13] dccd=c:

Critical pair: dccc=cccd.

Defines rule #1.

Overlap of [12] bccd=1 with [13] dccd=c:

Critical pair: bccc=ccd.

Defines rule #3.

Referenced by [21], [22].

Overlap of [12] bccd=1 with [14] dacd=a:

Critical pair: bcca=acd.

Defines rule #8.

Referenced by [27].

Overlap of [13] dccd=c with [14] dacd=a:

Critical pair: dcca=cacd.

Defines rule #6.

Overlap of [14] dacd=a with [13] dccd=c:

Critical pair: dacc=accd.

Defines rule #7.

Overlap of [14] dacd=a with [14] dacd=a:

Critical pair: daca=aacd.

Defines rule #16.

Overlap of [16] bccc=ccd with [3] cb=d:

Critical pair: bccd=ccdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [22].

Overlap of [16] bccc=ccd with [21] ccdb=1:

Critical pair: bc=ccddb.

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [12] bccd=1 with [22] ccddb=bc:

Critical pair: bbc=db.

Defines rule #12.

Referenced by [25], [26], [27], [29], [30], [33].

Overlap of [13] dccd=c with [22] ccddb=bc:

Critical pair: dbc=cdb.

Defines rule #10.

Referenced by [26], [27], [31].

Overlap of [23] bbc=db with [3] cb=d:

Critical pair: bbd=dbb.

Flip LHS and RHS.

Defines rule #22.

Referenced by [30].

Overlap of [23] bbc=db with [12] bccd=1:

Critical pair: b=dbcd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [28], [29].

Overlap of [23] bbc=db with [17] bcca=acd:

Critical pair: bacd=dbca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [32], [33].

Overlap of [5] abc=da with [26] cdbd=b:

Critical pair: abb=dadbd.

Flip LHS and RHS.

Defines rule #24.

Overlap of [23] bbc=db with [26] cdbd=b:

Critical pair: bbb=dbdbd.

Flip LHS and RHS.

Defines rule #25.

Overlap of [25] dbb=bbd with [23] bbc=db:

Critical pair: ddb=bbdc.

Defines rule #19.

Referenced by [31].

Overlap of [30] ddb=bbdc with [24] dbc=cdb:

Critical pair: dcdb=bbdcc.

Defines rule #20.

Overlap of [5] abc=da with [27] cdba=bacd:

Critical pair: abbacd=dadba.

Flip LHS and RHS.

Defines rule #26.

Overlap of [23] bbc=db with [27] cdba=bacd:

Critical pair: bbbacd=dbdba.

Flip LHS and RHS.

Defines rule #27.