| Back: | ⟨a, b | aa=a, babbbab=a⟩ |
|---|
Completion settings:
Axiom: aa=a.
Defines rule #1.
Referenced by [4], [5], [7], [8], [9], [10], [11].
Axiom: babbbab=a.
Referenced by [3], [4], [6], [8], [9], [10].
Overlap of [2] babbbab=a with [2] babbbab=a:
Critical pair: babba=abbab.
Referenced by [5], [6], [7], [9].
Overlap of [2] babbbab=a with [2] babbbab=a:
Critical pair: babbbaa=aabbbab.
Reduce LHS:
| [1] | babbb(aa) |
| ⇒ babbba |
Reduce RHS:
| [1] | (aa)bbbab |
| ⇒ abbbab |
Overlap of [3] babba=abbab with [1] aa=a:
Critical pair: babba=abbaba.
Reduce LHS:
| [3] | (babba) |
| ⇒ abbab |
Flip LHS and RHS.
Referenced by [8].
Overlap of [3] babba=abbab with [2] babbbab=a:
Critical pair: baba=abbabbbbab.
Flip LHS and RHS.
Referenced by [8].
Overlap of [3] babba=abbab with [3] babba=abbab:
Critical pair: bababbab=abbabbba.
Reduce LHS:
| [3] | ba(babba)b |
| [1] | ⇒ b(aa)bbabb |
| [3] | ⇒ (babba)bb |
| ⇒ abbabbb |
Reduce RHS:
| [4] | ab(babbba) |
| [4] | ⇒ a(babbba)b |
| [1] | ⇒ (aa)bbbabb |
| ⇒ abbbabb |
Flip LHS and RHS.
Referenced by [9].
Overlap of [5] abbaba=abbab with [2] babbbab=a:
Critical pair: abbaa=abbabbbbab.
Reduce LHS:
| [1] | abb(aa) |
| ⇒ abba |
Reduce RHS:
| [6] | (abbabbbbab) |
| ⇒ baba |
Flip LHS and RHS.
Overlap of [2] babbbab=a with [8] baba=abba:
Critical pair: babbabba=aa.
Reduce LHS:
| [3] | (babba)bba |
| [4] | ⇒ ab(babbba) |
| [4] | ⇒ a(babbba)b |
| [1] | ⇒ (aa)bbbabb |
| [7] | ⇒ (abbbabb) |
| ⇒ abbabbb |
Reduce RHS:
| [1] | (aa) |
| ⇒ a |
Overlap of [8] baba=abba with [2] babbbab=a:
Critical pair: baa=abbabbbab.
Reduce LHS:
| [1] | b(aa) |
| ⇒ ba |
Reduce RHS:
| [9] | (abbabbb)ab |
| [1] | ⇒ (aa)b |
| ⇒ ab |
Defines rule #2.
Referenced by [11].
Simplify [9] abbabbb=a.
Reduce LHS:
| [10] | ab(ba)bbb |
| [10] | ⇒ a(ba)bbbb |
| [1] | ⇒ (aa)bbbbb |
| ⇒ abbbbb |
Defines rule #3.