Certificate for #21778 ⟨a, b | aaa=1, babbbbb=a⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #3.

Referenced by [4], [5], [11], [12], [14], [18], [19], [22], [23], [24], [25], [26], [27], [28], [29], [30], [31], [32], [33], [34], [35], [38], [39], [41], [43], [45], [46], [47], [48], [49], [50], [51], [52], [53], [55], [59], [62], [64], [65], [66], [67], [69], [71], [75], [77], [78], [79], [82].

Axiom: babbbbb=a.

Referenced by [3], [6], [7], [8], [9], [15], [16], [21], [22], [30], [35], [38], [41], [44], [45], [46], [52], [56], [57], [58], [60], [61], [68], [69], [70], [72], [73], [74], [75], [76], [77], [81].

Overlap of [2] babbbbb=a with [2] babbbbb=a:

Critical pair: babbbba=aabbbbb.

Flip LHS and RHS.

Referenced by [4], [10].

Overlap of [1] aaa=1 with [3] aabbbbb=babbbba:

Critical pair: ababbbba=bbbbb.

Referenced by [5], [14].

Overlap of [4] ababbbba=bbbbb with [1] aaa=1:

Critical pair: ababbbb=bbbbbaa.

Referenced by [6], [14], [17].

Overlap of [5] ababbbb=bbbbbaa with [2] babbbbb=a:

Critical pair: aa=bbbbbaab.

Flip LHS and RHS.

Referenced by [7], [8], [9], [10], [14], [18].

Overlap of [2] babbbbb=a with [6] bbbbbaab=aa:

Critical pair: babaa=abaab.

Flip LHS and RHS.

Referenced by [11], [13], [20], [23], [31], [45], [48], [50], [51], [55], [63], [69].

Overlap of [2] babbbbb=a with [6] bbbbbaab=aa:

Critical pair: babbaa=abbaab.

Flip LHS and RHS.

Referenced by [18], [24], [25], [29], [32], [38], [41], [49], [52].

Overlap of [2] babbbbb=a with [6] bbbbbaab=aa:

Critical pair: babbbaa=abbbaab.

Flip LHS and RHS.

Referenced by [22], [25], [26], [28], [29], [30], [33], [34].

Overlap of [6] bbbbbaab=aa with [3] aabbbbb=babbbba:

Critical pair: bbbbbbabbbba=aabbbb.

Flip LHS and RHS.

Referenced by [37], [56].

Overlap of [1] aaa=1 with [7] abaab=babaa:

Critical pair: aababaa=baab.

Referenced by [12], [13].

Overlap of [11] aababaa=baab with [1] aaa=1:

Critical pair: aabab=baaba.

Referenced by [14], [42], [51], [55], [69].

Overlap of [11] aababaa=baab with [7] abaab=babaa:

Critical pair: aabbabaa=baabb.

Referenced by [19], [20].

Overlap of [4] ababbbba=bbbbb with [12] aabab=baaba:

Critical pair: ababbbbbaaba=bbbbbabab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [2] babbbbb=a with [14] bbbbbabab=aba:

Critical pair: bababa=ababab.

Flip LHS and RHS.

Referenced by [52].

Overlap of [2] babbbbb=a with [14] bbbbbabab=aba:

Critical pair: babbaba=abbabab.

Flip LHS and RHS.

Referenced by [46].

Overlap of [14] bbbbbabab=aba with [5] ababbbb=bbbbbaa:

Critical pair: bbbbbbbbbbaa=ababbb.

Flip LHS and RHS.

Referenced by [35], [36].

Overlap of [8] abbaab=babbaa with [6] bbbbbaab=aa:

Critical pair: abbaaaa=babbaabbbbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [13] aabbabaa=baabb with [1] aaa=1:

Critical pair: aabbab=baabba.

Referenced by [61].

Overlap of [13] aabbabaa=baabb with [7] abaab=babaa:

Critical pair: aabbbabaa=baabbb.

Referenced by [27].

Overlap of [18] bbbbbabbab=abba with [2] babbbbb=a:

Critical pair: bbbbbaba=abbabbbb.

Flip LHS and RHS.

Referenced by [40].

Overlap of [9] abbbaab=babbbaa with [18] bbbbbabbab=abba:

Critical pair: abbbaaabba=babbbaabbbbabbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [23], [24], [25], [26], [29], [37].

Overlap of [7] abaab=babaa with [22] bbbbaab=abbbbba:

Critical pair: abaaabbbbba=babaabbbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [8] abbaab=babbaa with [22] bbbbaab=abbbbba:

Critical pair: abbaaabbbbba=babbaabbbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30], [38].

Overlap of [18] bbbbbabbab=abba with [22] bbbbaab=abbbbba:

Critical pair: bbbbbabbaabbbbba=abbabbbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [43], [44].

Overlap of [22] bbbbaab=abbbbba with [22] bbbbaab=abbbbba:

Critical pair: bbbbaaabbbbba=abbbbbabbbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [20] aabbbabaa=baabbb with [1] aaa=1:

Critical pair: aabbbab=baabbba.

Referenced by [29], [34], [41].

Overlap of [9] abbbaab=babbbaa with [23] bbbbabab=abbbbbba:

Critical pair: abbbaaabbbbbba=babbbaabbbabab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [41], [52], [54], [56], [58].

Overlap of [27] aabbbab=baabbba with [23] bbbbabab=abbbbbba:

Critical pair: aabbbaabbbbbba=baabbbabbbabab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [9] abbbaab=babbbaa with [24] bbbbabbab=abbbbbbba:

Critical pair: abbbaaabbbbbbba=babbbaabbbabbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31], [32], [33], [34], [41], [44], [45].

Overlap of [7] abaab=babaa with [30] bbbaab=abbbbbbbbbba:

Critical pair: abaaabbbbbbbbbba=babaabbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [38], [52], [56].

Overlap of [8] abbaab=babbaa with [30] bbbaab=abbbbbbbbbba:

Critical pair: abbaaabbbbbbbbbba=babbaabbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46], [52].

Overlap of [9] abbbaab=babbbaa with [30] bbbaab=abbbbbbbbbba:

Critical pair: abbbaaabbbbbbbbbba=babbbaabbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [45], [52], [70].

Overlap of [27] aabbbab=baabbba with [30] bbbaab=abbbbbbbbbba:

Critical pair: aabbbaabbbbbbbbbba=baabbbabbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [17] ababbb=bbbbbbbbbbaa with [2] babbbbb=a:

Critical pair: ababba=bbbbbbbbbbaaabbbbb.

Reduce RHS:

Referenced by [39], [40].

Overlap of [23] bbbbabab=abbbbbba with [17] ababbb=bbbbbbbbbbaa:

Critical pair: bbbbbbbbbbbbbbaa=abbbbbbabb.

Flip LHS and RHS.

Referenced by [56].

Overlap of [22] bbbbaab=abbbbba with [10] aabbbb=bbbbbbabbbba:

Critical pair: bbbbbbbbbbabbbba=abbbbbabbb.

Flip LHS and RHS.

Referenced by [57], [68].

Overlap of [24] bbbbabbab=abbbbbbba with [31] bbbabab=abbbbbbbbbbba:

Critical pair: bbbbabbaabbbbbbbbbbba=abbbbbbbabbabab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [35] ababba=bbbbbbbbbbbbbbb with [1] aaa=1:

Critical pair: ababb=bbbbbbbbbbbbbbbaa.

Referenced by [42], [61].

Overlap of [35] ababba=bbbbbbbbbbbbbbb with [21] abbabbbb=bbbbbaba:

Critical pair: abbbbbbaba=bbbbbbbbbbbbbbbbbbb.

Referenced by [60], [61].

Overlap of [27] aabbbab=baabbba with [28] bbbbabbbbab=abbbbbbbbba:

Critical pair: aabbbaabbbbbbbbba=baabbbabbbabbbbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [12] aabab=baaba with [39] ababb=bbbbbbbbbbbbbbbaa:

Critical pair: abbbbbbbbbbbbbbbaa=baabab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [47].

Overlap of [25] abbbabbbaa=bbbbbbbbbbabb with [1] aaa=1:

Critical pair: abbbabbb=bbbbbbbbbbabba.

Referenced by [45], [46].

Overlap of [25] abbbabbbaa=bbbbbbbbbbabb with [30] bbbaab=abbbbbbbbbba:

Critical pair: abbbaabbbbbbbbbba=bbbbbbbbbbabbb.

Reduce LHS:

Referenced by [53].

Overlap of [43] abbbabbb=bbbbbbbbbbabba with [30] bbbaab=abbbbbbbbbba:

Critical pair: abbbababbbbbbbbbba=bbbbbbbbbbabbabaab.

Reduce LHS:

Reduce RHS:

Referenced by [46].

Overlap of [43] abbbabbb=bbbbbbbbbbabba with [45] abbbbabbbbaa=bbbbbabbb:

Critical pair: abbbbbbbbabbb=bbbbbbbbbbabbababbbbaa.

Reduce RHS:

Referenced by [58].

Overlap of [42] bbaaba=abbbbbbbbbbbbbbbaa with [1] aaa=1:

Critical pair: bbaab=abbbbbbbbbbbbbbbaaaa.

Reduce RHS:

Referenced by [48], [49], [50], [58], [61], [65], [68].

Overlap of [7] abaab=babaa with [47] bbaab=abbbbbbbbbbbbbbba:

Critical pair: abaaabbbbbbbbbbbbbbba=babaabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [51], [52].

Overlap of [8] abbaab=babbaa with [47] bbaab=abbbbbbbbbbbbbbba:

Critical pair: abbaaabbbbbbbbbbbbbbba=babbaabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [55], [69].

Overlap of [47] bbaab=abbbbbbbbbbbbbbba with [47] bbaab=abbbbbbbbbbbbbbba:

Critical pair: bbaaabbbbbbbbbbbbbbba=abbbbbbbbbbbbbbbabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [12] aabab=baaba with [48] bbabab=abbbbbbbbbbbbbbbba:

Critical pair: aabaabbbbbbbbbbbbbbbba=baabababab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [55].

Overlap of [32] bbbabbab=abbbbbbbbbbbba with [48] bbabab=abbbbbbbbbbbbbbbba:

Critical pair: bbbabbaabbbbbbbbbbbbbbbba=abbbbbbbbbbbbababab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [71].

Overlap of [44] abbbbabbbaa=bbbbbbbbbbabbb with [1] aaa=1:

Critical pair: abbbbabbb=bbbbbbbbbbabbba.

Referenced by [54].

Overlap of [28] bbbbabbbbab=abbbbbbbbba with [53] abbbbabbb=bbbbbbbbbbabbba:

Critical pair: bbbbbbbbbbbbbbabbba=abbbbbbbbbabb.

Flip LHS and RHS.

Referenced by [58].

Overlap of [12] aabab=baaba with [49] bbabbab=abbbbbbbbbbbbbbbbba:

Critical pair: aabaabbbbbbbbbbbbbbbbba=baabababbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [72].

Overlap of [10] aabbbb=bbbbbbabbbba with [36] abbbbbbabb=bbbbbbbbbbbbbbaa:

Critical pair: abbbbbbbbbbbbbbaa=bbbbbbabbbbabbabb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [59].

Overlap of [2] babbbbb=a with [37] abbbbbabbb=bbbbbbbbbbabbbba:

Critical pair: bbbbbbbbbbbabbbba=aabbb.

Flip LHS and RHS.

Referenced by [68], [75].

Overlap of [38] abbbabbaa=bbbbbbbbbbbbbbbabb with [47] bbaab=abbbbbbbbbbbbbbba:

Critical pair: abbbaabbbbbbbbbbbbbbba=bbbbbbbbbbbbbbbabbb.

Reduce LHS:

Referenced by [67], [68].

Overlap of [56] bbbabbbbaba=abbbbbbbbbbbbbbaa with [1] aaa=1:

Critical pair: bbbabbbbab=abbbbbbbbbbbbbbaaaa.

Reduce RHS:

Referenced by [73].

Overlap of [2] babbbbb=a with [40] abbbbbbaba=bbbbbbbbbbbbbbbbbbb:

Critical pair: bbbbbbbbbbbbbbbbbbbb=ababa.

Flip LHS and RHS.

Referenced by [62], [63].

Overlap of [39] ababb=bbbbbbbbbbbbbbbaa with [40] abbbbbbaba=bbbbbbbbbbbbbbbbbbb:

Critical pair: abbbbbbbbbbbbbbbbbbbb=bbbbbbbbbbbbbbbaabbbbaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [64].

Overlap of [60] ababa=bbbbbbbbbbbbbbbbbbbb with [1] aaa=1:

Critical pair: abab=bbbbbbbbbbbbbbbbbbbbaa.

Referenced by [72], [77].

Overlap of [60] ababa=bbbbbbbbbbbbbbbbbbbb with [7] abaab=babaa:

Critical pair: abbabaa=bbbbbbbbbbbbbbbbbbbbab.

Referenced by [66].

Overlap of [61] baabaa=abbbbbbbbbbbbbbbbbbbb with [1] aaa=1:

Critical pair: baab=abbbbbbbbbbbbbbbbbbbba.

Referenced by [65].

Overlap of [47] bbaab=abbbbbbbbbbbbbbba with [64] baab=abbbbbbbbbbbbbbbbbbbba:

Critical pair: bbaaabbbbbbbbbbbbbbbbbbbba=abbbbbbbbbbbbbbbaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [69].

Overlap of [63] abbabaa=bbbbbbbbbbbbbbbbbbbbab with [1] aaa=1:

Critical pair: abbab=bbbbbbbbbbbbbbbbbbbbaba.

Referenced by [71].

Overlap of [58] abbbbabbaa=bbbbbbbbbbbbbbbabbb with [1] aaa=1:

Critical pair: abbbbabb=bbbbbbbbbbbbbbbabbba.

Referenced by [69].

Overlap of [58] abbbbabbaa=bbbbbbbbbbbbbbbabbb with [47] bbaab=abbbbbbbbbbbbbbba:

Critical pair: abbbbaabbbbbbbbbbbbbbba=bbbbbbbbbbbbbbbabbbb.

Reduce LHS:

Referenced by [74].

Overlap of [12] aabab=baaba with [67] abbbbabb=bbbbbbbbbbbbbbbabbba:

Critical pair: aabbbbbbbbbbbbbbbbabbba=baababbbabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [70], [71], [72], [73], [75], [76], [77].

Simplify [33] bbbabbbab=abbbbbbbbbbbbba.

Reduce RHS:

Referenced by [75].

Overlap of [52] abbbbbbbbabaa=bbbbbbbbbbbbbbbbbbbabb with [69] abbbbbbb=bbbbbbbbbbbbbbbbbbbbbbbbab:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbabbabaa=bbbbbbbbbbbbbbbbbbbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [73], [75].

Overlap of [55] abbbbbbbbbbbbbbbbbab=bbbbbbbbbbbbbbbbbaba with [69] abbbbbbb=bbbbbbbbbbbbbbbbbbbbbbbbab:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbabbbbbbbbbbbab=bbbbbbbbbbbbbbbbbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [73], [75].

Simplify [59] bbbabbbbab=abbbbbbbbbbbbbba.

Reduce RHS:

Referenced by [77].

Overlap of [2] babbbbb=a with [68] abbbbbabbaa=bbbbbbbbbbbbbbbabbbb:

Critical pair: bbbbbbbbbbbbbbbbabbbb=aabbaa.

Flip LHS and RHS.

Referenced by [75].

Overlap of [1] aaa=1 with [74] aabbaa=bbbbbbbbbbbbbbbbabbbb:

Critical pair: abbbbbbbbbbbbbbbbabbbb=bbaa.

Reduce LHS:

Referenced by [79].

Overlap of [2] babbbbb=a with [69] abbbbbbb=bbbbbbbbbbbbbbbbbbbbbbbbab:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbab=abb.

Flip LHS and RHS.

Referenced by [77], [81].

Overlap of [69] abbbbbbb=bbbbbbbbbbbbbbbbbbbbbbbbab with [73] bbbabbbbab=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaa:

Critical pair: abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaa=bbbbbbbbbbbbbbbbbbbbbbbbababbbbab.

Reduce LHS:

Reduce RHS:

Referenced by [78].

Overlap of [77] bbbbbabaa=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [1] aaa=1:

Critical pair: bbbbbab=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbba.

Referenced by [80], [81].

Overlap of [75] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaa=bbaa with [1] aaa=1:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bbaaa.

Reduce RHS:

Referenced by [80].

Overlap of [79] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bb with [78] bbbbbab=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbba:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=bbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [83].

Overlap of [2] babbbbb=a with [76] abb=bbbbbbbbbbbbbbbbbbbbbbbbbab:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbabbbb=a.

Reduce LHS:

Referenced by [82], [83].

Overlap of [81] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=a with [1] aaa=1:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aaa.

Reduce RHS:

Defines rule #1.

Referenced by [83].

Overlap of [81] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=a with [80] bbab=bbbbbbbbbbbbbbbbbbbbbbbbbbba:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=ab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.