Certificate for #689 ⟨a, b | aabbbabba=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. bbbabb=d

Axiom: aabbbabba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [16], [18], [20], [23], [26].

Axiom: bbbabb=d.

Defines rule #16.

Referenced by [4], [12], [13], [18].

Overlap of [1] aabbbabba=1 with [3] bbbabb=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 [17].

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], [14], [18], [20], [28].

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], [15], [19], [21].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [16], [24], [25], [26], [27].

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

Critical pair: bbbad=dbabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [15].

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

Critical pair: bbbabd=dbbabb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [20], [21].

Overlap of [9] cd=1 with [12] dbabb=bbbda:

Critical pair: cbbbda=babb.

Referenced by [16].

Overlap of [10] ad=da with [12] dbabb=bbbda:

Critical pair: abbbda=dababb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [19].

Overlap of [14] cbbbda=babb with [2] aaa=c:

Critical pair: cbbbdc=babbaa.

Reduce LHS:

Defines rule #6.

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

Overlap of [5] ac=ca with [16] cbbb=babbaa:

Critical pair: ababbaa=cabbb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [16] cbbb=babbaa with [3] bbbabb=d:

Critical pair: cd=babbaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [10] ad=da with [15] dababb=abbbda:

Critical pair: aabbbda=daababb.

Flip LHS and RHS.

Referenced by [25].

Overlap of [9] cd=1 with [13] dbbabb=bbbabd:

Critical pair: cbbbabd=bbabb.

Reduce LHS:

Referenced by [22].

Overlap of [10] ad=da with [13] dbbabb=bbbabd:

Critical pair: abbbabd=dabbabb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [18] babbcbb=1 with [20] babbcbd=bbabb:

Critical pair: babbcbbbabb=abbcbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [2] aaa=c with [22] abbcbd=babb:

Critical pair: aababb=cbbcbd.

Defines rule #12.

Referenced by [25], [27].

Overlap of [22] abbcbd=babb with [11] dc=1:

Critical pair: abbcb=babbc.

Defines rule #8.

Referenced by [27].

Overlap of [19] daababb=aabbbda with [23] aababb=cbbcbd:

Critical pair: dcbbcbd=aabbbda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [25] aabbbda=bbcbd with [2] aaa=c:

Critical pair: aabbbdc=bbcbdaa.

Reduce LHS:

Defines rule #11.

Overlap of [23] aababb=cbbcbd with [24] abbcb=babbc:

Critical pair: aabbabbc=cbbcbdcb.

Reduce RHS:

Referenced by [28].

Overlap of [27] aabbabbc=cbbcbb with [9] cd=1:

Critical pair: aabbabb=cbbcbbd.

Defines rule #15.