| Back: | ⟨a, b | bab=aba, bba=aa⟩ |
|---|
Completion settings:
Axiom: bab=aba.
Defines rule #5.
Referenced by [3], [4], [6], [8], [10].
Axiom: bba=aa.
Defines rule #4.
Referenced by [3], [4], [6], [7].
Overlap of [1] bab=aba with [2] bba=aa:
Critical pair: baaa=ababa.
Reduce RHS:
| [1] | a(bab)a |
| ⇒ aabaa |
Flip LHS and RHS.
Referenced by [5].
Overlap of [2] bba=aa with [1] bab=aba:
Critical pair: baba=aab.
Reduce LHS:
| [1] | (bab)a |
| ⇒ abaa |
Flip LHS and RHS.
Defines rule #3.
Simplify [3] aabaa=baaa.
Reduce LHS:
| [4] | (aab)aa |
| ⇒ abaaaa |
Referenced by [6], [7], [8], [9], [11].
Overlap of [1] bab=aba with [5] abaaaa=baaa:
Critical pair: bbaaa=abaaaaa.
Reduce LHS:
| [2] | (bba)aa |
| ⇒ aaaa |
Reduce RHS:
| [5] | (abaaaa)a |
| ⇒ baaaa |
Flip LHS and RHS.
Overlap of [2] bba=aa with [5] abaaaa=baaa:
Critical pair: bbbaaa=aabaaaa.
Reduce LHS:
| [2] | b(bba)aa |
| [6] | ⇒ (baaaa) |
| ⇒ aaaa |
Reduce RHS:
| [5] | a(abaaaa) |
| ⇒ abaaa |
Flip LHS and RHS.
Referenced by [8], [9], [10], [11].
Overlap of [5] abaaaa=baaa with [4] aab=abaa:
Critical pair: abaaabaa=baaab.
Reduce LHS:
| [7] | (abaaa)baa |
| [4] | ⇒ aa(aab)aa |
| [7] | ⇒ aa(abaaa)a |
| ⇒ aaaaaaa |
Reduce RHS:
| [4] | ba(aab) |
| [4] | ⇒ b(aab)aa |
| [1] | ⇒ (bab)aaaa |
| [7] | ⇒ (abaaa)aa |
| ⇒ aaaaaa |
Referenced by [9].
Overlap of [4] aab=abaa with [5] abaaaa=baaa:
Critical pair: abaaa=abaaaaaa.
Reduce LHS:
| [7] | (abaaa) |
| ⇒ aaaa |
Reduce RHS:
| [7] | (abaaa)aaa |
| [8] | ⇒ (aaaaaaa) |
| ⇒ aaaaaa |
Flip LHS and RHS.
Referenced by [10].
Overlap of [1] bab=aba with [6] baaaa=aaaa:
Critical pair: baaaaa=abaaaaa.
Reduce LHS:
| [6] | (baaaa)a |
| ⇒ aaaaa |
Reduce RHS:
| [7] | (abaaa)aa |
| [9] | ⇒ (aaaaaa) |
| ⇒ aaaa |
Defines rule #1.
Referenced by [11].
Overlap of [5] abaaaa=baaa with [7] abaaa=aaaa:
Critical pair: aaaaa=baaa.
Reduce LHS:
| [10] | (aaaaa) |
| ⇒ aaaa |
Flip LHS and RHS.
Defines rule #2.