| Back: | ⟨a, b | aaab=a, babbb=a⟩ |
|---|
Completion settings:
Axiom: aaab=a.
Referenced by [3], [5], [6], [7], [10], [15].
Axiom: babbb=a.
Referenced by [3], [4], [5], [7], [8], [10].
Overlap of [1] aaab=a with [2] babbb=a:
Critical pair: aaaa=aabbb.
Flip LHS and RHS.
Overlap of [2] babbb=a with [2] babbb=a:
Critical pair: babba=aabbb.
Reduce RHS:
| [3] | (aabbb) |
| ⇒ aaaa |
Overlap of [4] babba=aaaa with [2] babbb=a:
Critical pair: baba=aaaabbb.
Reduce RHS:
| [1] | a(aaab)bb |
| ⇒ aabb |
Flip LHS and RHS.
Overlap of [1] aaab=a with [5] aabb=baba:
Critical pair: ababa=ab.
Referenced by [10], [11], [12], [13].
Overlap of [4] babba=aaaa with [5] aabb=baba:
Critical pair: babbbaba=aaaaabb.
Reduce LHS:
| [2] | (babbb)aba |
| ⇒ aaba |
Reduce RHS:
| [1] | aa(aaab)b |
| [1] | ⇒ (aaab) |
| ⇒ a |
Referenced by [8], [9], [12], [13].
Overlap of [7] aaba=a with [2] babbb=a:
Critical pair: aaa=abbb.
Flip LHS and RHS.
Referenced by [10].
Overlap of [7] aaba=a with [4] babba=aaaa:
Critical pair: aaaaaa=abba.
Flip LHS and RHS.
Referenced by [11].
Overlap of [6] ababa=ab with [2] babbb=a:
Critical pair: abaa=abbbb.
Reduce RHS:
| [8] | (abbb)b |
| [1] | ⇒ (aaab) |
| ⇒ a |
Overlap of [6] ababa=ab with [6] ababa=ab:
Critical pair: abab=abba.
Reduce RHS:
| [9] | (abba) |
| ⇒ aaaaaa |
Referenced by [13].
Overlap of [7] aaba=a with [6] ababa=ab:
Critical pair: aab=aba.
Referenced by [13].
Overlap of [7] aaba=a with [6] ababa=ab:
Critical pair: aabab=ababa.
Reduce LHS:
| [12] | (aab)ab |
| [10] | ⇒ (abaa)b |
| ⇒ ab |
Reduce RHS:
| [11] | (abab)a |
| ⇒ aaaaaaa |
Defines rule #3.
Simplify [10] abaa=a.
Reduce LHS:
| [13] | (ab)aa |
| ⇒ aaaaaaaaa |
Defines rule #1.
Referenced by [16].
Simplify [3] aabbb=aaaa.
Reduce LHS:
| [5] | (aabb)b |
| [13] | ⇒ b(ab)ab |
| [1] | ⇒ baaaaa(aaab) |
| ⇒ baaaaaa |
Referenced by [16].
Overlap of [15] baaaaaa=aaaa with [14] aaaaaaaaa=a:
Critical pair: ba=aaaaaaa.
Defines rule #2.