Certificate for #17659 ⟨a, b | aaaa=1, abbab=ba⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(b) = 0; deg(a) = 1

Axiom: aaaa=1.

Defines rule #30.

Referenced by [3], [5], [10], [17], [19], [45], [48].

Axiom: abbab=ba.

Referenced by [3], [4], [6], [7], [11], [13], [14], [17], [18], [20], [29], [32], [36], [38], [39], [40], [41], [44], [46], [47], [50], [57], [60], [61], [66], [70].

Overlap of [1] aaaa=1 with [2] abbab=ba:

Critical pair: aaaba=bbab.

Referenced by [5], [6], [21], [27], [30], [31], [45].

Overlap of [2] abbab=ba with [2] abbab=ba:

Critical pair: abbba=babab.

Flip LHS and RHS.

Referenced by [7], [8], [9], [15], [16], [20], [30], [31], [32], [36], [37], [41], [42], [62].

Overlap of [3] aaaba=bbab with [1] aaaa=1:

Critical pair: aaab=bbabaaa.

Flip LHS and RHS.

Referenced by [28], [36], [43].

Overlap of [3] aaaba=bbab with [2] abbab=ba:

Critical pair: aaabba=bbabbbab.

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

Overlap of [2] abbab=ba with [4] babab=abbba:

Critical pair: ababbba=baab.

Defines rule #15.

Referenced by [9], [10], [12], [16], [34], [52], [66], [73], [95].

Overlap of [4] babab=abbba with [4] babab=abbba:

Critical pair: baabbba=abbbaab.

Referenced by [25], [26], [75].

Overlap of [4] babab=abbba with [7] ababbba=baab:

Critical pair: bbaab=abbbabba.

Flip LHS and RHS.

Referenced by [11], [12], [13], [25], [36], [74].

Overlap of [7] ababbba=baab with [1] aaaa=1:

Critical pair: ababbb=baabaaa.

Flip LHS and RHS.

Referenced by [22].

Overlap of [2] abbab=ba with [9] abbbabba=bbaab:

Critical pair: abbbbaab=babbabba.

Reduce RHS:

Referenced by [17], [18], [33], [39].

Overlap of [7] ababbba=baab with [9] abbbabba=bbaab:

Critical pair: ababbbbbaab=baabbbbabba.

Flip LHS and RHS.

Referenced by [23].

Overlap of [9] abbbabba=bbaab with [2] abbab=ba:

Critical pair: abbbba=bbaabb.

Flip LHS and RHS.

Referenced by [14], [15], [16], [18], [20], [24], [25], [26], [37], [68], [71], [73].

Overlap of [2] abbab=ba with [13] bbaabb=abbbba:

Critical pair: abbaabbbba=babaabb.

Reduce LHS:

Referenced by [23].

Overlap of [4] babab=abbba with [13] bbaabb=abbbba:

Critical pair: babaabbbba=abbbabaabb.

Referenced by [36], [37].

Overlap of [7] ababbba=baab with [13] bbaabb=abbbba:

Critical pair: abababbbba=baababb.

Reduce LHS:

Referenced by [27], [31], [49].

Overlap of [1] aaaa=1 with [11] abbbbaab=bbaba:

Critical pair: aaabbaba=bbbbaab.

Reduce LHS:

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

Overlap of [13] bbaabb=abbbba with [11] abbbbaab=bbaba:

Critical pair: bbabbaba=abbbbabbaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [17] aabaa=bbbbaab with [1] aaaa=1:

Critical pair: aab=bbbbaabaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [17] aabaa=bbbbaab with [2] abbab=ba:

Critical pair: aababa=bbbbaabbbab.

Reduce RHS:

Referenced by [21].

Overlap of [17] aabaa=bbbbaab with [3] aaaba=bbab:

Critical pair: aabbbab=bbbbaababa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [86].

Overlap of [10] baabaaa=ababbb with [17] aabaa=bbbbaab:

Critical pair: bbbbbaaba=ababbb.

Referenced by [35].

Overlap of [12] baabbbbabba=ababbbbbaab with [14] aabbbbabba=babaabb:

Critical pair: bbabaabb=ababbbbbaab.

Flip LHS and RHS.

Referenced by [51].

Overlap of [19] bbbbbbbbaab=aab with [13] bbaabb=abbbba:

Critical pair: bbbbbbabbbba=aabb.

Defines rule #11.

Referenced by [37], [38], [39], [64], [69], [74], [80], [82], [89].

Overlap of [8] baabbba=abbbaab with [9] abbbabba=bbaab:

Critical pair: babbaab=abbbaabbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [8] baabbba=abbbaab with [13] bbaabb=abbbba:

Critical pair: baababbbba=abbbaababb.

Referenced by [53].

Overlap of [3] aaaba=bbab with [6] aaabba=bbabbbab:

Critical pair: aaabbbabbbab=bbabaabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [5] bbabaaa=aaab with [6] aaabba=bbabbbab:

Critical pair: bbabbbabbbab=aaabbba.

Flip LHS and RHS.

Defines rule #31.

Overlap of [6] aaabba=bbabbbab with [2] abbab=ba:

Critical pair: aaba=bbabbbabb.

Defines rule #13.

Referenced by [31], [32], [33], [34], [35], [36], [40], [44], [49], [53], [54], [65], [71], [73], [79], [99], [103].

Overlap of [6] aaabba=bbabbbab with [6] aaabba=bbabbbab:

Critical pair: aaabbbbabbbab=bbabbbabaabba.

Reduce RHS:

Referenced by [32].

Overlap of [3] aaaba=bbab with [29] aaba=bbabbbabb:

Critical pair: aaabbbabbbabb=bbababa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [6] aaabba=bbabbbab with [29] aaba=bbabbbabb:

Critical pair: aaabbbbabbbabb=bbabbbababa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [41], [50].

Overlap of [11] abbbbaab=bbaba with [29] aaba=bbabbbabb:

Critical pair: abbbbbbabbbabb=bbabaa.

Flip LHS and RHS.

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

Overlap of [29] aaba=bbabbbabb with [7] ababbba=baab:

Critical pair: abaab=bbabbbabbbbba.

Flip LHS and RHS.

Defines rule #22.

Referenced by [36], [37], [73], [74], [99], [103].

Simplify [22] bbbbbaaba=ababbb.

Reduce LHS:

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

Overlap of [35] bbbbbbbabbbabb=ababbb with [5] bbabaaa=aaab:

Critical pair: bbbbbbbabbbabaaab=ababbbbabaaa.

Reduce LHS:

Reduce RHS:

Referenced by [55].

Overlap of [35] bbbbbbbabbbabb=ababbb with [24] bbbbbbabbbba=aabb:

Critical pair: bbbbbbbabbbabaabb=ababbbbbbbbabbbba.

Reduce LHS:

Reduce RHS:

Referenced by [57].

Overlap of [24] bbbbbbabbbba=aabb with [2] abbab=ba:

Critical pair: bbbbbbabbbbba=aabbbbab.

Flip LHS and RHS.

Referenced by [57].

Overlap of [24] bbbbbbabbbba=aabb with [11] abbbbaab=bbaba:

Critical pair: bbbbbbbbaba=aabbab.

Reduce RHS:

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

Overlap of [2] abbab=ba with [39] bbbbbbbbaba=aba:

Critical pair: abbaaba=babbbbbbbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [70].

Overlap of [35] bbbbbbbabbbabb=ababbb with [39] bbbbbbbbaba=aba:

Critical pair: bbbbbbbabbbababa=ababbbbbbbbbbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [39] bbbbbbbbaba=aba with [4] babab=abbba:

Critical pair: bbbbbbbabbba=abab.

Defines rule #12.

Referenced by [70], [71], [83], [84], [108].

Overlap of [39] bbbbbbbbaba=aba with [5] bbabaaa=aaab:

Critical pair: bbbbbbaaab=abaaa.

Flip LHS and RHS.

Referenced by [44], [45], [58].

Overlap of [29] aaba=bbabbbabb with [43] abaaa=bbbbbbaaab:

Critical pair: aabbbbbbbaaab=bbabbbabbbaaa.

Reduce RHS:

Referenced by [59].

Overlap of [43] abaaa=bbbbbbaaab with [1] aaaa=1:

Critical pair: ab=bbbbbbaaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [46], [47], [63].

Overlap of [2] abbab=ba with [45] bbbbbbbbab=ab:

Critical pair: abbaab=babbbbbbbab.

Reduce LHS:

Referenced by [57], [64].

Overlap of [45] bbbbbbbbab=ab with [2] abbab=ba:

Critical pair: bbbbbbbbba=abbab.

Reduce RHS:

Referenced by [48].

Overlap of [47] bbbbbbbbba=ba with [1] aaaa=1:

Critical pair: bbbbbbbbb=baaaa.

Reduce RHS:

Defines rule #1.

Referenced by [60], [85], [91], [102].

Simplify [16] aabbbabbba=baababb.

Reduce RHS:

Defines rule #34.

Overlap of [18] abbbbabbaab=bbbaa with [32] bbbabbaa=babbbbbabbbbb:

Critical pair: abbabbbbbabbbbbb=bbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [52], [55], [56], [58], [59], [67].

Simplify [23] ababbbbbaab=bbabaabb.

Reduce RHS:

Referenced by [52].

Overlap of [51] ababbbbbaab=abbbbbbabbbabbbb with [50] bbbaa=babbbbabbbbbb:

Critical pair: ababbbabbbbabbbbbbb=abbbbbbabbbabbbb.

Reduce LHS:

Referenced by [74].

Simplify [26] baababbbba=abbbaababb.

Reduce RHS:

Referenced by [54].

Overlap of [53] baababbbba=abbbbbabbbabbbb with [29] aaba=bbabbbabb:

Critical pair: bbbabbbabbbbbba=abbbbbabbbabbbb.

Defines rule #24.

Referenced by [108], [109].

Simplify [36] bbbbbaaabbb=babbbbbbaab.

Reduce RHS:

Referenced by [56].

Overlap of [55] bbbbbaaabbb=babbbbabbbbabbbbbbb with [50] bbbaa=babbbbabbbbbb:

Critical pair: bbbabbbbabbbbbbabbb=babbbbabbbbabbbbbbb.

Referenced by [72].

Overlap of [37] abaabbbbabbbbbbbb=abaabbbba with [38] aabbbbab=bbbbbbabbbbba:

Critical pair: abbbbbbbabbbbbabbbbbbb=abaabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [74].

Simplify [43] abaaa=bbbbbbaaab.

Reduce RHS:

Referenced by [67], [72], [76].

Overlap of [44] aabbbbbbbaaab=bbbbbabbbbba with [50] bbbaa=babbbbabbbbbb:

Critical pair: aabbbbbabbbbabbbbbbab=bbbbbabbbbba.

Referenced by [77].

Overlap of [2] abbab=ba with [48] bbbbbbbbb=b:

Critical pair: abbab=babbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [61], [62], [63], [65], [69], [71], [72], [73], [77], [79], [81], [82], [83], [84], [85], [86], [87], [88], [89], [90], [91], [92], [93], [96], [97], [98], [99], [100], [101], [102], [103], [104], [105], [106], [107], [109], [110], [111].

Overlap of [2] abbab=ba with [60] babbbbbbbb=ba:

Critical pair: abba=babbbbbbb.

Defines rule #4.

Referenced by [64], [65], [70], [71], [73], [79], [80], [81], [82], [87], [89], [90], [91], [93], [98], [99], [100], [101], [103], [107].

Overlap of [4] babab=abbba with [60] babbbbbbbb=ba:

Critical pair: baba=abbbabbbbbbb.

Defines rule #6.

Referenced by [66], [67], [73], [80], [83], [84], [85], [86], [90], [91], [92], [97], [99], [101], [103], [109].

Overlap of [45] bbbbbbbbab=ab with [60] babbbbbbbb=ba:

Critical pair: bbbbbbbba=abbbbbbbb.

Defines rule #3.

Referenced by [85], [91].

Overlap of [24] bbbbbbabbbba=aabb with [61] abba=babbbbbbb:

Critical pair: bbbbbbabbbbbabbbbbbb=aabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [79], [80], [81], [101].

Overlap of [29] aaba=bbabbbabb with [61] abba=babbbbbbb:

Critical pair: aabbabbbbbbb=bbabbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [82], [83], [84], [85], [86].

Overlap of [2] abbab=ba with [62] baba=abbbabbbbbbb:

Critical pair: ababbbabbbbbbb=baa.

Reduce LHS:

Defines rule #5.

Referenced by [68].

Overlap of [62] baba=abbbabbbbbbb with [58] abaaa=bbbbabbbbabbbbbbab:

Critical pair: bbbbbabbbbabbbbbbab=abbbabbbbbbbaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [78].

Overlap of [13] bbaabb=abbbba with [66] baabbbbbbbb=baa:

Critical pair: bbaa=abbbbabbbbbb.

Defines rule #7.

Referenced by [69], [73], [74], [75], [81], [82], [84], [86], [87], [89], [90], [92], [93], [97], [100], [103], [109].

Overlap of [60] babbbbbbbb=ba with [68] bbaa=abbbbabbbbbb:

Critical pair: babbbbbbabbbbabbbbbb=baaa.

Reduce LHS:

Defines rule #18.

Referenced by [72], [92], [93].

Overlap of [2] abbab=ba with [42] bbbbbbbabbba=abab:

Critical pair: abbaabab=babbbbbbabbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [89], [101].

Overlap of [13] bbaabb=abbbba with [42] bbbbbbbabbba=abab:

Critical pair: bbaaabab=abbbbabbbbbabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [98].

Overlap of [58] abaaa=bbbbabbbbabbbbbbab with [69] baaabbbbbbbb=baaa:

Critical pair: abaaa=bbbbabbbbabbbbbbabbbbbbbbb.

Reduce LHS:

Reduce RHS:

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

Overlap of [13] bbaabb=abbbba with [34] bbabbbabbbbba=abaab:

Critical pair: bbaababaab=abbbbababbbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [77].

Overlap of [34] bbabbbabbbbba=abaab with [9] abbbabba=bbaab:

Critical pair: bbabbbabbbbbbbaab=abaabbbbabba.

Reduce LHS:

Reduce RHS:

Referenced by [87], [88].

Simplify [8] baabbba=abbbaab.

Reduce RHS:

Defines rule #19.

Referenced by [96].

Simplify [58] abaaa=bbbbabbbbabbbbbbab.

Reduce RHS:

Defines rule #38.

Overlap of [59] aabbbbbabbbbabbbbbbab=bbbbbabbbbba with [72] bbbbabbbbabbbbbbab=bbabbbbabbbbabbbbb:

Critical pair: aabbbabbbbabbbbabbbbb=bbbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [101].

Simplify [67] abbbabbbbbabbbbabbbbbb=bbbbbabbbbabbbbbbab.

Reduce RHS:

Referenced by [92].

Overlap of [29] aaba=bbabbbabb with [64] aabbbba=babbbbbbbabb:

Critical pair: aabbabbbbbbbabb=bbabbbabbabbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [87], [103].

Overlap of [64] aabbbba=babbbbbbbabb with [61] abba=babbbbbbb:

Critical pair: aabbbbbabbbbbbb=babbbbbbbabbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [90].

Overlap of [68] bbaa=abbbbabbbbbb with [64] aabbbba=babbbbbbbabb:

Critical pair: bbbabbbbbbbabb=abbbbabbbbbbbbbba.

Reduce RHS:

Referenced by [103], [105].

Overlap of [24] bbbbbbabbbba=aabb with [65] bbabbbabbbba=ababbbbbb:

Critical pair: bbbbbbabbababbbbbb=aabbbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #36.

Referenced by [107].

Overlap of [42] bbbbbbbabbba=abab with [65] bbabbbabbbba=ababbbbbb:

Critical pair: bbbbbababbbbbb=ababbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [109].

Overlap of [42] bbbbbbbabbba=abab with [65] bbabbbabbbba=ababbbbbb:

Critical pair: bbbbbbbabababbbbbb=ababbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Overlap of [63] bbbbbbbba=abbbbbbbb with [65] bbabbbabbbba=ababbbbbb:

Critical pair: bbbbbbababbbbbb=abbbbbbbbbbbabbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [95], [96], [97], [98].

Overlap of [21] bbbbbbabbbabbba=aabbbab with [65] bbabbbabbbba=ababbbbbb:

Critical pair: bbbbbbabababbbbbb=aabbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [68] bbaa=abbbbabbbbbb with [74] aabbbbbbabbbabbbb=baaabb:

Critical pair: bbbaaabb=abbbbabbbbbbbbbbbbabbbabbbb.

Reduce LHS:

Reduce RHS:

Referenced by [89].

Overlap of [74] aabbbbbbabbbabbbb=baaabb with [60] babbbbbbbb=ba:

Critical pair: aabbbbbbabbba=baaabbbbbb.

Defines rule #37.

Referenced by [89], [90], [91], [92], [93].

Overlap of [61] abba=babbbbbbb with [88] aabbbbbbabbba=baaabbbbbb:

Critical pair: abbbaaabbbbbb=babbbbbbbabbbbbbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [93], [103], [104].

Overlap of [62] baba=abbbabbbbbbb with [88] aabbbbbbabbba=baaabbbbbb:

Critical pair: babbaaabbbbbb=abbbabbbbbbbabbbbbbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #47.

Overlap of [88] aabbbbbbabbba=baaabbbbbb with [62] baba=abbbabbbbbbb:

Critical pair: aabbbbbbabbabbbabbbbbbb=baaabbbbbbba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [91] baaabbbbbbba=aaabbbbbb with [62] baba=abbbabbbbbbb:

Critical pair: baaabbbbbbabbbabbbbbbb=aaabbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #33.

Referenced by [94].

Overlap of [91] baaabbbbbbba=aaabbbbbb with [68] bbaa=abbbbabbbbbb:

Critical pair: baaabbbbbabbbbabbbbbb=aaabbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Referenced by [100].

Overlap of [91] baaabbbbbbba=aaabbbbbb with [92] aaabbbbbbba=bbbabbbbabbbbabb:

Critical pair: bbbbabbbbabbbbabb=aaabbbbbb.

Referenced by [102].

Overlap of [7] ababbba=baab with [85] abbbabbbba=bbbbbabbbabbbbb:

Critical pair: abbbbbbabbbabbbbb=baabbbbba.

Flip LHS and RHS.

Defines rule #20.

Overlap of [75] baabbba=ababbbbabbbbbbb with [85] abbbabbbba=bbbbbabbbabbbbb:

Critical pair: babbbbbabbbabbbbb=ababbbbabbbbbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #40.

Referenced by [109].

Overlap of [68] bbaa=abbbbabbbbbb with [85] abbbabbbba=bbbbbabbbabbbbb:

Critical pair: bbabbbbbabbbabbbbb=abbbbabbbbbbbbbabbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #42.

Overlap of [71] abbbbabbbbbabbba=bbbbabb with [85] abbbabbbba=bbbbbabbbabbbbb:

Critical pair: abbbbabbbbbbbbbbabbbabbbbb=bbbbabbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [99], [100].

Overlap of [34] bbabbbabbbbba=abaab with [98] bbbbabbbbbba=abbbbbbabbbb:

Critical pair: bbabbbababbbbbbabbbb=abaabbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #39.

Overlap of [68] bbaa=abbbbabbbbbb with [93] aaabbbbbba=babbbbbabbbbabb:

Critical pair: bbbabbbbbabbbbabb=abbbbabbbbbbabbbbbba.

Reduce RHS:

Referenced by [111].

Overlap of [62] baba=abbbabbbbbbb with [70] babbbbbbabbba=abbbbabbbabbb:

Critical pair: baabbbbabbbabbb=abbbabbbbbbbbbbbbbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #43.

Overlap of [94] bbbbabbbbabbbbabb=aaabbbbbb with [60] babbbbbbbb=ba:

Critical pair: bbbbabbbbabbbba=aaabbbbbbbbbbbb.

Reduce RHS:

Defines rule #27.

Overlap of [61] abba=babbbbbbb with [89] baaabbbbbabbb=abaabbbbbbabb:

Critical pair: ababaabbbbbbabb=babbbbbbbaabbbbbabbb.

Reduce LHS:

Reduce RHS:

Referenced by [106], [107].

Overlap of [89] baaabbbbbabbb=abaabbbbbbabb with [60] babbbbbbbb=ba:

Critical pair: baaabbbbba=abaabbbbbbabbbbbbb.

Defines rule #44.

Overlap of [81] bbbabbbbbbbabb=abbbbbabbbbbbb with [60] babbbbbbbb=ba:

Critical pair: bbbabbbbbbba=abbbbbabbbbbbbbbbbbb.

Reduce RHS:

Defines rule #8.

Overlap of [103] aaabbbbbabbbabb=bbbabbbbabbbbb with [60] babbbbbbbb=ba:

Critical pair: aaabbbbbabbba=bbbabbbbabbbbbbbbbbb.

Reduce RHS:

Defines rule #46.

Overlap of [103] aaabbbbbabbbabb=bbbabbbbabbbbb with [61] abba=babbbbbbb:

Critical pair: aaabbbbbabbbbabbbbbbb=bbbabbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [42] bbbbbbbabbba=abab with [54] bbbabbbabbbbbba=abbbbbabbbabbbb:

Critical pair: bbbbabbbbbabbbabbbb=ababbbbbbba.

Referenced by [110].

Overlap of [96] ababbbbabbba=babbbbbabbbabbbbb with [54] bbbabbbabbbbbba=abbbbbabbbabbbb:

Critical pair: abababbbbbabbbabbbb=babbbbbabbbabbbbbbbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #45.

Overlap of [108] bbbbabbbbbabbbabbbb=ababbbbbbba with [60] babbbbbbbb=ba:

Critical pair: bbbbabbbbbabbba=ababbbbbbbabbbb.

Defines rule #28.

Overlap of [100] bbbabbbbbabbbbabb=aabbbbbbbabbbbbbb with [60] babbbbbbbb=ba:

Critical pair: bbbabbbbbabbbba=aabbbbbbbabbbbbbbbbbbbb.

Reduce RHS:

Defines rule #26.