| Back: | ⟨a, b | aaa=1, abbbb=bab⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #4.
Referenced by [4].
Axiom: abbbb=bab.
Flip LHS and RHS.
Defines rule #2.
Overlap of [2] bab=abbbb with [2] bab=abbbb:
Critical pair: baabbbb=abbbbab.
Reduce RHS:
| [2] | abbb(bab) |
| [2] | ⇒ abb(bab)bbb |
| [2] | ⇒ ab(bab)bbbbbb |
| [2] | ⇒ a(bab)bbbbbbbbb |
| ⇒ aabbbbbbbbbbbbb |
Defines rule #3.
Referenced by [4].
Overlap of [2] bab=abbbb with [3] baabbbb=aabbbbbbbbbbbbb:
Critical pair: baaabbbbbbbbbbbbb=abbbbaabbbb.
Reduce LHS:
| [1] | b(aaa)bbbbbbbbbbbbb |
| ⇒ bbbbbbbbbbbbbb |
Reduce RHS:
| [3] | abbb(baabbbb) |
| [3] | ⇒ abb(baabbbb)bbbbbbbbb |
| [3] | ⇒ ab(baabbbb)bbbbbbbbbbbbbbbbbb |
| [3] | ⇒ a(baabbbb)bbbbbbbbbbbbbbbbbbbbbbbbbbb |
| [1] | ⇒ (aaa)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
| ⇒ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #1.