| Back: | ⟨a, b | aabaaaaab=ab⟩ |
|---|
Completion settings:
Axiom: aabaaaaab=ab.
Referenced by [2], [3], [4], [5], [6].
Overlap of [1] aabaaaaab=ab with [1] aabaaaaab=ab:
Critical pair: aabaaaab=abaaaaab.
Flip LHS and RHS.
Overlap of [2] abaaaaab=aabaaaab with [1] aabaaaaab=ab:
Critical pair: abaaaab=aabaaaabaaaaab.
Reduce RHS:
| [1] | aabaa(aabaaaaab) |
| ⇒ aabaaab |
Referenced by [4], [6], [7], [8].
Overlap of [3] abaaaab=aabaaab with [1] aabaaaaab=ab:
Critical pair: abaaab=aabaaabaaaaab.
Reduce RHS:
| [1] | aaba(aabaaaaab) |
| ⇒ aabaab |
Referenced by [5], [6], [7], [8], [9].
Overlap of [4] abaaab=aabaab with [1] aabaaaaab=ab:
Critical pair: abaab=aabaabaaaaab.
Reduce RHS:
| [1] | aab(aabaaaaab) |
| ⇒ aabab |
Defines rule #1.
Referenced by [6], [7], [8], [9].
Overlap of [1] aabaaaaab=ab with [2] abaaaaab=aabaaaab:
Critical pair: aaabaaaab=ab.
Reduce LHS:
| [3] | aa(abaaaab) |
| [4] | ⇒ aaa(abaaab) |
| [5] | ⇒ aaaa(abaab) |
| ⇒ aaaaaabab |
Defines rule #5.
Simplify [2] abaaaaab=aabaaaab.
Reduce RHS:
| [3] | a(abaaaab) |
| [4] | ⇒ aa(abaaab) |
| [5] | ⇒ aaa(abaab) |
| ⇒ aaaaabab |
Defines rule #4.
Simplify [3] abaaaab=aabaaab.
Reduce RHS:
| [4] | a(abaaab) |
| [5] | ⇒ aa(abaab) |
| ⇒ aaaabab |
Defines rule #3.
Simplify [4] abaaab=aabaab.
Reduce RHS:
| [5] | a(abaab) |
| ⇒ aaabab |
Defines rule #2.