Certificate for #3536 ⟨a, b, c | bb=ac, caa=a⟩

Completion settings:

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

Axiom: bb=ac.

Flip LHS and RHS.

Defines rule #18.

Referenced by [4], [5], [7], [9], [10], [12], [16], [29], [34], [39], [44], [46].

Axiom: caa=a.

Referenced by [4], [5], [6], [19], [26], [31], [35].

Axiom: aba=d.

Defines rule #22.

Referenced by [6], [7], [8], [11], [12], [25].

Overlap of [1] ac=bb with [2] caa=a:

Critical pair: aa=bbaa.

Flip LHS and RHS.

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

Overlap of [2] caa=a with [1] ac=bb:

Critical pair: cabb=ac.

Reduce RHS:

Referenced by [10], [11], [13], [14], [20], [29], [30], [32], [40].

Overlap of [2] caa=a with [3] aba=d:

Critical pair: cad=aba.

Reduce RHS:

Referenced by [9], [36].

Overlap of [3] aba=d with [1] ac=bb:

Critical pair: abbb=dc.

Referenced by [14], [15], [16].

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

Critical pair: abd=dba.

Defines rule #19.

Referenced by [13].

Overlap of [1] ac=bb with [6] cad=d:

Critical pair: ad=bbad.

Flip LHS and RHS.

Referenced by [11], [17].

Overlap of [1] ac=bb with [5] cabb=bb:

Critical pair: abb=bbabb.

Flip LHS and RHS.

Referenced by [40], [41].

Overlap of [5] cabb=bb with [9] bbad=ad:

Critical pair: cabad=bbbad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [3] aba=d with [11] bad=cdd:

Critical pair: acdd=dd.

Reduce LHS:

Referenced by [13], [15].

Overlap of [5] cabb=bb with [12] bbdd=dd:

Critical pair: cabdd=bbbdd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [15].

Overlap of [5] cabb=bb with [7] abbb=dc:

Critical pair: cdc=bbb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [16], [21], [22], [23], [24], [25], [26], [27], [40], [41], [43].

Overlap of [7] abbb=dc with [12] bbdd=dd:

Critical pair: abbdd=dcbdd.

Reduce LHS:

Reduce RHS:

Referenced by [18].

Overlap of [7] abbb=dc with [14] bbb=cdc:

Critical pair: acdc=dc.

Reduce LHS:

Referenced by [19], [20], [22], [29], [34].

Overlap of [9] bbad=ad with [11] bad=cdd:

Critical pair: bcdd=ad.

Flip LHS and RHS.

Referenced by [18], [25], [34], [36], [37].

Overlap of [15] add=dccdcdd with [17] ad=bcdd:

Critical pair: bcddd=dccdcdd.

Referenced by [38].

Overlap of [16] bbdc=dc with [2] caa=a:

Critical pair: bbda=dcaa.

Reduce RHS:

Referenced by [23], [24].

Overlap of [16] bbdc=dc with [5] cabb=bb:

Critical pair: bbdbb=dcabb.

Reduce RHS:

Referenced by [33].

Overlap of [14] bbb=cdc with [14] bbb=cdc:

Critical pair: bcdc=cdcb.

Defines rule #7.

Referenced by [28], [29], [31], [32], [33], [44], [46].

Overlap of [14] bbb=cdc with [16] bbdc=dc:

Critical pair: bdc=cdcdc.

Defines rule #5.

Referenced by [29], [30], [44], [46].

Overlap of [14] bbb=cdc with [19] bbda=da:

Critical pair: bda=cdcda.

Defines rule #15.

Referenced by [24].

Overlap of [14] bbb=cdc with [19] bbda=da:

Critical pair: bbda=cdcbda.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [4] bbaa=aa with [3] aba=d:

Critical pair: bbad=aaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [34], [36], [37], [38].

Overlap of [14] bbb=cdc with [4] bbaa=aa:

Critical pair: baa=cdcaa.

Reduce RHS:

Referenced by [27], [28].

Overlap of [14] bbb=cdc with [4] bbaa=aa:

Critical pair: bbaa=cdcbaa.

Reduce LHS:

Reduce RHS:

Defines rule #21.

Referenced by [28], [31], [35].

Simplify [26] baa=cda.

Reduce LHS:

Referenced by [31].

Overlap of [5] cabb=bb with [22] bdc=cdcdc:

Critical pair: cabcdcdc=bbdc.

Reduce LHS:

Reduce RHS:

Referenced by [44].

Overlap of [22] bdc=cdcdc with [5] cabb=bb:

Critical pair: bdbb=cdcdcabb.

Reduce RHS:

Defines rule #11.

Referenced by [33].

Overlap of [21] bcdc=cdcb with [2] caa=a:

Critical pair: bcda=cdcbaa.

Reduce RHS:

Defines rule #16.

Overlap of [21] bcdc=cdcb with [5] cabb=bb:

Critical pair: bcdbb=cdcbabb.

Flip LHS and RHS.

Referenced by [41].

Simplify [20] bbdbb=dbb.

Reduce LHS:

Referenced by [34].

Overlap of [1] ac=bb with [33] cdccdcdbb=dbb:

Critical pair: adbb=bbdccdcdbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [2] caa=a with [27] aa=cdccda:

Critical pair: ccdccda=a.

Defines rule #14.

Referenced by [39].

Overlap of [6] cad=d with [17] ad=bcdd:

Critical pair: cbcdd=d.

Reduce LHS:

Defines rule #2.

Referenced by [46].

Simplify [17] ad=bcdd.

Reduce RHS:

Defines rule #17.

Referenced by [44], [46].

Overlap of [18] bcddd=dccdcdd with [25] bcdd=cdccdd:

Critical pair: cdccddd=dccdcdd.

Flip LHS and RHS.

Defines rule #1.

Overlap of [35] ccdccda=a with [1] ac=bb:

Critical pair: ccdccdbb=ac.

Reduce RHS:

Defines rule #9.

Overlap of [14] bbb=cdc with [10] bbabb=abb:

Critical pair: babb=cdcabb.

Reduce RHS:

Referenced by [42].

Overlap of [14] bbb=cdc with [10] bbabb=abb:

Critical pair: bbabb=cdcbabb.

Reduce LHS:

Reduce RHS:

Referenced by [42], [45].

Simplify [40] babb=cdbb.

Reduce LHS:

Referenced by [43].

Overlap of [14] bbb=cdc with [42] bbcdbb=cdbb:

Critical pair: bcdbb=cdccdbb.

Defines rule #12.

Referenced by [45].

Overlap of [1] ac=bb with [29] cdccdcdc=dc:

Critical pair: adc=bbdccdcdc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [46].

Simplify [41] abb=bcdbb.

Reduce RHS:

Defines rule #20.

Overlap of [1] ac=bb with [24] cdccdcda=da:

Critical pair: ada=bbdccdcda.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.