Certificate for #1471 ⟨a, b | aabbbbbaba=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. aaa=c
  2. bbbbbab=d

Axiom: aabbbbbaba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [15], [17], [22].

Axiom: bbbbbab=d.

Defines rule #16.

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

Overlap of [1] aabbbbbaba=1 with [3] bbbbbab=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 [16], [29].

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], [17], [23], [25], [27], [30].

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

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [32].

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

Critical pair: bbbbbad=dbbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [13], [14].

Overlap of [9] cd=1 with [12] dbbbbab=bbbbbda:

Critical pair: cbbbbbda=bbbbab.

Referenced by [15].

Overlap of [10] ad=da with [12] dbbbbab=bbbbbda:

Critical pair: abbbbbda=dabbbbab.

Flip LHS and RHS.

Defines rule #13.

Overlap of [13] cbbbbbda=bbbbab with [2] aaa=c:

Critical pair: cbbbbbdc=bbbbabaa.

Reduce LHS:

Defines rule #10.

Referenced by [16], [17].

Overlap of [5] ac=ca with [15] cbbbbb=bbbbabaa:

Critical pair: abbbbabaa=cabbbbb.

Flip LHS and RHS.

Defines rule #12.

Referenced by [29].

Overlap of [15] cbbbbb=bbbbabaa with [3] bbbbbab=d:

Critical pair: cd=bbbbabaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18], [19], [20], [21].

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

Critical pair: bbbbabc=bbbabcb.

Flip LHS and RHS.

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

Overlap of [17] bbbbabcb=1 with [18] bbbabcb=bbbbabc:

Critical pair: bbbbabcbbbbabc=bbabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21].

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

Critical pair: bbbabcbbbbabc=bbbbabcbbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [20] babcb=bbabc with [17] bbbbabcb=1:

Critical pair: babc=bbabcbbbabcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [22], [28].

Overlap of [2] aaa=c with [21] abcb=babc:

Critical pair: aababc=cbcb.

Referenced by [23], [24].

Overlap of [22] aababc=cbcb with [9] cd=1:

Critical pair: aabab=cbcbd.

Defines rule #7.

Overlap of [22] aababc=cbcb with [20] babcb=bbabc:

Critical pair: aabbabc=cbcbb.

Referenced by [25], [26].

Overlap of [24] aabbabc=cbcbb with [9] cd=1:

Critical pair: aabbab=cbcbbd.

Defines rule #8.

Overlap of [24] aabbabc=cbcbb with [20] babcb=bbabc:

Critical pair: aabbbabc=cbcbbb.

Referenced by [27], [28].

Overlap of [26] aabbbabc=cbcbbb with [9] cd=1:

Critical pair: aabbbab=cbcbbbd.

Defines rule #9.

Overlap of [26] aabbbabc=cbcbbb with [21] abcb=babc:

Critical pair: aabbbbabc=cbcbbbb.

Referenced by [30].

Overlap of [5] ac=ca with [16] cabbbbb=abbbbabaa:

Critical pair: aabbbbabaa=caabbbbb.

Flip LHS and RHS.

Referenced by [31].

Overlap of [28] aabbbbabc=cbcbbbb with [9] cd=1:

Critical pair: aabbbbab=cbcbbbbd.

Defines rule #15.

Referenced by [31].

Simplify [29] caabbbbb=aabbbbabaa.

Reduce RHS:

Referenced by [32].

Overlap of [11] dc=1 with [31] caabbbbb=cbcbbbbdaa:

Critical pair: dcbcbbbbdaa=aabbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.