Certificate for #1373 ⟨a, b | aaabbababa=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. aaaa=c
  2. bbabab=d

Axiom: aaabbababa=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [9], [11], [19], [24], [26], [27], [28], [32], [35], [38].

Axiom: bbabab=d.

Defines rule #15.

Referenced by [4], [21], [26].

Overlap of [1] aaabbababa=1 with [3] bbabab=d:

Critical pair: aaada=1.

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

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [12], [15], [25], [28], [29], [34], [39], [40].

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

Critical pair: a=cda.

Flip LHS and RHS.

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

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

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaad=aada.

Referenced by [10], [12], [16].

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [13].

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

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13], [14], [15].

Overlap of [7] cada=aa with [4] aaada=1:

Critical pair: cad=aaaada.

Reduce RHS:

Referenced by [12], [15], [20].

Overlap of [4] aaada=1 with [10] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [13].

Overlap of [6] cda=a with [10] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [10] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

Referenced by [15], [16].

Overlap of [10] aadaa=cd with [10] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

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

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [17], [18], [22], [26], [36].

Simplify [13] adaaa=cd.

Reduce RHS:

Referenced by [19].

Overlap of [15] cddaa=ada with [16] cd=1:

Critical pair: daa=ada.

Flip LHS and RHS.

Referenced by [19].

Simplify [17] adaaa=1.

Reduce LHS:

Defines rule #2.

Referenced by [20], [24], [30], [32], [35], [38].

Overlap of [19] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [23], [31], [33], [35], [37].

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

Critical pair: bbabad=dbabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [22], [23].

Overlap of [16] cd=1 with [21] dbabab=bbabda:

Critical pair: cbbabda=babab.

Referenced by [24].

Overlap of [20] ad=da with [21] dbabab=bbabda:

Critical pair: abbabda=dababab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [33].

Overlap of [22] cbbabda=babab with [2] aaaa=c:

Critical pair: cbbabdc=bababaaa.

Reduce LHS:

Defines rule #8.

Referenced by [25], [26], [27], [29].

Overlap of [5] ac=ca with [24] cbbab=bababaaa:

Critical pair: abababaaa=cabbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [34].

Overlap of [24] cbbab=bababaaa with [3] bbabab=d:

Critical pair: cd=bababaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [24] cbbab=bababaaa with [26] bababcb=1:

Critical pair: cbba=bababaaaababcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [28], [29].

Overlap of [2] aaaa=c with [27] abcb=cbba:

Critical pair: aaacbba=cbcb.

Reduce LHS:

Referenced by [30].

Overlap of [24] cbbab=bababaaa with [27] abcb=cbba:

Critical pair: cbbcbba=bababaaacb.

Reduce RHS:

Referenced by [37].

Overlap of [19] dc=1 with [28] caaabba=cbcb:

Critical pair: dcbcb=aaabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [30] aaabba=bcb with [20] ad=da:

Critical pair: aaabbda=bcbd.

Referenced by [32].

Overlap of [31] aaabbda=bcbd with [2] aaaa=c:

Critical pair: aaabbdc=bcbdaaa.

Reduce LHS:

Defines rule #7.

Referenced by [35].

Overlap of [20] ad=da with [23] dababab=abbabda:

Critical pair: aabbabda=daababab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [35].

Overlap of [5] ac=ca with [25] cabbab=abababaaa:

Critical pair: aabababaaa=caabbab.

Flip LHS and RHS.

Defines rule #12.

Overlap of [20] ad=da with [33] daababab=aabbabda:

Critical pair: aaabbabda=daaababab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [16] cd=1 with [35] daaababab=bcbbda:

Critical pair: cbcbbda=aaababab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [29] cbbcbba=bababcaaab with [20] ad=da:

Critical pair: cbbcbbda=bababcaaabd.

Referenced by [38].

Overlap of [37] cbbcbbda=bababcaaabd with [2] aaaa=c:

Critical pair: cbbcbbdc=bababcaaabdaaa.

Reduce LHS:

Defines rule #16.

Referenced by [39].

Overlap of [5] ac=ca with [38] cbbcbb=bababcaaabdaaa:

Critical pair: abababcaaabdaaa=cabbcbb.

Flip LHS and RHS.

Defines rule #17.

Referenced by [40].

Overlap of [5] ac=ca with [39] cabbcbb=abababcaaabdaaa:

Critical pair: aabababcaaabdaaa=caabbcbb.

Flip LHS and RHS.

Defines rule #18.