Certificate for #1446 ⟨a, b | aabbaabbba=1⟩

Completion settings:

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

Axiom: aabbaabbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [14], [22], [23], [24], [25], [31].

Axiom: bbaabbb=d.

Referenced by [4], [12], [16], [17], [18].

Overlap of [1] aabbaabbba=1 with [3] bbaabbb=d:

Critical pair: aada=1.

Referenced by [6], [7], [8], [9], [10].

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

Critical pair: ac=ca.

Defines rule #3.

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

Overlap of [2] aaa=c with [4] aada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aad=ada.

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

Overlap of [6] cda=a with [4] aada=1:

Critical pair: cd=aada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [4] aada=1 with [7] aad=ada:

Critical pair: adaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [10], [11], [13], [19], [20], [21], [28].

Overlap of [4] aada=1 with [7] aad=ada:

Critical pair: aadada=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [14], [16], [26], [29].

Overlap of [2] aaa=c with [10] ad=da:

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [14], [15], [23], [24], [27], [30], [31].

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

Critical pair: bbaabd=daabbb.

Flip LHS and RHS.

Referenced by [13], [14], [24].

Overlap of [9] cd=1 with [12] daabbb=bbaabd:

Critical pair: cbbaabd=aabbb.

Flip LHS and RHS.

Referenced by [26].

Overlap of [10] ad=da with [12] daabbb=bbaabd:

Critical pair: abbaabd=daaabbb.

Reduce RHS:

Referenced by [15].

Overlap of [14] abbaabd=bbb with [11] dc=1:

Critical pair: abbaab=bbbc.

Defines rule #8.

Referenced by [16], [25].

Overlap of [15] abbaab=bbbc with [3] bbaabbb=d:

Critical pair: ad=bbbcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [17], [18], [19], [24], [27], [29], [30].

Overlap of [3] bbaabbb=d with [16] bbbcbb=da:

Critical pair: bbaabda=dbcbb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [21].

Overlap of [3] bbaabbb=d with [16] bbbcbb=da:

Critical pair: bbaabbda=dbbcbb.

Flip LHS and RHS.

Defines rule #11.

Overlap of [16] bbbcbb=da with [16] bbbcbb=da:

Critical pair: bbbcda=dabcbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [9] cd=1 with [19] dabcbb=bbba:

Critical pair: cbbba=abcbb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [22].

Overlap of [9] cd=1 with [17] dbcbb=bbaabda:

Critical pair: cbbaabda=bcbb.

Referenced by [22], [23], [24].

Overlap of [20] abcbb=cbbba with [21] cbbaabda=bcbb:

Critical pair: abbcbb=cbbbaaabda.

Reduce RHS:

Defines rule #12.

Overlap of [21] cbbaabda=bcbb with [2] aaa=c:

Critical pair: cbbaabdc=bcbbaa.

Reduce LHS:

Defines rule #6.

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

Overlap of [21] cbbaabda=bcbb with [12] daabbb=bbaabd:

Critical pair: cbbaabbbaabd=bcbbabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [23] cbbaab=bcbbaa with [15] abbaab=bbbc:

Critical pair: cbbabbbc=bcbbaabaab.

Reduce RHS:

Referenced by [28], [29].

Simplify [13] aabbb=cbbaabd.

Reduce RHS:

Defines rule #10.

Referenced by [31].

Overlap of [16] bbbcbb=da with [24] bcbbabbb=aabd:

Critical pair: bbbcbaabd=dacbbabbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [25] cbbabbbc=bbcbbcab with [9] cd=1:

Critical pair: cbbabbb=bbcbbcabd.

Defines rule #14.

Overlap of [25] cbbabbbc=bbcbbcab with [16] bbbcbb=da:

Critical pair: cbbada=bbcbbcabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [16] bbbcbb=da with [29] bbcbbcabbb=cbbdaa:

Critical pair: bbbccbbdaa=dacbbcabbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [31].

Overlap of [2] aaa=c with [30] abbcabbb=bbbccbbdaa:

Critical pair: aabbbccbbdaa=cbbcabbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.