| Back: | ⟨a, b | aba=aab, bbaa=a⟩ |
|---|
Completion settings:
Axiom: aba=aab.
Defines rule #1.
Referenced by [3].
Axiom: bbaa=a.
Referenced by [4], [5], [6], [7].
Overlap of [1] aba=aab with [1] aba=aab:
Critical pair: abaab=aabba.
Reduce LHS:
| [1] | (aba)ab |
| [1] | ⇒ a(aba)b |
| ⇒ aaabb |
Flip LHS and RHS.
Overlap of [2] bbaa=a with [3] aabba=aaabb:
Critical pair: bbaaabb=abba.
Reduce LHS:
| [2] | (bbaa)abb |
| ⇒ aabb |
Flip LHS and RHS.
Referenced by [5].
Overlap of [4] abba=aabb with [2] bbaa=a:
Critical pair: aa=aabba.
Reduce RHS:
| [3] | (aabba) |
| ⇒ aaabb |
Flip LHS and RHS.
Referenced by [6].
Overlap of [2] bbaa=a with [5] aaabb=aa:
Critical pair: bbaa=aabb.
Reduce LHS:
| [2] | (bbaa) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #3.
Referenced by [7].
Overlap of [2] bbaa=a with [6] aabb=a:
Critical pair: bba=abb.
Defines rule #2.