Certificate for #2894 ⟨a, b | aaaabbbbaba=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. aaaaa=c
  2. bbbbab=d

Axiom: aaaabbbbaba=1.

Referenced by [4].

Axiom: aaaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [10], [15], [17], [19], [24], [26], [29], [39].

Axiom: bbbbab=d.

Defines rule #19.

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

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

Critical pair: aaaada=1.

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

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

Critical pair: ac=ca.

Defines rule #3.

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

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [10].

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

Critical pair: aaaad=aaada.

Referenced by [9], [12], [19].

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

Critical pair: cd=aaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13].

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

Critical pair: cad=aaaaada.

Reduce RHS:

Referenced by [18].

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

Critical pair: bbbbad=dbbbab.

Flip LHS and RHS.

Referenced by [20].

Overlap of [4] aaaada=1 with [8] aaaad=aaada:

Critical pair: aaadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [13], [15], [19], [21], [26], [30], [32], [36].

Simplify [9] aaadaa=cd.

Reduce RHS:

Referenced by [14], [16].

Overlap of [13] aaadaa=1 with [13] aaadaa=1:

Critical pair: aaad=adaa.

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

Overlap of [2] aaaaa=c with [14] aaad=adaa:

Critical pair: aaadaa=cd.

Reduce LHS:

Reduce RHS:

Referenced by [16], [17].

Overlap of [13] aaadaa=1 with [14] aaad=adaa:

Critical pair: aaadaadaa=aad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [22].

Overlap of [16] aad=daa with [15] adaaaa=1:

Critical pair: a=daaaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [17] dca=a with [10] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [19], [20], [23], [35], [38].

Overlap of [2] aaaaa=c with [18] ad=da:

Critical pair: aaaada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [24], [38], [39].

Simplify [11] dbbbab=bbbbad.

Reduce RHS:

Defines rule #10.

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

Overlap of [12] cd=1 with [20] dbbbab=bbbbda:

Critical pair: cbbbbda=bbbab.

Referenced by [24].

Overlap of [16] aad=daa with [20] dbbbab=bbbbda:

Critical pair: aabbbbda=daabbbab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [35].

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

Critical pair: abbbbda=dabbbab.

Flip LHS and RHS.

Defines rule #12.

Overlap of [21] cbbbbda=bbbab with [2] aaaaa=c:

Critical pair: cbbbbdc=bbbabaaaa.

Reduce LHS:

Defines rule #9.

Referenced by [25], [26].

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

Critical pair: abbbabaaaa=cabbbb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [34].

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

Critical pair: cd=bbbabaaaaab.

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

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].

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

Critical pair: aaaababc=cbcb.

Referenced by [30], [31].

Overlap of [29] aaaababc=cbcb with [12] cd=1:

Critical pair: aaaabab=cbcbd.

Defines rule #7.

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

Critical pair: aaaabbabc=cbcbb.

Referenced by [32], [33].

Overlap of [31] aaaabbabc=cbcbb with [12] cd=1:

Critical pair: aaaabbab=cbcbbd.

Defines rule #8.

Overlap of [31] aaaabbabc=cbcbb with [27] bbabcb=bbbabc:

Critical pair: aaaabbbabc=cbcbbb.

Referenced by [36].

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

Critical pair: aabbbabaaaa=caabbbb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [37].

Overlap of [18] ad=da with [22] daabbbab=aabbbbda:

Critical pair: aaabbbbda=daaabbbab.

Flip LHS and RHS.

Defines rule #16.

Referenced by [38].

Overlap of [33] aaaabbbabc=cbcbbb with [12] cd=1:

Critical pair: aaaabbbab=cbcbbbd.

Defines rule #18.

Referenced by [38].

Overlap of [5] ac=ca with [34] caabbbb=aabbbabaaaa:

Critical pair: aaabbbabaaaa=caaabbbb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [18] ad=da with [35] daaabbbab=aaabbbbda:

Critical pair: aaaabbbbda=daaaabbbab.

Reduce RHS:

Referenced by [39].

Overlap of [38] aaaabbbbda=bcbbbd with [2] aaaaa=c:

Critical pair: aaaabbbbdc=bcbbbdaaaa.

Reduce LHS:

Defines rule #17.