| Back: | ⟨a, b | bb=aa, abab=aba⟩ |
|---|
Completion settings:
Axiom: bb=aa.
Defines rule #5.
Referenced by [3], [4], [5], [11].
Axiom: abab=aba.
Referenced by [4], [5], [6], [8], [9].
Overlap of [1] bb=aa with [1] bb=aa:
Critical pair: baa=aab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [5], [6], [8], [10], [11].
Overlap of [2] abab=aba with [1] bb=aa:
Critical pair: abaaa=abab.
Reduce RHS:
| [2] | (abab) |
| ⇒ aba |
Referenced by [7].
Overlap of [2] abab=aba with [2] abab=aba:
Critical pair: ababa=abaab.
Reduce LHS:
| [2] | (abab)a |
| ⇒ abaa |
Reduce RHS:
| [3] | ab(aab) |
| [1] | ⇒ a(bb)aa |
| ⇒ aaaaa |
Overlap of [3] aab=baa with [2] abab=aba:
Critical pair: aaba=baaab.
Reduce LHS:
| [3] | (aab)a |
| ⇒ baaa |
Reduce RHS:
| [3] | ba(aab) |
| [5] | ⇒ b(abaa) |
| ⇒ baaaaa |
Flip LHS and RHS.
Referenced by [8].
Simplify [4] abaaa=aba.
Reduce LHS:
| [5] | (abaa)a |
| ⇒ aaaaaa |
Flip LHS and RHS.
Defines rule #3.
Referenced by [8], [9], [10], [11].
Overlap of [2] abab=aba with [7] aba=aaaaaa:
Critical pair: aaaaaab=aba.
Reduce LHS:
| [3] | aaaa(aab) |
| [3] | ⇒ aa(aab)aa |
| [3] | ⇒ (aab)aaaa |
| [6] | ⇒ (baaaaa)a |
| ⇒ baaaa |
Reduce RHS:
| [7] | (aba) |
| ⇒ aaaaaa |
Referenced by [9].
Overlap of [2] abab=aba with [7] aba=aaaaaa:
Critical pair: abaaaaaa=abaa.
Reduce LHS:
| [8] | a(baaaa)aa |
| ⇒ aaaaaaaaa |
Reduce RHS:
| [7] | (aba)a |
| ⇒ aaaaaaa |
Referenced by [11].
Overlap of [3] aab=baa with [7] aba=aaaaaa:
Critical pair: aaaaaaa=baaa.
Flip LHS and RHS.
Referenced by [12].
Overlap of [7] aba=aaaaaa with [3] aab=baa:
Critical pair: abbaa=aaaaaaab.
Reduce LHS:
| [1] | a(bb)aa |
| ⇒ aaaaa |
Reduce RHS:
| [3] | aaaaa(aab) |
| [3] | ⇒ aaa(aab)aa |
| [3] | ⇒ a(aab)aaaa |
| [7] | ⇒ (aba)aaaaa |
| [9] | ⇒ (aaaaaaaaa)aa |
| [9] | ⇒ (aaaaaaaaa) |
| ⇒ aaaaaaa |
Flip LHS and RHS.
Defines rule #1.
Referenced by [12].
Simplify [10] baaa=aaaaaaa.
Reduce RHS:
| [11] | (aaaaaaa) |
| ⇒ aaaaa |
Defines rule #2.