Certificate for #2987 ⟨a, b | aaabbbababa=1⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(c) = deg(d) = deg(a) = 0, c < d < a; deg(b) = 1
• Auxiliary generators:
  1. aaaa=c
  2. bbbabab=d

Axiom: aaabbbababa=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [23], [28], [33], [34], [35], [37], [42], [46], [47], [50], [52].

Axiom: bbbabab=d.

Referenced by [4], [12], [14].

Overlap of [1] aaabbbababa=1 with [3] bbbabab=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [9], [10], [11].

Overlap of [2] aaaa=c with [2] aaaa=c:

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [24], [29], [34], [40].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

Overlap of [4] aaada=1 with [4] aaada=1:

Critical pair: aaad=aada.

Flip LHS and RHS.

Referenced by [9], [10], [11].

Overlap of [6] cda=a with [4] aaada=1:

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #2.

Referenced by [15], [20], [23], [25], [28], [33], [34], [37], [42], [46], [47], [50], [52].

Overlap of [4] aaada=1 with [7] aada=aaad:

Critical pair: aaadaaad=ada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] aada=aaad with [7] aada=aaad:

Critical pair: aadaaad=aaadada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [22], [26], [27], [30], [31], [32], [33], [38], [41], [43], [45], [48], [49], [51], [53], [54], [55], [56].

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

Critical pair: dc=adaaa.

Reduce RHS:

Defines rule #1.

Referenced by [13].

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

Critical pair: bbbabad=dbbabab.

Referenced by [13].

Overlap of [12] bbbabad=dbbabab with [11] dc=1:

Critical pair: bbbaba=dbbababc.

Referenced by [14], [30].

Overlap of [3] bbbabab=d with [13] bbbaba=dbbababc:

Critical pair: dbbababcb=d.

Referenced by [15], [16].

Overlap of [8] cd=1 with [14] dbbababcb=d:

Critical pair: cd=bbababcb.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [14] dbbababcb=d with [15] bbababcb=1:

Critical pair: dbbababc=dbababcb.

Referenced by [30].

Overlap of [15] bbababcb=1 with [15] bbababcb=1:

Critical pair: bbababc=bababcb.

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

Overlap of [15] bbababcb=1 with [17] bbababc=bababcb:

Critical pair: bababcbb=1.

Referenced by [19], [21].

Overlap of [15] bbababcb=1 with [17] bbababc=bababcb:

Critical pair: bbababcbababcb=bababc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [20], [21], [24], [25], [30], [33], [47].

Overlap of [17] bbababc=bababcb with [8] cd=1:

Critical pair: bbabab=bababcbd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Simplify [18] bababcbb=1.

Reduce LHS:

Referenced by [22].

Overlap of [10] da=ad with [21] ababcbbb=1:

Critical pair: d=adbabcbbb.

Flip LHS and RHS.

Referenced by [23].

Overlap of [2] aaaa=c with [22] adbabcbbb=d:

Critical pair: aaad=cdbabcbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [33], [34], [36].

Overlap of [19] bababc=ababcb with [5] ca=ac:

Critical pair: bababac=ababcba.

Defines rule #9.

Referenced by [29].

Overlap of [19] bababc=ababcb with [8] cd=1:

Critical pair: babab=ababcbd.

Flip LHS and RHS.

Referenced by [26], [27].

Overlap of [10] da=ad with [25] ababcbd=babab:

Critical pair: dbabab=adbabcbd.

Flip LHS and RHS.

Referenced by [28].

Overlap of [25] ababcbd=babab with [10] da=ad:

Critical pair: ababcbad=bababa.

Referenced by [31].

Overlap of [2] aaaa=c with [26] adbabcbd=dbabab:

Critical pair: aaadbabab=cdbabcbd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [38], [39].

Overlap of [24] bababac=ababcba with [5] ca=ac:

Critical pair: bababaac=ababcbaa.

Defines rule #11.

Referenced by [40].

Simplify [13] bbbaba=dbbababc.

Reduce RHS:

Referenced by [33].

Overlap of [27] ababcbad=bababa with [10] da=ad:

Critical pair: ababcbaad=bababaa.

Referenced by [41].

Overlap of [10] da=ad with [20] ababcbbd=bbabab:

Critical pair: dbbabab=adbabcbbd.

Flip LHS and RHS.

Referenced by [42].

Overlap of [30] bbbaba=adbabcbb with [19] bababc=ababcb:

Critical pair: bbbaababcb=adbabcbbbabc.

Reduce RHS:

Referenced by [34].

Overlap of [33] bbbaababcb=adbc with [23] babcbbb=aaad:

Critical pair: bbbaaaaad=adbcbb.

Reduce LHS:

Defines rule #8.

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

Overlap of [34] bbba=adbcbb with [2] aaaa=c:

Critical pair: bbbc=adbcbbaaa.

Flip LHS and RHS.

Referenced by [37].

Overlap of [34] bbba=adbcbb with [23] babcbbb=aaad:

Critical pair: bbaaad=adbcbbbcbbb.

Flip LHS and RHS.

Referenced by [46].

Overlap of [2] aaaa=c with [35] adbcbbaaa=bbbc:

Critical pair: aaabbbc=cdbcbbaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [47].

Overlap of [28] babcbd=aaadbabab with [10] da=ad:

Critical pair: babcbad=aaadbababa.

Defines rule #10.

Referenced by [43].

Overlap of [34] bbba=adbcbb with [28] babcbd=aaadbabab:

Critical pair: bbaaadbabab=adbcbbbcbd.

Flip LHS and RHS.

Referenced by [50].

Overlap of [29] bababaac=ababcbaa with [5] ca=ac:

Critical pair: bababaaac=ababcbaaa.

Defines rule #14.

Overlap of [31] ababcbaad=bababaa with [10] da=ad:

Critical pair: ababcbaaad=bababaaa.

Referenced by [47].

Overlap of [2] aaaa=c with [32] adbabcbbd=dbbabab:

Critical pair: aaadbbabab=cdbabcbbd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [44], [45].

Overlap of [38] babcbad=aaadbababa with [10] da=ad:

Critical pair: babcbaad=aaadbababaa.

Defines rule #12.

Referenced by [48].

Overlap of [34] bbba=adbcbb with [42] babcbbd=aaadbbabab:

Critical pair: bbaaadbbabab=adbcbbbcbbd.

Flip LHS and RHS.

Referenced by [52].

Overlap of [42] babcbbd=aaadbbabab with [10] da=ad:

Critical pair: babcbbad=aaadbbababa.

Defines rule #17.

Referenced by [49].

Overlap of [2] aaaa=c with [36] adbcbbbcbbb=bbaaad:

Critical pair: aaabbaaad=cdbcbbbcbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [19] bababc=ababcb with [41] ababcbaaad=bababaaa:

Critical pair: bbababaaa=ababcbbaaad.

Reduce RHS:

Defines rule #19.

Overlap of [43] babcbaad=aaadbababaa with [10] da=ad:

Critical pair: babcbaaad=aaadbababaaa.

Defines rule #15.

Overlap of [45] babcbbad=aaadbbababa with [10] da=ad:

Critical pair: babcbbaad=aaadbbababaa.

Defines rule #18.

Overlap of [2] aaaa=c with [39] adbcbbbcbd=bbaaadbabab:

Critical pair: aaabbaaadbabab=cdbcbbbcbd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [51].

Overlap of [50] bcbbbcbd=aaabbaaadbabab with [10] da=ad:

Critical pair: bcbbbcbad=aaabbaaadbababa.

Defines rule #22.

Referenced by [53].

Overlap of [2] aaaa=c with [44] adbcbbbcbbd=bbaaadbbabab:

Critical pair: aaabbaaadbbabab=cdbcbbbcbbd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [54].

Overlap of [51] bcbbbcbad=aaabbaaadbababa with [10] da=ad:

Critical pair: bcbbbcbaad=aaabbaaadbababaa.

Defines rule #23.

Referenced by [55].

Overlap of [52] bcbbbcbbd=aaabbaaadbbabab with [10] da=ad:

Critical pair: bcbbbcbbad=aaabbaaadbbababa.

Defines rule #26.

Referenced by [56].

Overlap of [53] bcbbbcbaad=aaabbaaadbababaa with [10] da=ad:

Critical pair: bcbbbcbaaad=aaabbaaadbababaaa.

Defines rule #24.

Overlap of [54] bcbbbcbbad=aaabbaaadbbababa with [10] da=ad:

Critical pair: bcbbbcbbaad=aaabbaaadbbababaa.

Defines rule #27.