| Back: | ⟨a, b | aaa=1, baab=abbb⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #1.
Referenced by [3], [4], [6], [9].
Axiom: baab=abbb.
Defines rule #2.
Referenced by [3], [5], [7], [8], [10].
Overlap of [2] baab=abbb with [2] baab=abbb:
Critical pair: baaabbb=abbbaab.
Reduce LHS:
| [1] | b(aaa)bbb |
| ⇒ bbbb |
Reduce RHS:
| [2] | abb(baab) |
| ⇒ abbabbb |
Flip LHS and RHS.
Overlap of [1] aaa=1 with [3] abbabbb=bbbb:
Critical pair: aabbbb=bbabbb.
Flip LHS and RHS.
Defines rule #3.
Overlap of [2] baab=abbb with [3] abbabbb=bbbb:
Critical pair: babbbb=abbbbabbb.
Reduce RHS:
| [4] | abb(bbabbb) |
| [2] | ⇒ ab(baab)bbb |
| ⇒ ababbbbbb |
Flip LHS and RHS.
Overlap of [1] aaa=1 with [5] ababbbbbb=babbbb:
Critical pair: aababbbb=babbbbbb.
Flip LHS and RHS.
Defines rule #4.
Referenced by [8].
Overlap of [2] baab=abbb with [5] ababbbbbb=babbbb:
Critical pair: bababbbb=abbbabbbbbb.
Reduce RHS:
| [4] | ab(bbabbb)bbb |
| [2] | ⇒ a(baab)bbbbbb |
| ⇒ aabbbbbbbbb |
Flip LHS and RHS.
Overlap of [6] babbbbbb=aababbbb with [4] bbabbb=aabbbb:
Critical pair: babbbbaabbbb=aababbbbabbb.
Reduce LHS:
| [2] | babbb(baab)bbb |
| [4] | ⇒ bab(bbabbb)bbb |
| [2] | ⇒ ba(baab)bbbbbb |
| [2] | ⇒ (baab)bbbbbbbb |
| ⇒ abbbbbbbbbbb |
Reduce RHS:
| [4] | aababb(bbabbb) |
| [2] | ⇒ aabab(baab)bbb |
| [5] | ⇒ aab(ababbbbbb) |
| [3] | ⇒ a(abbabbb)b |
| ⇒ abbbbb |
Referenced by [10].
Overlap of [1] aaa=1 with [7] aabbbbbbbbb=bababbbb:
Critical pair: abababbbb=bbbbbbbbb.
Flip LHS and RHS.
Defines rule #6.
Referenced by [11].
Overlap of [2] baab=abbb with [7] aabbbbbbbbb=bababbbb:
Critical pair: bbababbbb=abbbbbbbbbbb.
Reduce RHS:
| [8] | (abbbbbbbbbbb) |
| ⇒ abbbbb |
Defines rule #5.
Overlap of [9] bbbbbbbbb=abababbbb with [9] bbbbbbbbb=abababbbb:
Critical pair: babababbbb=abababbbbb.
Defines rule #7.