| Back: | ⟨a, b | abb=aaa, bbaa=a⟩ |
|---|
Completion settings:
Axiom: abb=aaa.
Flip LHS and RHS.
Referenced by [3], [4], [5], [8].
Axiom: bbaa=a.
Referenced by [4], [5], [6], [8], [9], [11].
Overlap of [1] aaa=abb with [1] aaa=abb:
Critical pair: aabb=abba.
Flip LHS and RHS.
Overlap of [2] bbaa=a with [1] aaa=abb:
Critical pair: bbabb=aa.
Flip LHS and RHS.
Referenced by [5], [6], [7], [8], [9], [10], [11], [12].
Overlap of [1] aaa=abb with [4] aa=bbabb:
Critical pair: aabbabb=abba.
Reduce LHS:
| [3] | a(abba)bb |
| [4] | ⇒ (aa)abbbb |
| [3] | ⇒ bb(abba)bbbb |
| [2] | ⇒ (bbaa)bbbbbb |
| ⇒ abbbbbb |
Reduce RHS:
| [3] | (abba) |
| [4] | ⇒ (aa)bb |
| ⇒ bbabbbb |
Flip LHS and RHS.
Overlap of [4] aa=bbabb with [4] aa=bbabb:
Critical pair: abbabb=bbabba.
Reduce LHS:
| [3] | (abba)bb |
| [4] | ⇒ (aa)bbbb |
| [5] | ⇒ (bbabbbb)bb |
| ⇒ abbbbbbbb |
Reduce RHS:
| [3] | bb(abba) |
| [2] | ⇒ (bbaa)bb |
| ⇒ abb |
Referenced by [8].
Simplify [3] abba=aabb.
Reduce RHS:
| [4] | (aa)bb |
| [5] | ⇒ (bbabbbb) |
| ⇒ abbbbbb |
Overlap of [1] aaa=abb with [7] abba=abbbbbb:
Critical pair: aaabbbbbb=abbbba.
Reduce LHS:
| [4] | (aa)abbbbbb |
| [5] | ⇒ bba(bbabbbb)bb |
| [2] | ⇒ (bbaa)bbbbbbbb |
| [6] | ⇒ (abbbbbbbb) |
| ⇒ abb |
Flip LHS and RHS.
Referenced by [10].
Overlap of [7] abba=abbbbbb with [2] bbaa=a:
Critical pair: aa=abbbbbba.
Reduce LHS:
| [4] | (aa) |
| ⇒ bbabb |
Flip LHS and RHS.
Referenced by [10].
Overlap of [7] abba=abbbbbb with [4] aa=bbabb:
Critical pair: abbbbabb=abbbbbba.
Reduce LHS:
| [8] | (abbbba)bb |
| ⇒ abbbb |
Reduce RHS:
| [9] | (abbbbbba) |
| ⇒ bbabb |
Flip LHS and RHS.
Referenced by [11], [12], [13].
Overlap of [2] bbaa=a with [4] aa=bbabb:
Critical pair: bbbbabb=a.
Reduce LHS:
| [10] | bb(bbabb) |
| [10] | ⇒ (bbabb)bb |
| ⇒ abbbbbb |
Defines rule #1.
Referenced by [13].
Simplify [4] aa=bbabb.
Reduce RHS:
| [10] | (bbabb) |
| ⇒ abbbb |
Defines rule #3.
Overlap of [10] bbabb=abbbb with [11] abbbbbb=a:
Critical pair: bba=abbbbbbbb.
Reduce RHS:
| [11] | (abbbbbb)bb |
| ⇒ abb |
Defines rule #2.