Certificate for #3091 ⟨a, b | aababbbbaba=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. babbbbab=d

Axiom: aababbbbaba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [23], [27], [30], [33], [36], [39].

Axiom: babbbbab=d.

Referenced by [4], [12], [17], [19], [22], [24].

Overlap of [1] aababbbbaba=1 with [3] babbbbab=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], [20], [25].

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], [26], [28], [29], [32], [35], [38], [40].

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], [19], [21], [28], [32], [35], [38], [40].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [22], [24], [29].

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

Critical pair: babbbd=dbbbab.

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [9] cd=1 with [12] dbbbab=babbbd:

Critical pair: cbabbbd=bbbab.

Referenced by [15].

Overlap of [10] ad=da with [12] dbbbab=babbbd:

Critical pair: ababbbd=dabbbab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [21].

Overlap of [13] cbabbbd=bbbab with [11] dc=1:

Critical pair: cbabbb=bbbabc.

Defines rule #8.

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

Overlap of [5] ac=ca with [15] cbabbb=bbbabc:

Critical pair: abbbabc=cababbb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [20].

Overlap of [15] cbabbb=bbbabc with [3] babbbbab=d:

Critical pair: cd=bbbabcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [15] cbabbb=bbbabc with [17] bbbabcbab=1:

Critical pair: cba=bbbabcabcbab.

Flip LHS and RHS.

Referenced by [22].

Overlap of [17] bbbabcbab=1 with [3] babbbbab=d:

Critical pair: bbbabcbad=abbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [5] ac=ca with [16] cababbb=abbbabc:

Critical pair: aabbbabc=caababbb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [34].

Overlap of [10] ad=da with [14] dabbbab=ababbbd:

Critical pair: aababbbd=daabbbab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [29].

Overlap of [3] babbbbab=d with [18] bbbabcabcbab=cba:

Critical pair: babcba=dcabcbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [23], [24], [25], [31], [37].

Overlap of [2] aaa=c with [22] abcbab=babcba:

Critical pair: aababcba=cbcbab.

Referenced by [30], [31].

Overlap of [12] dbbbab=babbbd with [22] abcbab=babcba:

Critical pair: dbbbbabcba=babbbdcbab.

Reduce RHS:

Referenced by [26].

Overlap of [22] abcbab=babcba with [22] abcbab=babcba:

Critical pair: abcbbabcba=babcbacbab.

Reduce RHS:

Referenced by [36], [37].

Overlap of [9] cd=1 with [24] dbbbbabcba=d:

Critical pair: cd=bbbbabcba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [26] bbbbabcba=1 with [2] aaa=c:

Critical pair: bbbbabcbc=aa.

Referenced by [28].

Overlap of [27] bbbbabcbc=aa with [9] cd=1:

Critical pair: bbbbabcb=aad.

Reduce RHS:

Defines rule #19.

Referenced by [29].

Overlap of [28] bbbbabcb=daa with [28] bbbbabcb=daa:

Critical pair: bbbbabcdaa=daabbbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [34].

Overlap of [23] aababcba=cbcbab with [2] aaa=c:

Critical pair: aababcbc=cbcbabaa.

Referenced by [32].

Overlap of [23] aababcba=cbcbab with [22] abcbab=babcba:

Critical pair: aabbabcba=cbcbabb.

Referenced by [33].

Overlap of [30] aababcbc=cbcbabaa with [9] cd=1:

Critical pair: aababcb=cbcbabaad.

Reduce RHS:

Defines rule #7.

Overlap of [31] aabbabcba=cbcbabb with [2] aaa=c:

Critical pair: aabbabcbc=cbcbabbaa.

Referenced by [35].

Overlap of [20] caababbb=aabbbabc with [29] aababbbb=bbbbabaa:

Critical pair: cbbbbabaa=aabbbabcb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [33] aabbabcbc=cbcbabbaa with [9] cd=1:

Critical pair: aabbabcb=cbcbabbaad.

Reduce RHS:

Defines rule #12.

Overlap of [25] abcbbabcba=babcbcabab with [2] aaa=c:

Critical pair: abcbbabcbc=babcbcababaa.

Referenced by [38].

Overlap of [25] abcbbabcba=babcbcabab with [22] abcbab=babcba:

Critical pair: abcbbbabcba=babcbcababb.

Referenced by [39].

Overlap of [36] abcbbabcbc=babcbcababaa with [9] cd=1:

Critical pair: abcbbabcb=babcbcababaad.

Reduce RHS:

Defines rule #16.

Overlap of [37] abcbbbabcba=babcbcababb with [2] aaa=c:

Critical pair: abcbbbabcbc=babcbcababbaa.

Referenced by [40].

Overlap of [39] abcbbbabcbc=babcbcababbaa with [9] cd=1:

Critical pair: abcbbbabcb=babcbcababbaad.

Reduce RHS:

Defines rule #20.