Certificate for #1425 ⟨a, b | aabababbba=1⟩

Completion settings:

• Auxiliary generators:
  1. c = aaa
  2. d = bababbb
• Reduction order:
  • Left-to-right recursive path with deg(c) = deg(d) = deg(a) = 0, c < d < a; deg(b) = 1

Axiom: aabababbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [14], [19], [21], [23], [24], [27], [32], [37], [44], [45], [48].

Axiom: bababbb=d.

Referenced by [4], [12], [17], [20], [25].

Overlap of [1] aabababbba=1 with [3] bababbb=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 [14], [30], [32], [35], [41].

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], [13], [19], [22], [28], [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], [17], [28], [32], [38], [39], [42], [46], [47], [49].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [19], [30], [32], [36], [44], [45], [48].

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

Critical pair: bababbd=dababbb.

Flip LHS and RHS.

Referenced by [13], [26].

Overlap of [9] cd=1 with [12] dababbb=bababbd:

Critical pair: cbababbd=ababbb.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] ababbb=cbababbd:

Critical pair: aacbababbd=cbabbb.

Reduce LHS:

Referenced by [15].

Overlap of [11] dc=1 with [14] caabababbd=cbabbb:

Critical pair: dcbabbb=aabababbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [15] aabababbd=babbb with [11] dc=1:

Critical pair: aabababb=babbbc.

Referenced by [17], [18], [29].

Overlap of [16] aabababb=babbbc with [3] bababbb=d:

Critical pair: aad=babbbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [16] aabababb=babbbc with [17] babbbcb=daa:

Critical pair: aabababdaa=babbbcabbbcb.

Flip LHS and RHS.

Referenced by [30].

Overlap of [17] babbbcb=daa with [17] babbbcb=daa:

Critical pair: babbbcdaa=daaabbbcb.

Reduce LHS:

Reduce RHS:

Referenced by [20], [21].

Overlap of [3] bababbb=d with [19] babbbaa=bbbcb:

Critical pair: bababbbbbcb=dabbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [19] babbbaa=bbbcb with [2] aaa=c:

Critical pair: babbbc=bbbcba.

Referenced by [25], [29], [30].

Overlap of [9] cd=1 with [20] dabbbaa=dbbcb:

Critical pair: cdbbcb=abbbaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [20] dabbbaa=dbbcb with [2] aaa=c:

Critical pair: dabbbc=dbbcba.

Referenced by [26].

Overlap of [2] aaa=c with [22] abbbaa=bbcb:

Critical pair: aabbcb=cbbbaa.

Defines rule #11.

Overlap of [3] bababbb=d with [22] abbbaa=bbcb:

Critical pair: babbbcb=daa.

Reduce LHS:

Defines rule #17.

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

Overlap of [12] dababbb=bababbd with [22] abbbaa=bbcb:

Critical pair: dabbbcb=bababbdaa.

Reduce LHS:

Defines rule #14.

Referenced by [42], [43].

Overlap of [22] abbbaa=bbcb with [2] aaa=c:

Critical pair: abbbc=bbcba.

Referenced by [28].

Overlap of [27] abbbc=bbcba with [9] cd=1:

Critical pair: abbb=bbcbad.

Reduce RHS:

Defines rule #8.

Referenced by [30], [31], [32], [40], [43].

Simplify [16] aabababb=babbbc.

Reduce RHS:

Defines rule #16.

Overlap of [18] babbbcabbbcb=aabababdaa with [21] babbbc=bbbcba:

Critical pair: bbbcbaabbbcb=aabababdaa.

Reduce LHS:

Defines rule #13.

Overlap of [25] bbbcbab=daa with [28] abbb=bbcbda:

Critical pair: bbbcbbbcbda=daabb.

Referenced by [44].

Overlap of [28] abbb=bbcbda with [25] bbbcbab=daa:

Critical pair: adaa=bbcbdacbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [33], [34].

Overlap of [32] bbcbabab=1 with [32] bbcbabab=1:

Critical pair: bbcbaba=bcbabab.

Flip LHS and RHS.

Referenced by [34].

Overlap of [32] bbcbabab=1 with [33] bcbabab=bbcbaba:

Critical pair: bbcbababbcbaba=cbabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [35], [36].

Overlap of [5] ac=ca with [34] cbabab=bcbaba:

Critical pair: abcbaba=cababab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [41].

Overlap of [11] dc=1 with [34] cbabab=bcbaba:

Critical pair: dbcbaba=babab.

Referenced by [37].

Overlap of [36] dbcbaba=babab with [2] aaa=c:

Critical pair: dbcbabc=bababaa.

Referenced by [38].

Overlap of [37] dbcbabc=bababaa with [9] cd=1:

Critical pair: dbcbab=bababaad.

Reduce RHS:

Defines rule #7.

Referenced by [39], [40].

Overlap of [10] ad=da with [38] dbcbab=bababdaa:

Critical pair: abababdaa=dabcbab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [38] dbcbab=bababdaa with [28] abbb=bbcbda:

Critical pair: dbcbbbcbda=bababdaabb.

Referenced by [45].

Overlap of [5] ac=ca with [35] cababab=abcbaba:

Critical pair: aabcbaba=caababab.

Flip LHS and RHS.

Defines rule #12.

Overlap of [10] ad=da with [26] dbbcbab=bababbdaa:

Critical pair: abababbdaa=dabbcbab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [26] dbbcbab=bababbdaa with [28] abbb=bbcbda:

Critical pair: dbbcbbbcbda=bababbdaabb.

Referenced by [48].

Overlap of [31] bbbcbbbcbda=daabb with [2] aaa=c:

Critical pair: bbbcbbbcbdc=daabbaa.

Reduce LHS:

Defines rule #23.

Overlap of [40] dbcbbbcbda=bababdaabb with [2] aaa=c:

Critical pair: dbcbbbcbdc=bababdaabbaa.

Reduce LHS:

Defines rule #18.

Referenced by [46].

Overlap of [10] ad=da with [45] dbcbbbcb=bababdaabbaa:

Critical pair: abababdaabbaa=dabcbbbcb.

Flip LHS and RHS.

Defines rule #19.

Referenced by [47].

Overlap of [10] ad=da with [46] dabcbbbcb=abababdaabbaa:

Critical pair: aabababdaabbaa=daabcbbbcb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [43] dbbcbbbcbda=bababbdaabb with [2] aaa=c:

Critical pair: dbbcbbbcbdc=bababbdaabbaa.

Reduce LHS:

Defines rule #21.

Referenced by [49].

Overlap of [10] ad=da with [48] dbbcbbbcb=bababbdaabbaa:

Critical pair: abababbdaabbaa=dabbcbbbcb.

Flip LHS and RHS.

Defines rule #22.