| Back: | ⟨a, b | abaaaab=b⟩ |
|---|
Completion settings:
Axiom: abaaaab=b.
Referenced by [2], [3], [4], [5], [6].
Overlap of [1] abaaaab=b with [1] abaaaab=b:
Critical pair: abaaab=baaaab.
Flip LHS and RHS.
Overlap of [2] baaaab=abaaab with [1] abaaaab=b:
Critical pair: baaab=abaaabaaaab.
Reduce RHS:
| [1] | abaa(abaaaab) |
| ⇒ abaab |
Referenced by [4], [6], [7], [8].
Overlap of [3] baaab=abaab with [1] abaaaab=b:
Critical pair: baab=abaabaaaab.
Reduce RHS:
| [1] | aba(abaaaab) |
| ⇒ abab |
Referenced by [5], [6], [7], [8], [9].
Overlap of [4] baab=abab with [1] abaaaab=b:
Critical pair: bab=ababaaaab.
Reduce RHS:
| [1] | ab(abaaaab) |
| ⇒ abb |
Defines rule #1.
Referenced by [6], [7], [8], [9].
Overlap of [1] abaaaab=b with [2] baaaab=abaaab:
Critical pair: aabaaab=b.
Reduce LHS:
| [3] | aa(baaab) |
| [4] | ⇒ aaa(baab) |
| [5] | ⇒ aaaa(bab) |
| ⇒ aaaaabb |
Defines rule #5.
Simplify [2] baaaab=abaaab.
Reduce RHS:
| [3] | a(baaab) |
| [4] | ⇒ aa(baab) |
| [5] | ⇒ aaa(bab) |
| ⇒ aaaabb |
Defines rule #4.
Simplify [3] baaab=abaab.
Reduce RHS:
| [4] | a(baab) |
| [5] | ⇒ aa(bab) |
| ⇒ aaabb |
Defines rule #3.
Simplify [4] baab=abab.
Reduce RHS:
| [5] | a(bab) |
| ⇒ aabb |
Defines rule #2.