Certificate for #22279 ⟨a, b | aaa=1, abbabb=ba⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #13.

Referenced by [3], [5], [8], [11], [16], [19], [29], [50], [59], [99], [104].

Axiom: abbabb=ba.

Referenced by [3], [4], [6], [9], [14], [20], [28], [30], [33], [34], [35], [41], [42], [60], [61], [62], [78], [86], [89], [92], [93], [94], [95], [96], [98].

Overlap of [1] aaa=1 with [2] abbabb=ba:

Critical pair: aaba=bbabb.

Referenced by [5], [6], [7], [8], [15], [28], [36], [37], [44], [47], [53], [55], [60], [69], [90].

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

Critical pair: abbba=baabb.

Flip LHS and RHS.

Referenced by [8], [10], [13], [22], [28], [31], [37], [40], [49], [54], [55], [60], [89], [92], [97].

Overlap of [3] aaba=bbabb with [1] aaa=1:

Critical pair: aab=bbabbaa.

Flip LHS and RHS.

Referenced by [9], [10], [12], [21], [32], [100].

Overlap of [3] aaba=bbabb with [2] abbabb=ba:

Critical pair: aabba=bbabbbbabb.

Referenced by [13], [14], [15], [16], [19], [51].

Overlap of [3] aaba=bbabb with [3] aaba=bbabb:

Critical pair: aabbbabb=bbabbaba.

Referenced by [40], [41], [63].

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

Critical pair: baababbba=abbbaaabb.

Reduce LHS:

Reduce RHS:

Referenced by [28], [29], [30], [31], [32], [33], [35], [43], [45], [52], [57], [58], [61], [65].

Overlap of [2] abbabb=ba with [5] bbabbaa=aab:

Critical pair: abbabaab=bababbaa.

Referenced by [41].

Overlap of [5] bbabbaa=aab with [4] baabb=abbba:

Critical pair: bbababbba=aabbb.

Referenced by [11], [12], [16], [17], [22], [38], [48], [49], [60].

Overlap of [10] bbababbba=aabbb with [1] aaa=1:

Critical pair: bbababbb=aabbbaa.

Flip LHS and RHS.

Referenced by [18].

Overlap of [10] bbababbba=aabbb with [5] bbabbaa=aab:

Critical pair: bbababaab=aabbbbbaa.

Referenced by [24].

Overlap of [4] baabb=abbba with [6] aabba=bbabbbbabb:

Critical pair: bbbabbbbabb=abbbaa.

Flip LHS and RHS.

Referenced by [18], [32], [37], [42], [43], [101].

Overlap of [6] aabba=bbabbbbabb with [2] abbabb=ba:

Critical pair: aba=bbabbbbabbbb.

Flip LHS and RHS.

Referenced by [17], [23], [36], [51], [53], [66].

Overlap of [6] aabba=bbabbbbabb with [3] aaba=bbabb:

Critical pair: aabbbbabb=bbabbbbabbaba.

Flip LHS and RHS.

Referenced by [67].

Overlap of [6] aabba=bbabbbbabb with [10] bbababbba=aabbb:

Critical pair: aaaabbb=bbabbbbabbbabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [10] bbababbba=aabbb with [14] bbabbbbabbbb=aba:

Critical pair: bbabababa=aabbbbbbbabbbb.

Referenced by [26].

Simplify [11] aabbbaa=bbababbb.

Reduce LHS:

Referenced by [19], [20], [21], [22], [23], [38], [50].

Overlap of [1] aaa=1 with [18] abbbabbbbabb=bbababbb:

Critical pair: aabbababbb=bbbabbbbabb.

Reduce LHS:

Referenced by [25], [51].

Overlap of [2] abbabb=ba with [18] abbbabbbbabb=bbababbb:

Critical pair: abbbbababbb=bababbbbabb.

Referenced by [22].

Overlap of [18] abbbabbbbabb=bbababbb with [5] bbabbaa=aab:

Critical pair: abbbabbbbabaab=bbababbbbabbaa.

Reduce RHS:

Referenced by [22].

Overlap of [18] abbbabbbbabb=bbababbb with [10] bbababbba=aabbb:

Critical pair: abbbabbbbabaabbb=bbababbbbababbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [18] abbbabbbbabb=bbababbb with [14] bbabbbbabbbb=aba:

Critical pair: ababa=bbababbbbb.

Referenced by [24], [26], [27], [36], [46], [49], [58], [59], [61].

Overlap of [12] bbababaab=aabbbbbaa with [23] ababa=bbababbbbb:

Critical pair: bbbbababbbbbab=aabbbbbaa.

Flip LHS and RHS.

Referenced by [70].

Overlap of [16] bbabbbbabbbabbba=abbb with [19] bbabbbbabbbabbb=bbbabbbbabb:

Critical pair: bbbabbbbabba=abbb.

Referenced by [34], [35], [36], [39].

Overlap of [17] bbabababa=aabbbbbbbabbbb with [23] ababa=bbababbbbb:

Critical pair: bbbbababbbbbba=aabbbbbbbabbbb.

Flip LHS and RHS.

Referenced by [72].

Simplify [22] bbabbababbbbabba=bbabababbbab.

Reduce RHS:

Referenced by [68].

Overlap of [4] baabb=abbba with [8] bbbabbbbba=abbbbb:

Critical pair: baababbbbb=abbbabbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31], [74].

Overlap of [8] bbbabbbbba=abbbbb with [1] aaa=1:

Critical pair: bbbabbbbb=abbbbbaa.

Flip LHS and RHS.

Referenced by [44], [45], [46], [50].

Overlap of [8] bbbabbbbba=abbbbb with [2] abbabb=ba:

Critical pair: bbbabbbbbba=abbbbbbbabb.

Flip LHS and RHS.

Referenced by [57], [59], [70], [73].

Overlap of [8] bbbabbbbba=abbbbb with [4] baabb=abbba:

Critical pair: bbbabbbbabbba=abbbbbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [42].

Overlap of [8] bbbabbbbba=abbbbb with [5] bbabbaa=aab:

Critical pair: bbbabbbaab=abbbbbbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38], [39], [44], [75].

Overlap of [8] bbbabbbbba=abbbbb with [8] bbbabbbbba=abbbbb:

Critical pair: bbbabbabbbbb=abbbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [43], [46], [62], [77].

Overlap of [2] abbabb=ba with [25] bbbabbbbabba=abbb:

Critical pair: abbababbb=babbabbbbabba.

Reduce RHS:

Referenced by [37], [38], [39], [50], [54], [55], [56], [69], [76].

Overlap of [8] bbbabbbbba=abbbbb with [25] bbbabbbbabba=abbb:

Critical pair: bbbabbabbb=abbbbbbbbbabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [77].

Overlap of [25] bbbabbbbabba=abbb with [23] ababa=bbababbbbb:

Critical pair: bbbabbbbabbbbababbbbb=abbbbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [49].

Overlap of [4] baabb=abbba with [34] abbababbb=bbbaa:

Critical pair: babbbaa=abbbaababbb.

Reduce LHS:

Reduce RHS:

Referenced by [38], [39], [43], [44], [75].

Overlap of [18] abbbabbbbabb=bbababbb with [34] abbababbb=bbbaa:

Critical pair: abbbabbbbbbbaa=bbababbbababbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [44], [78].

Overlap of [25] bbbabbbbabba=abbb with [34] abbababbb=bbbaa:

Critical pair: bbbabbbbbbbaa=abbbbabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [46], [62], [66], [74], [80].

Overlap of [4] baabb=abbba with [7] aabbbabb=bbabbaba:

Critical pair: bbbabbaba=abbbababb.

Flip LHS and RHS.

Referenced by [47], [48], [49], [50], [56].

Overlap of [7] aabbbabb=bbabbaba with [2] abbabb=ba:

Critical pair: aabbbba=bbabbabaabb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [81].

Overlap of [2] abbabb=ba with [13] abbbaa=bbbabbbbabb:

Critical pair: abbbbbabbbbabb=babaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [82].

Overlap of [8] bbbabbbbba=abbbbb with [13] abbbaa=bbbabbbbabb:

Critical pair: bbbabbbbbbbbabbbbabb=abbbbbbbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [84].

Overlap of [3] aaba=bbabb with [29] abbbbbaa=bbbabbbbb:

Critical pair: aabbbbabbbbb=bbabbbbbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [85].

Overlap of [8] bbbabbbbba=abbbbb with [29] abbbbbaa=bbbabbbbb:

Critical pair: bbbbbbabbbbb=abbbbba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [46], [47], [57], [59], [65], [67], [70], [71], [81], [90].

Overlap of [23] ababa=bbababbbbb with [29] abbbbbaa=bbbabbbbb:

Critical pair: ababbbbabbbbb=bbababbbbbbbbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [87].

Overlap of [3] aaba=bbabb with [40] abbbababb=bbbabbaba:

Critical pair: aabbbbabbaba=bbabbbbbababb.

Reduce RHS:

Referenced by [88].

Overlap of [10] bbababbba=aabbb with [40] abbbababb=bbbabbaba:

Critical pair: bbababbbbbbabbaba=aabbbbbbababb.

Referenced by [89].

Overlap of [40] abbbababb=bbbabbaba with [10] bbababbba=aabbb:

Critical pair: abaabbb=bbbabbababa.

Reduce LHS:

Reduce RHS:

Referenced by [64].

Overlap of [40] abbbababb=bbbabbaba with [29] abbbbbaa=bbbabbbbb:

Critical pair: abbbabbbbabbbbb=bbbabbababbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [51], [52], [53], [54], [55], [56], [57], [58], [62], [68], [72], [90], [91].

Overlap of [6] aabba=bbabbbbabb with [50] bbababbbbbb=bbbbbba:

Critical pair: aabbbbbba=bbabbbbabbbabbbbbb.

Reduce RHS:

Referenced by [59], [60], [61], [62].

Overlap of [8] bbbabbbbba=abbbbb with [50] bbababbbbbb=bbbbbba:

Critical pair: bbbabbbbbbbbba=abbbbbbabbbbbb.

Flip LHS and RHS.

Referenced by [57], [61], [64], [76].

Overlap of [14] bbabbbbabbbb=aba with [50] bbababbbbbb=bbbbbba:

Critical pair: bbabbbbabbbbbbbba=abaababbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [57].

Overlap of [34] abbababbb=bbbaa with [50] bbababbbbbb=bbbbbba:

Critical pair: abbbbbba=bbbaabbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [55], [57], [60], [61], [64], [107], [108].

Overlap of [34] abbababbb=bbbaa with [50] bbababbbbbb=bbbbbba:

Critical pair: abbababbbbbbbba=bbbaabababbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [73].

Overlap of [40] abbbababb=bbbabbaba with [50] bbababbbbbb=bbbbbba:

Critical pair: abbbbbbba=bbbabbababbbb.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [50] bbababbbbbb=bbbbbba with [8] bbbabbbbba=abbbbb:

Critical pair: bbababbbbabbbbb=bbbbbbababbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [76].

Overlap of [50] bbababbbbbb=bbbbbba with [50] bbababbbbbb=bbbbbba:

Critical pair: bbababbbbbbbbbbba=bbbbbbabababbbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [66], [71], [81], [87].

Overlap of [51] aabbbbbba=babab with [1] aaa=1:

Critical pair: aabbbbbb=bababaa.

Reduce RHS:

Referenced by [61], [89].

Overlap of [51] aabbbbbba=babab with [10] bbababbba=aabbb:

Critical pair: aabbbbaabbb=bababbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [61], [63], [67].

Overlap of [51] aabbbbbba=babab with [23] ababa=bbababbbbb:

Critical pair: aabbbbbbbbababbbbb=bababbaba.

Reduce LHS:

Reduce RHS:

Referenced by [64].

Overlap of [51] aabbbbbba=babab with [50] bbababbbbbb=bbbbbba:

Critical pair: aabbbbbbbbbba=bababbabbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [74], [78], [80], [86].

Simplify [7] aabbbabb=bbabbaba.

Reduce RHS:

Referenced by [64].

Overlap of [63] aabbbabb=bbbabbbbbbbba with [49] aabbbab=bbbbabbbabbbbbbbbbbbb:

Critical pair: bbbbabbbabbbbbbbbbbbbb=bbbabbbbbbbba.

Reduce LHS:

Referenced by [70], [73], [89], [97].

Overlap of [8] bbbabbbbba=abbbbb with [45] abbbbba=bbbbbbabbbbb:

Critical pair: bbbbbbbbbabbbbb=abbbbb.

Referenced by [73], [76], [81], [85], [90], [97].

Overlap of [14] bbabbbbabbbb=aba with [39] abbbbabbb=bbbbbbbbbbbabbbbbbbbbbb:

Critical pair: bbbbbbbbbbbbbabbbbbbbbbbbb=aba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [76], [81], [83], [88], [91], [103].

Overlap of [15] bbabbbbabbaba=aabbbbabb with [60] babbaba=bbabbbbbbbba:

Critical pair: bbabbbbbabbbbbbbba=aabbbbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [79].

Simplify [27] bbabbababbbbabba=bbbbababbbbbbbbab.

Reduce RHS:

Referenced by [69].

Overlap of [68] bbabbababbbbabba=bbbbbbbbabbab with [34] abbababbb=bbbaa:

Critical pair: bbbbbaababba=bbbbbbbbabbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [73].

Simplify [24] aabbbbbaa=bbbbababbbbbab.

Reduce RHS:

Referenced by [71].

Overlap of [70] aabbbbbaa=bbbbbbbbabbbbbbbbab with [45] abbbbba=bbbbbbabbbbb:

Critical pair: abbbbbbabbbbba=bbbbbbbbabbbbbbbbab.

Reduce LHS:

Referenced by [73].

Simplify [26] aabbbbbbbabbbb=bbbbababbbbbba.

Reduce RHS:

Referenced by [73].

Overlap of [72] aabbbbbbbabbbb=bbbbbbbbaa with [30] abbbbbbbabb=bbbabbbbbba:

Critical pair: abbbabbbbbbabb=bbbbbbbbaa.

Reduce LHS:

Referenced by [94].

Overlap of [28] abbbbabbba=bbbabbbbbbb with [39] abbbbabbb=bbbbbbbbbbbabbbbbbbbbbb:

Critical pair: bbbbbbbbbbbabbbbbbbbbbba=bbbabbbbbbb.

Reduce LHS:

Referenced by [77], [100].

Simplify [32] abbbbbbbaa=bbbbbbabbbbabbb.

Reduce RHS:

Referenced by [102].

Overlap of [34] abbababbb=bbbaa with [66] aba=bbbbabbbbbbbbbbbb:

Critical pair: abbbbbbabbbbbbbbbbbbbbb=bbbaa.

Reduce LHS:

Referenced by [82].

Overlap of [35] abbbbbbbbbabba=bbbbab with [74] bbabba=bbbabbbbbbb:

Critical pair: abbbbbbbbbbabbbbbbb=bbbbab.

Reduce LHS:

Referenced by [79], [81], [83], [84], [91], [101], [103].

Simplify [38] aabbbbabbb=abbbbbbbbbbbabbbbbbbbbbb.

Reduce RHS:

Referenced by [79].

Overlap of [78] aabbbbabbb=ba with [67] aabbbbabb=bbbbbbbbabbbbbbbbbbbbba:

Critical pair: bbbbbbbbabbbbbbbbbbbbbab=ba.

Reduce LHS:

Referenced by [89].

Simplify [39] abbbbabbb=bbbbbbbbbbbabbbbbbbbbbb.

Reduce RHS:

Referenced by [92].

Overlap of [41] bbbababbaab=aabbbba with [66] aba=bbbbabbbbbbbbbbbb:

Critical pair: bbbbbbbabbbbbbbbbbbbbbaab=aabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [88].

Simplify [42] babaa=bbbbbbabbbbbbbbbabb.

Reduce RHS:

Referenced by [83].

Overlap of [82] babaa=abbbbbbbab with [66] aba=bbbbabbbbbbbbbbbb:

Critical pair: bbbbbabbbbbbbbbbbba=abbbbbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [90], [107].

Simplify [43] abbbbbbbbaa=bbbbbbbabbbbbbbbbbbbb.

Reduce RHS:

Defines rule #17.

Simplify [44] abbbbbbbbbbbabbbbbbbbbbbbb=bbbbbbbbbbabbbbbbbbbbb.

Reduce RHS:

Referenced by [86].

Overlap of [85] abbbbbbbbbbbabbbbbbbbbbbbb=babbbbbbbbbbb with [62] bbbbbbbbbbbabbbbbbbbbbb=bbabb:

Critical pair: abbabbbb=babbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [87], [88].

Overlap of [46] abbbbbbbbbbbbabbbbbbbbbbbbb=bbbbbbbbabbbbbbbba with [58] bbbbbbbbbbbbabbbbb=bbbabbbbb:

Critical pair: abbbabbbbbbbbbbbbb=bbbbbbbbabbbbbbbba.

Reduce LHS:

Referenced by [94].

Overlap of [47] aabbbbabbaba=bbbbbbbbabbbbbbabb with [81] aabbbba=babbbbbb:

Critical pair: babbbbbbbbaba=bbbbbbbbabbbbbbabb.

Reduce LHS:

Referenced by [97].

Simplify [48] bbababbbbbbabbaba=aabbbbbbababb.

Reduce RHS:

Referenced by [90].

Overlap of [89] bbababbbbbbabbaba=babba with [50] bbababbbbbb=bbbbbba:

Critical pair: bbbbbbaabbaba=babba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [50] bbababbbbbb=bbbbbba with [66] aba=bbbbabbbbbbbbbbbb:

Critical pair: bbbbbbabbbbbbbbbbbbbbbbbb=bbbbbba.

Reduce LHS:

Referenced by [102].

Overlap of [4] baabb=abbba with [80] abbbbabbb=bbabb:

Critical pair: babbabb=abbbabbabbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [93].

Overlap of [2] abbabb=ba with [92] abbbbab=bba:

Critical pair: abbbba=babbab.

Reduce RHS:

Defines rule #6.

Referenced by [101].

Overlap of [2] abbabb=ba with [90] babba=bbabbbbbbb:

Critical pair: abbbabbbbbbb=baa.

Reduce LHS:

Referenced by [99].

Overlap of [90] babba=bbabbbbbbb with [2] abbabb=ba:

Critical pair: bba=bbabbbbbbbbb.

Flip LHS and RHS.

Referenced by [96], [97].

Overlap of [2] abbabb=ba with [95] bbabbbbbbbbb=bba:

Critical pair: abba=babbbbbbb.

Defines rule #5.

Referenced by [98], [105].

Overlap of [95] bbabbbbbbbbb=bba with [95] bbabbbbbbbbb=bba:

Critical pair: bbabbbbbbbbba=bbaabbbbbbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [2] abbabb=ba with [96] abba=babbbbbbb:

Critical pair: babbbbbbbbb=ba.

Referenced by [106].

Overlap of [94] bbbbbbbbbbaa=baa with [1] aaa=1:

Critical pair: bbbbbbbbbb=baaa.

Reduce RHS:

Defines rule #1.

Overlap of [5] bbabbaa=aab with [74] bbabba=bbbabbbbbbb:

Critical pair: bbbabbbbbbba=aab.

Flip LHS and RHS.

Defines rule #8.

Simplify [13] abbbaa=bbbabbbbabb.

Reduce RHS:

Defines rule #14.

Referenced by [104].

Simplify [75] abbbbbbbaa=bbbbbbbbabbbbbbbbbbb.

Reduce RHS:

Defines rule #16.

Simplify [66] aba=bbbbabbbbbbbbbbbb.

Reduce RHS:

Defines rule #4.

Referenced by [104], [105], [107].

Overlap of [103] aba=bbbbabbb with [1] aaa=1:

Critical pair: ab=bbbbabbbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [106], [108].

Overlap of [96] abba=babbbbbbb with [103] aba=bbbbabbb:

Critical pair: abbbbbbabbb=babbbbbbbba.

Defines rule #11.

Overlap of [104] bbbbbbbbbab=ab with [98] babbbbbbbbb=ba:

Critical pair: bbbbbbbbba=abbbbbbbbb.

Flip LHS and RHS.

Defines rule #3.

Overlap of [54] bbabbbab=abbbbbba with [103] aba=bbbbabbb:

Critical pair: bbabbbbbbbabbb=abbbbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [104] bbbbbbbbbab=ab with [54] bbabbbab=abbbbbba:

Critical pair: bbbbbbbabbbbbba=abbbab.

Flip LHS and RHS.

Defines rule #9.