| Back: | ⟨a, b | aaa=1, bababbb=a⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #16.
Referenced by [4], [6], [7], [8], [14], [16], [18], [19], [21], [25], [26], [27], [28], [32], [33], [34], [36], [41], [50], [51], [55], [56], [60], [75], [79], [85], [86], [87], [90], [103], [105], [118], [126], [138], [139], [140], [172], [192], [200], [207], [231], [232], [242], [252], [259], [261], [267].
Axiom: bababbb=a.
Referenced by [3], [5], [7], [8], [9], [10], [11], [12], [13], [22], [23], [37], [40], [49], [51], [57], [62], [78], [82], [85], [86], [91], [94], [99], [103], [104], [105], [107], [109], [110], [111], [112], [115], [118], [119], [122], [124], [125], [126], [131], [137], [139].
Overlap of [2] bababbb=a with [2] bababbb=a:
Critical pair: bababba=aababbb.
Referenced by [4], [5], [10], [15], [23], [28], [34], [41], [50], [62], [84], [98], [112], [125], [126], [129], [140].
Overlap of [3] bababba=aababbb with [1] aaa=1:
Critical pair: bababb=aababbbaa.
Flip LHS and RHS.
Overlap of [3] bababba=aababbb with [2] bababbb=a:
Critical pair: bababa=aababbbbabbb.
Flip LHS and RHS.
Referenced by [20], [49], [50], [51], [52], [53], [103], [111], [117], [118].
Overlap of [1] aaa=1 with [4] aababbbaa=bababb:
Critical pair: abababb=babbbaa.
Flip LHS and RHS.
Referenced by [7], [8], [12], [13], [23], [51], [61], [62], [86], [95], [105], [107], [109], [115], [122], [129].
Overlap of [2] bababbb=a with [6] babbbaa=abababb:
Critical pair: baabababb=aaa.
Reduce RHS:
| [1] | (aaa) |
| ⇒ 1 |
Referenced by [16].
Overlap of [6] babbbaa=abababb with [4] aababbbaa=bababb:
Critical pair: babbbbababb=abababbbabbbaa.
Reduce RHS:
| [2] | a(bababbb)abbbaa |
| [1] | ⇒ (aaa)bbbaa |
| ⇒ bbbaa |
Overlap of [8] babbbbababb=bbbaa with [2] bababbb=a:
Critical pair: babbba=bbbaab.
Flip LHS and RHS.
Referenced by [10], [11], [12], [13].
Overlap of [2] bababbb=a with [9] bbbaab=babbba:
Critical pair: bababbabbba=abaab.
Reduce LHS:
| [3] | (bababba)bbba |
| ⇒ aababbbbbba |
Referenced by [18], [19], [20].
Overlap of [2] bababbb=a with [9] bbbaab=babbba:
Critical pair: bababbbabbba=abbaab.
Reduce LHS:
| [2] | (bababbb)abbba |
| ⇒ aabbba |
Flip LHS and RHS.
Overlap of [9] bbbaab=babbba with [4] aababbbaa=bababb:
Critical pair: bbbbababb=babbbaabbbaa.
Reduce RHS:
| [6] | (babbbaa)bbbaa |
| [2] | ⇒ a(bababbb)bbaa |
| ⇒ aabbaa |
Flip LHS and RHS.
Referenced by [17], [28], [43].
Overlap of [9] bbbaab=babbba with [8] babbbbababb=bbbaa:
Critical pair: bbbaabbbaa=babbbaabbbbababb.
Reduce LHS:
| [9] | (bbbaab)bbaa |
| ⇒ babbbabbaa |
Reduce RHS:
| [6] | (babbbaa)bbbbababb |
| [2] | ⇒ a(bababbb)bbbababb |
| ⇒ aabbbababb |
Referenced by [50].
Overlap of [1] aaa=1 with [11] abbaab=aabbba:
Critical pair: aaaabbba=bbaab.
Reduce LHS:
| [1] | (aaa)abbba |
| ⇒ abbba |
Flip LHS and RHS.
Referenced by [16], [17], [20], [23], [24], [27], [33], [50], [51], [52], [55], [56], [57], [58], [62], [63], [80], [82], [85], [89], [91], [99], [101], [104], [106], [108], [119], [129], [130], [141], [143].
Overlap of [3] bababba=aababbb with [11] abbaab=aabbba:
Critical pair: babaabbba=aababbbab.
Referenced by [50], [57], [59].
Overlap of [14] bbaab=abbba with [7] baabababb=1:
Critical pair: bbaa=abbbaaabababb.
Reduce RHS:
| [1] | abbb(aaa)bababb |
| ⇒ abbbbababb |
Flip LHS and RHS.
Referenced by [29], [44], [120].
Overlap of [14] bbaab=abbba with [12] aabbaa=bbbbababb:
Critical pair: bbbbbbababb=abbbabaa.
Flip LHS and RHS.
Referenced by [64].
Overlap of [1] aaa=1 with [10] aababbbbbba=abaab:
Critical pair: aabaab=babbbbbba.
Referenced by [29], [31], [32], [38], [61], [63].
Overlap of [1] aaa=1 with [10] aababbbbbba=abaab:
Critical pair: aaabaab=ababbbbbba.
Reduce LHS:
| [1] | (aaa)baab |
| ⇒ baab |
Flip LHS and RHS.
Referenced by [21], [22], [23], [24], [81], [92], [93], [125], [127].
Overlap of [10] aababbbbbba=abaab with [14] bbaab=abbba:
Critical pair: aababbbbabbba=abaabab.
Reduce LHS:
| [5] | (aababbbbabbb)a |
| ⇒ bababaa |
Referenced by [25], [30], [32], [46], [49], [50], [51], [58], [62], [66].
Overlap of [19] ababbbbbba=baab with [1] aaa=1:
Critical pair: ababbbbbb=baabaa.
Flip LHS and RHS.
Referenced by [30], [31], [32].
Overlap of [19] ababbbbbba=baab with [2] bababbb=a:
Critical pair: ababbbbba=baabbabbb.
Flip LHS and RHS.
Referenced by [45], [57], [58], [82], [87], [99], [104], [109].
Overlap of [19] ababbbbbba=baab with [3] bababba=aababbb:
Critical pair: ababbbbbaababbb=baabbabba.
Reduce LHS:
| [14] | ababbb(bbaab)abbb |
| [6] | ⇒ ababb(babbbaa)bbb |
| [2] | ⇒ ababba(bababbb)bb |
| [14] | ⇒ aba(bbaab)b |
| ⇒ abaabbbab |
Flip LHS and RHS.
Referenced by [54].
Overlap of [19] ababbbbbba=baab with [14] bbaab=abbba:
Critical pair: ababbbbabbba=baabab.
Overlap of [20] bababaa=abaabab with [1] aaa=1:
Critical pair: babab=abaababa.
Flip LHS and RHS.
Overlap of [1] aaa=1 with [25] abaababa=babab:
Critical pair: aababab=baababa.
Flip LHS and RHS.
Referenced by [28], [32], [118].
Overlap of [14] bbaab=abbba with [25] abaababa=babab:
Critical pair: bbababab=abbbaaababa.
Reduce RHS:
| [1] | abbb(aaa)baba |
| ⇒ abbbbaba |
Referenced by [33], [34], [39], [47], [56], [61], [80].
Overlap of [26] baababa=aababab with [12] aabbaa=bbbbababb:
Critical pair: baababbbbbababb=aababababbaa.
Reduce RHS:
| [3] | aaba(bababba)a |
| [1] | ⇒ aab(aaa)babbba |
| ⇒ aabbabbba |
Referenced by [68].
Overlap of [18] aabaab=babbbbbba with [16] abbbbababb=bbaa:
Critical pair: aababbaa=babbbbbbabbbababb.
Referenced by [30].
Overlap of [20] bababaa=abaabab with [21] baabaa=ababbbbbb:
Critical pair: babaababbbbbb=abaababbaa.
Reduce RHS:
| [29] | ab(aababbaa) |
| ⇒ abbabbbbbbabbbababb |
Flip LHS and RHS.
Referenced by [35].
Overlap of [21] baabaa=ababbbbbb with [18] aabaab=babbbbbba:
Critical pair: bbabbbbbba=ababbbbbbb.
Referenced by [35], [51], [62], [78], [84], [85], [86], [87], [88], [89], [97], [100], [107], [128], [131], [144].
Overlap of [26] baababa=aababab with [21] baabaa=ababbbbbb:
Critical pair: baabaababbbbbb=aababababaa.
Reduce LHS:
| [21] | (baabaa)babbbbbb |
| ⇒ ababbbbbbbabbbbbb |
Reduce RHS:
| [20] | aaba(bababaa) |
| [18] | ⇒ (aabaab)aabab |
| [1] | ⇒ babbbbbb(aaa)bab |
| ⇒ babbbbbbbab |
Overlap of [14] bbaab=abbba with [27] bbababab=abbbbaba:
Critical pair: bbaaabbbbaba=abbbabababab.
Reduce LHS:
| [1] | bb(aaa)bbbbaba |
| ⇒ bbbbbbaba |
Reduce RHS:
| [27] | ab(bbababab)ab |
| ⇒ ababbbbabaab |
Flip LHS and RHS.
Referenced by [69].
Overlap of [27] bbababab=abbbbaba with [3] bababba=aababbb:
Critical pair: bbaaababbb=abbbbababa.
Reduce LHS:
| [1] | bb(aaa)babbb |
| ⇒ bbbabbb |
Flip LHS and RHS.
Referenced by [36], [37], [38], [57].
Overlap of [30] abbabbbbbbabbbababb=babaababbbbbb with [31] bbabbbbbba=ababbbbbbb:
Critical pair: aababbbbbbbbbbababb=babaababbbbbb.
Referenced by [70].
Overlap of [1] aaa=1 with [34] abbbbababa=bbbabbb:
Critical pair: aabbbabbb=bbbbababa.
Flip LHS and RHS.
Referenced by [46], [47], [48], [57], [89], [108], [129].
Overlap of [2] bababbb=a with [34] abbbbababa=bbbabbb:
Critical pair: babbbbabbb=abababa.
Flip LHS and RHS.
Referenced by [39], [40], [41], [42], [95], [117].
Overlap of [18] aabaab=babbbbbba with [34] abbbbababa=bbbabbb:
Critical pair: aababbbabbb=babbbbbbabbbababa.
Flip LHS and RHS.
Referenced by [71].
Overlap of [27] bbababab=abbbbaba with [37] abababa=babbbbabbb:
Critical pair: bbbabbbbabbb=abbbbabaa.
Flip LHS and RHS.
Overlap of [37] abababa=babbbbabbb with [2] bababbb=a:
Critical pair: abaa=babbbbabbbbbb.
Referenced by [43], [44], [45], [46], [48], [49], [50], [51], [53], [54], [58], [59], [62], [64], [66], [67], [70], [73], [80], [83], [84], [92], [99], [106], [111], [112], [117], [119], [121], [125], [195], [207].
Overlap of [37] abababa=babbbbabbb with [3] bababba=aababbb:
Critical pair: abaaababbb=babbbbabbbbba.
Reduce LHS:
| [1] | ab(aaa)babbb |
| ⇒ abbabbb |
Flip LHS and RHS.
Referenced by [110], [111], [112], [113], [114], [115], [132].
Overlap of [37] abababa=babbbbabbb with [37] abababa=babbbbabbb:
Critical pair: abbabbbbabbb=babbbbabbbba.
Flip LHS and RHS.
Referenced by [106], [117], [134], [150].
Overlap of [40] abaa=babbbbabbbbbb with [12] aabbaa=bbbbababb:
Critical pair: abbbbbababb=babbbbabbbbbbbbaa.
Flip LHS and RHS.
Referenced by [57].
Overlap of [40] abaa=babbbbabbbbbb with [16] abbbbababb=bbaa:
Critical pair: ababbaa=babbbbabbbbbbbbbbababb.
Flip LHS and RHS.
Referenced by [151].
Overlap of [40] abaa=babbbbabbbbbb with [22] baabbabbb=ababbbbba:
Critical pair: aababbbbba=babbbbabbbbbbbbabbb.
Referenced by [65], [68], [113], [153].
Overlap of [36] bbbbababa=aabbbabbb with [20] bababaa=abaabab:
Critical pair: bbbabaabab=aabbbabbba.
Reduce LHS:
| [40] | bbb(abaa)bab |
| ⇒ bbbbabbbbabbbbbbbab |
Flip LHS and RHS.
Overlap of [36] bbbbababa=aabbbabbb with [27] bbababab=abbbbaba:
Critical pair: bbabbbbaba=aabbbabbbb.
Referenced by [116].
Overlap of [36] bbbbababa=aabbbabbb with [40] abaa=babbbbabbbbbb:
Critical pair: bbbbabbabbbbabbbbbb=aabbbabbba.
Reduce RHS:
| [46] | (aabbbabbba) |
| ⇒ bbbbabbbbabbbbbbbab |
Flip LHS and RHS.
Overlap of [5] aababbbbabbb=bababa with [2] bababbb=a:
Critical pair: aababbbbabba=bababaababbb.
Reduce RHS:
| [20] | (bababaa)babbb |
| [40] | ⇒ (abaa)babbabbb |
| ⇒ babbbbabbbbbbbabbabbb |
Referenced by [51].
Overlap of [5] aababbbbabbb=bababa with [3] bababba=aababbb:
Critical pair: aababbbbabbaababbb=bababaababba.
Reduce LHS:
| [14] | aababbbba(bbaab)abbb |
| [14] | ⇒ aababb(bbaab)bbaabbb |
| [13] | ⇒ aabab(babbbabbaa)bbb |
| [15] | ⇒ aa(babaabbba)babbbbb |
| [1] | ⇒ (aaa)ababbbabbabbbbb |
| ⇒ ababbbabbabbbbb |
Reduce RHS:
| [20] | (bababaa)babba |
| [40] | ⇒ (abaa)babbabba |
| ⇒ babbbbabbbbbbbabbabba |
Flip LHS and RHS.
Referenced by [51].
Overlap of [5] aababbbbabbb=bababa with [20] bababaa=abaabab:
Critical pair: aababbbbabbabaabab=bababaababaa.
Reduce LHS:
| [49] | (aababbbbabba)baabab |
| [14] | ⇒ babbbbabbbbbbbabbabb(bbaab)ab |
| [50] | ⇒ (babbbbabbbbbbbabbabba)bbbaab |
| [14] | ⇒ ababbbabbabbbbbb(bbaab) |
| [31] | ⇒ ababbba(bbabbbbbba)bbba |
| [6] | ⇒ a(babbbaa)babbbbbbbbbba |
| [2] | ⇒ aa(bababbb)abbbbbbbbbba |
| [1] | ⇒ (aaa)abbbbbbbbbba |
| ⇒ abbbbbbbbbba |
Reduce RHS:
| [20] | (bababaa)babaa |
| [40] | ⇒ (abaa)babbabaa |
| [40] | ⇒ babbbbabbbbbbbabb(abaa) |
| ⇒ babbbbabbbbbbbabbbabbbbabbbbbb |
Flip LHS and RHS.
Referenced by [75].
Overlap of [14] bbaab=abbba with [5] aababbbbabbb=bababa:
Critical pair: bbbababa=abbbaabbbbabbb.
Reduce RHS:
| [14] | ab(bbaab)bbbabbb |
| ⇒ ababbbabbbabbb |
Flip LHS and RHS.
Overlap of [40] abaa=babbbbabbbbbb with [5] aababbbbabbb=bababa:
Critical pair: abbababa=babbbbabbbbbbbabbbbabbb.
Flip LHS and RHS.
Referenced by [76].
Simplify [23] baabbabba=abaabbbab.
Reduce RHS:
| [40] | (abaa)bbbab |
| ⇒ babbbbabbbbbbbbbab |
Referenced by [55], [56], [57], [58], [82], [99], [112], [147].
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [14] bbaab=abbba:
Critical pair: baabbaabbba=babbbbabbbbbbbbbabab.
Reduce LHS:
| [14] | baa(bbaab)bba |
| [1] | ⇒ b(aaa)bbbabba |
| ⇒ bbbbabba |
Flip LHS and RHS.
Referenced by [65], [86], [92].
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [27] bbababab=abbbbaba:
Critical pair: baabbaabbbbaba=babbbbabbbbbbbbbabbabab.
Reduce LHS:
| [14] | baa(bbaab)bbbaba |
| [1] | ⇒ b(aaa)bbbabbbaba |
| ⇒ bbbbabbbaba |
Flip LHS and RHS.
Referenced by [154].
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [34] abbbbababa=bbbabbb:
Critical pair: baabbabbbbbabbb=babbbbabbbbbbbbbabbbbbababa.
Reduce LHS:
| [22] | (baabbabbb)bbabbb |
| ⇒ ababbbbbabbabbb |
Reduce RHS:
| [36] | babbbbabbbbbbbbbab(bbbbababa) |
| [15] | ⇒ babbbbabbbbbbbb(babaabbba)bbb |
| [43] | ⇒ (babbbbabbbbbbbbaa)babbbabbbb |
| [2] | ⇒ abbbb(bababbb)abbbabbbb |
| [14] | ⇒ abb(bbaab)bbabbbb |
| ⇒ abbabbbabbabbbb |
Flip LHS and RHS.
Referenced by [156].
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [40] abaa=babbbbabbbbbb:
Critical pair: baabbabbbabbbbabbbbbb=babbbbabbbbbbbbbabbaa.
Reduce LHS:
| [22] | (baabbabbb)abbbbabbbbbb |
| [14] | ⇒ ababbb(bbaab)bbbabbbbbb |
| [52] | ⇒ (ababbbabbbabbb)abbbbbb |
| [20] | ⇒ bb(bababaa)bbbbbb |
| [40] | ⇒ bb(abaa)babbbbbbb |
| ⇒ bbbabbbbabbbbbbbabbbbbbb |
Flip LHS and RHS.
Referenced by [61].
Simplify [15] babaabbba=aababbbab.
Reduce LHS:
| [40] | b(abaa)bbba |
| ⇒ bbabbbbabbbbbbbbba |
Flip LHS and RHS.
Referenced by [60], [61], [62], [63], [71], [86], [92], [119], [146].
Overlap of [1] aaa=1 with [59] aababbbab=bbabbbbabbbbbbbbba:
Critical pair: abbabbbbabbbbbbbbba=babbbab.
Referenced by [76].
Overlap of [59] aababbbab=bbabbbbabbbbbbbbba with [6] babbbaa=abababb:
Critical pair: aababbabababb=bbabbbbabbbbbbbbbabbaa.
Reduce LHS:
| [27] | aaba(bbababab)b |
| [18] | ⇒ (aabaab)bbbabab |
| ⇒ babbbbbbabbbabab |
Reduce RHS:
| [58] | b(babbbbabbbbbbbbbabbaa) |
| [48] | ⇒ (bbbbabbbbabbbbbbbab)bbbbbb |
| ⇒ bbbbabbabbbbabbbbbbbbbbbb |
Referenced by [72].
Overlap of [59] aababbbab=bbabbbbabbbbbbbbba with [20] bababaa=abaabab:
Critical pair: aababbabaabab=bbabbbbabbbbbbbbbaabaa.
Reduce LHS:
| [40] | aababb(abaa)bab |
| [59] | ⇒ (aababbbab)bbbabbbbbbbab |
| ⇒ bbabbbbabbbbbbbbbabbbabbbbbbbab |
Reduce RHS:
| [14] | bbabbbbabbbbbbb(bbaab)aa |
| [6] | ⇒ bbabbbbabbbbbb(babbbaa)a |
| [31] | ⇒ bbabb(bbabbbbbba)bababba |
| [2] | ⇒ bbab(bababbb)bbbbbababba |
| [2] | ⇒ b(bababbb)bbababba |
| [3] | ⇒ bab(bababba) |
| [40] | ⇒ b(abaa)babbb |
| ⇒ bbabbbbabbbbbbbabbb |
Referenced by [77].
Overlap of [18] aabaab=babbbbbba with [59] aababbbab=bbabbbbabbbbbbbbba:
Critical pair: aabbbabbbbabbbbbbbbba=babbbbbbaabbbab.
Reduce RHS:
| [14] | babbbb(bbaab)bbab |
| ⇒ babbbbabbbabbab |
Referenced by [158].
Simplify [17] abbbabaa=bbbbbbababb.
Reduce LHS:
| [40] | abbb(abaa) |
| ⇒ abbbbabbbbabbbbbb |
Referenced by [65], [88], [96], [142].
Overlap of [24] ababbbbabbba=baabab with [64] abbbbabbbbabbbbbb=bbbbbbababb:
Critical pair: ababbbbabbbbbbbbbababb=baababbbbbabbbbabbbbbb.
Reduce LHS:
| [55] | a(babbbbabbbbbbbbbabab)b |
| ⇒ abbbbabbab |
Reduce RHS:
| [45] | b(aababbbbba)bbbbabbbbbb |
| ⇒ bbabbbbabbbbbbbbabbbbbbbabbbbbb |
Flip LHS and RHS.
Referenced by [160].
Simplify [20] bababaa=abaabab.
Reduce RHS:
| [40] | (abaa)bab |
| ⇒ babbbbabbbbbbbab |
Referenced by [67].
Overlap of [66] bababaa=babbbbabbbbbbbab with [40] abaa=babbbbabbbbbb:
Critical pair: babbabbbbabbbbbb=babbbbabbbbbbbab.
Flip LHS and RHS.
Referenced by [70], [75], [76], [77], [84], [99], [119].
Overlap of [28] baababbbbbababb=aabbabbba with [45] aababbbbba=babbbbabbbbbbbbabbb:
Critical pair: bbabbbbabbbbbbbbabbbbabb=aabbabbba.
Referenced by [75].
Overlap of [33] ababbbbabaab=bbbbbbaba with [39] abbbbabaa=bbbabbbbabbb:
Critical pair: abbbbabbbbabbbb=bbbbbbaba.
Referenced by [137].
Simplify [35] aababbbbbbbbbbababb=babaababbbbbb.
Reduce RHS:
| [40] | b(abaa)babbbbbb |
| [67] | ⇒ b(babbbbabbbbbbbab)bbbbb |
| ⇒ bbabbabbbbabbbbbbbbbbb |
Referenced by [148].
Simplify [38] babbbbbbabbbababa=aababbbabbb.
Reduce RHS:
| [59] | (aababbbab)bb |
| ⇒ bbabbbbabbbbbbbbbabb |
Referenced by [72].
Overlap of [71] babbbbbbabbbababa=bbabbbbabbbbbbbbbabb with [61] babbbbbbabbbabab=bbbbabbabbbbabbbbbbbbbbbb:
Critical pair: bbbbabbabbbbabbbbbbbbbbbba=bbabbbbabbbbbbbbbabb.
Referenced by [161].
Overlap of [39] abbbbabaa=bbbabbbbabbb with [40] abaa=babbbbabbbbbb:
Critical pair: abbbbbabbbbabbbbbb=bbbabbbbabbb.
Simplify [46] aabbbabbba=bbbbabbbbabbbbbbbab.
Reduce RHS:
| [48] | (bbbbabbbbabbbbbbbab) |
| ⇒ bbbbabbabbbbabbbbbb |
Referenced by [93].
Overlap of [51] babbbbabbbbbbbabbbabbbbabbbbbb=abbbbbbbbbba with [67] babbbbabbbbbbbab=babbabbbbabbbbbb:
Critical pair: babbabbbbabbbbbbbbabbbbabbbbbb=abbbbbbbbbba.
Reduce LHS:
| [68] | ba(bbabbbbabbbbbbbbabbbbabb)bbbb |
| [1] | ⇒ b(aaa)bbabbbabbbb |
| ⇒ bbbabbbabbbb |
Referenced by [78], [81], [84], [89], [98], [99], [100], [108], [113], [115], [119], [122], [124], [128], [134], [136].
Overlap of [53] babbbbabbbbbbbabbbbabbb=abbababa with [67] babbbbabbbbbbbab=babbabbbbabbbbbb:
Critical pair: babbabbbbabbbbbbbbbabbb=abbababa.
Reduce LHS:
| [60] | b(abbabbbbabbbbbbbbba)bbb |
| ⇒ bbabbbabbbb |
Flip LHS and RHS.
Referenced by [79], [80], [81], [82], [83], [89], [108], [134].
Simplify [62] bbabbbbabbbbbbbbbabbbabbbbbbbab=bbabbbbabbbbbbbabbb.
Reduce RHS:
| [67] | b(babbbbabbbbbbbab)bb |
| ⇒ bbabbabbbbabbbbbbbb |
Referenced by [78].
Overlap of [77] bbabbbbabbbbbbbbbabbbabbbbbbbab=bbabbabbbbabbbbbbbb with [75] bbbabbbabbbb=abbbbbbbbbba:
Critical pair: bbabbbbabbbbbbabbbbbbbbbbabbbab=bbabbabbbbabbbbbbbb.
Reduce LHS:
| [31] | bbabb(bbabbbbbba)bbbbbbbbbbabbbab |
| [2] | ⇒ bbab(bababbb)bbbbbbbbbbbbbbabbbab |
| [2] | ⇒ b(bababbb)bbbbbbbbbbbabbbab |
| ⇒ babbbbbbbbbbbabbbab |
Flip LHS and RHS.
Referenced by [84], [99], [119], [148], [162], [163].
Overlap of [1] aaa=1 with [76] abbababa=bbabbbabbbb:
Critical pair: aabbabbbabbbb=bbababa.
Referenced by [123].
Overlap of [14] bbaab=abbba with [76] abbababa=bbabbbabbbb:
Critical pair: bbabbabbbabbbb=abbbabababa.
Reduce RHS:
| [27] | ab(bbababab)a |
| [40] | ⇒ ababbbb(abaa) |
| [73] | ⇒ ab(abbbbbabbbbabbbbbb) |
| ⇒ abbbbabbbbabbb |
Referenced by [137].
Overlap of [19] ababbbbbba=baab with [76] abbababa=bbabbbabbbb:
Critical pair: ababbbbbbbbabbbabbbb=baabbbababa.
Reduce LHS:
| [75] | ababbbbb(bbbabbbabbbb) |
| ⇒ ababbbbbabbbbbbbbbba |
Flip LHS and RHS.
Referenced by [165].
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [76] abbababa=bbabbbabbbb:
Critical pair: baabbabbbbabbbabbbb=babbbbabbbbbbbbbabbbababa.
Reduce LHS:
| [22] | (baabbabbb)babbbabbbb |
| [2] | ⇒ ababbbb(bababbb)abbbb |
| [14] | ⇒ ababb(bbaab)bbb |
| ⇒ ababbabbbabbb |
Flip LHS and RHS.
Referenced by [167].
Overlap of [76] abbababa=bbabbbabbbb with [40] abaa=babbbbabbbbbb:
Critical pair: abbabbabbbbabbbbbb=bbabbbabbbba.
Referenced by [169].
Overlap of [3] bababba=aababbb with [31] bbabbbbbba=ababbbbbbb:
Critical pair: babaababbbbbbb=aababbbbbbbbba.
Reduce LHS:
| [40] | b(abaa)babbbbbbb |
| [67] | ⇒ b(babbbbabbbbbbbab)bbbbbb |
| [78] | ⇒ (bbabbabbbbabbbbbbbb)bbbb |
| [75] | ⇒ babbbbbbbb(bbbabbbabbbb)b |
| ⇒ babbbbbbbbabbbbbbbbbbab |
Flip LHS and RHS.
Referenced by [170].
Overlap of [14] bbaab=abbba with [31] bbabbbbbba=ababbbbbbb:
Critical pair: bbaaababbbbbbb=abbbababbbbbba.
Reduce LHS:
| [1] | bb(aaa)babbbbbbb |
| ⇒ bbbabbbbbbb |
Reduce RHS:
| [2] | abb(bababbb)bbba |
| ⇒ abbabbba |
Flip LHS and RHS.
Defines rule #29.
Referenced by [90], [91], [92], [93], [94], [95], [96], [97], [99], [104], [114], [123], [136], [137], [157], [159], [167], [182], [199], [229], [262].
Overlap of [59] aababbbab=bbabbbbabbbbbbbbba with [31] bbabbbbbba=ababbbbbbb:
Critical pair: aababbbaababbbbbbb=bbabbbbabbbbbbbbbababbbbbba.
Reduce LHS:
| [6] | aa(babbbaa)babbbbbbb |
| [1] | ⇒ (aaa)bababbbabbbbbbb |
| [2] | ⇒ (bababbb)abbbbbbb |
| ⇒ aabbbbbbb |
Reduce RHS:
| [55] | b(babbbbabbbbbbbbbabab)bbbbba |
| ⇒ bbbbbabbabbbbba |
Flip LHS and RHS.
Referenced by [233], [234], [235].
Overlap of [22] baabbabbb=ababbbbba with [31] bbabbbbbba=ababbbbbbb:
Critical pair: baaababbbbbbb=ababbbbbabbba.
Reduce LHS:
| [1] | b(aaa)babbbbbbb |
| ⇒ bbabbbbbbb |
Flip LHS and RHS.
Referenced by [127].
Overlap of [31] bbabbbbbba=ababbbbbbb with [64] abbbbabbbbabbbbbb=bbbbbbababb:
Critical pair: bbabbbbbbbbbbbbababb=ababbbbbbbbbbbabbbbabbbbbb.
Flip LHS and RHS.
Referenced by [171].
Overlap of [31] bbabbbbbba=ababbbbbbb with [76] abbababa=bbabbbabbbb:
Critical pair: bbabbbbbbbbabbbabbbb=ababbbbbbbbbababa.
Reduce LHS:
| [75] | bbabbbbb(bbbabbbabbbb) |
| ⇒ bbabbbbbabbbbbbbbbba |
Reduce RHS:
| [36] | ababbbbb(bbbbababa) |
| [14] | ⇒ ababbb(bbaab)bbabbb |
| ⇒ ababbbabbbabbabbb |
Flip LHS and RHS.
Referenced by [173].
Overlap of [1] aaa=1 with [85] abbabbba=bbbabbbbbbb:
Critical pair: aabbbabbbbbbb=bbabbba.
Referenced by [102].
Overlap of [14] bbaab=abbba with [85] abbabbba=bbbabbbbbbb:
Critical pair: bbabbbabbbbbbb=abbbababbba.
Reduce RHS:
| [2] | abb(bababbb)a |
| ⇒ abbaa |
Flip LHS and RHS.
Referenced by [98], [99], [100], [101], [136], [151], [159].
Overlap of [59] aababbbab=bbabbbbabbbbbbbbba with [85] abbabbba=bbbabbbbbbb:
Critical pair: aababbbbbbabbbbbbb=bbabbbbabbbbbbbbbababbba.
Reduce LHS:
| [19] | a(ababbbbbba)bbbbbbb |
| [40] | ⇒ (abaa)bbbbbbbb |
| ⇒ babbbbabbbbbbbbbbbbbb |
Reduce RHS:
| [55] | b(babbbbabbbbbbbbbabab)bba |
| ⇒ bbbbbabbabba |
Flip LHS and RHS.
Overlap of [19] ababbbbbba=baab with [85] abbabbba=bbbabbbbbbb:
Critical pair: ababbbbbbbbbabbbbbbb=baabbbabbba.
Reduce RHS:
| [74] | b(aabbbabbba) |
| ⇒ bbbbbabbabbbbabbbbbb |
Flip LHS and RHS.
Referenced by [160].
Overlap of [85] abbabbba=bbbabbbbbbb with [2] bababbb=a:
Critical pair: abbabba=bbbabbbbbbbbabbb.
Defines rule #28.
Referenced by [113], [147], [174], [187], [199], [207], [208], [231], [234].
Overlap of [85] abbabbba=bbbabbbbbbb with [6] babbbaa=abababb:
Critical pair: ababababb=bbbabbbbbbba.
Reduce LHS:
| [37] | (abababa)bb |
| ⇒ babbbbabbbbb |
Flip LHS and RHS.
Referenced by [149], [168], [187], [199], [209], [210], [226].
Overlap of [85] abbabbba=bbbabbbbbbb with [64] abbbbabbbbabbbbbb=bbbbbbababb:
Critical pair: abbabbbbbbbbbababb=bbbabbbbbbbbbbbabbbbabbbbbb.
Referenced by [175].
Overlap of [85] abbabbba=bbbabbbbbbb with [85] abbabbba=bbbabbbbbbb:
Critical pair: abbabbbbbbabbbbbbb=bbbabbbbbbbbbabbba.
Reduce LHS:
| [31] | a(bbabbbbbba)bbbbbbb |
| ⇒ aababbbbbbbbbbbbbb |
Flip LHS and RHS.
Overlap of [3] bababba=aababbb with [91] abbaa=bbabbbabbbbbbb:
Critical pair: babbbabbbabbbbbbb=aababbba.
Reduce LHS:
| [75] | ba(bbbabbbabbbb)bbb |
| ⇒ baabbbbbbbbbbabbb |
Flip LHS and RHS.
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [91] abbaa=bbabbbabbbbbbb:
Critical pair: baabbabbbbabbbabbbbbbb=babbbbabbbbbbbbbabbbaa.
Reduce LHS:
| [22] | (baabbabbb)babbbabbbbbbb |
| [2] | ⇒ ababbbb(bababbb)abbbbbbb |
| [14] | ⇒ ababb(bbaab)bbbbbb |
| [85] | ⇒ ab(abbabbba)bbbbbb |
| ⇒ abbbbabbbbbbbbbbbbb |
Reduce RHS:
| [97] | bab(bbbabbbbbbbbbabbba)a |
| [40] | ⇒ b(abaa)babbbbbbbbbbbbbba |
| [67] | ⇒ b(babbbbabbbbbbbab)bbbbbbbbbbbbba |
| [78] | ⇒ (bbabbabbbbabbbbbbbb)bbbbbbbbbbba |
| [75] | ⇒ babbbbbbbb(bbbabbbabbbb)bbbbbbbba |
| ⇒ babbbbbbbbabbbbbbbbbbabbbbbbbba |
Flip LHS and RHS.
Referenced by [177].
Overlap of [31] bbabbbbbba=ababbbbbbb with [91] abbaa=bbabbbabbbbbbb:
Critical pair: bbabbbbbbbbabbbabbbbbbb=ababbbbbbbbbaa.
Reduce LHS:
| [75] | bbabbbbb(bbbabbbabbbb)bbb |
| ⇒ bbabbbbbabbbbbbbbbbabbb |
Flip LHS and RHS.
Referenced by [178].
Overlap of [91] abbaa=bbabbbabbbbbbb with [14] bbaab=abbba:
Critical pair: aabbba=bbabbbabbbbbbbb.
Defines rule #18.
Referenced by [102], [115], [116], [122], [124], [166], [173], [199], [206], [250], [257], [269].
Simplify [90] aabbbabbbbbbb=bbabbba.
Reduce LHS:
| [101] | (aabbba)bbbbbbb |
| ⇒ bbabbbabbbbbbbbbbbbbbb |
Referenced by [103], [104], [105], [106], [107], [108], [109], [115], [122], [135], [159].
Overlap of [5] aababbbbabbb=bababa with [102] bbabbbabbbbbbbbbbbbbbb=bbabbba:
Critical pair: aababbbbabbbbabbba=bababababbbabbbbbbbbbbbbbbb.
Reduce LHS:
| [5] | (aababbbbabbb)babbba |
| [2] | ⇒ baba(bababbb)a |
| [1] | ⇒ bab(aaa) |
| ⇒ bab |
Reduce RHS:
| [2] | baba(bababbb)abbbbbbbbbbbbbbb |
| [1] | ⇒ bab(aaa)bbbbbbbbbbbbbbb |
| ⇒ babbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [104], [125], [126], [127], [128], [131], [136], [137], [142], [144], [149], [152], [156], [160], [166], [168], [175].
Overlap of [22] baabbabbb=ababbbbba with [102] bbabbbabbbbbbbbbbbbbbb=bbabbba:
Critical pair: baabbabbbbabbba=ababbbbbababbbabbbbbbbbbbbbbbb.
Reduce LHS:
| [22] | (baabbabbb)babbba |
| [2] | ⇒ ababbbb(bababbb)a |
| ⇒ ababbbbaa |
Reduce RHS:
| [2] | ababbbb(bababbb)abbbbbbbbbbbbbbb |
| [14] | ⇒ ababb(bbaab)bbbbbbbbbbbbbb |
| [85] | ⇒ ab(abbabbba)bbbbbbbbbbbbbb |
| [103] | ⇒ abbb(babbbbbbbbbbbbbbbb)bbbbb |
| ⇒ abbbbabbbbbb |
Referenced by [180].
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [2] bababbb=a:
Critical pair: bbabbbabbbbbbbbbbbbbba=bbabbbaababbb.
Reduce RHS:
| [6] | b(babbbaa)babbb |
| [2] | ⇒ ba(bababbb)abbb |
| [1] | ⇒ b(aaa)bbb |
| ⇒ bbbb |
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [14] bbaab=abbba:
Critical pair: bbabbbabbbbbbbbbbbbbbabbba=bbabbbabaab.
Reduce LHS:
| [105] | (bbabbbabbbbbbbbbbbbbba)bbba |
| ⇒ bbbbbbba |
Reduce RHS:
| [40] | bbabbb(abaa)b |
| [42] | ⇒ b(babbbbabbbba)bbbbbbb |
| ⇒ babbabbbbabbbbbbbbbb |
Flip LHS and RHS.
Referenced by [117].
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [31] bbabbbbbba=ababbbbbbb:
Critical pair: bbabbbabbbbbbbbbbbbbababbbbbbb=bbabbbaabbbbbba.
Reduce LHS:
| [2] | bbabbbabbbbbbbbbbbb(bababbb)bbbb |
| ⇒ bbabbbabbbbbbbbbbbbabbbb |
Reduce RHS:
| [6] | b(babbbaa)bbbbbba |
| [2] | ⇒ ba(bababbb)bbbbba |
| ⇒ baabbbbba |
Referenced by [181].
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [36] bbbbababa=aabbbabbb:
Critical pair: bbabbbabbbbbbbbbbbbbaabbbabbb=bbabbbabbababa.
Reduce LHS:
| [14] | bbabbbabbbbbbbbbbb(bbaab)bbabbb |
| ⇒ bbabbbabbbbbbbbbbbabbbabbabbb |
Reduce RHS:
| [76] | bbabbb(abbababa) |
| [75] | ⇒ bbabb(bbbabbbabbbb) |
| ⇒ bbabbabbbbbbbbbba |
Referenced by [182].
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [102] bbabbbabbbbbbbbbbbbbbb=bbabbba:
Critical pair: bbabbbabbbbbbbbbbbbbbbabbba=bbabbbaabbbabbbbbbbbbbbbbbb.
Reduce LHS:
| [102] | (bbabbbabbbbbbbbbbbbbbb)abbba |
| [6] | ⇒ b(babbbaa)bbba |
| [2] | ⇒ ba(bababbb)bba |
| ⇒ baabba |
Reduce RHS:
| [6] | b(babbbaa)bbbabbbbbbbbbbbbbbb |
| [2] | ⇒ ba(bababbb)bbabbbbbbbbbbbbbbb |
| [22] | ⇒ (baabbabbb)bbbbbbbbbbbb |
| ⇒ ababbbbbabbbbbbbbbbbb |
Overlap of [2] bababbb=a with [41] babbbbabbbbba=abbabbb:
Critical pair: baabbabbb=ababbbbba.
Reduce LHS:
| [109] | (baabba)bbb |
| ⇒ ababbbbbabbbbbbbbbbbbbbb |
Referenced by [122].
Overlap of [5] aababbbbabbb=bababa with [41] babbbbabbbbba=abbabbb:
Critical pair: aababbbabbabbb=bababababbbbba.
Reduce LHS:
| [98] | (aababbba)bbabbb |
| ⇒ baabbbbbbbbbbabbbbbabbb |
Reduce RHS:
| [2] | baba(bababbb)bba |
| [40] | ⇒ b(abaa)bba |
| ⇒ bbabbbbabbbbbbbba |
Referenced by [183].
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [41] babbbbabbbbba=abbabbb:
Critical pair: baabbababbabbb=babbbbabbbbbbbbbabbbbbabbbbba.
Reduce LHS:
| [3] | baab(bababba)bbb |
| [40] | ⇒ ba(abaa)babbbbbb |
| [2] | ⇒ (bababbb)babbbbbbbabbbbbb |
| [32] | ⇒ (ababbbbbbbabbbbbb) |
| ⇒ babbbbbbbab |
Flip LHS and RHS.
Referenced by [184].
Overlap of [24] ababbbbabbba=baabab with [41] babbbbabbbbba=abbabbb:
Critical pair: ababbbbabbabbabbb=baababbbbbabbbbba.
Reduce LHS:
| [94] | ababbbb(abbabba)bbb |
| [32] | ⇒ (ababbbbbbbabbbbbb)bbabbbbbb |
| [75] | ⇒ babbbb(bbbabbbabbbb)bb |
| ⇒ babbbbabbbbbbbbbbabb |
Reduce RHS:
| [45] | b(aababbbbba)bbbbba |
| ⇒ bbabbbbabbbbbbbbabbbbbbbba |
Flip LHS and RHS.
Referenced by [185].
Overlap of [41] babbbbabbbbba=abbabbb with [85] abbabbba=bbbabbbbbbb:
Critical pair: babbbbabbbbbbbbabbbbbbb=abbabbbbbabbba.
Flip LHS and RHS.
Referenced by [186].
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [41] babbbbabbbbba=abbabbb:
Critical pair: bbabbbabbbbbbbbbbbbbbabbabbb=bbabbbaabbbbabbbbba.
Reduce LHS:
| [105] | (bbabbbabbbbbbbbbbbbbba)bbabbb |
| ⇒ bbbbbbabbb |
Reduce RHS:
| [6] | b(babbbaa)bbbbabbbbba |
| [2] | ⇒ ba(bababbb)bbbabbbbba |
| [101] | ⇒ b(aabbba)bbbbba |
| [75] | ⇒ (bbbabbbabbbb)bbbbbbbbba |
| ⇒ abbbbbbbbbbabbbbbbbbba |
Flip LHS and RHS.
Simplify [47] bbabbbbaba=aabbbabbbb.
Reduce RHS:
| [101] | (aabbba)bbbb |
| ⇒ bbabbbabbbbbbbbbbbb |
Referenced by [117], [118], [119], [120], [121], [122], [133].
Overlap of [5] aababbbbabbb=bababa with [116] bbabbbbaba=bbabbbabbbbbbbbbbbb:
Critical pair: aababbbbabbbabbbbbbbbbbbb=bababababa.
Reduce LHS:
| [5] | (aababbbbabbb)abbbbbbbbbbbb |
| [40] | ⇒ bab(abaa)bbbbbbbbbbbb |
| [106] | ⇒ (babbabbbbabbbbbbbbbb)bbbbbbbb |
| ⇒ bbbbbbbabbbbbbbb |
Reduce RHS:
| [37] | b(abababa)ba |
| [42] | ⇒ b(babbbbabbbba) |
| ⇒ babbabbbbabbb |
Flip LHS and RHS.
Referenced by [134], [164], [169].
Overlap of [5] aababbbbabbb=bababa with [116] bbabbbbaba=bbabbbabbbbbbbbbbbb:
Critical pair: aababbbbabbbbabbbabbbbbbbbbbbb=bababababbbbaba.
Reduce LHS:
| [5] | (aababbbbabbb)babbbabbbbbbbbbbbb |
| [2] | ⇒ baba(bababbb)abbbbbbbbbbbb |
| [1] | ⇒ bab(aaa)bbbbbbbbbbbb |
| ⇒ babbbbbbbbbbbbb |
Reduce RHS:
| [2] | baba(bababbb)baba |
| [26] | ⇒ ba(baababa) |
| [1] | ⇒ b(aaa)babab |
| ⇒ bbabab |
Flip LHS and RHS.
Referenced by [123], [142], [144], [149], [152], [160], [168], [171], [176].
Overlap of [59] aababbbab=bbabbbbabbbbbbbbba with [116] bbabbbbaba=bbabbbabbbbbbbbbbbb:
Critical pair: aababbbabbbabbbbbbbbbbbb=bbabbbbabbbbbbbbbabbbaba.
Reduce LHS:
| [52] | a(ababbbabbbabbb)bbbbbbbbb |
| [2] | ⇒ abbba(bababbb)bbbbbb |
| [14] | ⇒ ab(bbaab)bbbbb |
| ⇒ ababbbabbbbb |
Reduce RHS:
| [97] | bbab(bbbabbbbbbbbbabbba)ba |
| [40] | ⇒ bb(abaa)babbbbbbbbbbbbbbba |
| [67] | ⇒ bb(babbbbabbbbbbbab)bbbbbbbbbbbbbba |
| [78] | ⇒ b(bbabbabbbbabbbbbbbb)bbbbbbbbbbbba |
| [75] | ⇒ bbabbbbbbbb(bbbabbbabbbb)bbbbbbbbba |
| [115] | ⇒ bbabbbbbbbb(abbbbbbbbbbabbbbbbbbba) |
| ⇒ bbabbbbbbbbbbbbbbabbb |
Referenced by [188].
Overlap of [116] bbabbbbaba=bbabbbabbbbbbbbbbbb with [16] abbbbababb=bbaa:
Critical pair: bbbbaa=bbabbbabbbbbbbbbbbbbb.
Referenced by [188].
Overlap of [116] bbabbbbaba=bbabbbabbbbbbbbbbbb with [40] abaa=babbbbabbbbbb:
Critical pair: bbabbbbbabbbbabbbbbb=bbabbbabbbbbbbbbbbba.
Reduce LHS:
| [73] | bb(abbbbbabbbbabbbbbb) |
| ⇒ bbbbbabbbbabbb |
Flip LHS and RHS.
Overlap of [102] bbabbbabbbbbbbbbbbbbbb=bbabbba with [116] bbabbbbaba=bbabbbabbbbbbbbbbbb:
Critical pair: bbabbbabbbbbbbbbbbbbbbabbbabbbbbbbbbbbb=bbabbbaabbbbaba.
Reduce LHS:
| [102] | (bbabbbabbbbbbbbbbbbbbb)abbbabbbbbbbbbbbb |
| [6] | ⇒ b(babbbaa)bbbabbbbbbbbbbbb |
| [2] | ⇒ ba(bababbb)bbabbbbbbbbbbbb |
| [109] | ⇒ (baabba)bbbbbbbbbbbb |
| [110] | ⇒ (ababbbbbabbbbbbbbbbbbbbb)bbbbbbbbb |
| ⇒ ababbbbbabbbbbbbbb |
Reduce RHS:
| [6] | b(babbbaa)bbbbaba |
| [2] | ⇒ ba(bababbb)bbbaba |
| [101] | ⇒ b(aabbba)ba |
| [75] | ⇒ (bbbabbbabbbb)bbbbba |
| ⇒ abbbbbbbbbbabbbbba |
Flip LHS and RHS.
Referenced by [183].
Simplify [79] aabbabbbabbbb=bbababa.
Reduce LHS:
| [85] | a(abbabbba)bbbb |
| ⇒ abbbabbbbbbbbbbb |
Reduce RHS:
| [118] | (bbabab)a |
| ⇒ babbbbbbbbbbbbba |
Flip LHS and RHS.
Defines rule #7.
Referenced by [124], [125], [126], [127], [128], [129], [130], [131], [132], [133], [134], [135], [136], [137], [145], [187], [194], [199], [202], [203], [205], [212], [233], [235], [240], [244], [247], [250], [254], [257], [260], [262], [263], [269].
Overlap of [2] bababbb=a with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: baabbbabbbbbbbbbbb=abbbbbbbbbba.
Reduce LHS:
| [101] | b(aabbba)bbbbbbbbbbb |
| [75] | ⇒ (bbbabbbabbbb)bbbbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbabbbbbbbbbbbbbbb |
Overlap of [2] bababbb=a with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: bababbabbbabbbbbbbbbbb=aabbbbbbbbbbbbba.
Reduce LHS:
| [3] | (bababba)bbbabbbbbbbbbbb |
| [19] | ⇒ a(ababbbbbba)bbbbbbbbbbb |
| [40] | ⇒ (abaa)bbbbbbbbbbbb |
| [103] | ⇒ babbb(babbbbbbbbbbbbbbbb)bb |
| ⇒ babbbbabbb |
Flip LHS and RHS.
Defines rule #26.
Referenced by [257].
Overlap of [3] bababba=aababbb with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: babababbbabbbbbbbbbbb=aababbbbbbbbbbbbbbbba.
Reduce LHS:
| [2] | ba(bababbb)abbbbbbbbbbb |
| [1] | ⇒ b(aaa)bbbbbbbbbbb |
| ⇒ bbbbbbbbbbbb |
Reduce RHS:
| [103] | aa(babbbbbbbbbbbbbbbb)a |
| ⇒ aababa |
Flip LHS and RHS.
Referenced by [138], [139], [140].
Overlap of [19] ababbbbbba=baab with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: ababbbbbabbbabbbbbbbbbbb=baabbbbbbbbbbbbbba.
Reduce LHS:
| [87] | (ababbbbbabbba)bbbbbbbbbbb |
| [103] | ⇒ b(babbbbbbbbbbbbbbbb)bb |
| ⇒ bbabbb |
Flip LHS and RHS.
Referenced by [189].
Overlap of [31] bbabbbbbba=ababbbbbbb with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: bbabbbbbabbbabbbbbbbbbbb=ababbbbbbbbbbbbbbbbbbbba.
Reduce LHS:
| [75] | bbabb(bbbabbbabbbb)bbbbbbb |
| ⇒ bbabbabbbbbbbbbbabbbbbbb |
Reduce RHS:
| [103] | a(babbbbbbbbbbbbbbbb)bbbba |
| ⇒ ababbbbba |
Referenced by [182].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [3] bababba=aababbb:
Critical pair: babbbbbbbbbbbbaababbb=abbbabbbbbbbbbbbbabba.
Reduce LHS:
| [14] | babbbbbbbbbb(bbaab)abbb |
| [6] | ⇒ babbbbbbbbb(babbbaa)bbb |
| [36] | ⇒ babbbbb(bbbbababa)bbbbb |
| [14] | ⇒ babbb(bbaab)bbabbbbbbbb |
| ⇒ babbbabbbabbabbbbbbbb |
Referenced by [190].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [14] bbaab=abbba:
Critical pair: babbbbbbbbbbbabbba=abbbabbbbbbbbbbbab.
Referenced by [148], [162], [163], [182].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [31] bbabbbbbba=ababbbbbbb:
Critical pair: babbbbbbbbbbbababbbbbbb=abbbabbbbbbbbbbbbbbbbba.
Reduce LHS:
| [2] | babbbbbbbbbb(bababbb)bbbb |
| ⇒ babbbbbbbbbbabbbb |
Reduce RHS:
| [103] | abb(babbbbbbbbbbbbbbbb)ba |
| ⇒ abbbabba |
Flip LHS and RHS.
Defines rule #35.
Referenced by [158], [190], [250].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [41] babbbbabbbbba=abbabbb:
Critical pair: babbbbbbbbbbbbabbabbb=abbbabbbbbbbbbbbbbbbabbbbba.
Flip LHS and RHS.
Referenced by [191].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [116] bbabbbbaba=bbabbbabbbbbbbbbbbb:
Critical pair: babbbbbbbbbbbbbabbbabbbbbbbbbbbb=abbbabbbbbbbbbbbbbbbaba.
Reduce LHS:
| [123] | (babbbbbbbbbbbbba)bbbabbbbbbbbbbbb |
| ⇒ abbbabbbbbbbbbbbbbbabbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [192].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [76] abbababa=bbabbbabbbb:
Critical pair: babbbbbbbbbbbbbbbabbbabbbb=abbbabbbbbbbbbbbbbababa.
Reduce LHS:
| [75] | babbbbbbbbbbbb(bbbabbbabbbb) |
| ⇒ babbbbbbbbbbbbabbbbbbbbbba |
Reduce RHS:
| [123] | abb(babbbbbbbbbbbbba)baba |
| [121] | ⇒ a(bbabbbabbbbbbbbbbbba)ba |
| [42] | ⇒ abbbb(babbbbabbbba) |
| [117] | ⇒ abbb(babbabbbbabbb) |
| ⇒ abbbbbbbbbbabbbbbbbb |
Referenced by [136].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [102] bbabbbabbbbbbbbbbbbbbb=bbabbba:
Critical pair: babbbbbbbbbbbbbabbba=abbbabbbbbbbbbbbbbbabbbbbbbbbbbbbbb.
Reduce LHS:
| [123] | (babbbbbbbbbbbbba)bbba |
| ⇒ abbbabbbbbbbbbbbbbba |
Flip LHS and RHS.
Referenced by [193].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [91] abbaa=bbabbbabbbbbbb:
Critical pair: babbbbbbbbbbbbbbbabbbabbbbbbb=abbbabbbbbbbbbbbbbaa.
Reduce LHS:
| [75] | babbbbbbbbbbbb(bbbabbbabbbb)bbb |
| [134] | ⇒ (babbbbbbbbbbbbabbbbbbbbbba)bbb |
| ⇒ abbbbbbbbbbabbbbbbbbbbb |
Reduce RHS:
| [123] | abb(babbbbbbbbbbbbba)a |
| [85] | ⇒ (abbabbba)bbbbbbbbbbba |
| [103] | ⇒ bb(babbbbbbbbbbbbbbbb)bba |
| ⇒ bbbabbba |
Flip LHS and RHS.
Defines rule #10.
Referenced by [143], [145], [151], [182], [187], [188], [199], [203], [204], [205], [206], [212], [235], [240], [244], [254], [257], [260], [262], [263], [269].
Overlap of [85] abbabbba=bbbabbbbbbb with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: abbabbabbbabbbbbbbbbbb=bbbabbbbbbbbbbbbbbbbbbbba.
Reduce LHS:
| [80] | a(bbabbabbbabbbb)bbbbbbb |
| [69] | ⇒ a(abbbbabbbbabbbb)bbbbbb |
| [2] | ⇒ abbbbb(bababbb)bbb |
| ⇒ abbbbbabbb |
Reduce RHS:
| [103] | bb(babbbbbbbbbbbbbbbb)bbbba |
| ⇒ bbbabbbbba |
Flip LHS and RHS.
Defines rule #11.
Referenced by [155], [197], [198], [206], [209], [210], [227], [234], [238], [257], [260].
Overlap of [1] aaa=1 with [126] aababa=bbbbbbbbbbbb:
Critical pair: abbbbbbbbbbbb=baba.
Flip LHS and RHS.
Referenced by [154], [166], [180], [194], [195], [196], [198], [201], [208].
Overlap of [126] aababa=bbbbbbbbbbbb with [2] bababbb=a:
Critical pair: aaa=bbbbbbbbbbbbbbb.
Reduce LHS:
| [1] | (aaa) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.
Referenced by [141], [142], [143], [144], [145], [155], [170], [173], [179], [182], [183], [185], [187], [188], [190], [191], [192], [193], [196], [199], [201], [203], [204], [205], [206], [209], [212], [213], [214], [215], [216], [217], [223], [227], [228], [229], [230], [233], [234], [235], [236], [237], [239], [240], [241], [243], [244], [246], [247], [248], [249], [250], [251], [253], [254], [255], [257], [258], [259], [260], [262], [263], [264], [265], [266], [267], [268], [269], [270].
Overlap of [126] aababa=bbbbbbbbbbbb with [3] bababba=aababbb:
Critical pair: aaaababbb=bbbbbbbbbbbbbba.
Reduce LHS:
| [1] | (aaa)ababbb |
| ⇒ ababbb |
Referenced by [149], [153], [155], [156], [165], [170], [173], [179], [180], [182], [183], [188], [192].
Overlap of [14] bbaab=abbba with [139] bbbbbbbbbbbbbbb=1:
Critical pair: bbaa=abbbabbbbbbbbbbbbbb.
Referenced by [166], [175], [192], [203], [204], [205], [206].
Overlap of [64] abbbbabbbbabbbbbb=bbbbbbababb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbbbabbbba=bbbbbbababbbbbbbbbbb.
Reduce RHS:
| [118] | bbbb(bbabab)bbbbbbbbbb |
| [103] | ⇒ bbbb(babbbbbbbbbbbbbbbb)bbbbbbb |
| ⇒ bbbbbabbbbbbbb |
Referenced by [150], [234], [243].
Overlap of [139] bbbbbbbbbbbbbbb=1 with [14] bbaab=abbba:
Critical pair: bbbbbbbbbbbbbabbba=aab.
Reduce LHS:
| [136] | bbbbbbbbbb(bbbabbba) |
| ⇒ bbbbbbbbbbabbbbbbbbbbabbbbbbbbbbb |
Referenced by [145].
Overlap of [139] bbbbbbbbbbbbbbb=1 with [31] bbabbbbbba=ababbbbbbb:
Critical pair: bbbbbbbbbbbbbababbbbbbb=abbbbbba.
Reduce LHS:
| [118] | bbbbbbbbbbb(bbabab)bbbbbb |
| [103] | ⇒ bbbbbbbbbbb(babbbbbbbbbbbbbbbb)bbb |
| ⇒ bbbbbbbbbbbbabbbb |
Flip LHS and RHS.
Defines rule #3.
Referenced by [149], [155], [160], [168], [170], [179], [184], [236], [237], [239], [252], [269].
Overlap of [139] bbbbbbbbbbbbbbb=1 with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: bbbbbbbbbbbbbbabbbabbbbbbbbbbb=abbbbbbbbbbbbba.
Reduce LHS:
| [136] | bbbbbbbbbbb(bbbabbba)bbbbbbbbbbb |
| [143] | ⇒ b(bbbbbbbbbbabbbbbbbbbbabbbbbbbbbbb)bbbbbbbbbbb |
| ⇒ baabbbbbbbbbbbb |
Overlap of [59] aababbbab=bbabbbbabbbbbbbbba with [98] aababbba=baabbbbbbbbbbabbb:
Critical pair: baabbbbbbbbbbabbbb=bbabbbbabbbbbbbbba.
Flip LHS and RHS.
Overlap of [54] baabbabba=babbbbabbbbbbbbbab with [94] abbabba=bbbabbbbbbbbabbb:
Critical pair: babbbabbbbbbbbabbb=babbbbabbbbbbbbbab.
Flip LHS and RHS.
Referenced by [152], [155], [168], [172], [184].
Simplify [70] aababbbbbbbbbbababb=bbabbabbbbabbbbbbbbbbb.
Reduce RHS:
| [78] | (bbabbabbbbabbbbbbbb)bbb |
| [130] | ⇒ (babbbbbbbbbbbabbba)bbbb |
| ⇒ abbbabbbbbbbbbbbabbbbb |
Referenced by [149].
Overlap of [148] aababbbbbbbbbbababb=abbbabbbbbbbbbbbabbbbb with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: abbbbbbbbbbbbbbabbbbbbbababb=abbbabbbbbbbbbbbabbbbb.
Reduce LHS:
| [95] | abbbbbbbbbbb(bbbabbbbbbba)babb |
| [144] | ⇒ abbbbbbbbbbbbabbbb(abbbbbba)bb |
| [103] | ⇒ abbbbbbbbbbb(babbbbbbbbbbbbbbbb)abbbbbb |
| [118] | ⇒ abbbbbbbbbb(bbabab)bbbbb |
| [103] | ⇒ abbbbbbbbbb(babbbbbbbbbbbbbbbb)bb |
| ⇒ abbbbbbbbbbbabbb |
Flip LHS and RHS.
Referenced by [162].
Overlap of [42] babbbbabbbba=abbabbbbabbb with [142] abbbbabbbba=bbbbbabbbbbbbb:
Critical pair: bbbbbbabbbbbbbb=abbabbbbabbb.
Flip LHS and RHS.
Referenced by [249].
Simplify [44] babbbbabbbbbbbbbbababb=ababbaa.
Reduce RHS:
| [91] | ab(abbaa) |
| [136] | ⇒ a(bbbabbba)bbbbbbb |
| [124] | ⇒ a(abbbbbbbbbbabbbbbbbbbbbbbbb)bbb |
| ⇒ aabbbbbbbbbbabbb |
Referenced by [152].
Overlap of [151] babbbbabbbbbbbbbbababb=aabbbbbbbbbbabbb with [118] bbabab=babbbbbbbbbbbbb:
Critical pair: babbbbabbbbbbbbbabbbbbbbbbbbbbb=aabbbbbbbbbbabbb.
Reduce LHS:
| [147] | (babbbbabbbbbbbbbab)bbbbbbbbbbbbb |
| [103] | ⇒ babbbabbbbbbb(babbbbbbbbbbbbbbbb) |
| ⇒ babbbabbbbbbbbab |
Referenced by [155], [166], [168], [172], [184], [207], [244].
Overlap of [45] aababbbbba=babbbbabbbbbbbbabbb with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: abbbbbbbbbbbbbbabba=babbbbabbbbbbbbabbb.
Flip LHS and RHS.
Referenced by [160], [186], [187], [199].
Simplify [56] babbbbabbbbbbbbbabbabab=bbbbabbbaba.
Reduce RHS:
| [138] | bbbbabb(baba) |
| ⇒ bbbbabbabbbbbbbbbbbb |
Referenced by [155].
Overlap of [154] babbbbabbbbbbbbbabbabab=bbbbabbabbbbbbbbbbbb with [147] babbbbabbbbbbbbbab=babbbabbbbbbbbabbb:
Critical pair: babbbabbbbbbbbabbbbabab=bbbbabbabbbbbbbbbbbb.
Reduce LHS:
| [152] | (babbbabbbbbbbbab)bbbabab |
| [144] | ⇒ aabbbbbbbbbb(abbbbbba)bab |
| [139] | ⇒ aa(bbbbbbbbbbbbbbb)bbbbbbbabbbbbab |
| [137] | ⇒ aabbbb(bbbabbbbba)b |
| [137] | ⇒ aab(bbbabbbbba)bbbb |
| [140] | ⇒ a(ababbb)bbabbbbbbb |
| ⇒ abbbbbbbbbbbbbbabbabbbbbbb |
Simplify [57] abbabbbabbabbbb=ababbbbbabbabbb.
Reduce RHS:
| [140] | (ababbb)bbabbabbb |
| [92] | ⇒ bbbbbbbbb(bbbbbabbabba)bbb |
| [103] | ⇒ bbbbbbbbbbabbb(babbbbbbbbbbbbbbbb)b |
| ⇒ bbbbbbbbbbabbbbabb |
Referenced by [157].
Overlap of [156] abbabbbabbabbbb=bbbbbbbbbbabbbbabb with [85] abbabbba=bbbabbbbbbb:
Critical pair: bbbabbbbbbbbbabbbb=bbbbbbbbbbabbbbabb.
Flip LHS and RHS.
Simplify [63] aabbbabbbbabbbbbbbbba=babbbbabbbabbab.
Reduce RHS:
| [131] | babbbb(abbbabba)b |
| ⇒ babbbbbabbbbbbbbbbabbbbb |
Referenced by [159].
Overlap of [158] aabbbabbbbabbbbbbbbba=babbbbbabbbbbbbbbbabbbbb with [146] bbabbbbabbbbbbbbba=baabbbbbbbbbbabbbb:
Critical pair: aabbaabbbbbbbbbbabbbb=babbbbbabbbbbbbbbbabbbbb.
Reduce LHS:
| [91] | a(abbaa)bbbbbbbbbbabbbb |
| [102] | ⇒ a(bbabbbabbbbbbbbbbbbbbb)bbabbbb |
| [85] | ⇒ (abbabbba)bbabbbb |
| ⇒ bbbabbbbbbbbbabbbb |
Flip LHS and RHS.
Overlap of [65] bbabbbbabbbbbbbbabbbbbbbabbbbbb=abbbbabbab with [153] babbbbabbbbbbbbabbb=abbbbbbbbbbbbbbabba:
Critical pair: babbbbbbbbbbbbbbabbabbbbabbbbbb=abbbbabbab.
Reduce LHS:
| [93] | babbbbbbbbb(bbbbbabbabbbbabbbbbb) |
| [118] | ⇒ babbbbbbb(bbabab)bbbbbbbbabbbbbbb |
| [103] | ⇒ babbbbbbb(babbbbbbbbbbbbbbbb)bbbbbabbbbbbb |
| [144] | ⇒ babbbbbbbb(abbbbbba)bbbbbbb |
| [103] | ⇒ (babbbbbbbbbbbbbbbb)bbbbabbbbbbbbbbb |
| ⇒ babbbbbabbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [258].
Simplify [72] bbbbabbabbbbabbbbbbbbbbbba=bbabbbbabbbbbbbbbabb.
Reduce RHS:
| [146] | (bbabbbbabbbbbbbbba)bb |
| ⇒ baabbbbbbbbbbabbbbbb |
Referenced by [162].
Overlap of [161] bbbbabbabbbbabbbbbbbbbbbba=baabbbbbbbbbbabbbbbb with [78] bbabbabbbbabbbbbbbb=babbbbbbbbbbbabbbab:
Critical pair: bbbabbbbbbbbbbbabbbabbbbba=baabbbbbbbbbbabbbbbb.
Reduce LHS:
| [130] | bb(babbbbbbbbbbbabbba)bbbbba |
| [149] | ⇒ bb(abbbabbbbbbbbbbbabbbbb)ba |
| ⇒ bbabbbbbbbbbbbabbbba |
Simplify [78] bbabbabbbbabbbbbbbb=babbbbbbbbbbbabbbab.
Reduce RHS:
| [130] | (babbbbbbbbbbbabbba)b |
| ⇒ abbbabbbbbbbbbbbabb |
Referenced by [164].
Overlap of [163] bbabbabbbbabbbbbbbb=abbbabbbbbbbbbbbabb with [117] babbabbbbabbb=bbbbbbbabbbbbbbb:
Critical pair: bbbbbbbbabbbbbbbbbbbbb=abbbabbbbbbbbbbbabb.
Flip LHS and RHS.
Referenced by [213].
Simplify [81] baabbbababa=ababbbbbabbbbbbbbbba.
Reduce RHS:
| [140] | (ababbb)bbabbbbbbbbbba |
| ⇒ bbbbbbbbbbbbbbabbabbbbbbbbbba |
Referenced by [166].
Overlap of [165] baabbbababa=bbbbbbbbbbbbbbabbabbbbbbbbbba with [101] aabbba=bbabbbabbbbbbbb:
Critical pair: bbbabbbabbbbbbbbbaba=bbbbbbbbbbbbbbabbabbbbbbbbbba.
Reduce LHS:
| [138] | bbbabbbabbbbbbbb(baba) |
| [152] | ⇒ bb(babbbabbbbbbbbab)bbbbbbbbbbb |
| [141] | ⇒ (bbaa)bbbbbbbbbbabbbbbbbbbbbbbb |
| [103] | ⇒ abb(babbbbbbbbbbbbbbbb)bbbbbbbbabbbbbbbbbbbbbb |
| ⇒ abbbabbbbbbbbbabbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [214].
Simplify [82] babbbbabbbbbbbbbabbbababa=ababbabbbabbb.
Reduce RHS:
| [85] | ab(abbabbba)bbb |
| ⇒ abbbbabbbbbbbbbb |
Referenced by [168].
Overlap of [167] babbbbabbbbbbbbbabbbababa=abbbbabbbbbbbbbb with [147] babbbbabbbbbbbbbab=babbbabbbbbbbbabbb:
Critical pair: babbbabbbbbbbbabbbbbababa=abbbbabbbbbbbbbb.
Reduce LHS:
| [152] | (babbbabbbbbbbbab)bbbbababa |
| [95] | ⇒ aabbbbbbb(bbbabbbbbbba)baba |
| [144] | ⇒ aabbbbbbbbabbbb(abbbbbba)ba |
| [103] | ⇒ aabbbbbbb(babbbbbbbbbbbbbbbb)abbbbba |
| [118] | ⇒ aabbbbbb(bbabab)bbbba |
| [103] | ⇒ aabbbbbb(babbbbbbbbbbbbbbbb)ba |
| ⇒ aabbbbbbbabba |
Referenced by [243], [261], [262].
Overlap of [83] abbabbabbbbabbbbbb=bbabbbabbbba with [117] babbabbbbabbb=bbbbbbbabbbbbbbb:
Critical pair: abbbbbbbbabbbbbbbbbbb=bbabbbabbbba.
Flip LHS and RHS.
Referenced by [209].
Overlap of [84] aababbbbbbbbba=babbbbbbbbabbbbbbbbbbab with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: abbbbbbbbbbbbbbabbbbbba=babbbbbbbbabbbbbbbbbbab.
Reduce LHS:
| [144] | abbbbbbbbbbbbbb(abbbbbba) |
| [139] | ⇒ a(bbbbbbbbbbbbbbb)bbbbbbbbbbbabbbb |
| ⇒ abbbbbbbbbbbabbbb |
Flip LHS and RHS.
Simplify [88] ababbbbbbbbbbbabbbbabbbbbb=bbabbbbbbbbbbbbababb.
Reduce RHS:
| [118] | bbabbbbbbbbbb(bbabab)b |
| ⇒ bbabbbbbbbbbbbabbbbbbbbbbbbbb |
Referenced by [172].
Overlap of [171] ababbbbbbbbbbbabbbbabbbbbb=bbabbbbbbbbbbbabbbbbbbbbbbbbb with [157] bbbbbbbbbbabbbbabb=bbbabbbbbbbbbabbbb:
Critical pair: ababbbbabbbbbbbbbabbbbbbbb=bbabbbbbbbbbbbabbbbbbbbbbbbbb.
Reduce LHS:
| [147] | a(babbbbabbbbbbbbbab)bbbbbbb |
| [152] | ⇒ a(babbbabbbbbbbbab)bbbbbbbbb |
| [1] | ⇒ (aaa)bbbbbbbbbbabbbbbbbbbbbb |
| ⇒ bbbbbbbbbbabbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [202].
Overlap of [89] ababbbabbbabbabbb=bbabbbbbabbbbbbbbbba with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: bbbbbbbbbbbbbbaabbbabbabbb=bbabbbbbabbbbbbbbbba.
Reduce LHS:
| [101] | bbbbbbbbbbbbbb(aabbba)bbabbb |
| [139] | ⇒ (bbbbbbbbbbbbbbb)babbbabbbbbbbbbbabbb |
| ⇒ babbbabbbbbbbbbbabbb |
Flip LHS and RHS.
Referenced by [178].
Overlap of [92] bbbbbabbabba=babbbbabbbbbbbbbbbbbb with [94] abbabba=bbbabbbbbbbbabbb:
Critical pair: bbbbbbbbabbbbbbbbabbb=babbbbabbbbbbbbbbbbbb.
Simplify [96] abbabbbbbbbbbababb=bbbabbbbbbbbbbbabbbbabbbbbb.
Reduce RHS:
| [162] | b(bbabbbbbbbbbbbabbbba)bbbbbb |
| [141] | ⇒ (bbaa)bbbbbbbbbbabbbbbbbbbbbb |
| [103] | ⇒ abb(babbbbbbbbbbbbbbbb)bbbbbbbbabbbbbbbbbbbb |
| ⇒ abbbabbbbbbbbbabbbbbbbbbbbb |
Referenced by [176].
Overlap of [175] abbabbbbbbbbbababb=abbbabbbbbbbbbabbbbbbbbbbbb with [118] bbabab=babbbbbbbbbbbbb:
Critical pair: abbabbbbbbbbabbbbbbbbbbbbbb=abbbabbbbbbbbbabbbbbbbbbbbb.
Flip LHS and RHS.
Referenced by [214].
Overlap of [99] babbbbbbbbabbbbbbbbbbabbbbbbbba=abbbbabbbbbbbbbbbbb with [170] babbbbbbbbabbbbbbbbbbab=abbbbbbbbbbbabbbb:
Critical pair: abbbbbbbbbbbabbbbbbbbbbba=abbbbabbbbbbbbbbbbb.
Referenced by [216].
Simplify [100] ababbbbbbbbbaa=bbabbbbbabbbbbbbbbbabbb.
Reduce RHS:
| [173] | (bbabbbbbabbbbbbbbbba)bbb |
| ⇒ babbbabbbbbbbbbbabbbbbb |
Referenced by [179].
Overlap of [178] ababbbbbbbbbaa=babbbabbbbbbbbbbabbbbbb with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: bbbbbbbbbbbbbbabbbbbbaa=babbbabbbbbbbbbbabbbbbb.
Reduce LHS:
| [144] | bbbbbbbbbbbbbb(abbbbbba)a |
| [139] | ⇒ (bbbbbbbbbbbbbbb)bbbbbbbbbbbabbbba |
| ⇒ bbbbbbbbbbbabbbba |
Flip LHS and RHS.
Referenced by [217].
Overlap of [104] ababbbbaa=abbbbabbbbbb with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: bbbbbbbbbbbbbbabaa=abbbbabbbbbb.
Reduce LHS:
| [138] | bbbbbbbbbbbbb(baba)a |
| ⇒ bbbbbbbbbbbbbabbbbbbbbbbbba |
Referenced by [218].
Overlap of [107] bbabbbabbbbbbbbbbbbabbbb=baabbbbba with [121] bbabbbabbbbbbbbbbbba=bbbbbabbbbabbb:
Critical pair: bbbbbabbbbabbbbbbb=baabbbbba.
Flip LHS and RHS.
Referenced by [191].
Overlap of [108] bbabbbabbbbbbbbbbbabbbabbabbb=bbabbabbbbbbbbbba with [130] babbbbbbbbbbbabbba=abbbabbbbbbbbbbbab:
Critical pair: bbabbabbbabbbbbbbbbbbabbbabbb=bbabbabbbbbbbbbba.
Reduce LHS:
| [130] | bbabbabb(babbbbbbbbbbbabbba)bbb |
| [85] | ⇒ bbabb(abbabbba)bbbbbbbbbbbabbbb |
| [139] | ⇒ bbabbbbba(bbbbbbbbbbbbbbb)bbbabbbb |
| [136] | ⇒ bbabb(bbbabbba)bbbb |
| [128] | ⇒ (bbabbabbbbbbbbbbabbbbbbb)bbbbbbbb |
| [140] | ⇒ (ababbb)bbabbbbbbbb |
| ⇒ bbbbbbbbbbbbbbabbabbbbbbbb |
Flip LHS and RHS.
Referenced by [185], [215], [240].
Overlap of [111] baabbbbbbbbbbabbbbbabbb=bbabbbbabbbbbbbba with [122] abbbbbbbbbbabbbbba=ababbbbbabbbbbbbbb:
Critical pair: baababbbbbabbbbbbbbbbbb=bbabbbbabbbbbbbba.
Reduce LHS:
| [140] | ba(ababbb)bbabbbbbbbbbbbb |
| [155] | ⇒ b(abbbbbbbbbbbbbbabbabbbbbbb)bbbbb |
| [139] | ⇒ bbbbbabba(bbbbbbbbbbbbbbb)bb |
| ⇒ bbbbbabbabb |
Flip LHS and RHS.
Overlap of [112] babbbbabbbbbbbbbabbbbbabbbbba=babbbbbbbab with [147] babbbbabbbbbbbbbab=babbbabbbbbbbbabbb:
Critical pair: babbbabbbbbbbbabbbbbbbabbbbba=babbbbbbbab.
Reduce LHS:
| [152] | (babbbabbbbbbbbab)bbbbbbabbbbba |
| [115] | ⇒ a(abbbbbbbbbbabbbbbbbbba)bbbbba |
| [144] | ⇒ (abbbbbba)bbbbbbbba |
| ⇒ bbbbbbbbbbbbabbbbbbbbbbbba |
Referenced by [218].
Overlap of [113] bbabbbbabbbbbbbbabbbbbbbba=babbbbabbbbbbbbbbabb with [183] bbabbbbabbbbbbbba=bbbbbabbabb:
Critical pair: bbbbbabbabbbbbbbbbba=babbbbabbbbbbbbbbabb.
Reduce LHS:
| [182] | bbb(bbabbabbbbbbbbbba) |
| [139] | ⇒ (bbbbbbbbbbbbbbb)bbabbabbbbbbbb |
| ⇒ bbabbabbbbbbbb |
Flip LHS and RHS.
Referenced by [190].
Simplify [114] abbabbbbbabbba=babbbbabbbbbbbbabbbbbbb.
Reduce RHS:
| [153] | (babbbbabbbbbbbbabbb)bbbb |
| ⇒ abbbbbbbbbbbbbbabbabbbb |
Referenced by [187].
Overlap of [186] abbabbbbbabbba=abbbbbbbbbbbbbbabbabbbb with [136] bbbabbba=abbbbbbbbbbabbbbbbbbbbb:
Critical pair: abbabbabbbbbbbbbbabbbbbbbbbbb=abbbbbbbbbbbbbbabbabbbb.
Reduce LHS:
| [94] | (abbabba)bbbbbbbbbbabbbbbbbbbbb |
| [123] | ⇒ bbbabbbbbbb(babbbbbbbbbbbbba)bbbbbbbbbbb |
| [95] | ⇒ (bbbabbbbbbba)bbbabbbbbbbbbbbbbbbbbbbbbb |
| [153] | ⇒ (babbbbabbbbbbbbabbb)bbbbbbbbbbbbbbbbbbb |
| [155] | ⇒ (abbbbbbbbbbbbbbabbabbbbbbb)bbbbbbbbbbbb |
| [139] | ⇒ bbbbabba(bbbbbbbbbbbbbbb)bbbbbbbbb |
| ⇒ bbbbabbabbbbbbbbb |
Flip LHS and RHS.
Referenced by [199].
Overlap of [119] ababbbabbbbb=bbabbbbbbbbbbbbbbabbb with [140] ababbb=bbbbbbbbbbbbbba:
Critical pair: bbbbbbbbbbbbbbaabbbbb=bbabbbbbbbbbbbbbbabbb.
Reduce LHS:
| [120] | bbbbbbbbbb(bbbbaa)bbbbb |
| [139] | ⇒ bbbbbbbbbbbbabbba(bbbbbbbbbbbbbbb)bbbb |
| [136] | ⇒ bbbbbbbbb(bbbabbba)bbbb |
| [124] | ⇒ bbbbbbbbb(abbbbbbbbbbabbbbbbbbbbbbbbb) |
| ⇒ bbbbbbbbbabbbbbbbbbba |
Referenced by [204], [212], [240], [244].
Overlap of [127] baabbbbbbbbbbbbbba=bbabbb with [145] baabbbbbbbbbbbb=abbbbbbbbbbbbba:
Critical pair: abbbbbbbbbbbbbabba=bbabbb.
Defines rule #50.
Referenced by [232].
Overlap of [129] babbbabbbabbabbbbbbbb=abbbabbbbbbbbbbbbabba with [131] abbbabba=babbbbbbbbbbabbbb:
Critical pair: babbbbabbbbbbbbbbabbbbbbbbbbbb=abbbabbbbbbbbbbbbabba.
Reduce LHS:
| [185] | (babbbbabbbbbbbbbbabb)bbbbbbbbbb |
| [139] | ⇒ bbabba(bbbbbbbbbbbbbbb)bbb |
| ⇒ bbabbabbb |
Flip LHS and RHS.
Referenced by [220].
Overlap of [132] abbbabbbbbbbbbbbbbbbabbbbba=babbbbbbbbbbbbabbabbb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbbaabbbbba=babbbbbbbbbbbbabbabbb.
Reduce LHS:
| [181] | abb(baabbbbba) |
| ⇒ abbbbbbbabbbbabbbbbbb |
Flip LHS and RHS.
Referenced by [221].
Overlap of [133] abbbabbbbbbbbbbbbbbbaba=abbbabbbbbbbbbbbbbbabbbbbbbbbbbb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbbaaba=abbbabbbbbbbbbbbbbbabbbbbbbbbbbb.
Reduce LHS:
| [141] | ab(bbaa)ba |
| [139] | ⇒ ababbba(bbbbbbbbbbbbbbb)a |
| [140] | ⇒ (ababbb)aa |
| [1] | ⇒ bbbbbbbbbbbbbb(aaa) |
| ⇒ bbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [193].
Overlap of [135] abbbabbbbbbbbbbbbbbabbbbbbbbbbbbbbb=abbbabbbbbbbbbbbbbba with [192] abbbabbbbbbbbbbbbbbabbbbbbbbbbbb=bbbbbbbbbbbbbb:
Critical pair: bbbbbbbbbbbbbbbbb=abbbabbbbbbbbbbbbbba.
Reduce LHS:
| [139] | (bbbbbbbbbbbbbbb)bb |
| ⇒ bb |
Flip LHS and RHS.
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [138] baba=abbbbbbbbbbbb:
Critical pair: babbbbbbbbbbbbabbbbbbbbbbbb=abbbabbbbbbbbbbbba.
Flip LHS and RHS.
Defines rule #38.
Overlap of [138] baba=abbbbbbbbbbbb with [40] abaa=babbbbabbbbbb:
Critical pair: bbabbbbabbbbbb=abbbbbbbbbbbba.
Referenced by [198], [219], [221], [233].
Overlap of [139] bbbbbbbbbbbbbbb=1 with [138] baba=abbbbbbbbbbbb:
Critical pair: bbbbbbbbbbbbbbabbbbbbbbbbbb=aba.
Flip LHS and RHS.
Defines rule #2.
Referenced by [227], [239], [240], [247], [250], [264], [267].
Overlap of [137] bbbabbbbba=abbbbbabbb with [137] bbbabbbbba=abbbbbabbb:
Critical pair: bbbabbabbbbbabbb=abbbbbabbbbbbbba.
Referenced by [245].
Overlap of [137] bbbabbbbba=abbbbbabbb with [138] baba=abbbbbbbbbbbb:
Critical pair: bbbabbbbabbbbbbbbbbbb=abbbbbabbbba.
Reduce LHS:
| [195] | b(bbabbbbabbbbbb)bbbbbb |
| ⇒ babbbbbbbbbbbbabbbbbb |
Flip LHS and RHS.
Referenced by [226].
Overlap of [85] abbabbba=bbbabbbbbbb with [101] aabbba=bbabbbabbbbbbbb:
Critical pair: abbabbbbbabbbabbbbbbbb=bbbabbbbbbbabbba.
Reduce LHS:
| [136] | abbabb(bbbabbba)bbbbbbbb |
| [139] | ⇒ abbabbabbbbbbbbbba(bbbbbbbbbbbbbbb)bbbb |
| [94] | ⇒ (abbabba)bbbbbbbbbbabbbb |
| [123] | ⇒ bbbabbbbbbb(babbbbbbbbbbbbba)bbbb |
| [95] | ⇒ (bbbabbbbbbba)bbbabbbbbbbbbbbbbbb |
| [153] | ⇒ (babbbbabbbbbbbbabbb)bbbbbbbbbbbb |
| [187] | ⇒ (abbbbbbbbbbbbbbabbabbbb)bbbbbbbb |
| [139] | ⇒ bbbbabba(bbbbbbbbbbbbbbb)bb |
| ⇒ bbbbabbabb |
Reduce RHS:
| [95] | (bbbabbbbbbba)bbba |
| ⇒ babbbbabbbbbbbba |
Flip LHS and RHS.
Referenced by [207], [208], [238], [253].
Overlap of [1] aaa=1 with [193] abbbabbbbbbbbbbbbbba=bb:
Critical pair: aabb=bbbabbbbbbbbbbbbbba.
Flip LHS and RHS.
Defines rule #12.
Referenced by [204], [205], [206], [210], [236], [239], [254], [260], [263].
Overlap of [138] baba=abbbbbbbbbbbb with [193] abbbabbbbbbbbbbbbbba=bb:
Critical pair: babbb=abbbbbbbbbbbbbbbabbbbbbbbbbbbbba.
Reduce RHS:
| [139] | a(bbbbbbbbbbbbbbb)abbbbbbbbbbbbbba |
| ⇒ aabbbbbbbbbbbbbba |
Flip LHS and RHS.
Defines rule #27.
Referenced by [202], [237], [246], [259].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [201] aabbbbbbbbbbbbbba=babbb:
Critical pair: babbbbbbbbbbbbbbabbb=abbbabbbbbbbbbbbabbbbbbbbbbbbbba.
Reduce RHS:
| [172] | ab(bbabbbbbbbbbbbabbbbbbbbbbbbbb)a |
| ⇒ abbbbbbbbbbbabbbbbbbbbbbba |
Flip LHS and RHS.
Referenced by [223].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [141] bbaa=abbbabbbbbbbbbbbbbb:
Critical pair: babbbbbbbbbbbabbbabbbbbbbbbbbbbb=abbbabbbbbbbbbbba.
Reduce LHS:
| [136] | babbbbbbbb(bbbabbba)bbbbbbbbbbbbbb |
| [170] | ⇒ (babbbbbbbbabbbbbbbbbbab)bbbbbbbbbbbbbbbbbbbbbbbb |
| [139] | ⇒ abbbbbbbbbbba(bbbbbbbbbbbbbbb)bbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbabbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [213].
Overlap of [139] bbbbbbbbbbbbbbb=1 with [141] bbaa=abbbabbbbbbbbbbbbbb:
Critical pair: bbbbbbbbbbbbbbabbbabbbbbbbbbbbbbb=baa.
Reduce LHS:
| [136] | bbbbbbbbbbb(bbbabbba)bbbbbbbbbbbbbb |
| [188] | ⇒ bb(bbbbbbbbbabbbbbbbbbba)bbbbbbbbbbbbbbbbbbbbbbbbb |
| [200] | ⇒ b(bbbabbbbbbbbbbbbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbb |
| [145] | ⇒ (baabbbbbbbbbbbb)bbbbbbbbbbbbbbbbbb |
| [139] | ⇒ abbbbbbbbbbbbba(bbbbbbbbbbbbbbb)bbb |
| ⇒ abbbbbbbbbbbbbabbb |
Flip LHS and RHS.
Defines rule #5.
Referenced by [212], [235], [240], [244], [250], [254], [257], [260], [269].
Overlap of [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb with [200] bbbabbbbbbbbbbbbbba=aabb:
Critical pair: babbbbbbbbbbaabb=abbbabbbbbbbbbbbbbbbbbbbbbbbbba.
Reduce LHS:
| [141] | babbbbbbbb(bbaa)bb |
| [139] | ⇒ babbbbbbbbabbba(bbbbbbbbbbbbbbb)b |
| [136] | ⇒ babbbbb(bbbabbba)b |
| [159] | ⇒ (babbbbbabbbbbbbbbbabbbbb)bbbbbbb |
| ⇒ bbbabbbbbbbbbabbbbbbbbbbb |
Reduce RHS:
| [139] | abbba(bbbbbbbbbbbbbbb)bbbbbbbbbba |
| ⇒ abbbabbbbbbbbbba |
Flip LHS and RHS.
Overlap of [137] bbbabbbbba=abbbbbabbb with [200] bbbabbbbbbbbbbbbbba=aabb:
Critical pair: bbbabbaabb=abbbbbabbbbbbbbbbbbbbbbba.
Reduce LHS:
| [141] | bbba(bbaa)bb |
| [139] | ⇒ bbbaabbba(bbbbbbbbbbbbbbb)b |
| [101] | ⇒ bbb(aabbba)b |
| [136] | ⇒ bb(bbbabbba)bbbbbbbbb |
| [139] | ⇒ bbabbbbbbbbbba(bbbbbbbbbbbbbbb)bbbbb |
| ⇒ bbabbbbbbbbbbabbbbb |
Reduce RHS:
| [139] | abbbbba(bbbbbbbbbbbbbbb)bba |
| ⇒ abbbbbabba |
Flip LHS and RHS.
Defines rule #43.
Overlap of [40] abaa=babbbbabbbbbb with [94] abbabba=bbbabbbbbbbbabbb:
Critical pair: ababbbabbbbbbbbabbb=babbbbabbbbbbbbabba.
Reduce LHS:
| [152] | a(babbbabbbbbbbbab)bb |
| [1] | ⇒ (aaa)bbbbbbbbbbabbbbb |
| ⇒ bbbbbbbbbbabbbbb |
Reduce RHS:
| [199] | (babbbbabbbbbbbba)bba |
| ⇒ bbbbabbabbbba |
Flip LHS and RHS.
Referenced by [233].
Overlap of [138] baba=abbbbbbbbbbbb with [94] abbabba=bbbabbbbbbbbabbb:
Critical pair: babbbbabbbbbbbbabbb=abbbbbbbbbbbbbbabba.
Reduce LHS:
| [199] | (babbbbabbbbbbbba)bbb |
| ⇒ bbbbabbabbbbb |
Flip LHS and RHS.
Defines rule #51.
Overlap of [137] bbbabbbbba=abbbbbabbb with [95] bbbabbbbbbba=babbbbabbbbb:
Critical pair: bbbabbbabbbbabbbbb=abbbbbabbbbbbbbbba.
Reduce LHS:
| [169] | b(bbabbbabbbba)bbbbb |
| [139] | ⇒ babbbbbbbba(bbbbbbbbbbbbbbb)b |
| ⇒ babbbbbbbbab |
Flip LHS and RHS.
Defines rule #44.
Referenced by [211].
Overlap of [200] bbbabbbbbbbbbbbbbba=aabb with [95] bbbabbbbbbba=babbbbabbbbb:
Critical pair: bbbabbbbbbbbbbbbabbbbabbbbb=aabbbbbbbbba.
Reduce LHS:
| [157] | bbbabb(bbbbbbbbbbabbbbabb)bbb |
| [137] | ⇒ (bbbabbbbba)bbbbbbbbbabbbbbbb |
| ⇒ abbbbbabbbbbbbbbbbbabbbbbbb |
Referenced by [225].
Overlap of [159] babbbbbabbbbbbbbbbabbbbb=bbbabbbbbbbbbabbbb with [209] abbbbbabbbbbbbbbba=babbbbbbbbab:
Critical pair: bbabbbbbbbbabbbbbb=bbbabbbbbbbbbabbbb.
Flip LHS and RHS.
Simplify [162] bbabbbbbbbbbbbabbbba=baabbbbbbbbbbabbbbbb.
Reduce RHS:
| [204] | (baa)bbbbbbbbbbabbbbbb |
| [123] | ⇒ abbbbbbbbbbbb(babbbbbbbbbbbbba)bbbbbb |
| [139] | ⇒ abbbbbbbbbbbbabbba(bbbbbbbbbbbbbbb)bb |
| [136] | ⇒ abbbbbbbbb(bbbabbba)bb |
| [188] | ⇒ a(bbbbbbbbbabbbbbbbbbba)bbbbbbbbbbbbb |
| [139] | ⇒ abbabbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)b |
| ⇒ abbabbbbbbbbbbbbbbab |
Referenced by [244].
Overlap of [164] abbbabbbbbbbbbbbabb=bbbbbbbbabbbbbbbbbbbbb with [203] abbbabbbbbbbbbbba=abbbbbbbbbbbabbbbbbbbbbbbb:
Critical pair: abbbbbbbbbbbabbbbbbbbbbbbbbb=bbbbbbbbabbbbbbbbbbbbb.
Reduce LHS:
| [139] | abbbbbbbbbbba(bbbbbbbbbbbbbbb) |
| ⇒ abbbbbbbbbbba |
Defines rule #4.
Referenced by [216], [223], [229], [236], [237], [247].
Simplify [166] bbbbbbbbbbbbbbabbabbbbbbbbbba=abbbabbbbbbbbbabbbbbbbbbbbbbb.
Reduce RHS:
| [176] | (abbbabbbbbbbbbabbbbbbbbbbbb)bb |
| [139] | ⇒ abbabbbbbbbba(bbbbbbbbbbbbbbb)b |
| ⇒ abbabbbbbbbbab |
Referenced by [215].
Overlap of [214] bbbbbbbbbbbbbbabbabbbbbbbbbba=abbabbbbbbbbab with [182] bbabbabbbbbbbbbba=bbbbbbbbbbbbbbabbabbbbbbbb:
Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbabbabbbbbbbb=abbabbbbbbbbab.
Reduce LHS:
| [139] | (bbbbbbbbbbbbbbb)bbbbbbbbbbbabbabbbbbbbb |
| ⇒ bbbbbbbbbbbabbabbbbbbbb |
Flip LHS and RHS.
Referenced by [254].
Overlap of [177] abbbbbbbbbbbabbbbbbbbbbba=abbbbabbbbbbbbbbbbb with [213] abbbbbbbbbbba=bbbbbbbbabbbbbbbbbbbbb:
Critical pair: bbbbbbbbabbbbbbbbbbbbbbbbbbbbbbbba=abbbbabbbbbbbbbbbbb.
Reduce LHS:
| [139] | bbbbbbbba(bbbbbbbbbbbbbbb)bbbbbbbbba |
| ⇒ bbbbbbbbabbbbbbbbba |
Referenced by [243].
Overlap of [179] babbbabbbbbbbbbbabbbbbb=bbbbbbbbbbbabbbba with [205] abbbabbbbbbbbbba=bbbabbbbbbbbbabbbbbbbbbbb:
Critical pair: bbbbabbbbbbbbbabbbbbbbbbbbbbbbbb=bbbbbbbbbbbabbbba.
Reduce LHS:
| [211] | b(bbbabbbbbbbbbabbbb)bbbbbbbbbbbbb |
| [139] | ⇒ bbbabbbbbbbba(bbbbbbbbbbbbbbb)bbbb |
| ⇒ bbbabbbbbbbbabbbb |
Flip LHS and RHS.
Overlap of [180] bbbbbbbbbbbbbabbbbbbbbbbbba=abbbbabbbbbb with [184] bbbbbbbbbbbbabbbbbbbbbbbba=babbbbbbbab:
Critical pair: bbabbbbbbbab=abbbbabbbbbb.
Referenced by [226], [227], [228].
Overlap of [183] bbabbbbabbbbbbbba=bbbbbabbabb with [195] bbabbbbabbbbbb=abbbbbbbbbbbba:
Critical pair: abbbbbbbbbbbbabba=bbbbbabbabb.
Defines rule #49.
Overlap of [190] abbbabbbbbbbbbbbbabba=bbabbabbb with [219] abbbbbbbbbbbbabba=bbbbbabbabb:
Critical pair: abbbbbbbbabbabb=bbabbabbb.
Simplify [191] babbbbbbbbbbbbabbabbb=abbbbbbbabbbbabbbbbbb.
Reduce RHS:
| [195] | abbbbb(bbabbbbabbbbbb)b |
| ⇒ abbbbbabbbbbbbbbbbbab |
Referenced by [222].
Overlap of [221] babbbbbbbbbbbbabbabbb=abbbbbabbbbbbbbbbbbab with [219] abbbbbbbbbbbbabba=bbbbbabbabb:
Critical pair: bbbbbbabbabbbbb=abbbbbabbbbbbbbbbbbab.
Flip LHS and RHS.
Referenced by [225].
Overlap of [202] abbbbbbbbbbbabbbbbbbbbbbba=babbbbbbbbbbbbbbabbb with [213] abbbbbbbbbbba=bbbbbbbbabbbbbbbbbbbbb:
Critical pair: bbbbbbbbabbbbbbbbbbbbbbbbbbbbbbbbba=babbbbbbbbbbbbbbabbb.
Reduce LHS:
| [139] | bbbbbbbba(bbbbbbbbbbbbbbb)bbbbbbbbbba |
| ⇒ bbbbbbbbabbbbbbbbbba |
Referenced by [245].
Simplify [205] abbbabbbbbbbbbba=bbbabbbbbbbbbabbbbbbbbbbb.
Reduce RHS:
| [211] | (bbbabbbbbbbbbabbbb)bbbbbbb |
| ⇒ bbabbbbbbbbabbbbbbbbbbbbb |
Defines rule #37.
Overlap of [210] abbbbbabbbbbbbbbbbbabbbbbbb=aabbbbbbbbba with [222] abbbbbabbbbbbbbbbbbab=bbbbbbabbabbbbb:
Critical pair: bbbbbbabbabbbbbbbbbbb=aabbbbbbbbba.
Flip LHS and RHS.
Defines rule #23.
Overlap of [218] bbabbbbbbbab=abbbbabbbbbb with [95] bbbabbbbbbba=babbbbabbbbb:
Critical pair: bbabbbbbabbbbabbbbb=abbbbabbbbbbbbbbbba.
Reduce LHS:
| [198] | bb(abbbbbabbbba)bbbbb |
| ⇒ bbbabbbbbbbbbbbbabbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #42.
Overlap of [218] bbabbbbbbbab=abbbbabbbbbb with [137] bbbabbbbba=abbbbbabbb:
Critical pair: bbabbbbabbbbbabbb=abbbbabbbbbbbbbba.
Reduce LHS:
| [137] | bbab(bbbabbbbba)bbb |
| [196] | ⇒ bb(aba)bbbbbabbbbbb |
| [139] | ⇒ (bbbbbbbbbbbbbbb)babbbbbbbbbbbbbbbbbabbbbbb |
| [139] | ⇒ ba(bbbbbbbbbbbbbbb)bbabbbbbb |
| ⇒ babbabbbbbb |
Flip LHS and RHS.
Defines rule #41.
Referenced by [254].
Overlap of [218] bbabbbbbbbab=abbbbabbbbbb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: bbabbbbbbba=abbbbabbbbbbbbbbbbbbbbbbbb.
Reduce RHS:
| [139] | abbbba(bbbbbbbbbbbbbbb)bbbbb |
| ⇒ abbbbabbbbb |
Defines rule #9.
Referenced by [263].
Overlap of [220] abbbbbbbbabbabb=bbabbabbb with [85] abbabbba=bbbabbbbbbb:
Critical pair: abbbbbbbbbbbabbbbbbb=bbabbabbbba.
Reduce LHS:
| [213] | (abbbbbbbbbbba)bbbbbbb |
| [139] | ⇒ bbbbbbbba(bbbbbbbbbbbbbbb)bbbbb |
| ⇒ bbbbbbbbabbbbb |
Flip LHS and RHS.
Referenced by [251].
Overlap of [220] abbbbbbbbabbabb=bbabbabbb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbbbbbbbabba=bbabbabbbbbbbbbbbbbbbb.
Reduce RHS:
| [139] | bbabba(bbbbbbbbbbbbbbb)b |
| ⇒ bbabbab |
Defines rule #46.
Referenced by [231], [243], [254].
Overlap of [1] aaa=1 with [230] abbbbbbbbabba=bbabbab:
Critical pair: aabbabbab=bbbbbbbbabba.
Reduce LHS:
| [94] | a(abbabba)b |
| ⇒ abbbabbbbbbbbabbbb |
Overlap of [1] aaa=1 with [189] abbbbbbbbbbbbbabba=bbabbb:
Critical pair: aabbabbb=bbbbbbbbbbbbbabba.
Overlap of [86] bbbbbabbabbbbba=aabbbbbbb with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: bbbbbabbabbbbabbbabbbbbbbbbbb=aabbbbbbbbbbbbbbbbbbbba.
Reduce LHS:
| [207] | b(bbbbabbabbbba)bbbabbbbbbbbbbb |
| [174] | ⇒ bbb(bbbbbbbbabbbbbbbbabbb)bbbbbbbb |
| [195] | ⇒ bb(bbabbbbabbbbbb)bbbbbbbbbbbbbbbb |
| [139] | ⇒ bbabbbbbbbbbbbba(bbbbbbbbbbbbbbb)b |
| ⇒ bbabbbbbbbbbbbbab |
Reduce RHS:
| [139] | aa(bbbbbbbbbbbbbbb)bbbbba |
| ⇒ aabbbbba |
Flip LHS and RHS.
Defines rule #20.
Referenced by [242], [243], [260].
Overlap of [86] bbbbbabbabbbbba=aabbbbbbb with [137] bbbabbbbba=abbbbbabbb:
Critical pair: bbbbbabbabbabbbbbabbb=aabbbbbbbbbbbba.
Reduce LHS:
| [94] | bbbbb(abbabba)bbbbbabbb |
| [174] | ⇒ (bbbbbbbbabbbbbbbbabbb)bbbbbabbb |
| [139] | ⇒ babbbba(bbbbbbbbbbbbbbb)bbbbabbb |
| [142] | ⇒ b(abbbbabbbba)bbb |
| ⇒ bbbbbbabbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #25.
Overlap of [139] bbbbbbbbbbbbbbb=1 with [86] bbbbbabbabbbbba=aabbbbbbb:
Critical pair: bbbbbbbbbbaabbbbbbb=abbabbbbba.
Reduce LHS:
| [204] | bbbbbbbbb(baa)bbbbbbb |
| [123] | ⇒ bbbbbbbb(babbbbbbbbbbbbba)bbbbbbbbbb |
| [139] | ⇒ bbbbbbbbabbba(bbbbbbbbbbbbbbb)bbbbbb |
| [136] | ⇒ bbbbb(bbbabbba)bbbbbb |
| [139] | ⇒ bbbbbabbbbbbbbbba(bbbbbbbbbbbbbbb)bb |
| ⇒ bbbbbabbbbbbbbbbabb |
Flip LHS and RHS.
Defines rule #30.
Overlap of [200] bbbabbbbbbbbbbbbbba=aabb with [144] abbbbbba=bbbbbbbbbbbbabbbb:
Critical pair: bbbabbbbbbbbbbbbbbbbbbbbbbbbbbabbbb=aabbbbbbbba.
Reduce LHS:
| [139] | bbba(bbbbbbbbbbbbbbb)bbbbbbbbbbbabbbb |
| [213] | ⇒ bbb(abbbbbbbbbbba)bbbb |
| [139] | ⇒ bbbbbbbbbbba(bbbbbbbbbbbbbbb)bb |
| ⇒ bbbbbbbbbbbabb |
Flip LHS and RHS.
Defines rule #22.
Overlap of [201] aabbbbbbbbbbbbbba=babbb with [144] abbbbbba=bbbbbbbbbbbbabbbb:
Critical pair: aabbbbbbbbbbbbbbbbbbbbbbbbbbabbbb=babbbbbbbbba.
Reduce LHS:
| [139] | aa(bbbbbbbbbbbbbbb)bbbbbbbbbbbabbbb |
| [213] | ⇒ a(abbbbbbbbbbba)bbbb |
| [139] | ⇒ abbbbbbbba(bbbbbbbbbbbbbbb)bb |
| ⇒ abbbbbbbbabb |
Flip LHS and RHS.
Defines rule #6.
Referenced by [238], [239], [249], [257], [260], [263], [266].
Overlap of [137] bbbabbbbba=abbbbbabbb with [237] babbbbbbbbba=abbbbbbbbabb:
Critical pair: bbbabbbbabbbbbbbbabb=abbbbbabbbbbbbbbbbba.
Reduce LHS:
| [199] | bb(babbbbabbbbbbbba)bb |
| ⇒ bbbbbbabbabbbb |
Flip LHS and RHS.
Referenced by [246].
Overlap of [237] babbbbbbbbba=abbbbbbbbabb with [200] bbbabbbbbbbbbbbbbba=aabb:
Critical pair: babbbbbbaabb=abbbbbbbbabbbbbbbbbbbbbbbba.
Reduce LHS:
| [144] | b(abbbbbba)abb |
| [217] | ⇒ bb(bbbbbbbbbbbabbbba)bb |
| ⇒ bbbbbabbbbbbbbabbbbbb |
Reduce RHS:
| [139] | abbbbbbbba(bbbbbbbbbbbbbbb)ba |
| [196] | ⇒ abbbbbbbb(aba) |
| [139] | ⇒ a(bbbbbbbbbbbbbbb)bbbbbbbabbbbbbbbbbbb |
| ⇒ abbbbbbbabbbbbbbbbbbb |
Referenced by [249].
Overlap of [232] aabbabbb=bbbbbbbbbbbbbabba with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: aababbbabbbbbbbbbbb=bbbbbbbbbbbbbabbabbbbbbbbbba.
Reduce LHS:
| [196] | a(aba)bbbabbbbbbbbbbb |
| [139] | ⇒ abbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)abbbbbbbbbbb |
| [204] | ⇒ abbbbbbbbbbbbb(baa)bbbbbbbbbbb |
| [123] | ⇒ abbbbbbbbbbbb(babbbbbbbbbbbbba)bbbbbbbbbbbbbb |
| [139] | ⇒ abbbbbbbbbbbbabbba(bbbbbbbbbbbbbbb)bbbbbbbbbb |
| [136] | ⇒ abbbbbbbbb(bbbabbba)bbbbbbbbbb |
| [188] | ⇒ a(bbbbbbbbbabbbbbbbbbba)bbbbbbbbbbbbbbbbbbbbb |
| [139] | ⇒ abbabbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)bbbbbbbbb |
| ⇒ abbabbbbbbbbbbbbbbabbbbbbbbb |
Reduce RHS:
| [182] | bbbbbbbbbbb(bbabbabbbbbbbbbba) |
| [139] | ⇒ (bbbbbbbbbbbbbbb)bbbbbbbbbbabbabbbbbbbb |
| ⇒ bbbbbbbbbbabbabbbbbbbb |
Referenced by [244].
Overlap of [232] aabbabbb=bbbbbbbbbbbbbabba with [139] bbbbbbbbbbbbbbb=1:
Critical pair: aabba=bbbbbbbbbbbbbabbabbbbbbbbbbbb.
Defines rule #17.
Overlap of [1] aaa=1 with [233] aabbbbba=bbabbbbbbbbbbbbab:
Critical pair: abbabbbbbbbbbbbbab=bbbbba.
Referenced by [246], [247], [248], [249].
Overlap of [233] aabbbbba=bbabbbbbbbbbbbbab with [230] abbbbbbbbabba=bbabbab:
Critical pair: aabbbbbbbabbab=bbabbbbbbbbbbbbabbbbbbbbbabba.
Reduce LHS:
| [168] | (aabbbbbbbabba)b |
| ⇒ abbbbabbbbbbbbbbb |
Reduce RHS:
| [216] | bbabbbb(bbbbbbbbabbbbbbbbba)bba |
| [139] | ⇒ bbabbbbabbbba(bbbbbbbbbbbbbbb)a |
| [142] | ⇒ bb(abbbbabbbba)a |
| ⇒ bbbbbbbabbbbbbbba |
Flip LHS and RHS.
Referenced by [249].
Overlap of [212] bbabbbbbbbbbbbabbbba=abbabbbbbbbbbbbbbbab with [217] bbbbbbbbbbbabbbba=bbbabbbbbbbbabbbb:
Critical pair: bbabbbabbbbbbbbabbbb=abbabbbbbbbbbbbbbbab.
Reduce LHS:
| [152] | b(babbbabbbbbbbbab)bbb |
| [204] | ⇒ (baa)bbbbbbbbbbabbbbbb |
| [123] | ⇒ abbbbbbbbbbbb(babbbbbbbbbbbbba)bbbbbb |
| [139] | ⇒ abbbbbbbbbbbbabbba(bbbbbbbbbbbbbbb)bb |
| [136] | ⇒ abbbbbbbbb(bbbabbba)bb |
| [188] | ⇒ a(bbbbbbbbbabbbbbbbbbba)bbbbbbbbbbbbb |
| [240] | ⇒ (abbabbbbbbbbbbbbbbabbbbbbbbb)bbbbbbb |
| [139] | ⇒ bbbbbbbbbbabba(bbbbbbbbbbbbbbb) |
| ⇒ bbbbbbbbbbabba |
Flip LHS and RHS.
Overlap of [197] bbbabbabbbbbabbb=abbbbbabbbbbbbba with [235] abbabbbbba=bbbbbabbbbbbbbbbabb:
Critical pair: bbbbbbbbabbbbbbbbbbabbbbb=abbbbbabbbbbbbba.
Reduce LHS:
| [223] | (bbbbbbbbabbbbbbbbbba)bbbbb |
| ⇒ babbbbbbbbbbbbbbabbbbbbbb |
Flip LHS and RHS.
Referenced by [256].
Overlap of [201] aabbbbbbbbbbbbbba=babbb with [242] abbabbbbbbbbbbbbab=bbbbba:
Critical pair: aabbbbbbbbbbbbbbbbbbba=babbbbbabbbbbbbbbbbbab.
Reduce LHS:
| [139] | aa(bbbbbbbbbbbbbbb)bbbba |
| ⇒ aabbbba |
Reduce RHS:
| [238] | b(abbbbbabbbbbbbbbbbba)b |
| ⇒ bbbbbbbabbabbbbb |
Defines rule #19.
Referenced by [260].
Overlap of [242] abbabbbbbbbbbbbbab=bbbbba with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: abbabbbbbbbbbbbabbbabbbbbbbbbbb=bbbbbabbbbbbbbbbbba.
Reduce LHS:
| [213] | abb(abbbbbbbbbbba)bbbabbbbbbbbbbb |
| [139] | ⇒ abbbbbbbbbba(bbbbbbbbbbbbbbb)babbbbbbbbbbb |
| [196] | ⇒ abbbbbbbbbb(aba)bbbbbbbbbbb |
| [139] | ⇒ a(bbbbbbbbbbbbbbb)bbbbbbbbbabbbbbbbbbbbbbbbbbbbbbbb |
| [139] | ⇒ abbbbbbbbba(bbbbbbbbbbbbbbb)bbbbbbbb |
| ⇒ abbbbbbbbbabbbbbbbb |
Flip LHS and RHS.
Defines rule #14.
Referenced by [266].
Overlap of [242] abbabbbbbbbbbbbbab=bbbbba with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbabbbbbbbbbbbba=bbbbbabbbbbbbbbbbbbb.
Defines rule #33.
Overlap of [242] abbabbbbbbbbbbbbab=bbbbba with [237] babbbbbbbbba=abbbbbbbbabb:
Critical pair: abbabbbbbbbbbbbabbbbbbbbabb=bbbbbabbbbbbbba.
Reduce LHS:
| [243] | abbabbbb(bbbbbbbabbbbbbbba)bb |
| [150] | ⇒ (abbabbbbabbb)babbbbbbbbbbbbb |
| [237] | ⇒ bbbbb(babbbbbbbbba)bbbbbbbbbbbbb |
| [239] | ⇒ (bbbbbabbbbbbbbabbbbbb)bbbbbbbbb |
| [139] | ⇒ abbbbbbba(bbbbbbbbbbbbbbb)bbbbbb |
| ⇒ abbbbbbbabbbbbb |
Flip LHS and RHS.
Defines rule #13.
Referenced by [256], [257], [263], [266].
Overlap of [131] abbbabba=babbbbbbbbbbabbbb with [123] babbbbbbbbbbbbba=abbbabbbbbbbbbbb:
Critical pair: abbbababbbabbbbbbbbbbb=babbbbbbbbbbabbbbbbbbbbbbbbbbba.
Reduce LHS:
| [196] | abbb(aba)bbbabbbbbbbbbbb |
| [139] | ⇒ a(bbbbbbbbbbbbbbb)bbabbbbbbbbbbbbbbbabbbbbbbbbbb |
| [139] | ⇒ abba(bbbbbbbbbbbbbbb)abbbbbbbbbbb |
| [204] | ⇒ ab(baa)bbbbbbbbbbb |
| [123] | ⇒ a(babbbbbbbbbbbbba)bbbbbbbbbbbbbb |
| [139] | ⇒ aabbba(bbbbbbbbbbbbbbb)bbbbbbbbbb |
| [101] | ⇒ (aabbba)bbbbbbbbbb |
| [139] | ⇒ bbabbba(bbbbbbbbbbbbbbb)bbb |
| ⇒ bbabbbabbb |
Reduce RHS:
| [139] | babbbbbbbbbba(bbbbbbbbbbbbbbb)bba |
| ⇒ babbbbbbbbbbabba |
Flip LHS and RHS.
Overlap of [139] bbbbbbbbbbbbbbb=1 with [229] bbabbabbbba=bbbbbbbbabbbbb:
Critical pair: bbbbbbbbbbbbbbbbbbbbbabbbbb=abbabbbba.
Reduce LHS:
| [139] | (bbbbbbbbbbbbbbb)bbbbbbabbbbb |
| ⇒ bbbbbbabbbbb |
Flip LHS and RHS.
Referenced by [252].
Overlap of [1] aaa=1 with [251] abbabbbba=bbbbbbabbbbb:
Critical pair: aabbbbbbabbbbb=bbabbbba.
Reduce LHS:
| [144] | a(abbbbbba)bbbbb |
| ⇒ abbbbbbbbbbbbabbbbbbbbb |
Flip LHS and RHS.
Defines rule #8.
Referenced by [266].
Overlap of [139] bbbbbbbbbbbbbbb=1 with [199] babbbbabbbbbbbba=bbbbabbabb:
Critical pair: bbbbbbbbbbbbbbbbbbabbabb=abbbbabbbbbbbba.
Reduce LHS:
| [139] | (bbbbbbbbbbbbbbb)bbbabbabb |
| ⇒ bbbabbabb |
Flip LHS and RHS.
Defines rule #40.
Referenced by [254].
Overlap of [253] abbbbabbbbbbbba=bbbabbabb with [230] abbbbbbbbabba=bbabbab:
Critical pair: abbbbabbbbbbbbbbabbab=bbbabbabbbbbbbbbbabba.
Reduce LHS:
| [227] | (abbbbabbbbbbbbbba)bbab |
| [215] | ⇒ b(abbabbbbbbbbab) |
| ⇒ bbbbbbbbbbbbabbabbbbbbbb |
Reduce RHS:
| [250] | bbbab(babbbbbbbbbbabba) |
| [136] | ⇒ (bbbabbba)bbbabbb |
| [200] | ⇒ abbbbbbb(bbbabbbbbbbbbbbbbba)bbb |
| [204] | ⇒ abbbbbb(baa)bbbbb |
| [123] | ⇒ abbbbb(babbbbbbbbbbbbba)bbbbbbbb |
| [139] | ⇒ abbbbbabbba(bbbbbbbbbbbbbbb)bbbb |
| [136] | ⇒ abb(bbbabbba)bbbb |
| [139] | ⇒ abbabbbbbbbbbba(bbbbbbbbbbbbbbb) |
| ⇒ abbabbbbbbbbbba |
Flip LHS and RHS.
Defines rule #32.
Overlap of [139] bbbbbbbbbbbbbbb=1 with [250] babbbbbbbbbbabba=bbabbbabbb:
Critical pair: bbbbbbbbbbbbbbbbabbbabbb=abbbbbbbbbbabba.
Reduce LHS:
| [139] | (bbbbbbbbbbbbbbb)babbbabbb |
| ⇒ babbbabbb |
Flip LHS and RHS.
Defines rule #48.
Overlap of [245] abbbbbabbbbbbbba=babbbbbbbbbbbbbbabbbbbbbb with [249] bbbbbabbbbbbbba=abbbbbbbabbbbbb:
Critical pair: aabbbbbbbabbbbbb=babbbbbbbbbbbbbbabbbbbbbb.
Referenced by [257].
Overlap of [125] aabbbbbbbbbbbbba=babbbbabbb with [235] abbabbbbba=bbbbbabbbbbbbbbbabb:
Critical pair: aabbbbbbbbbbbbbbbbbbabbbbbbbbbbabb=babbbbabbbbbabbbbba.
Reduce LHS:
| [139] | aa(bbbbbbbbbbbbbbb)bbbabbbbbbbbbbabb |
| [101] | ⇒ (aabbba)bbbbbbbbbbabb |
| [139] | ⇒ bbabbba(bbbbbbbbbbbbbbb)bbbabb |
| [136] | ⇒ bba(bbbabbba)bb |
| [204] | ⇒ b(baa)bbbbbbbbbbabbbbbbbbbbbbb |
| [123] | ⇒ (babbbbbbbbbbbbba)bbbbbbbbbbbbbabbbbbbbbbbbbb |
| [139] | ⇒ abbba(bbbbbbbbbbbbbbb)bbbbbbbbbabbbbbbbbbbbbb |
| [237] | ⇒ abb(babbbbbbbbba)bbbbbbbbbbbbb |
| [139] | ⇒ abbabbbbbbbba(bbbbbbbbbbbbbbb) |
| ⇒ abbabbbbbbbba |
Reduce RHS:
| [137] | bab(bbbabbbbba)bbbbba |
| [249] | ⇒ baba(bbbbbabbbbbbbba) |
| [256] | ⇒ bab(aabbbbbbbabbbbbb) |
| [244] | ⇒ b(abbabbbbbbbbbbbbbbab)bbbbbbb |
| ⇒ bbbbbbbbbbbabbabbbbbbb |
Defines rule #31.
Overlap of [160] abbbbabbab=babbbbbabbbbbbbbbbb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbbbabba=babbbbbabbbbbbbbbbbbbbbbbbbbbbbbb.
Reduce RHS:
| [139] | babbbbba(bbbbbbbbbbbbbbb)bbbbbbbbbb |
| ⇒ babbbbbabbbbbbbbbb |
Defines rule #39.
Overlap of [201] aabbbbbbbbbbbbbba=babbb with [258] abbbbabba=babbbbbabbbbbbbbbb:
Critical pair: aabbbbbbbbbbbbbbbabbbbbabbbbbbbbbb=babbbbbbbabba.
Reduce LHS:
| [139] | aa(bbbbbbbbbbbbbbb)abbbbbabbbbbbbbbb |
| [1] | ⇒ (aaa)bbbbbabbbbbbbbbb |
| ⇒ bbbbbabbbbbbbbbb |
Flip LHS and RHS.
Referenced by [260].
Overlap of [259] babbbbbbbabba=bbbbbabbbbbbbbbb with [258] abbbbabba=babbbbbabbbbbbbbbb:
Critical pair: babbbbbbbabbbabbbbbabbbbbbbbbb=bbbbbabbbbbbbbbbbbbbabba.
Reduce LHS:
| [137] | babbbbbbba(bbbabbbbba)bbbbbbbbbb |
| [233] | ⇒ babbbbbbb(aabbbbba)bbbbbbbbbbbbb |
| [237] | ⇒ (babbbbbbbbba)bbbbbbbbbbbbabbbbbbbbbbbbbb |
| [200] | ⇒ abbbbb(bbbabbbbbbbbbbbbbba)bbbbbbbbbbbbbb |
| [139] | ⇒ abbbbbaa(bbbbbbbbbbbbbbb)b |
| [204] | ⇒ abbbb(baa)b |
| [123] | ⇒ abbb(babbbbbbbbbbbbba)bbbb |
| [139] | ⇒ abbbabbba(bbbbbbbbbbbbbbb) |
| [136] | ⇒ a(bbbabbba) |
| ⇒ aabbbbbbbbbbabbbbbbbbbbb |
Reduce RHS:
| [200] | bb(bbbabbbbbbbbbbbbbba)bba |
| [246] | ⇒ bb(aabbbba) |
| ⇒ bbbbbbbbbabbabbbbb |
Referenced by [262].
Overlap of [1] aaa=1 with [168] aabbbbbbbabba=abbbbabbbbbbbbbb:
Critical pair: aaabbbbabbbbbbbbbb=abbbbbbbabba.
Reduce LHS:
| [1] | (aaa)bbbbabbbbbbbbbb |
| ⇒ bbbbabbbbbbbbbb |
Flip LHS and RHS.
Defines rule #45.
Overlap of [168] aabbbbbbbabba=abbbbabbbbbbbbbb with [85] abbabbba=bbbabbbbbbb:
Critical pair: aabbbbbbbbbbabbbbbbb=abbbbabbbbbbbbbbbbba.
Reduce RHS:
| [123] | abbb(babbbbbbbbbbbbba) |
| [136] | ⇒ a(bbbabbba)bbbbbbbbbbb |
| [260] | ⇒ (aabbbbbbbbbbabbbbbbbbbbb)bbbbbbbbbbb |
| [139] | ⇒ bbbbbbbbbabba(bbbbbbbbbbbbbbb)b |
| ⇒ bbbbbbbbbabbab |
Referenced by [263].
Overlap of [200] bbbabbbbbbbbbbbbbba=aabb with [249] bbbbbabbbbbbbba=abbbbbbbabbbbbb:
Critical pair: bbbabbbbbbbbbabbbbbbbabbbbbb=aabbbbbbbbbba.
Reduce LHS:
| [237] | bb(babbbbbbbbba)bbbbbbbabbbbbb |
| [237] | ⇒ bbabbbbbbb(babbbbbbbbba)bbbbbb |
| [228] | ⇒ (bbabbbbbbba)bbbbbbbbabbbbbbbb |
| [123] | ⇒ abbb(babbbbbbbbbbbbba)bbbbbbbb |
| [139] | ⇒ abbbabbba(bbbbbbbbbbbbbbb)bbbb |
| [136] | ⇒ a(bbbabbba)bbbb |
| [262] | ⇒ (aabbbbbbbbbbabbbbbbb)bbbbbbbb |
| ⇒ bbbbbbbbbabbabbbbbbbbb |
Flip LHS and RHS.
Defines rule #24.
Referenced by [269].
Overlap of [196] aba=bbbbbbbbbbbbbbabbbbbbbbbbbb with [231] abbbabbbbbbbbabbbb=bbbbbbbbabba:
Critical pair: abbbbbbbbbabba=bbbbbbbbbbbbbbabbbbbbbbbbbbbbbabbbbbbbbabbbb.
Reduce RHS:
| [139] | bbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)abbbbbbbbabbbb |
| [236] | ⇒ bbbbbbbbbbbbbb(aabbbbbbbba)bbbb |
| [139] | ⇒ (bbbbbbbbbbbbbbb)bbbbbbbbbbabbbbbb |
| ⇒ bbbbbbbbbbabbbbbb |
Defines rule #47.
Overlap of [231] abbbabbbbbbbbabbbb=bbbbbbbbabba with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbbabbbbbbbba=bbbbbbbbabbabbbbbbbbbbb.
Defines rule #36.
Overlap of [249] bbbbbabbbbbbbba=abbbbbbbabbbbbb with [252] bbabbbba=abbbbbbbbbbbbabbbbbbbbb:
Critical pair: bbbbbabbbbbbabbbbbbbbbbbbabbbbbbbbb=abbbbbbbabbbbbbbbbba.
Reduce LHS:
| [247] | bbbbbab(bbbbbabbbbbbbbbbbba)bbbbbbbbb |
| [237] | ⇒ bbbbba(babbbbbbbbba)bbbbbbbbbbbbbbbbb |
| [139] | ⇒ bbbbbaabbbbbbbba(bbbbbbbbbbbbbbb)bbbb |
| [236] | ⇒ bbbbb(aabbbbbbbba)bbbb |
| [139] | ⇒ (bbbbbbbbbbbbbbb)babbbbbb |
| ⇒ babbbbbb |
Flip LHS and RHS.
Referenced by [267].
Overlap of [1] aaa=1 with [266] abbbbbbbabbbbbbbbbba=babbbbbb:
Critical pair: aababbbbbb=bbbbbbbabbbbbbbbbba.
Reduce LHS:
| [196] | a(aba)bbbbbb |
| [139] | ⇒ abbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)bbb |
| ⇒ abbbbbbbbbbbbbbabbb |
Flip LHS and RHS.
Defines rule #15.
Referenced by [269].
Overlap of [244] abbabbbbbbbbbbbbbbab=bbbbbbbbbbabba with [139] bbbbbbbbbbbbbbb=1:
Critical pair: abbabbbbbbbbbbbbbba=bbbbbbbbbbabbabbbbbbbbbbbbbb.
Defines rule #34.
Overlap of [263] aabbbbbbbbbba=bbbbbbbbbabbabbbbbbbbb with [144] abbbbbba=bbbbbbbbbbbbabbbb:
Critical pair: aabbbbbbbbbbbbbbbbbbbbbbabbbb=bbbbbbbbbabbabbbbbbbbbbbbbbba.
Reduce LHS:
| [139] | aa(bbbbbbbbbbbbbbb)bbbbbbbabbbb |
| ⇒ aabbbbbbbabbbb |
Reduce RHS:
| [139] | bbbbbbbbbabba(bbbbbbbbbbbbbbb)a |
| [204] | ⇒ bbbbbbbbbab(baa) |
| [123] | ⇒ bbbbbbbbba(babbbbbbbbbbbbba)bbb |
| [101] | ⇒ bbbbbbbbb(aabbba)bbbbbbbbbbbbbb |
| [139] | ⇒ bbbbbbbbbbbabbba(bbbbbbbbbbbbbbb)bbbbbbb |
| [136] | ⇒ bbbbbbbb(bbbabbba)bbbbbbb |
| [267] | ⇒ b(bbbbbbbabbbbbbbbbba)bbbbbbbbbbbbbbbbbb |
| [139] | ⇒ babbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)bbbbbb |
| ⇒ babbbbbbbbbbbbbbabbbbbb |
Referenced by [270].
Overlap of [269] aabbbbbbbabbbb=babbbbbbbbbbbbbbabbbbbb with [139] bbbbbbbbbbbbbbb=1:
Critical pair: aabbbbbbba=babbbbbbbbbbbbbbabbbbbbbbbbbbbbbbb.
Reduce RHS:
| [139] | babbbbbbbbbbbbbba(bbbbbbbbbbbbbbb)bb |
| ⇒ babbbbbbbbbbbbbbabb |
Defines rule #21.