Certificate for #3064 ⟨a, b | aabababaaba=1⟩

Completion settings:

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

Axiom: aabababaaba=1.

Referenced by [4].

Axiom: ba=c.

Defines rule #6.

Referenced by [4], [5], [6], [11], [13], [30], [33], [36].

Axiom: acaa=d.

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

Overlap of [1] aabababaaba=1 with [2] ba=c:

Critical pair: aacbabaaba=1.

Reduce LHS:

Referenced by [6], [7], [8], [9], [10], [15], [16], [20].

Overlap of [2] ba=c with [3] acaa=d:

Critical pair: bd=ccaa.

Flip LHS and RHS.

Referenced by [29].

Overlap of [2] ba=c with [4] aacccac=1:

Critical pair: b=cacccac.

Flip LHS and RHS.

Referenced by [10], [11], [12], [13], [14], [17].

Overlap of [3] acaa=d with [4] aacccac=1:

Critical pair: ac=dcccac.

Flip LHS and RHS.

Referenced by [14], [18].

Overlap of [3] acaa=d with [4] aacccac=1:

Critical pair: aca=dacccac.

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] aacccac=1 with [3] acaa=d:

Critical pair: aacccd=aa.

Referenced by [19].

Overlap of [4] aacccac=1 with [6] cacccac=b:

Critical pair: aacccab=acccac.

Referenced by [22].

Overlap of [6] cacccac=b with [3] acaa=d:

Critical pair: cacccd=baa.

Reduce RHS:

Referenced by [15], [16], [17], [18].

Overlap of [6] cacccac=b with [6] cacccac=b:

Critical pair: caccb=bccac.

Referenced by [41].

Overlap of [6] cacccac=b with [6] cacccac=b:

Critical pair: cacccab=bacccac.

Reduce RHS:

Referenced by [24].

Overlap of [7] dcccac=ac with [6] cacccac=b:

Critical pair: dccb=acccac.

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [4] aacccac=1 with [11] cacccd=ca:

Critical pair: aaccca=ccd.

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

Overlap of [4] aacccac=1 with [11] cacccd=ca:

Critical pair: aacccaca=acccd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [6] cacccac=b with [11] cacccd=ca:

Critical pair: caccca=bccd.

Referenced by [24], [39].

Overlap of [7] dcccac=ac with [11] cacccd=ca:

Critical pair: dccca=acccd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Simplify [9] aacccd=aa.

Reduce LHS:

Referenced by [31], [34].

Overlap of [4] aacccac=1 with [15] aaccca=ccd:

Critical pair: ccdc=1.

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

Overlap of [8] dacccac=aca with [14] acccac=dccb:

Critical pair: ddccb=aca.

Flip LHS and RHS.

Defines rule #4.

Referenced by [33], [34], [35], [36].

Simplify [10] aacccab=acccac.

Reduce RHS:

Referenced by [23].

Overlap of [22] aacccab=dccb with [15] aaccca=ccd:

Critical pair: ccdb=dccb.

Referenced by [24].

Overlap of [13] cacccab=ccccac with [17] caccca=bccd:

Critical pair: bccdb=ccccac.

Reduce LHS:

Defines rule #15.

Referenced by [43].

Overlap of [20] ccdc=1 with [20] ccdc=1:

Critical pair: ccd=cdc.

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

Overlap of [20] ccdc=1 with [25] ccd=cdc:

Critical pair: cdcc=1.

Referenced by [27], [28].

Overlap of [20] ccdc=1 with [25] ccd=cdc:

Critical pair: ccdcdc=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [28], [35], [36], [39], [43], [45].

Simplify [26] cdcc=1.

Reduce LHS:

Defines rule #2.

Referenced by [29], [31], [32], [34], [35], [36], [37], [40], [41], [42], [43], [44], [45], [46].

Overlap of [28] dccc=1 with [5] ccaa=bd:

Critical pair: dcbd=aa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [30], [31], [34], [36].

Overlap of [2] ba=c with [29] aa=dcbd:

Critical pair: bdcbd=ca.

Referenced by [32], [38].

Overlap of [19] adccca=aa with [29] aa=dcbd:

Critical pair: adcccdcbd=aaa.

Reduce LHS:

Reduce RHS:

Referenced by [42].

Overlap of [30] bdcbd=ca with [28] dccc=1:

Critical pair: bdcb=caccc.

Defines rule #14.

Referenced by [38].

Overlap of [2] ba=c with [21] aca=ddccb:

Critical pair: bddccb=cca.

Defines rule #16.

Overlap of [19] adccca=aa with [21] aca=ddccb:

Critical pair: adcccddccb=aaca.

Reduce LHS:

Reduce RHS:

Defines rule #13.

Overlap of [21] aca=ddccb with [21] aca=ddccb:

Critical pair: acddccb=ddccbca.

Reduce LHS:

Defines rule #9.

Overlap of [21] aca=ddccb with [29] aa=dcbd:

Critical pair: acdcbd=ddccba.

Reduce LHS:

Reduce RHS:

Referenced by [37].

Overlap of [36] adccbd=d with [28] dccc=1:

Critical pair: adccb=dccc.

Reduce RHS:

Defines rule #12.

Overlap of [30] bdcbd=ca with [32] bdcb=caccc:

Critical pair: bdccaccc=cacb.

Flip LHS and RHS.

Referenced by [46].

Simplify [17] caccca=bccd.

Reduce RHS:

Referenced by [40].

Overlap of [28] dccc=1 with [39] caccca=bdcc:

Critical pair: dccbdcc=accca.

Flip LHS and RHS.

Defines rule #5.

Overlap of [28] dccc=1 with [12] caccb=bccac:

Critical pair: dccbccac=accb.

Flip LHS and RHS.

Defines rule #10.

Overlap of [31] adcbd=dcbda with [28] dccc=1:

Critical pair: adcb=dcbdaccc.

Defines rule #11.

Overlap of [24] bdccb=ccccac with [24] bdccb=ccccac:

Critical pair: bdccccccac=ccccacdccb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [28] dccc=1 with [43] ccccab=bcccac:

Critical pair: dbcccac=cab.

Flip LHS and RHS.

Referenced by [45].

Overlap of [28] dccc=1 with [44] cab=dbcccac:

Critical pair: dccdbcccac=ab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [28] dccc=1 with [38] cacb=bdccaccc:

Critical pair: dccbdccaccc=acb.

Flip LHS and RHS.

Defines rule #8.