Certificate for #1433 ⟨a, b | aababbbaba=1⟩

Completion settings:

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

Axiom: aababbbaba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [25], [28], [30], [33].

Axiom: babbbab=d.

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

Overlap of [1] aababbbaba=1 with [3] babbbab=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], [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], [22], [26], [27], [32], [34].

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

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [27].

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

Critical pair: babbd=dbbab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [13], [14].

Overlap of [9] cd=1 with [12] dbbab=babbd:

Critical pair: cbabbd=bbab.

Referenced by [15].

Overlap of [10] ad=da with [12] dbbab=babbd:

Critical pair: ababbd=dabbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [21].

Overlap of [13] cbabbd=bbab with [11] dc=1:

Critical pair: cbabb=bbabc.

Defines rule #6.

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

Overlap of [5] ac=ca with [15] cbabb=bbabc:

Critical pair: abbabc=cababb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [20].

Overlap of [15] cbabb=bbabc with [3] babbbab=d:

Critical pair: cd=bbabcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19], [23], [24].

Overlap of [3] babbbab=d with [17] bbabcbab=1:

Critical pair: babbba=dbabcbab.

Flip LHS and RHS.

Referenced by [22].

Overlap of [17] bbabcbab=1 with [3] babbbab=d:

Critical pair: bbabcbad=abbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [5] ac=ca with [16] cababb=abbabc:

Critical pair: aabbabc=caababb.

Flip LHS and RHS.

Defines rule #12.

Referenced by [31].

Overlap of [10] ad=da with [14] dabbab=ababbd:

Critical pair: aababbd=daabbab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [27].

Overlap of [9] cd=1 with [18] dbabcbab=babbba:

Critical pair: cbabbba=babcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [17] bbabcbab=1 with [22] babcbab=bbabcba:

Critical pair: bbabcbabbabcba=abcbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [28], [29].

Overlap of [17] bbabcbab=1 with [22] babcbab=bbabcba:

Critical pair: bbbabcba=1.

Referenced by [25].

Overlap of [24] bbbabcba=1 with [2] aaa=c:

Critical pair: bbbabcbc=aa.

Referenced by [26].

Overlap of [25] bbbabcbc=aa with [9] cd=1:

Critical pair: bbbabcb=aad.

Reduce RHS:

Defines rule #17.

Referenced by [27].

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

Critical pair: bbbabcdaa=daabbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [31].

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

Critical pair: aababcba=cbcbab.

Referenced by [30].

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

Critical pair: abcbbabcba=babcbacbab.

Reduce RHS:

Referenced by [33].

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

Critical pair: aababcbc=cbcbabaa.

Referenced by [32].

Overlap of [20] caababb=aabbabc with [27] aababbb=bbbabaa:

Critical pair: cbbbabaa=aabbabcb.

Flip LHS and RHS.

Defines rule #15.

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

Critical pair: aababcb=cbcbabaad.

Reduce RHS:

Defines rule #11.

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

Critical pair: abcbbabcbc=babcbcababaa.

Referenced by [34].

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

Critical pair: abcbbabcb=babcbcababaad.

Reduce RHS:

Defines rule #18.