| Back: | ⟨a, b | abaaaaab=b⟩ |
|---|
Completion settings:
Axiom: abaaaaab=b.
Referenced by [2], [3], [4], [5], [6], [7].
Overlap of [1] abaaaaab=b with [1] abaaaaab=b:
Critical pair: abaaaab=baaaaab.
Flip LHS and RHS.
Overlap of [2] baaaaab=abaaaab with [1] abaaaaab=b:
Critical pair: baaaab=abaaaabaaaaab.
Reduce RHS:
| [1] | abaaa(abaaaaab) |
| ⇒ abaaab |
Referenced by [4], [7], [8], [9].
Overlap of [3] baaaab=abaaab with [1] abaaaaab=b:
Critical pair: baaab=abaaabaaaaab.
Reduce RHS:
| [1] | abaa(abaaaaab) |
| ⇒ abaab |
Referenced by [5], [7], [8], [9], [10].
Overlap of [4] baaab=abaab with [1] abaaaaab=b:
Critical pair: baab=abaabaaaaab.
Reduce RHS:
| [1] | aba(abaaaaab) |
| ⇒ abab |
Referenced by [6], [7], [8], [9], [10], [11].
Overlap of [5] baab=abab with [1] abaaaaab=b:
Critical pair: bab=ababaaaaab.
Reduce RHS:
| [1] | ab(abaaaaab) |
| ⇒ abb |
Defines rule #1.
Referenced by [7], [8], [9], [10], [11].
Overlap of [1] abaaaaab=b with [2] baaaaab=abaaaab:
Critical pair: aabaaaab=b.
Reduce LHS:
| [3] | aa(baaaab) |
| [4] | ⇒ aaa(baaab) |
| [5] | ⇒ aaaa(baab) |
| [6] | ⇒ aaaaa(bab) |
| ⇒ aaaaaabb |
Defines rule #6.
Simplify [2] baaaaab=abaaaab.
Reduce RHS:
| [3] | a(baaaab) |
| [4] | ⇒ aa(baaab) |
| [5] | ⇒ aaa(baab) |
| [6] | ⇒ aaaa(bab) |
| ⇒ aaaaabb |
Defines rule #5.
Simplify [3] baaaab=abaaab.
Reduce RHS:
| [4] | a(baaab) |
| [5] | ⇒ aa(baab) |
| [6] | ⇒ aaa(bab) |
| ⇒ aaaabb |
Defines rule #4.
Simplify [4] baaab=abaab.
Reduce RHS:
| [5] | a(baab) |
| [6] | ⇒ aa(bab) |
| ⇒ aaabb |
Defines rule #3.
Simplify [5] baab=abab.
Reduce RHS:
| [6] | a(bab) |
| ⇒ aabb |
Defines rule #2.