| Back: | ⟨a, b | baab=aa, babb=b⟩ |
|---|
Completion settings:
Axiom: baab=aa.
Referenced by [3], [4], [5], [6], [7], [12].
Axiom: babb=b.
Defines rule #5.
Overlap of [1] baab=aa with [2] babb=b:
Critical pair: baab=aaabb.
Reduce LHS:
| [1] | (baab) |
| ⇒ aa |
Flip LHS and RHS.
Referenced by [5], [8], [10], [11].
Overlap of [2] babb=b with [1] baab=aa:
Critical pair: babaa=baab.
Reduce RHS:
| [1] | (baab) |
| ⇒ aa |
Overlap of [3] aaabb=aa with [1] baab=aa:
Critical pair: aaabaa=aaaab.
Referenced by [8].
Overlap of [4] babaa=aa with [1] baab=aa:
Critical pair: baaa=aab.
Referenced by [7], [8], [9], [10], [11], [13].
Overlap of [1] baab=aa with [6] baaa=aab:
Critical pair: baaaab=aaaaa.
Reduce LHS:
| [6] | (baaa)ab |
| ⇒ aabab |
Referenced by [11].
Overlap of [3] aaabb=aa with [6] baaa=aab:
Critical pair: aaabaab=aaaaa.
Reduce LHS:
| [5] | (aaabaa)b |
| [3] | ⇒ a(aaabb) |
| ⇒ aaa |
Flip LHS and RHS.
Referenced by [11].
Overlap of [4] babaa=aa with [6] baaa=aab:
Critical pair: baaab=aaa.
Reduce LHS:
| [6] | (baaa)b |
| ⇒ aabb |
Referenced by [10], [12], [14].
Overlap of [6] baaa=aab with [3] aaabb=aa:
Critical pair: baa=aabbb.
Reduce RHS:
| [9] | (aabb)b |
| ⇒ aaab |
Flip LHS and RHS.
Referenced by [11].
Overlap of [6] baaa=aab with [3] aaabb=aa:
Critical pair: baaa=aababb.
Reduce LHS:
| [6] | (baaa) |
| ⇒ aab |
Reduce RHS:
| [7] | (aabab)b |
| [8] | ⇒ (aaaaa)b |
| [10] | ⇒ (aaab) |
| ⇒ baa |
Flip LHS and RHS.
Defines rule #2.
Overlap of [1] baab=aa with [11] baa=aab:
Critical pair: aabb=aa.
Reduce LHS:
| [9] | (aabb) |
| ⇒ aaa |
Defines rule #1.
Referenced by [14].
Overlap of [6] baaa=aab with [11] baa=aab:
Critical pair: aaba=aab.
Defines rule #3.
Simplify [9] aabb=aaa.
Reduce RHS:
| [12] | (aaa) |
| ⇒ aa |
Defines rule #4.