Certificate for #1408 ⟨a, b | aabaababba=1⟩

Completion settings:

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

Axiom: aabaababba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [15], [16], [18], [20], [23], [25], [26], [27], [29], [31], [37], [39], [40], [43], [44], [45], [48], [49], [51], [52].

Axiom: baababb=d.

Defines rule #12.

Referenced by [4], [11], [15], [19], [22].

Overlap of [1] aabaababba=1 with [3] baababb=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.

Flip LHS and RHS.

Defines rule #3.

Referenced by [20], [25], [29], [39], [49].

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.

Flip LHS and RHS.

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

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

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

Referenced by [14], [16], [20], [23], [24], [25], [29], [37], [39], [40], [48], [49], [51], [52].

Overlap of [4] aada=1 with [7] ada=aad:

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [12], [34], [37], [38], [40], [46], [47], [50].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [15], [26], [34], [38], [46], [47], [50].

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

Critical pair: baababd=daababb.

Reduce RHS:

Defines rule #7.

Referenced by [12], [13], [16], [20], [23], [37].

Overlap of [11] baababd=aadbabb with [9] da=ad:

Critical pair: baababad=aadbabba.

Referenced by [29].

Overlap of [11] baababd=aadbabb with [10] dc=1:

Critical pair: baabab=aadbabbc.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] aadbabbc=baabab:

Critical pair: abaabab=cdbabbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [15], [30], [33].

Overlap of [3] baababb=d with [14] babbc=abaabab:

Critical pair: baaabaabab=dc.

Reduce LHS:

Reduce RHS:

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

Overlap of [15] bcbaabab=1 with [11] baababd=aadbabb:

Critical pair: bcbaabaaadbabb=aababd.

Reduce LHS:

Defines rule #25.

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

Critical pair: bcbaaba=cbaabab.

Defines rule #11.

Referenced by [18], [19], [20], [26], [28], [49].

Overlap of [17] bcbaaba=cbaabab with [2] aaa=c:

Critical pair: bcbaabc=cbaababaa.

Flip LHS and RHS.

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

Overlap of [17] bcbaaba=cbaabab with [3] baababb=d:

Critical pair: bcbaad=cbaababababb.

Flip LHS and RHS.

Referenced by [41].

Overlap of [17] bcbaaba=cbaabab with [11] baababd=aadbabb:

Critical pair: bcbaaaadbabb=cbaababababd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [42].

Overlap of [15] bcbaabab=1 with [18] cbaababaa=bcbaabc:

Critical pair: bbcbaabc=aa.

Referenced by [24].

Overlap of [18] cbaababaa=bcbaabc with [3] baababb=d:

Critical pair: cbaabad=bcbaabcbabb.

Flip LHS and RHS.

Defines rule #27.

Overlap of [18] cbaababaa=bcbaabc with [11] baababd=aadbabb:

Critical pair: cbaabaaadbabb=bcbaabcbabd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [21] bbcbaabc=aa with [8] cd=1:

Critical pair: bbcbaab=aad.

Referenced by [25].

Overlap of [24] bbcbaab=aad with [24] bbcbaab=aad:

Critical pair: bbcbaaaad=aadbcbaab.

Reduce LHS:

Defines rule #9.

Referenced by [26], [35], [37], [39], [40], [49].

Overlap of [25] bbcba=aadbcbaab with [2] aaa=c:

Critical pair: bbcbc=aadbcbaabaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27], [28], [29], [30], [32].

Overlap of [2] aaa=c with [26] aabaababa=bbcbc:

Critical pair: abbcbc=cbaababa.

Flip LHS and RHS.

Referenced by [28], [38], [39], [41], [42].

Overlap of [17] bcbaaba=cbaabab with [26] aabaababa=bbcbc:

Critical pair: bcbbbcbc=cbaababababa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [26] aabaababa=bbcbc with [12] baababad=aadbabba:

Critical pair: aaaadbabba=bbcbcd.

Reduce LHS:

Reduce RHS:

Referenced by [31], [32], [33], [36].

Overlap of [26] aabaababa=bbcbc with [14] babbc=abaabab:

Critical pair: aabaabaabaabab=bbcbcbbc.

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aaa=c with [29] ababba=bbcb:

Critical pair: aabbcb=cbabba.

Flip LHS and RHS.

Referenced by [34], [35].

Overlap of [26] aabaababa=bbcbc with [29] ababba=bbcb:

Critical pair: aabaabbbcb=bbcbcbba.

Flip LHS and RHS.

Defines rule #21.

Overlap of [29] ababba=bbcb with [14] babbc=abaabab:

Critical pair: abababaabab=bbcbbbc.

Flip LHS and RHS.

Defines rule #13.

Overlap of [10] dc=1 with [31] cbabba=aabbcb:

Critical pair: daabbcb=babba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [36], [37], [40].

Overlap of [25] bbcba=aadbcbaab with [31] cbabba=aabbcb:

Critical pair: bbaabbcb=aadbcbaabbba.

Flip LHS and RHS.

Referenced by [48].

Overlap of [29] ababba=bbcb with [34] babba=aadbbcb:

Critical pair: ababaadbbcb=bbcbbba.

Flip LHS and RHS.

Defines rule #19.

Overlap of [34] babba=aadbbcb with [11] baababd=aadbabb:

Critical pair: babaadbabb=aadbbcbababd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [10] dc=1 with [27] cbaababa=abbcbc:

Critical pair: dabbcbc=baababa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [39], [40].

Overlap of [27] cbaababa=abbcbc with [38] baababa=adbbcbc:

Critical pair: cbaabaadbbcbc=abbcbcababa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [34] babba=aadbbcb with [38] baababa=adbbcbc:

Critical pair: babadbbcbc=aadbbcbababa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [19] cbaababababb=bcbaad with [27] cbaababa=abbcbc:

Critical pair: abbcbcbabb=bcbaad.

Referenced by [43].

Overlap of [20] cbaababababd=bcbababb with [27] cbaababa=abbcbc:

Critical pair: abbcbcbabd=bcbababb.

Referenced by [44].

Overlap of [2] aaa=c with [41] abbcbcbabb=bcbaad:

Critical pair: aabcbaad=cbbcbcbabb.

Flip LHS and RHS.

Referenced by [46].

Overlap of [2] aaa=c with [42] abbcbcbabd=bcbababb:

Critical pair: aabcbababb=cbbcbcbabd.

Flip LHS and RHS.

Referenced by [47].

Overlap of [2] aaa=c with [28] abbcbcbaba=bcbbbcbc:

Critical pair: aabcbbbcbc=cbbcbcbaba.

Flip LHS and RHS.

Referenced by [50].

Overlap of [10] dc=1 with [43] cbbcbcbabb=aabcbaad:

Critical pair: daabcbaad=bbcbcbabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Overlap of [10] dc=1 with [44] cbbcbcbabd=aabcbababb:

Critical pair: daabcbababb=bbcbcbabd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [2] aaa=c with [35] aadbcbaabbba=bbaabbcb:

Critical pair: abbaabbcb=cdbcbaabbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [49].

Overlap of [48] bcbaabbba=abbaabbcb with [2] aaa=c:

Critical pair: bcbaabbbc=abbaabbcbaa.

Reduce RHS:

Defines rule #14.

Overlap of [10] dc=1 with [45] cbbcbcbaba=aabcbbbcbc:

Critical pair: daabcbbbcbc=bbcbcbaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [2] aaa=c with [37] adbcbaabbabd=babaadbabb:

Critical pair: aababaadbabb=cdbcbaabbabd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [2] aaa=c with [40] adbcbaabbaba=babadbbcbc:

Critical pair: aababadbbcbc=cdbcbaabbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.