Certificate for #3163 ⟨a, b | aabbbbbabba=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. bbbbbabb=d

Axiom: aabbbbbabba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [16], [18], [27].

Axiom: bbbbbabb=d.

Defines rule #18.

Referenced by [4], [12], [13], [18], [21], [22], [25].

Overlap of [1] aabbbbbabba=1 with [3] bbbbbabb=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], [32].

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], [24], [26], [28], [30], [33], [38].

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

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

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

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

Critical pair: bbbbbad=dbbbabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [14], [15].

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

Critical pair: bbbbbabd=dbbbbabb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [35].

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

Critical pair: cbbbbbda=bbbabb.

Referenced by [16].

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

Critical pair: abbbbbda=dabbbabb.

Flip LHS and RHS.

Defines rule #12.

Overlap of [14] cbbbbbda=bbbabb with [2] aaa=c:

Critical pair: cbbbbbdc=bbbabbaa.

Reduce LHS:

Defines rule #9.

Referenced by [17], [18].

Overlap of [5] ac=ca with [16] cbbbbb=bbbabbaa:

Critical pair: abbbabbaa=cabbbbb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [32].

Overlap of [16] cbbbbb=bbbabbaa with [3] bbbbbabb=d:

Critical pair: cd=bbbabbaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [18] bbbabbcbb=1 with [18] bbbabbcbb=1:

Critical pair: bbbabbc=babbcbb.

Flip LHS and RHS.

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

Overlap of [18] bbbabbcbb=1 with [18] bbbabbcbb=1:

Critical pair: bbbabbcb=bbabbcbb.

Reduce RHS:

Referenced by [22].

Overlap of [3] bbbbbabb=d with [19] babbcbb=bbbabbc:

Critical pair: bbbbbabbbbabbc=dabbcbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [19] babbcbb=bbbabbc with [18] bbbabbcbb=1:

Critical pair: babbcb=bbbabbcbbabbcbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [23].

Simplify [21] dabbcbb=dbbabbc.

Reduce LHS:

Referenced by [24].

Overlap of [9] cd=1 with [23] dbabbcb=dbbabbc:

Critical pair: cdbbabbc=babbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [3] bbbbbabb=d with [24] babbcb=bbabbc:

Critical pair: bbbbbabbbabbc=dabbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [9] cd=1 with [25] dabbcb=dbabbc:

Critical pair: cdbabbc=abbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [27], [29], [31], [34].

Overlap of [2] aaa=c with [26] abbcb=babbc:

Critical pair: aababbc=cbbcb.

Referenced by [28], [29].

Overlap of [27] aababbc=cbbcb with [9] cd=1:

Critical pair: aababb=cbbcbd.

Defines rule #7.

Overlap of [27] aababbc=cbbcb with [26] abbcb=babbc:

Critical pair: aabbabbc=cbbcbb.

Referenced by [30], [31].

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

Critical pair: aabbabb=cbbcbbd.

Defines rule #8.

Overlap of [29] aabbabbc=cbbcbb with [26] abbcb=babbc:

Critical pair: aabbbabbc=cbbcbbb.

Referenced by [33], [34].

Overlap of [5] ac=ca with [17] cabbbbb=abbbabbaa:

Critical pair: aabbbabbaa=caabbbbb.

Flip LHS and RHS.

Referenced by [36].

Overlap of [31] aabbbabbc=cbbcbbb with [9] cd=1:

Critical pair: aabbbabb=cbbcbbbd.

Defines rule #14.

Referenced by [36].

Overlap of [31] aabbbabbc=cbbcbbb with [26] abbcb=babbc:

Critical pair: aabbbbabbc=cbbcbbbb.

Referenced by [38].

Overlap of [10] ad=da with [13] dbbbbabb=bbbbbabd:

Critical pair: abbbbbabd=dabbbbabb.

Flip LHS and RHS.

Defines rule #16.

Simplify [32] caabbbbb=aabbbabbaa.

Reduce RHS:

Referenced by [37].

Overlap of [11] dc=1 with [36] caabbbbb=cbbcbbbdaa:

Critical pair: dcbbcbbbdaa=aabbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [34] aabbbbabbc=cbbcbbbb with [9] cd=1:

Critical pair: aabbbbabb=cbbcbbbbd.

Defines rule #17.