| Back: | ⟨a, b | aa=1, abbbbab=bb⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #4.
Referenced by [3], [5], [8], [9], [10].
Axiom: abbbbab=bb.
Overlap of [1] aa=1 with [2] abbbbab=bb:
Critical pair: abb=bbbbab.
Flip LHS and RHS.
Referenced by [4], [6], [7], [9].
Overlap of [2] abbbbab=bb with [2] abbbbab=bb:
Critical pair: abbbbbb=bbbbbab.
Reduce RHS:
| [3] | b(bbbbab) |
| ⇒ babb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [2] abbbbab=bb with [4] babb=abbbbbb:
Critical pair: abbbabbbbbb=bbb.
Reduce LHS:
| [4] | abb(babb)bbbb |
| [4] | ⇒ ab(babb)bbbbbbbb |
| [4] | ⇒ a(babb)bbbbbbbbbbbb |
| [1] | ⇒ (aa)bbbbbbbbbbbbbbbbbb |
| ⇒ bbbbbbbbbbbbbbbbbb |
Overlap of [5] bbbbbbbbbbbbbbbbbb=bbb with [3] bbbbab=abb:
Critical pair: bbbbbbbbbbbbbbabb=bbbab.
Reduce LHS:
| [3] | bbbbbbbbbb(bbbbab)b |
| [3] | ⇒ bbbbbb(bbbbab)bb |
| [3] | ⇒ bb(bbbbab)bbb |
| [4] | ⇒ b(babb)bbb |
| [4] | ⇒ (babb)bbbbbbb |
| ⇒ abbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [7].
Overlap of [5] bbbbbbbbbbbbbbbbbb=bbb with [6] bbbab=abbbbbbbbbbbbb:
Critical pair: bbbbbbbbbbbbbbbbabbbbbbbbbbbbb=bbbbab.
Reduce LHS:
| [3] | bbbbbbbbbbbb(bbbbab)bbbbbbbbbbbb |
| [3] | ⇒ bbbbbbbb(bbbbab)bbbbbbbbbbbbb |
| [3] | ⇒ bbbb(bbbbab)bbbbbbbbbbbbbb |
| [3] | ⇒ (bbbbab)bbbbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbbbbbb |
Reduce RHS:
| [3] | (bbbbab) |
| ⇒ abb |
Overlap of [1] aa=1 with [7] abbbbbbbbbbbbbbbbb=abb:
Critical pair: aabb=bbbbbbbbbbbbbbbbb.
Reduce LHS:
| [1] | (aa)bb |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [7] abbbbbbbbbbbbbbbbb=abb with [3] bbbbab=abb:
Critical pair: abbbbbbbbbbbbbabb=abbab.
Reduce LHS:
| [3] | abbbbbbbbb(bbbbab)b |
| [3] | ⇒ abbbbb(bbbbab)bb |
| [3] | ⇒ ab(bbbbab)bbb |
| [4] | ⇒ a(babb)bbb |
| [1] | ⇒ (aa)bbbbbbbbb |
| ⇒ bbbbbbbbb |
Flip LHS and RHS.
Referenced by [10].
Overlap of [1] aa=1 with [9] abbab=bbbbbbbbb:
Critical pair: abbbbbbbbb=bbab.
Flip LHS and RHS.
Defines rule #3.