| Back: | ⟨a, b | bab=aba, bbb=aa⟩ |
|---|
Completion settings:
Axiom: bab=aba.
Defines rule #5.
Referenced by [4], [5], [6], [7].
Axiom: bbb=aa.
Defines rule #7.
Referenced by [3], [5], [6], [9], [11].
Overlap of [2] bbb=aa with [2] bbb=aa:
Critical pair: baa=aab.
Flip LHS and RHS.
Defines rule #4.
Overlap of [1] bab=aba with [1] bab=aba:
Critical pair: baaba=abaab.
Reduce LHS:
| [3] | b(aab)a |
| ⇒ bbaaa |
Reduce RHS:
| [3] | ab(aab) |
| ⇒ abbaa |
Flip LHS and RHS.
Referenced by [12].
Overlap of [1] bab=aba with [2] bbb=aa:
Critical pair: baaa=ababb.
Reduce RHS:
| [1] | a(bab)b |
| [3] | ⇒ (aab)ab |
| [3] | ⇒ ba(aab) |
| [1] | ⇒ (bab)aa |
| ⇒ abaaa |
Flip LHS and RHS.
Overlap of [2] bbb=aa with [1] bab=aba:
Critical pair: bbaba=aaab.
Reduce LHS:
| [1] | b(bab)a |
| [1] | ⇒ (bab)aa |
| [5] | ⇒ (abaaa) |
| ⇒ baaa |
Reduce RHS:
| [3] | a(aab) |
| ⇒ abaa |
Flip LHS and RHS.
Overlap of [1] bab=aba with [6] abaa=baaa:
Critical pair: bbaaa=abaaa.
Reduce RHS:
| [6] | (abaa)a |
| ⇒ baaaa |
Referenced by [10].
Simplify [5] abaaa=baaa.
Reduce LHS:
| [6] | (abaa)a |
| ⇒ baaaa |
Overlap of [2] bbb=aa with [8] baaaa=baaa:
Critical pair: bbbaaa=aaaaaa.
Reduce LHS:
| [2] | (bbb)aaa |
| ⇒ aaaaa |
Flip LHS and RHS.
Defines rule #1.
Simplify [7] bbaaa=baaaa.
Reduce RHS:
| [8] | (baaaa) |
| ⇒ baaa |
Overlap of [2] bbb=aa with [10] bbaaa=baaa:
Critical pair: bbaaa=aaaaa.
Reduce LHS:
| [10] | (bbaaa) |
| ⇒ baaa |
Defines rule #2.
Simplify [4] abbaa=bbaaa.
Reduce RHS:
| [10] | (bbaaa) |
| [11] | ⇒ (baaa) |
| ⇒ aaaaa |
Defines rule #6.
Simplify [6] abaa=baaa.
Reduce RHS:
| [11] | (baaa) |
| ⇒ aaaaa |
Defines rule #3.