Certificate for #1366 ⟨a, b | aaabbaaaba=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. bbaaab=d

Axiom: aaabbaaaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [12], [21], [24], [29], [33].

Axiom: bbaaab=d.

Referenced by [4], [9], [15].

Overlap of [1] aaabbaaaba=1 with [3] bbaaab=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10], [11], [12], [13].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [21], [32], [33].

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 [10], [11], [12].

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

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #2.

Referenced by [16], [18], [23], [31], [32], [33].

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

Critical pair: bbaaad=dbaaab.

Referenced by [13], [14].

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

Critical pair: aaadaaad=ada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

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 [12], [19], [25], [30], [31].

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

Critical pair: dc=adaaa.

Reduce RHS:

Defines rule #1.

Referenced by [14], [25], [26], [27], [30].

Overlap of [9] bbaaad=dbaaab with [4] aaada=1:

Critical pair: bb=dbaaaba.

Flip LHS and RHS.

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

Overlap of [9] bbaaad=dbaaab with [12] dc=1:

Critical pair: bbaaa=dbaaabc.

Referenced by [15], [28].

Overlap of [3] bbaaab=d with [14] bbaaa=dbaaabc:

Critical pair: dbaaabcb=d.

Referenced by [18], [19].

Overlap of [8] cd=1 with [13] dbaaaba=bb:

Critical pair: cbb=baaaba.

Flip LHS and RHS.

Defines rule #9.

Referenced by [17].

Overlap of [13] dbaaaba=bb with [16] baaaba=cbb:

Critical pair: dbaaacbb=bbaaba.

Flip LHS and RHS.

Defines rule #14.

Overlap of [8] cd=1 with [15] dbaaabcb=d:

Critical pair: cd=baaabcb.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [15] dbaaabcb=d with [18] baaabcb=1:

Critical pair: dbaaabc=daaabcb.

Reduce RHS:

Referenced by [28].

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

Critical pair: baaabc=aaabcb.

Defines rule #6.

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

Overlap of [13] dbaaaba=bb with [20] baaabc=aaabcb:

Critical pair: dbaaaaaabcb=bbaabc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [31].

Overlap of [18] baaabcb=1 with [20] baaabc=aaabcb:

Critical pair: aaabcbb=1.

Referenced by [24].

Overlap of [20] baaabc=aaabcb with [8] cd=1:

Critical pair: baaab=aaabcbd.

Flip LHS and RHS.

Referenced by [29].

Overlap of [2] aaaa=c with [22] aaabcbb=1:

Critical pair: a=cbcbb.

Flip LHS and RHS.

Referenced by [25].

Overlap of [12] dc=1 with [24] cbcbb=a:

Critical pair: da=bcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [26], [31], [32].

Overlap of [25] bcbb=ad with [25] bcbb=ad:

Critical pair: bcbad=adcbb.

Reduce RHS:

Referenced by [27].

Overlap of [26] bcbad=abb with [12] dc=1:

Critical pair: bcba=abbc.

Defines rule #8.

Simplify [14] bbaaa=dbaaabc.

Reduce RHS:

Defines rule #10.

Referenced by [33].

Overlap of [2] aaaa=c with [23] aaabcbd=baaab:

Critical pair: abaaab=cbcbd.

Flip LHS and RHS.

Referenced by [30].

Overlap of [12] dc=1 with [29] cbcbd=abaaab:

Critical pair: dabaaab=bcbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [25] bcbb=ad with [21] bbaabc=dbaacbcb:

Critical pair: bcdbaacbcb=adaabc.

Reduce LHS:

Reduce RHS:

Referenced by [32].

Overlap of [31] bbaacbcb=aaadbc with [25] bcbb=ad:

Critical pair: bbaacbcad=aaadbccbb.

Reduce LHS:

Defines rule #15.

Referenced by [33].

Overlap of [32] bbaacba=aaadbccbb with [2] aaaa=c:

Critical pair: bbaacbc=aaadbccbbaaa.

Reduce RHS:

Defines rule #13.