Certificate for #21739 ⟨a, b | aaa=1, abbabba=b⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #22.

Referenced by [5], [9], [10], [19], [23], [57].

Axiom: abbabba=b.

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

Axiom: bbaba=c.

Referenced by [6], [12], [13], [14], [15], [20], [21], [24], [33], [41], [44].

Axiom: abacc=d.

Referenced by [5], [6], [7], [23], [42].

Overlap of [1] aaa=1 with [4] abacc=d:

Critical pair: aad=bacc.

Defines rule #17.

Referenced by [48].

Overlap of [3] bbaba=c with [4] abacc=d:

Critical pair: bbd=ccc.

Flip LHS and RHS.

Defines rule #9.

Referenced by [7], [8], [18], [42], [53], [54].

Overlap of [4] abacc=d with [6] ccc=bbd:

Critical pair: ababbd=dc.

Referenced by [30], [43].

Overlap of [6] ccc=bbd with [6] ccc=bbd:

Critical pair: cbbd=bbdc.

Flip LHS and RHS.

Referenced by [44].

Overlap of [1] aaa=1 with [2] abbabba=b:

Critical pair: aab=bbabba.

Flip LHS and RHS.

Referenced by [22].

Overlap of [2] abbabba=b with [1] aaa=1:

Critical pair: abbabb=baa.

Flip LHS and RHS.

Referenced by [20], [21], [45].

Overlap of [2] abbabba=b with [2] abbabba=b:

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [13], [16], [17], [20], [21], [24], [25], [28], [31], [32], [41], [48], [50], [53], [55].

Overlap of [2] abbabba=b with [3] bbaba=c:

Critical pair: abbac=bba.

Referenced by [19], [21], [25].

Overlap of [11] bbba=abbb with [3] bbaba=c:

Critical pair: bc=abbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14], [15], [16], [17], [30], [32], [36], [37].

Overlap of [3] bbaba=c with [13] ababbb=bc:

Critical pair: bbbc=cbbb.

Defines rule #6.

Referenced by [18], [20], [21], [48], [53], [55], [56], [58], [59].

Overlap of [3] bbaba=c with [13] ababbb=bc:

Critical pair: bbabbc=cbabbb.

Flip LHS and RHS.

Referenced by [24], [25], [28].

Overlap of [13] ababbb=bc with [11] bbba=abbb:

Critical pair: abababbb=bcba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [13] ababbb=bc with [11] bbba=abbb:

Critical pair: ababbabbb=bcbba.

Referenced by [26].

Overlap of [14] bbbc=cbbb with [6] ccc=bbd:

Critical pair: bbbbbd=cbbbcc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [1] aaa=1 with [12] abbac=bba:

Critical pair: aabba=bbac.

Referenced by [20], [28].

Overlap of [3] bbaba=c with [10] baa=abbabb:

Critical pair: bbaabbabb=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [48], [56].

Overlap of [10] baa=abbabb with [12] abbac=bba:

Critical pair: babba=abbabbbbac.

Reduce RHS:

Referenced by [22], [26].

Simplify [9] bbabba=aab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [23], [24], [25], [28].

Overlap of [1] aaa=1 with [22] aab=baccbbb:

Critical pair: abaccbbb=b.

Reduce LHS:

Referenced by [27], [30], [31], [34], [38].

Overlap of [22] aab=baccbbb with [3] bbaba=c:

Critical pair: aac=baccbbbbaba.

Reduce RHS:

Defines rule #18.

Referenced by [26].

Overlap of [22] aab=baccbbb with [12] abbac=bba:

Critical pair: abba=baccbbbbac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [17] ababbabbb=bcbba with [21] babba=accbbb:

Critical pair: aaccbbbbbb=bcbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [18] bbdbbb=bbbbbd with [23] dbbb=b:

Critical pair: bbb=bbbbbd.

Flip LHS and RHS.

Referenced by [34], [35].

Overlap of [19] aabba=bbac with [22] aab=baccbbb:

Critical pair: baccbbbba=bbac.

Reduce LHS:

Referenced by [29].

Overlap of [25] bacbbabbcc=abba with [28] bacbbabbc=bbac:

Critical pair: bbacc=abba.

Flip LHS and RHS.

Defines rule #20.

Referenced by [45], [48], [53], [54].

Overlap of [7] ababbd=dc with [23] dbbb=b:

Critical pair: ababbb=dcbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [23] dbbb=b with [11] bbba=abbb:

Critical pair: dabbb=ba.

Referenced by [32], [35], [40].

Overlap of [31] dabbb=ba with [11] bbba=abbb:

Critical pair: dababbb=baba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33], [44].

Overlap of [3] bbaba=c with [32] baba=dbc:

Critical pair: bbadbc=cba.

Flip LHS and RHS.

Referenced by [46].

Overlap of [23] dbbb=b with [27] bbbbbd=bbb:

Critical pair: dbbb=bbbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [36], [37], [38], [39], [40], [41], [48], [50], [53], [55], [56], [58], [60], [61].

Overlap of [31] dabbb=ba with [27] bbbbbd=bbb:

Critical pair: dabbb=babbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [49], [54], [55].

Overlap of [13] ababbb=bc with [34] bbbd=b:

Critical pair: abab=bcd.

Referenced by [37].

Overlap of [13] ababbb=bc with [34] bbbd=b:

Critical pair: ababb=bcbd.

Reduce LHS:

Referenced by [43].

Overlap of [23] dbbb=b with [34] bbbd=b:

Critical pair: db=bd.

Defines rule #1.

Referenced by [41], [42], [44], [46], [49], [50], [53], [55], [56], [63], [64], [65], [66], [67].

Overlap of [30] dcbbb=bc with [34] bbbd=b:

Critical pair: dcb=bcd.

Referenced by [43].

Overlap of [31] dabbb=ba with [34] bbbd=b:

Critical pair: dab=bad.

Referenced by [41], [48], [49], [50].

Overlap of [38] db=bd with [3] bbaba=c:

Critical pair: dc=bdbaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [42], [43], [47].

Overlap of [4] abacc=d with [41] aba=dc:

Critical pair: dccc=d.

Reduce LHS:

Defines rule #3.

Referenced by [51], [53].

Overlap of [7] ababbd=dc with [41] aba=dc:

Critical pair: dcbbd=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [46], [47], [53], [55], [56].

Overlap of [3] bbaba=c with [32] baba=dbc:

Critical pair: bdbc=c.

Reduce LHS:

Defines rule #4.

Referenced by [48], [53], [55], [56], [62], [63], [65], [67].

Simplify [10] baa=abbabb.

Reduce RHS:

Defines rule #21.

Simplify [33] cba=bbadbc.

Reduce RHS:

Defines rule #14.

Referenced by [48].

Simplify [41] aba=dc.

Reduce RHS:

Defines rule #19.

Referenced by [48], [53], [56], [57].

Overlap of [5] aad=bacc with [40] dab=bad:

Critical pair: aabad=baccab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [38] db=bd with [35] babbd=ba:

Critical pair: dba=bdabbd.

Reduce LHS:

Reduce RHS:

Referenced by [50].

Overlap of [38] db=bd with [49] bda=bbabdd:

Critical pair: dbbabdd=bdda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [42] bbdd=d with [50] bdda=abdd:

Critical pair: babdd=da.

Flip LHS and RHS.

Defines rule #11.

Referenced by [55].

Simplify [26] bcbba=baccbbccbbbbbb.

Reduce RHS:

Referenced by [56].

Overlap of [29] abba=bbacc with [29] abba=bbacc:

Critical pair: abbbbacc=bbaccbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [54].

Overlap of [29] abba=bbacc with [53] bbaccbba=b:

Critical pair: ab=bbaccccbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [55], [56].

Overlap of [38] db=bd with [54] bbacbba=ab:

Critical pair: dab=bdbacbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [57].

Overlap of [54] bbacbba=ab with [54] bbacbba=ab:

Critical pair: bbacab=abcbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [1] aaa=1 with [55] acbba=bad:

Critical pair: aabad=cbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [14] bbbc=cbbb with [56] bcbcdddd=ccbbbbbb:

Critical pair: bbccbbbbbb=cbbbbcdddd.

Reduce RHS:

Referenced by [59], [60].

Overlap of [14] bbbc=cbbb with [58] bbccbbbbbb=cbcbddd:

Critical pair: bcbcbddd=cbbbcbbbbbb.

Reduce RHS:

Referenced by [63].

Overlap of [58] bbccbbbbbb=cbcbddd with [34] bbbd=b:

Critical pair: bbccbbbb=cbcbdddd.

Referenced by [61].

Overlap of [60] bbccbbbb=cbcbdddd with [34] bbbd=b:

Critical pair: bbccbb=cbcbddddd.

Referenced by [62].

Overlap of [61] bbccbb=cbcbddddd with [44] cbbd=c:

Critical pair: bbcc=cbcbdddddd.

Defines rule #8.

Overlap of [59] bcbcbddd=ccbbbbbbbbb with [38] db=bd:

Critical pair: bcbcbddbd=ccbbbbbbbbbb.

Reduce LHS:

Referenced by [64].

Overlap of [63] bcbcdd=ccbbbbbbbbbb with [38] db=bd:

Critical pair: bcbcdbd=ccbbbbbbbbbbb.

Reduce LHS:

Referenced by [65].

Overlap of [64] bcbcbdd=ccbbbbbbbbbbb with [38] db=bd:

Critical pair: bcbcbdbd=ccbbbbbbbbbbbb.

Reduce LHS:

Referenced by [66].

Overlap of [65] bcbcd=ccbbbbbbbbbbbb with [38] db=bd:

Critical pair: bcbcbd=ccbbbbbbbbbbbbb.

Referenced by [67].

Overlap of [66] bcbcbd=ccbbbbbbbbbbbbb with [38] db=bd:

Critical pair: bcbcbbd=ccbbbbbbbbbbbbbb.

Reduce LHS:

Defines rule #7.