Certificate for #4169 ⟨a, b | aabbaabba=ba⟩

Completion settings:

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

Axiom: aabbaabba=ba.

Referenced by [3], [4], [5], [7], [16].

Axiom: bbbbbba=c.

Referenced by [4], [6], [15], [26], [31], [32], [33], [41].

Overlap of [1] aabbaabba=ba with [1] aabbaabba=ba:

Critical pair: aabbba=baabba.

Flip LHS and RHS.

Referenced by [4], [5], [6], [7], [8], [9], [10], [11], [16], [35].

Overlap of [2] bbbbbba=c with [1] aabbaabba=ba:

Critical pair: bbbbbbba=cabbaabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [5], [9], [12], [13], [15], [17].

Overlap of [4] cabaabbba=bc with [1] aabbaabba=ba:

Critical pair: cabaabbbba=bcabbaabba.

Reduce RHS:

Referenced by [12], [13], [18].

Overlap of [2] bbbbbba=c with [3] baabba=aabbba:

Critical pair: bbbbbaabbba=cabba.

Referenced by [19].

Overlap of [3] baabba=aabbba with [1] aabbaabba=ba:

Critical pair: bba=aabbbaabba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [8], [10], [20].

Overlap of [3] baabba=aabbba with [3] baabba=aabbba:

Critical pair: baabaabbba=aabbbaabba.

Reduce RHS:

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

Overlap of [4] cabaabbba=bc with [3] baabba=aabbba:

Critical pair: cabaabbaabbba=bcabba.

Reduce LHS:

Referenced by [21].

Overlap of [3] baabba=aabbba with [7] aabbaabbba=bba:

Critical pair: bbba=aabbbaabbba.

Flip LHS and RHS.

Referenced by [21].

Overlap of [3] baabba=aabbba with [8] baabaabbba=bba:

Critical pair: baabbba=aabbbaabaabbba.

Reduce RHS:

Referenced by [13], [14], [16], [17], [19], [20], [23], [24], [31], [35], [36].

Overlap of [5] cabaabbbba=bbc with [8] baabaabbba=bba:

Critical pair: cabaabbbbba=bbcabaabbba.

Reduce RHS:

Referenced by [15], [39].

Overlap of [5] cabaabbbba=bbc with [11] baabbba=aabbbba:

Critical pair: cabaabbbaabbbba=bbcabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [11] baabbba=aabbbba with [8] baabaabbba=bba:

Critical pair: baabbbba=aabbbbaabaabbba.

Reduce RHS:

Referenced by [18], [19], [20], [23], [24], [35], [36].

Overlap of [12] cabaabbbbba=bbbc with [8] baabaabbba=bba:

Critical pair: cabaabbbbbba=bbbcabaabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22], [27], [28], [30], [39], [42].

Overlap of [1] aabbaabba=ba with [3] baabba=aabbba:

Critical pair: aabaabbba=ba.

Reduce LHS:

Referenced by [24], [25], [26], [32], [44].

Overlap of [4] cabaabbba=bc with [11] baabbba=aabbbba:

Critical pair: caaabbbba=bc.

Referenced by [22], [23], [26], [27], [45].

Overlap of [5] cabaabbbba=bbc with [14] baabbbba=aabbbbba:

Critical pair: caaabbbbba=bbc.

Referenced by [26], [28], [34], [37], [46].

Overlap of [6] bbbbbaabbba=cabba with [11] baabbba=aabbbba:

Critical pair: bbbbaabbbba=cabba.

Reduce LHS:

Referenced by [47].

Overlap of [7] aabbaabbba=bba with [11] baabbba=aabbbba:

Critical pair: aabaabbbba=bba.

Reduce LHS:

Referenced by [31], [32], [33], [34], [37].

Overlap of [9] caaabbbaabbba=bcabba with [10] aabbbaabbba=bbba:

Critical pair: cabbba=bcabba.

Flip LHS and RHS.

Referenced by [25], [29], [34], [38], [49].

Overlap of [15] bbbbc=cabaac with [17] caaabbbba=bc:

Critical pair: bbbbbc=cabaacaaabbbba.

Reduce LHS:

Reduce RHS:

Referenced by [28], [30], [40], [51].

Overlap of [17] caaabbbba=bc with [11] baabbba=aabbbba:

Critical pair: caaabbbaabbbba=bcabbba.

Reduce LHS:

Referenced by [53].

Overlap of [16] aaaabbbba=ba with [11] baabbba=aabbbba:

Critical pair: aaaabbbaabbbba=baabbba.

Reduce LHS:

Reduce RHS:

Referenced by [55].

Overlap of [21] bcabba=cabbba with [16] aaaabbbba=ba:

Critical pair: bcabbba=cabbbaaaabbbba.

Reduce RHS:

Referenced by [53], [57].

Overlap of [18] caaabbbbba=bbc with [16] aaaabbbba=ba:

Critical pair: caaabbbbbba=bbcaaabbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27], [28], [29], [39], [43], [66], [81].

Overlap of [26] bbbc=caaac with [17] caaabbbba=bc:

Critical pair: bbbbc=caaacaaabbbba.

Reduce LHS:

Reduce RHS:

Referenced by [30], [39], [40], [42], [52].

Overlap of [26] bbbc=caaac with [18] caaabbbbba=bbc:

Critical pair: bbbbbc=caaacaaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [30], [40], [51].

Overlap of [26] bbbc=caaac with [21] bcabba=cabbba:

Critical pair: bbcabbba=caaacabba.

Reduce LHS:

Referenced by [34], [59].

Overlap of [15] bbbbc=cabaac with [27] cabaac=caaabc:

Critical pair: bbbbcaaabc=cabaacabaac.

Reduce LHS:

Reduce RHS:

Referenced by [48].

Overlap of [11] baabbba=aabbbba with [20] aaaabbbbba=bba:

Critical pair: baabbbbba=aabbbbaaaabbbbba.

Reduce RHS:

Referenced by [36].

Overlap of [16] aaaabbbba=ba with [20] aaaabbbbba=bba:

Critical pair: aaaabbbbbba=baaaabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [33], [34], [35], [36], [37], [38], [41], [44], [45], [46], [48], [49], [53], [54], [55], [56], [57], [58], [60].

Overlap of [20] aaaabbbbba=bba with [20] aaaabbbbba=bba:

Critical pair: aaaabbbbbbba=bbaaaabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [35], [37], [38], [39], [40], [44], [61].

Overlap of [21] bcabba=cabbba with [20] aaaabbbbba=bba:

Critical pair: bcabbbba=cabbbaaaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [59].

Overlap of [32] bbba=aaaac with [3] baabba=aabbba:

Critical pair: bbaabbba=aaaacabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48].

Overlap of [32] bbba=aaaac with [11] baabbba=aabbbba:

Critical pair: bbaabbbba=aaaacabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [54], [56], [67], [68], [69], [70], [73].

Overlap of [32] bbba=aaaac with [20] aaaabbbbba=bba:

Critical pair: bbbbba=aaaacaaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [38], [62].

Overlap of [21] bcabba=cabbba with [33] baaaac=aaaabc:

Critical pair: bcabaaaabc=cabbbaaaac.

Reduce LHS:

Reduce RHS:

Referenced by [63].

Overlap of [33] baaaac=aaaabc with [12] cabaabbbbba=bbbc:

Critical pair: baaaabbbc=aaaabcabaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [45], [46], [53], [55], [57], [60], [61].

Overlap of [33] baaaac=aaaabc with [27] cabaac=caaabc:

Critical pair: baaaacaaabc=aaaabcabaac.

Reduce LHS:

Reduce RHS:

Referenced by [48], [62].

Overlap of [2] bbbbbba=c with [32] bbba=aaaac:

Critical pair: bbbaaaac=c.

Reduce LHS:

Referenced by [48], [54], [56], [63], [64], [67], [68], [71], [74], [76], [82].

Simplify [15] bbbbc=cabaac.

Reduce RHS:

Referenced by [43].

Overlap of [42] bbbbc=caaabc with [26] bbbc=caaac:

Critical pair: bcaaac=caaabc.

Referenced by [48], [64], [65], [70], [72], [76], [77], [78].

Overlap of [16] aaaabbbba=ba with [32] bbba=aaaac:

Critical pair: aaaabaaaac=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [45], [46], [47], [48], [50], [53], [54], [55], [56], [57], [60], [61], [62], [64], [65], [70], [73], [77], [80], [87], [90].

Overlap of [17] caaabbbba=bc with [32] bbba=aaaac:

Critical pair: caaabaaaac=bc.

Reduce LHS:

Referenced by [80], [83].

Overlap of [18] caaabbbbba=bbc with [32] bbba=aaaac:

Critical pair: caaabbaaaac=bbc.

Reduce LHS:

Referenced by [84].

Simplify [19] bbbaabbbbba=cabba.

Reduce RHS:

Referenced by [48].

Overlap of [47] bbbaabbbbba=caaaaaaaaabcaaaaaaabc with [32] bbba=aaaac:

Critical pair: aaaacabbbbba=caaaaaaaaabcaaaaaaabc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50], [54], [56], [85].

Simplify [21] bcabba=cabbba.

Reduce RHS:

Referenced by [50].

Overlap of [49] bcabba=caaaaac with [44] ba=aaaaaaaabc:

Critical pair: bcabaaaaaaaabc=caaaaac.

Reduce LHS:

Referenced by [54], [56].

Simplify [22] bcabaac=cabaabc.

Reduce RHS:

Referenced by [52].

Overlap of [51] bcabaac=caaabbc with [27] cabaac=caaabc:

Critical pair: bcaaabc=caaabbc.

Referenced by [65], [80], [84].

Simplify [23] caaabbaabbbbba=bcabbba.

Reduce RHS:

Referenced by [54].

Overlap of [53] caaabbaabbbbba=caaaaaaaaacaaabc with [44] ba=aaaaaaaabc:

Critical pair: caaabaaaaaaaabcabbbbba=caaaaaaaaacaaabc.

Reduce LHS:

Referenced by [77].

Simplify [24] aaaabbaabbbbba=aabbbba.

Reduce RHS:

Referenced by [56].

Overlap of [55] aaaabbaabbbbba=aaaaaaaaaacaaabc with [44] ba=aaaaaaaabc:

Critical pair: aaaabaaaaaaaabcabbbbba=aaaaaaaaaacaaabc.

Reduce LHS:

Referenced by [80].

Simplify [25] bcabbba=cabbbba.

Reduce RHS:

Referenced by [58].

Overlap of [57] bcabbba=caaaaaaaaacaaabc with [32] bbba=aaaac:

Critical pair: bcaaaaac=caaaaaaaaacaaabc.

Referenced by [70], [72], [73], [76].

Simplify [29] bcabbbba=caaacabba.

Reduce RHS:

Referenced by [60].

Overlap of [59] bcabbbba=caaaaabbc with [32] bbba=aaaac:

Critical pair: bcabaaaac=caaaaabbc.

Reduce LHS:

Referenced by [87].

Overlap of [33] baaaac=aaaabc with [44] ba=aaaaaaaabc:

Critical pair: aaaaaaaabcaaac=aaaabc.

Reduce LHS:

Referenced by [64], [65], [70], [72], [73], [76], [77], [83], [87].

Overlap of [37] baaaabc=aaaabbc with [44] ba=aaaaaaaabc:

Critical pair: aaaaaaaabcaaabc=aaaabbc.

Reduce LHS:

Referenced by [84].

Simplify [38] bcaaaaabbc=caaaaacaaac.

Reduce RHS:

Referenced by [66].

Overlap of [44] ba=aaaaaaaabc with [41] aaaacaaac=c:

Critical pair: bc=aaaaaaaabcaaacaaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [65], [69], [75], [77], [84], [88].

Overlap of [44] ba=aaaaaaaabc with [64] aaaacaaabc=bc:

Critical pair: bbc=aaaaaaaabcaaacaaabc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [85].

Overlap of [26] bbbc=caaac with [63] bcaaaaabbc=cac:

Critical pair: bbcac=caaacaaaaabbc.

Referenced by [89].

Overlap of [36] aaaacaaaaac=aac with [36] aaaacaaaaac=aac:

Critical pair: aaaacaaac=aacaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [71], [72], [73], [74], [75], [79].

Overlap of [36] aaaacaaaaac=aac with [41] aaaacaaac=c:

Critical pair: aaaacac=aacaaac.

Flip LHS and RHS.

Referenced by [76], [77], [82], [89], [90].

Overlap of [36] aaaacaaaaac=aac with [64] aaaacaaabc=bc:

Critical pair: aaaacabc=aacaaabc.

Flip LHS and RHS.

Referenced by [79], [88].

Overlap of [44] ba=aaaaaaaabc with [36] aaaacaaaaac=aac:

Critical pair: baac=aaaaaaaabcaaacaaaaac.

Reduce LHS:

Reduce RHS:

Referenced by [73], [87], [90].

Overlap of [41] aaaacaaac=c with [67] aacaaaaac=c:

Critical pair: aaaacac=caaaaac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [76].

Overlap of [43] bcaaac=caaabc with [67] aacaaaaac=c:

Critical pair: bcac=caaabcaaaaac.

Reduce RHS:

Referenced by [76], [77], [90], [91].

Overlap of [44] ba=aaaaaaaabc with [67] aacaaaaac=c:

Critical pair: bc=aaaaaaaabcacaaaaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [77], [78], [79], [80], [87], [90].

Overlap of [67] aacaaaaac=c with [41] aaaacaaac=c:

Critical pair: aacac=caaac.

Flip LHS and RHS.

Defines rule #1.

Referenced by [76], [77], [81], [87], [89], [90], [91], [95].

Overlap of [67] aacaaaaac=c with [64] aaaacaaabc=bc:

Critical pair: aacabc=caaabc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [76], [77], [78], [80], [93].

Overlap of [43] bcaaac=caaabc with [74] caaac=aacac:

Critical pair: bcaaaaacac=caaabcaaac.

Reduce LHS:

Reduce RHS:

Referenced by [77], [90], [91].

Overlap of [64] aaaacaaabc=bc with [74] caaac=aacac:

Critical pair: aaaacaaabaacac=bcaaac.

Reduce LHS:

Reduce RHS:

Referenced by [90].

Overlap of [43] bcaaac=caaabc with [73] aacaaaaabc=bc:

Critical pair: bcabc=caaabcaaaaabc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [90].

Overlap of [67] aacaaaaac=c with [73] aacaaaaabc=bc:

Critical pair: aacaaabc=caaaaabc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [87].

Overlap of [73] aacaaaaabc=bc with [75] caaabc=aacabc:

Critical pair: aacaaaaabaacabc=bcaaabc.

Reduce LHS:

Reduce RHS:

Referenced by [87].

Simplify [26] bbbc=caaac.

Reduce RHS:

Defines rule #16.

Referenced by [95].

Overlap of [41] aaaacaaac=c with [68] aacaaac=aaaacac:

Critical pair: aaaaaacac=c.

Defines rule #3.

Referenced by [91].

Overlap of [45] caaaaaaaaaaacaaabc=bc with [61] aaaaaaaacaaabc=aaaabc:

Critical pair: caaaaaaabc=bc.

Defines rule #7.

Referenced by [86], [92], [93], [94].

Overlap of [46] caaaaaaaaaaabcaaaaaaacaaabc=bbc with [64] aaaacaaabc=bc:

Critical pair: caaaaaaaaaaabcaaabc=bbc.

Reduce LHS:

Defines rule #13.

Referenced by [95].

Simplify [48] caaaaaaaaabcaaaaaaabc=aaaaaacaaabbc.

Reduce RHS:

Referenced by [86].

Overlap of [85] caaaaaaaaabcaaaaaaabc=aabbc with [83] caaaaaaabc=bc:

Critical pair: caaaaaaaaabbc=aabbc.

Defines rule #14.

Overlap of [60] bcaaaaaaaaacaaabc=caaaaabbc with [61] aaaaaaaacaaabc=aaaabc:

Critical pair: bcaaaaabc=caaaaabbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [89], [96].

Overlap of [64] aaaacaaabc=bc with [69] aacaaabc=aaaacabc:

Critical pair: aaaaaacabc=bc.

Defines rule #6.

Referenced by [94].

Simplify [66] bbcac=caaacaaaaabbc.

Reduce RHS:

Referenced by [90].

Overlap of [89] bbcac=aaaacacaaabbc with [72] bcac=caaacaaaaabc:

Critical pair: bcaaacaaaaabc=aaaacacaaabbc.

Reduce LHS:

Referenced by [92], [97].

Simplify [72] bcac=caaacaaaaabc.

Reduce RHS:

Defines rule #9.

Referenced by [92], [95].

Overlap of [91] bcac=cabc with [83] caaaaaaabc=bc:

Critical pair: bcabc=cabcaaaaaaabc.

Reduce LHS:

Reduce RHS:

Referenced by [97].

Overlap of [75] caaabc=aacabc with [83] caaaaaaabc=bc:

Critical pair: caaabbc=aacabcaaaaaaabc.

Reduce RHS:

Defines rule #10.

Referenced by [96].

Overlap of [88] aaaaaacabc=bc with [83] caaaaaaabc=bc:

Critical pair: aaaaaacabbc=bcaaaaaaabc.

Reduce RHS:

Defines rule #12.

Overlap of [91] bcac=cabc with [84] caaaaaaabbc=bbc:

Critical pair: bcabbc=cabcaaaaaaabbc.

Reduce RHS:

Defines rule #17.

Simplify [87] caaaaabbc=aacaaabbc.

Reduce RHS:

Defines rule #11.

Simplify [90] bcabc=aaaacacaaabbc.

Reduce RHS:

Defines rule #15.