Certificate for #3000 ⟨a, b | aaabbbbbaba=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. bbbbbab=d

Axiom: aaabbbbbaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [9], [11], [19], [24], [26], [31], [42].

Axiom: bbbbbab=d.

Defines rule #18.

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

Overlap of [1] aaabbbbbaba=1 with [3] bbbbbab=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], [39].

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], [32], [34], [36], [40].

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], [41], [42].

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

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [23], [38], [41].

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

Critical pair: bbbbbad=dbbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [22], [23].

Overlap of [16] cd=1 with [21] dbbbbab=bbbbbda:

Critical pair: cbbbbbda=bbbbab.

Referenced by [24].

Overlap of [20] ad=da with [21] dbbbbab=bbbbbda:

Critical pair: abbbbbda=dabbbbab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [38].

Overlap of [22] cbbbbbda=bbbbab with [2] aaaa=c:

Critical pair: cbbbbbdc=bbbbabaaa.

Reduce LHS:

Defines rule #10.

Referenced by [25], [26].

Overlap of [5] ac=ca with [24] cbbbbb=bbbbabaaa:

Critical pair: abbbbabaaa=cabbbbb.

Flip LHS and RHS.

Defines rule #12.

Referenced by [39].

Overlap of [24] cbbbbb=bbbbabaaa with [3] bbbbbab=d:

Critical pair: cd=bbbbabaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27], [28], [29], [30].

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

Critical pair: bbbbabc=bbbabcb.

Flip LHS and RHS.

Referenced by [28], [29], [30].

Overlap of [26] bbbbabcb=1 with [27] bbbabcb=bbbbabc:

Critical pair: bbbbabcbbbbabc=bbabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [27] bbbabcb=bbbbabc with [27] bbbabcb=bbbbabc:

Critical pair: bbbabcbbbbabc=bbbbabcbbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [29] babcb=bbabc with [26] bbbbabcb=1:

Critical pair: babc=bbabcbbbabcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [31], [33], [35], [37].

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

Critical pair: aaababc=cbcb.

Referenced by [32], [33].

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

Critical pair: aaabab=cbcbd.

Defines rule #7.

Overlap of [31] aaababc=cbcb with [30] abcb=babc:

Critical pair: aaabbabc=cbcbb.

Referenced by [34], [35].

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

Critical pair: aaabbab=cbcbbd.

Defines rule #8.

Overlap of [33] aaabbabc=cbcbb with [30] abcb=babc:

Critical pair: aaabbbabc=cbcbbb.

Referenced by [36], [37].

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

Critical pair: aaabbbab=cbcbbbd.

Defines rule #9.

Overlap of [35] aaabbbabc=cbcbbb with [30] abcb=babc:

Critical pair: aaabbbbabc=cbcbbbb.

Referenced by [40].

Overlap of [20] ad=da with [23] dabbbbab=abbbbbda:

Critical pair: aabbbbbda=daabbbbab.

Flip LHS and RHS.

Defines rule #15.

Referenced by [41].

Overlap of [5] ac=ca with [25] cabbbbb=abbbbabaaa:

Critical pair: aabbbbabaaa=caabbbbb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [37] aaabbbbabc=cbcbbbb with [16] cd=1:

Critical pair: aaabbbbab=cbcbbbbd.

Defines rule #17.

Referenced by [41].

Overlap of [20] ad=da with [38] daabbbbab=aabbbbbda:

Critical pair: aaabbbbbda=daaabbbbab.

Reduce RHS:

Referenced by [42].

Overlap of [41] aaabbbbbda=bcbbbbd with [2] aaaa=c:

Critical pair: aaabbbbbdc=bcbbbbdaaa.

Reduce LHS:

Defines rule #16.