Certificate for #1386 ⟨a, b | aaabbbbaba=1⟩

Completion settings:

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

Axiom: aaabbbbaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [9], [11], [19], [24], [26], [29], [38].

Axiom: bbbbab=d.

Defines rule #17.

Referenced by [4], [21], [26].

Overlap of [1] aaabbbbaba=1 with [3] bbbbab=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10], [11], [12], [14], [16].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [12], [15], [25], [35].

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

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10], [11], [13], [14].

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

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaad=aada.

Referenced by [10], [12], [16].

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [13].

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

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13], [14], [15].

Overlap of [7] cada=aa with [4] aaada=1:

Critical pair: cad=aaaada.

Reduce RHS:

Referenced by [12], [15], [20].

Overlap of [4] aaada=1 with [10] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [13].

Overlap of [6] cda=a with [10] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [10] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

Referenced by [15], [16].

Overlap of [10] aadaa=cd with [10] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [4] aaada=1 with [8] aaad=aada:

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [17], [18], [22], [26], [30], [32], [36].

Simplify [13] adaaa=cd.

Reduce RHS:

Referenced by [19].

Overlap of [15] cddaa=ada with [16] cd=1:

Critical pair: daa=ada.

Flip LHS and RHS.

Referenced by [19].

Simplify [17] adaaa=1.

Reduce LHS:

Defines rule #2.

Referenced by [20], [24], [37], [38].

Overlap of [19] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [23], [34], [37].

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

Critical pair: bbbbad=dbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [22], [23].

Overlap of [16] cd=1 with [21] dbbbab=bbbbda:

Critical pair: cbbbbda=bbbab.

Referenced by [24].

Overlap of [20] ad=da with [21] dbbbab=bbbbda:

Critical pair: abbbbda=dabbbab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [34].

Overlap of [22] cbbbbda=bbbab with [2] aaaa=c:

Critical pair: cbbbbdc=bbbabaaa.

Reduce LHS:

Defines rule #9.

Referenced by [25], [26].

Overlap of [5] ac=ca with [24] cbbbb=bbbabaaa:

Critical pair: abbbabaaa=cabbbb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [35].

Overlap of [24] cbbbb=bbbabaaa with [3] bbbbab=d:

Critical pair: cd=bbbabaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27], [28].

Overlap of [26] bbbabcb=1 with [26] bbbabcb=1:

Critical pair: bbbabc=bbabcb.

Flip LHS and RHS.

Referenced by [28].

Overlap of [27] bbabcb=bbbabc with [27] bbabcb=bbbabc:

Critical pair: bbabcbbbabc=bbbabcbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [29], [31], [33].

Overlap of [2] aaaa=c with [28] abcb=babc:

Critical pair: aaababc=cbcb.

Referenced by [30], [31].

Overlap of [29] aaababc=cbcb with [16] cd=1:

Critical pair: aaabab=cbcbd.

Defines rule #7.

Overlap of [29] aaababc=cbcb with [28] abcb=babc:

Critical pair: aaabbabc=cbcbb.

Referenced by [32], [33].

Overlap of [31] aaabbabc=cbcbb with [16] cd=1:

Critical pair: aaabbab=cbcbbd.

Defines rule #8.

Overlap of [31] aaabbabc=cbcbb with [28] abcb=babc:

Critical pair: aaabbbabc=cbcbbb.

Referenced by [36].

Overlap of [20] ad=da with [23] dabbbab=abbbbda:

Critical pair: aabbbbda=daabbbab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [37].

Overlap of [5] ac=ca with [25] cabbbb=abbbabaaa:

Critical pair: aabbbabaaa=caabbbb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [33] aaabbbabc=cbcbbb with [16] cd=1:

Critical pair: aaabbbab=cbcbbbd.

Defines rule #16.

Referenced by [37].

Overlap of [20] ad=da with [34] daabbbab=aabbbbda:

Critical pair: aaabbbbda=daaabbbab.

Reduce RHS:

Referenced by [38].

Overlap of [37] aaabbbbda=bcbbbd with [2] aaaa=c:

Critical pair: aaabbbbdc=bcbbbdaaa.

Reduce LHS:

Defines rule #15.