Certificate for #698 ⟨a, b | abaaaabba=1⟩

Completion settings:

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

Axiom: abaaaabba=1.

Referenced by [4].

Axiom: aaaa=c.

Referenced by [4], [7], [8], [9], [10], [14].

Axiom: bcb=d.

Referenced by [4], [5], [12], [16], [21], [26], [27], [33], [35].

Overlap of [1] abaaaabba=1 with [2] aaaa=c:

Critical pair: abcbba=1.

Reduce LHS:

Referenced by [6], [8], [9], [11].

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

Critical pair: bcd=dcb.

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

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

Critical pair: adb=dba.

Defines rule #7.

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

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

Critical pair: ac=ca.

Defines rule #11.

Referenced by [9], [12], [28], [30].

Overlap of [2] aaaa=c with [4] adba=1:

Critical pair: aaa=cdba.

Referenced by [9], [10].

Overlap of [4] adba=1 with [2] aaaa=c:

Critical pair: adbc=aaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [2] aaaa=c with [6] adb=dba:

Critical pair: aaadba=cdb.

Reduce LHS:

Referenced by [18].

Overlap of [4] adba=1 with [6] adb=dba:

Critical pair: dbaa=1.

Referenced by [13], [14], [15], [17], [19].

Overlap of [6] adb=dba with [3] bcb=d:

Critical pair: add=dbacb.

Reduce RHS:

Defines rule #8.

Referenced by [28].

Overlap of [5] bcd=dcb with [11] dbaa=1:

Critical pair: bc=dcbbaa.

Flip LHS and RHS.

Referenced by [20].

Overlap of [11] dbaa=1 with [2] aaaa=c:

Critical pair: dbc=aa.

Flip LHS and RHS.

Defines rule #15.

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

Overlap of [14] aa=dbc with [6] adb=dba:

Critical pair: adba=dbcdb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [18].

Overlap of [15] ddcbb=1 with [3] bcb=d:

Critical pair: ddcbd=cb.

Referenced by [17], [27].

Overlap of [16] ddcbd=cb with [11] dbaa=1:

Critical pair: ddcb=cbbaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [10] ddcbbaa=cdb with [15] ddcbb=1:

Critical pair: aa=cdb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [11] dbaa=1 with [14] aa=dbc:

Critical pair: dbdbc=1.

Defines rule #4.

Referenced by [21], [22], [25], [31], [36].

Overlap of [13] dcbbaa=bc with [14] aa=dbc:

Critical pair: dcbbdbc=bc.

Reduce LHS:

Referenced by [24], [25].

Overlap of [19] dbdbc=1 with [3] bcb=d:

Critical pair: dbdd=b.

Defines rule #2.

Referenced by [22], [23], [24], [25], [32], [34].

Overlap of [21] dbdd=b with [19] dbdbc=1:

Critical pair: dbd=bbdbc.

Flip LHS and RHS.

Defines rule #3.

Overlap of [21] dbdd=b with [21] dbdd=b:

Critical pair: dbdb=bbdd.

Flip LHS and RHS.

Defines rule #1.

Overlap of [21] dbdd=b with [20] dddcb=bc:

Critical pair: dbbc=bdcb.

Flip LHS and RHS.

Referenced by [27].

Overlap of [21] dbdd=b with [20] dddcb=bc:

Critical pair: dbdbc=bddcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [25] bddcb=1 with [3] bcb=d:

Critical pair: bddcd=cb.

Referenced by [29].

Overlap of [16] ddcbd=cb with [24] bdcb=dbbc:

Critical pair: ddcdbbc=cbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [28], [29], [34].

Overlap of [7] ac=ca with [27] cd=ddddc:

Critical pair: addddc=cad.

Reduce LHS:

Referenced by [31].

Overlap of [26] bddcd=cb with [27] cd=ddddc:

Critical pair: bddddddc=cb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [30], [32].

Overlap of [7] ac=ca with [29] cb=bddddddc:

Critical pair: abddddddc=cab.

Referenced by [32].

Overlap of [19] dbdbc=1 with [28] dbcabddc=cad:

Critical pair: dbcad=abddc.

Flip LHS and RHS.

Defines rule #13.

Overlap of [30] abddddddc=cab with [29] cb=bddddddc:

Critical pair: abddddddbddddddc=cabb.

Reduce LHS:

Defines rule #14.

Referenced by [33], [34].

Overlap of [32] abdddbc=cabb with [3] bcb=d:

Critical pair: abdddd=cabbb.

Defines rule #10.

Overlap of [32] abdddbc=cabb with [27] cd=ddddc:

Critical pair: abdddbddddc=cabbd.

Reduce LHS:

Defines rule #12.

Referenced by [35].

Overlap of [34] abdbc=cabbd with [3] bcb=d:

Critical pair: abdd=cabbdb.

Flip LHS and RHS.

Referenced by [36].

Overlap of [19] dbdbc=1 with [35] cabbdb=abdd:

Critical pair: dbdbabdd=abbdb.

Flip LHS and RHS.

Defines rule #9.