Certificate for #3187 ⟨a, b | abaaabaabab=1⟩

Completion settings:

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

Axiom: abaaabaabab=1.

Referenced by [4].

Axiom: ab=c.

Defines rule #6.

Referenced by [4], [6], [13], [18], [21].

Axiom: aaca=d.

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

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

Critical pair: caaabaabab=1.

Reduce LHS:

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

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

Critical pair: cdc=dcc.

Flip LHS and RHS.

Referenced by [8].

Overlap of [3] aaca=d with [2] ab=c:

Critical pair: aacc=db.

Referenced by [10].

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

Critical pair: aacd=daca.

Flip LHS and RHS.

Referenced by [11], [16].

Overlap of [5] dcc=cdc with [4] cdcc=1:

Critical pair: dc=cdcdcc.

Reduce RHS:

Defines rule #1.

Referenced by [9], [11], [12], [16], [20], [25], [26], [27], [28], [31], [32], [33].

Overlap of [4] cdcc=1 with [8] dc=cd:

Critical pair: ccdc=1.

Reduce LHS:

Defines rule #2.

Referenced by [10], [11], [15], [17], [20], [23], [24], [25], [28], [29], [30], [31], [32], [33].

Overlap of [6] aacc=db with [9] cccd=1:

Critical pair: aa=dbcd.

Defines rule #3.

Referenced by [11], [12], [13], [14], [16], [19].

Overlap of [9] cccd=1 with [7] daca=aacd:

Critical pair: cccaacd=aca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [3] aaca=d with [10] aa=dbcd:

Critical pair: dbcdca=d.

Reduce LHS:

Referenced by [15].

Overlap of [10] aa=dbcd with [2] ab=c:

Critical pair: ac=dbcdb.

Flip LHS and RHS.

Referenced by [17], [22].

Overlap of [10] aa=dbcd with [10] aa=dbcd:

Critical pair: adbcd=dbcda.

Flip LHS and RHS.

Referenced by [24].

Overlap of [9] cccd=1 with [12] dbccda=d:

Critical pair: cccd=bccda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [16].

Overlap of [15] bccda=1 with [7] daca=aacd:

Critical pair: bccaacd=ca.

Reduce LHS:

Referenced by [25].

Overlap of [9] cccd=1 with [13] dbcdb=ac:

Critical pair: cccac=bcdb.

Flip LHS and RHS.

Defines rule #14.

Referenced by [21], [22], [28].

Overlap of [11] aca=bccdd with [2] ab=c:

Critical pair: acc=bccddb.

Flip LHS and RHS.

Defines rule #16.

Overlap of [11] aca=bccdd with [10] aa=dbcd:

Critical pair: acdbcd=bccdda.

Flip LHS and RHS.

Defines rule #13.

Overlap of [11] aca=bccdd with [11] aca=bccdd:

Critical pair: acbccdd=bccddca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [2] ab=c with [17] bcdb=cccac:

Critical pair: acccac=ccdb.

Referenced by [23].

Overlap of [17] bcdb=cccac with [13] dbcdb=ac:

Critical pair: bcac=cccaccdb.

Referenced by [30].

Overlap of [21] acccac=ccdb with [9] cccd=1:

Critical pair: accca=ccdbccd.

Defines rule #5.

Overlap of [9] cccd=1 with [14] dbcda=adbcd:

Critical pair: cccadbcd=bcda.

Flip LHS and RHS.

Defines rule #11.

Overlap of [16] bccdbccdd=ca with [8] dc=cd:

Critical pair: bccdbccdcd=cac.

Reduce LHS:

Referenced by [26], [32].

Overlap of [25] bccdbd=cac with [8] dc=cd:

Critical pair: bccdbcd=cacc.

Referenced by [27], [28].

Overlap of [26] bccdbcd=cacc with [8] dc=cd:

Critical pair: bccdbccd=caccc.

Referenced by [31], [32].

Overlap of [26] bccdbcd=cacc with [17] bcdb=cccac:

Critical pair: bccdcccac=caccb.

Reduce LHS:

Referenced by [29].

Overlap of [28] bccac=caccb with [9] cccd=1:

Critical pair: bcca=caccbccd.

Defines rule #10.

Overlap of [22] bcac=cccaccdb with [9] cccd=1:

Critical pair: bca=cccaccdbccd.

Defines rule #8.

Overlap of [27] bccdbccd=caccc with [8] dc=cd:

Critical pair: bccdbcccd=cacccc.

Reduce LHS:

Defines rule #15.

Overlap of [27] bccdbccd=caccc with [25] bccdbd=cac:

Critical pair: bccdcac=cacccbd.

Reduce LHS:

Referenced by [33].

Overlap of [32] bac=cacccbd with [9] cccd=1:

Critical pair: ba=cacccbdccd.

Reduce RHS:

Defines rule #7.