| Back: | ⟨a, b | aaa=1, abbb=bba⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #5.
Referenced by [3], [4], [7], [9].
Axiom: abbb=bba.
Flip LHS and RHS.
Defines rule #3.
Referenced by [3], [5], [6], [8].
Overlap of [2] bba=abbb with [1] aaa=1:
Critical pair: bb=abbbaa.
Reduce RHS:
| [2] | ab(bba)a |
| [2] | ⇒ abab(bba) |
| ⇒ abababbb |
Flip LHS and RHS.
Overlap of [1] aaa=1 with [3] abababbb=bb:
Critical pair: aabb=bababbb.
Flip LHS and RHS.
Overlap of [3] abababbb=bb with [2] bba=abbb:
Critical pair: abababbabbb=bbba.
Reduce LHS:
| [2] | ababa(bba)bbb |
| ⇒ ababaabbbbbb |
Reduce RHS:
| [2] | b(bba) |
| ⇒ babbb |
Referenced by [7].
Overlap of [2] bba=abbb with [4] bababbb=aabb:
Critical pair: baabb=abbbbabbb.
Reduce RHS:
| [2] | abb(bba)bbb |
| [2] | ⇒ a(bba)bbbbbb |
| ⇒ aabbbbbbbbb |
Defines rule #4.
Referenced by [7].
Simplify [5] ababaabbbbbb=babbb.
Reduce LHS:
| [6] | aba(baabb)bbbb |
| [1] | ⇒ ab(aaa)bbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbbb |
Flip LHS and RHS.
Overlap of [7] babbb=abbbbbbbbbbbbbb with [2] bba=abbb:
Critical pair: bababbb=abbbbbbbbbbbbbba.
Reduce LHS:
| [4] | (bababbb) |
| ⇒ aabb |
Reduce RHS:
| [2] | abbbbbbbbbbbb(bba) |
| [2] | ⇒ abbbbbbbbbb(bba)bbb |
| [2] | ⇒ abbbbbbbb(bba)bbbbbb |
| [2] | ⇒ abbbbbb(bba)bbbbbbbbb |
| [2] | ⇒ abbbb(bba)bbbbbbbbbbbb |
| [2] | ⇒ abb(bba)bbbbbbbbbbbbbbb |
| [2] | ⇒ a(bba)bbbbbbbbbbbbbbbbbb |
| ⇒ aabbbbbbbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [9].
Overlap of [1] aaa=1 with [8] aabbbbbbbbbbbbbbbbbbbbb=aabb:
Critical pair: aaabb=bbbbbbbbbbbbbbbbbbbbb.
Reduce LHS:
| [1] | (aaa)bb |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #1.
Referenced by [10].
Overlap of [7] babbb=abbbbbbbbbbbbbb with [9] bbbbbbbbbbbbbbbbbbbbb=bb:
Critical pair: babb=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Reduce RHS:
| [9] | a(bbbbbbbbbbbbbbbbbbbbb)bbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbb |
Defines rule #2.