| Back: | ⟨a, b | aa=1, ababbab=bb⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #4.
Referenced by [3], [6], [13], [14].
Axiom: ababbab=bb.
Overlap of [1] aa=1 with [2] ababbab=bb:
Critical pair: abb=babbab.
Flip LHS and RHS.
Referenced by [4], [5], [8], [9], [11].
Overlap of [3] babbab=abb with [2] ababbab=bb:
Critical pair: babbbb=abbabbab.
Reduce RHS:
| [3] | ab(babbab) |
| ⇒ ababb |
Flip LHS and RHS.
Defines rule #5.
Referenced by [5], [6], [7], [8], [11], [12], [14].
Overlap of [3] babbab=abb with [3] babbab=abb:
Critical pair: bababb=abbbab.
Reduce LHS:
| [4] | b(ababb) |
| ⇒ bbabbbb |
Flip LHS and RHS.
Defines rule #7.
Overlap of [1] aa=1 with [4] ababb=babbbb:
Critical pair: ababbbb=babb.
Reduce LHS:
| [4] | (ababb)bb |
| ⇒ babbbbbb |
Overlap of [2] ababbab=bb with [4] ababb=babbbb:
Critical pair: babbbbab=bb.
Referenced by [9], [10], [12], [13], [14].
Overlap of [3] babbab=abb with [4] ababb=babbbb:
Critical pair: babbbabbbb=abbabb.
Reduce LHS:
| [5] | b(abbbab)bbb |
| [6] | ⇒ bb(babbbbbb)b |
| ⇒ bbbabbb |
Flip LHS and RHS.
Referenced by [10], [11], [13].
Overlap of [7] babbbbab=bb with [3] babbab=abb:
Critical pair: babbbabb=bbbab.
Reduce LHS:
| [5] | b(abbbab)b |
| ⇒ bbbabbbbb |
Overlap of [8] abbabb=bbbabbb with [7] babbbbab=bb:
Critical pair: abbb=bbbabbbbbab.
Reduce RHS:
| [9] | (bbbabbbbb)ab |
| ⇒ bbbabab |
Flip LHS and RHS.
Referenced by [11], [12], [13], [15].
Overlap of [4] ababb=babbbb with [10] bbbabab=abbb:
Critical pair: abababbb=babbbbbbabab.
Reduce LHS:
| [4] | ab(ababb)b |
| [8] | ⇒ (abbabb)bbb |
| [9] | ⇒ (bbbabbbbb)b |
| ⇒ bbbabb |
Reduce RHS:
| [6] | (babbbbbb)abab |
| [3] | ⇒ (babbab)ab |
| ⇒ abbab |
Flip LHS and RHS.
Defines rule #6.
Referenced by [14].
Overlap of [7] babbbbab=bb with [10] bbbabab=abbb:
Critical pair: bababbb=bbab.
Reduce LHS:
| [4] | b(ababb)b |
| ⇒ bbabbbbb |
Defines rule #2.
Overlap of [8] abbabb=bbbabbb with [10] bbbabab=abbb:
Critical pair: abbaabbb=bbbabbbbabab.
Reduce LHS:
| [1] | abb(aa)bbb |
| ⇒ abbbbb |
Reduce RHS:
| [7] | bb(babbbbab)ab |
| ⇒ bbbbab |
Flip LHS and RHS.
Defines rule #3.
Referenced by [14].
Overlap of [4] ababb=babbbb with [11] abbab=bbbabb:
Critical pair: abbbbabb=babbbbab.
Reduce LHS:
| [13] | a(bbbbab)b |
| [1] | ⇒ (aa)bbbbbb |
| ⇒ bbbbbb |
Reduce RHS:
| [7] | (babbbbab) |
| ⇒ bb |
Defines rule #1.
Referenced by [15].
Overlap of [14] bbbbbb=bb with [10] bbbabab=abbb:
Critical pair: bbbabbb=bbabab.
Flip LHS and RHS.
Defines rule #8.