| Back: | ⟨a, b | abba=bbb, baba=1⟩ |
|---|
Completion settings:
Axiom: abba=bbb.
Axiom: baba=1.
Referenced by [4], [5], [7], [8], [9], [11].
Overlap of [1] abba=bbb with [1] abba=bbb:
Critical pair: abbbbb=bbbbba.
Flip LHS and RHS.
Overlap of [1] abba=bbb with [2] baba=1:
Critical pair: ab=bbbba.
Flip LHS and RHS.
Referenced by [6].
Overlap of [2] baba=1 with [1] abba=bbb:
Critical pair: babbbb=bba.
Flip LHS and RHS.
Referenced by [6], [9], [10], [12].
Simplify [4] bbbba=ab.
Reduce LHS:
| [5] | bb(bba) |
| [5] | ⇒ b(bba)bbbb |
| [5] | ⇒ (bba)bbbbbbbb |
| ⇒ babbbbbbbbbbbb |
Overlap of [2] baba=1 with [6] babbbbbbbbbbbb=ab:
Critical pair: baab=bbbbbbbbbbbb.
Referenced by [9].
Overlap of [6] babbbbbbbbbbbb=ab with [2] baba=1:
Critical pair: babbbbbbbbbbb=ababa.
Reduce RHS:
| [2] | a(baba) |
| ⇒ a |
Referenced by [10].
Overlap of [5] bba=babbbb with [2] baba=1:
Critical pair: b=babbbbba.
Reduce RHS:
| [3] | ba(bbbbba) |
| [7] | ⇒ (baab)bbbb |
| ⇒ bbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [13].
Overlap of [5] bba=babbbb with [6] babbbbbbbbbbbb=ab:
Critical pair: bab=babbbbbbbbbbbbbbbb.
Reduce RHS:
| [8] | (babbbbbbbbbbb)bbbbb |
| ⇒ abbbbb |
Referenced by [11].
Overlap of [2] baba=1 with [10] bab=abbbbb:
Critical pair: abbbbba=1.
Reduce LHS:
| [3] | a(bbbbba) |
| ⇒ aabbbbb |
Referenced by [12], [13], [14], [15].
Overlap of [11] aabbbbb=1 with [5] bba=babbbb:
Critical pair: aabbbbbabbbb=ba.
Reduce LHS:
| [11] | (aabbbbb)abbbb |
| ⇒ abbbb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [11] aabbbbb=1 with [9] bbbbbbbbbbbbbbbb=b:
Critical pair: aab=bbbbbbbbbbb.
Referenced by [14].
Overlap of [11] aabbbbb=1 with [13] aab=bbbbbbbbbbb:
Critical pair: bbbbbbbbbbbbbbb=1.
Defines rule #1.
Referenced by [15].
Overlap of [11] aabbbbb=1 with [14] bbbbbbbbbbbbbbb=1:
Critical pair: aa=bbbbbbbbbb.
Defines rule #3.