Certificate for #3146 ⟨a, b | aabbbababba=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. bbbababb=d

Axiom: aabbbababba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [16], [18], [24], [28], [29], [31], [34], [37], [41], [44].

Axiom: bbbababb=d.

Defines rule #18.

Referenced by [4], [12], [13], [18], [19], [20], [29], [30], [32].

Overlap of [1] aabbbababba=1 with [3] bbbababb=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], [22], [33], [43].

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], [31], [38], [40], [42], [45].

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], [29], [38], [40], [42], [45].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [16], [22], [25], [26], [27], [28], [29], [33].

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

Critical pair: bbbabad=dbababb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [15].

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

Critical pair: bbbababd=dbbababb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [9] cd=1 with [12] dbababb=bbbabda:

Critical pair: cbbbabda=bababb.

Referenced by [16].

Overlap of [10] ad=da with [12] dbababb=bbbabda:

Critical pair: abbbabda=dabababb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [21], [22].

Overlap of [14] cbbbabda=bababb with [2] aaa=c:

Critical pair: cbbbabdc=bababbaa.

Reduce LHS:

Defines rule #6.

Referenced by [17], [18], [19], [31], [35].

Overlap of [5] ac=ca with [16] cbbbab=bababbaa:

Critical pair: abababbaa=cabbbab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [16] cbbbab=bababbaa with [3] bbbababb=d:

Critical pair: cd=bababbaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20], [23].

Overlap of [16] cbbbab=bababbaa with [3] bbbababb=d:

Critical pair: cbbbad=bababbaabbababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [18] bababbcbb=1 with [3] bbbababb=d:

Critical pair: bababbcbd=bbababb.

Referenced by [22], [23].

Overlap of [10] ad=da with [15] dabababb=abbbabda:

Critical pair: aabbbabda=daabababb.

Flip LHS and RHS.

Referenced by [27].

Overlap of [15] dabababb=abbbabda with [20] bababbcbd=bbababb:

Critical pair: dabbababb=abbbabdacbd.

Reduce RHS:

Defines rule #16.

Overlap of [18] bababbcbb=1 with [20] bababbcbd=bbababb:

Critical pair: bababbcbbbababb=ababbcbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [2] aaa=c with [23] ababbcbd=bababb:

Critical pair: aabababb=cbabbcbd.

Defines rule #14.

Referenced by [26], [27].

Overlap of [23] ababbcbd=bababb with [11] dc=1:

Critical pair: ababbcb=bababbc.

Defines rule #9.

Referenced by [26], [31].

Overlap of [24] aabababb=cbabbcbd with [25] ababbcb=bababbc:

Critical pair: aabbababbc=cbabbcbdcb.

Reduce RHS:

Referenced by [39].

Overlap of [21] daabababb=aabbbabda with [24] aabababb=cbabbcbd:

Critical pair: dcbabbcbd=aabbbabda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [27] aabbbabda=babbcbd with [2] aaa=c:

Critical pair: aabbbabdc=babbcbdaa.

Reduce LHS:

Defines rule #12.

Referenced by [29], [36].

Overlap of [28] aabbbab=babbcbdaa with [3] bbbababb=d:

Critical pair: aad=babbcbdaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [3] bbbababb=d with [29] babbcbbb=daa:

Critical pair: bbbababdaa=dabbcbbb.

Flip LHS and RHS.

Referenced by [31].

Overlap of [9] cd=1 with [30] dabbcbbb=bbbababdaa:

Critical pair: cbbbababdaa=abbcbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [31] abbcbbb=bbababbaa with [3] bbbababb=d:

Critical pair: abbcbbd=bbababbaabbababb.

Reduce RHS:

Referenced by [33].

Overlap of [32] abbcbbd=bcbbbda with [11] dc=1:

Critical pair: abbcbb=bcbbbdac.

Reduce RHS:

Defines rule #8.

Referenced by [34], [35], [36], [39].

Overlap of [2] aaa=c with [33] abbcbb=bcbbba:

Critical pair: aabcbbba=cbbcbb.

Referenced by [37].

Overlap of [16] cbbbab=bababbaa with [33] abbcbb=bcbbba:

Critical pair: cbbbbcbbba=bababbaabcbb.

Referenced by [41].

Overlap of [28] aabbbab=babbcbdaa with [33] abbcbb=bcbbba:

Critical pair: aabbbbcbbba=babbcbdaabcbb.

Referenced by [44].

Overlap of [34] aabcbbba=cbbcbb with [2] aaa=c:

Critical pair: aabcbbbc=cbbcbbaa.

Referenced by [38].

Overlap of [37] aabcbbbc=cbbcbbaa with [9] cd=1:

Critical pair: aabcbbb=cbbcbbaad.

Reduce RHS:

Defines rule #13.

Simplify [26] aabbababbc=cbabbcbb.

Reduce RHS:

Referenced by [40].

Overlap of [39] aabbababbc=cbbcbbba with [9] cd=1:

Critical pair: aabbababb=cbbcbbbad.

Reduce RHS:

Defines rule #17.

Overlap of [35] cbbbbcbbba=bababbaabcbb with [2] aaa=c:

Critical pair: cbbbbcbbbc=bababbaabcbbaa.

Referenced by [42].

Overlap of [41] cbbbbcbbbc=bababbaabcbbaa with [9] cd=1:

Critical pair: cbbbbcbbb=bababbaabcbbaad.

Reduce RHS:

Defines rule #19.

Referenced by [43].

Overlap of [5] ac=ca with [42] cbbbbcbbb=bababbaabcbbdaa:

Critical pair: abababbaabcbbdaa=cabbbbcbbb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [36] aabbbbcbbba=babbcbdaabcbb with [2] aaa=c:

Critical pair: aabbbbcbbbc=babbcbdaabcbbaa.

Referenced by [45].

Overlap of [44] aabbbbcbbbc=babbcbdaabcbbaa with [9] cd=1:

Critical pair: aabbbbcbbb=babbcbdaabcbbaad.

Reduce RHS:

Defines rule #21.