| Back: | ⟨a, b | aaa=1, bbbb=abab⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #10.
Referenced by [3].
Axiom: bbbb=abab.
Flip LHS and RHS.
Defines rule #6.
Referenced by [3], [4], [5], [6], [12].
Overlap of [1] aaa=1 with [2] abab=bbbb:
Critical pair: aabbbb=bab.
Defines rule #5.
Referenced by [5], [6], [7], [8], [9], [12], [13].
Overlap of [2] abab=bbbb with [2] abab=bbbb:
Critical pair: abbbbb=bbbbab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [5], [6], [7], [8], [9], [12].
Overlap of [2] abab=bbbb with [4] bbbbab=abbbbb:
Critical pair: abaabbbbb=bbbbbbbab.
Reduce LHS:
| [3] | ab(aabbbb)b |
| ⇒ abbabb |
Reduce RHS:
| [4] | bbb(bbbbab) |
| ⇒ bbbabbbbb |
Defines rule #7.
Overlap of [3] aabbbb=bab with [4] bbbbab=abbbbb:
Critical pair: aababbbbb=babbab.
Reduce LHS:
| [2] | a(abab)bbbb |
| ⇒ abbbbbbbb |
Flip LHS and RHS.
Defines rule #8.
Referenced by [9].
Overlap of [3] aabbbb=bab with [4] bbbbab=abbbbb:
Critical pair: aabbabbbbb=babbbab.
Reduce LHS:
| [5] | a(abbabb)bbb |
| ⇒ abbbabbbbbbbb |
Flip LHS and RHS.
Defines rule #9.
Referenced by [9].
Overlap of [3] aabbbb=bab with [4] bbbbab=abbbbb:
Critical pair: aabbbabbbbb=babbbbab.
Reduce RHS:
| [4] | ba(bbbbab) |
| [3] | ⇒ b(aabbbb)b |
| ⇒ bbabb |
Referenced by [9], [10], [11].
Overlap of [8] aabbbabbbbb=bbabb with [4] bbbbab=abbbbb:
Critical pair: aabbbabbbabbbbb=bbabbbbab.
Reduce LHS:
| [7] | aabb(babbbab)bbbb |
| [5] | ⇒ a(abbabb)babbbbbbbbbbbb |
| [4] | ⇒ abbbabb(bbbbab)bbbbbbbbbbb |
| [6] | ⇒ abb(babbab)bbbbbbbbbbbbbbb |
| [5] | ⇒ (abbabb)bbbbbbbbbbbbbbbbbbbbb |
| ⇒ bbbabbbbbbbbbbbbbbbbbbbbbbbbbb |
Reduce RHS:
| [4] | bba(bbbbab) |
| [3] | ⇒ bb(aabbbb)b |
| ⇒ bbbabb |
Referenced by [10].
Overlap of [8] aabbbabbbbb=bbabb with [9] bbbabbbbbbbbbbbbbbbbbbbbbbbbbb=bbbabb:
Critical pair: aabbbabb=bbabbbbbbbbbbbbbbbbbbbbbbb.
Defines rule #11.
Overlap of [8] aabbbabbbbb=bbabb with [10] aabbbabb=bbabbbbbbbbbbbbbbbbbbbbbbb:
Critical pair: bbabbbbbbbbbbbbbbbbbbbbbbbbbb=bbabb.
Defines rule #3.
Overlap of [10] aabbbabb=bbabbbbbbbbbbbbbbbbbbbbbbb with [4] bbbbab=abbbbb:
Critical pair: aabbbaabbbbb=bbabbbbbbbbbbbbbbbbbbbbbbbbbab.
Reduce LHS:
| [3] | aabbb(aabbbb)b |
| [3] | ⇒ (aabbbb)abb |
| [2] | ⇒ b(abab)b |
| ⇒ bbbbbb |
Reduce RHS:
| [4] | bbabbbbbbbbbbbbbbbbbbbbb(bbbbab) |
| [4] | ⇒ bbabbbbbbbbbbbbbbbbb(bbbbab)bbbb |
| [4] | ⇒ bbabbbbbbbbbbbbb(bbbbab)bbbbbbbb |
| [4] | ⇒ bbabbbbbbbbb(bbbbab)bbbbbbbbbbbb |
| [4] | ⇒ bbabbbbb(bbbbab)bbbbbbbbbbbbbbbb |
| [4] | ⇒ bbab(bbbbab)bbbbbbbbbbbbbbbbbbbb |
| [2] | ⇒ bb(abab)bbbbbbbbbbbbbbbbbbbbbbbb |
| ⇒ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #1.
Referenced by [13].
Overlap of [3] aabbbb=bab with [12] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bbbbbb:
Critical pair: aabbbbbb=babbbbbbbbbbbbbbbbbbbbbbbbbbb.
Reduce LHS:
| [3] | (aabbbb)bb |
| ⇒ babbb |
Flip LHS and RHS.
Defines rule #2.