Certificate for #23326 ⟨a, b | aaa=1, bbbb=abba⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #13.

Referenced by [5], [6], [19], [44], [50], [52], [53].

Axiom: bbbb=abba.

Flip LHS and RHS.

Referenced by [5], [6], [7], [11], [18], [20], [22].

Axiom: bbbbb=c.

Referenced by [4], [7], [8], [10], [11], [14], [18], [20], [21], [22], [23], [24], [35], [41], [42], [45].

Overlap of [3] bbbbb=c with [3] bbbbb=c:

Critical pair: bc=cb.

Flip LHS and RHS.

Referenced by [7], [9], [11], [12], [13], [16], [17], [18], [20], [24], [28], [37], [40], [42], [43], [45], [47], [49], [54].

Overlap of [1] aaa=1 with [2] abba=bbbb:

Critical pair: aabbbb=bba.

Referenced by [10], [11], [18], [38], [39], [46].

Overlap of [2] abba=bbbb with [1] aaa=1:

Critical pair: abb=bbbbaa.

Flip LHS and RHS.

Referenced by [14], [21], [43].

Overlap of [2] abba=bbbb with [2] abba=bbbb:

Critical pair: abbbbbb=bbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [8], [9], [11], [18], [22], [25], [28], [37], [42], [43].

Overlap of [3] bbbbb=c with [7] bca=abc:

Critical pair: bbbbabc=cca.

Referenced by [16], [18], [30].

Overlap of [4] cb=bc with [7] bca=abc:

Critical pair: cabc=bcca.

Flip LHS and RHS.

Referenced by [11].

Overlap of [5] aabbbb=bba with [3] bbbbb=c:

Critical pair: aac=bbab.

Referenced by [12], [15], [18], [29], [32], [36], [38], [39], [40], [46], [47].

Overlap of [5] aabbbb=bba with [9] bcca=cabc:

Critical pair: aabbbcabc=bbacca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [10] aac=bbab with [4] cb=bc:

Critical pair: aabc=bbabb.

Referenced by [13], [29].

Overlap of [12] aabc=bbabb with [4] cb=bc:

Critical pair: aabbc=bbabbb.

Referenced by [17], [38].

Overlap of [3] bbbbb=c with [6] bbbbaa=abb:

Critical pair: babb=caa.

Flip LHS and RHS.

Referenced by [15], [18], [26], [40], [43], [48].

Overlap of [10] aac=bbab with [14] caa=babb:

Critical pair: aababb=bbabaa.

Flip LHS and RHS.

Referenced by [35], [36].

Overlap of [8] bbbbabc=cca with [4] cb=bc:

Critical pair: bbbbabbc=ccab.

Referenced by [31].

Overlap of [13] aabbc=bbabbb with [4] cb=bc:

Critical pair: aabbbc=bbabbbb.

Referenced by [32].

Overlap of [5] aabbbb=bba with [11] bbacca=abccc:

Critical pair: aabbabccc=bbaacca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [1] aaa=1 with [18] abbbc=acccc:

Critical pair: aaacccc=bbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [23], [24], [25], [37], [38], [39], [43], [49].

Overlap of [2] abba=bbbb with [18] abbbc=acccc:

Critical pair: abbacccc=bbbbbbbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [21], [23], [26], [30], [31].

Overlap of [6] bbbbaa=abb with [18] abbbc=acccc:

Critical pair: bbbbaacccc=abbbbbc.

Reduce LHS:

Reduce RHS:

Referenced by [26], [33].

Overlap of [18] abbbc=acccc with [7] bca=abc:

Critical pair: abbabc=acccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [26], [27], [53].

Overlap of [3] bbbbb=c with [19] bbbc=cccc:

Critical pair: bbcccc=cc.

Reduce LHS:

Referenced by [34].

Overlap of [3] bbbbb=c with [19] bbbc=cccc:

Critical pair: bbbcccc=cbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [29], [30], [31], [33], [34], [37], [38], [39], [40], [41], [42], [45].

Overlap of [19] bbbc=cccc with [7] bca=abc:

Critical pair: bbabc=cccca.

Referenced by [29], [30], [32], [38], [39], [40], [46].

Overlap of [14] caa=babb with [22] acccca=cc:

Critical pair: cacc=babbcccca.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [22] acccca=cc with [22] acccca=cc:

Critical pair: acccccc=cccccca.

Flip LHS and RHS.

Defines rule #7.

Referenced by [28], [30], [31], [38], [39], [40], [41], [42], [43], [44], [49].

Overlap of [4] cb=bc with [26] bacca=cacc:

Critical pair: ccacc=bcacca.

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [12] aabc=bbabb with [24] bcc=ccccccc:

Critical pair: aaccccccc=bbabbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [8] bbbbabc=cca with [25] bbabc=cccca:

Critical pair: bbcccca=cca.

Reduce LHS:

Referenced by [31], [38], [39].

Overlap of [16] bbbbabbc=ccab with [29] bbabbc=ccccaccccc:

Critical pair: bbccccaccccc=ccab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [40], [47], [49].

Overlap of [17] aabbbc=bbabbbb with [18] abbbc=acccc:

Critical pair: aacccc=bbabbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [38].

Overlap of [21] abccccccccc=acc with [24] bcc=ccccccc:

Critical pair: acccccccccccccc=acc.

Referenced by [37], [42].

Overlap of [23] bccccccccc=cc with [24] bcc=ccccccc:

Critical pair: cccccccccccccc=cc.

Referenced by [40].

Overlap of [3] bbbbb=c with [15] bbabaa=aababb:

Critical pair: bbbaababb=cabaa.

Referenced by [49].

Overlap of [15] bbabaa=aababb with [10] aac=bbab:

Critical pair: bbabbbab=aababbc.

Flip LHS and RHS.

Referenced by [49].

Overlap of [4] cb=bc with [32] bbabbbb=ccccacc:

Critical pair: cccccacc=bcbabbbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [39], [48], [51].

Overlap of [5] aabbbb=bba with [32] bbabbbb=ccccacc:

Critical pair: aabbccccacc=bbaabbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [41], [42], [43], [44].

Overlap of [5] aabbbb=bba with [37] bacc=cccccacc:

Critical pair: aabbbcccccacc=bbaacc.

Reduce LHS:

Reduce RHS:

Referenced by [40].

Overlap of [10] aac=bbab with [39] accacccc=cca:

Critical pair: acca=bbabcacccc.

Reduce RHS:

Defines rule #10.

Overlap of [3] bbbbb=c with [38] bbbba=ccacccccc:

Critical pair: bccacccccc=ca.

Reduce LHS:

Defines rule #5.

Referenced by [49], [51].

Overlap of [3] bbbbb=c with [38] bbbba=ccacccccc:

Critical pair: bbccacccccc=cba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [6] bbbbaa=abb with [38] bbbba=ccacccccc:

Critical pair: ccacccccca=abb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48], [52].

Overlap of [38] bbbba=ccacccccc with [1] aaa=1:

Critical pair: bbbb=ccaccccccaa.

Reduce RHS:

Referenced by [45], [46].

Overlap of [3] bbbbb=c with [44] bbbb=cccccccc:

Critical pair: ccccccccb=c.

Reduce LHS:

Defines rule #1.

Referenced by [51].

Overlap of [5] aabbbb=bba with [44] bbbb=cccccccc:

Critical pair: aacccccccc=bba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [47], [49].

Simplify [10] aac=bbab.

Reduce RHS:

Defines rule #9.

Simplify [14] caa=babb.

Reduce RHS:

Defines rule #12.

Overlap of [35] bbbaababb=cabaa with [46] bba=ccccacccccc:

Critical pair: bccccaccccccababb=cabaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [53].

Overlap of [1] aaa=1 with [42] abc=acccccc:

Critical pair: aaacccccc=bc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [54].

Overlap of [37] bacc=cccccacc with [45] ccccccccccccc=c:

Critical pair: bac=cccccaccccccccccccc.

Reduce RHS:

Defines rule #8.

Overlap of [1] aaa=1 with [43] abb=acccccccccc:

Critical pair: aaacccccccccc=bb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Overlap of [49] cabaa=cacccacccc with [1] aaa=1:

Critical pair: cab=cacccacccca.

Reduce RHS:

Defines rule #6.

Simplify [4] cb=bc.

Reduce RHS:

Defines rule #3.