| Back: | ⟨a, b | aba=b, bbbbb=b⟩ |
|---|
Completion settings:
Axiom: aba=b.
Referenced by [4], [5], [7], [9], [13].
Axiom: bbbbb=b.
Defines rule #3.
Axiom: baa=c.
Overlap of [1] aba=b with [1] aba=b:
Critical pair: abb=bba.
Flip LHS and RHS.
Overlap of [1] aba=b with [3] baa=c:
Critical pair: ac=ba.
Flip LHS and RHS.
Defines rule #5.
Referenced by [6], [7], [10], [11], [13], [14], [15].
Overlap of [3] baa=c with [5] ba=ac:
Critical pair: aca=c.
Referenced by [7], [9], [10], [14].
Overlap of [5] ba=ac with [1] aba=b:
Critical pair: bb=acba.
Reduce RHS:
| [5] | ac(ba) |
| [6] | ⇒ (aca)c |
| ⇒ cc |
Flip LHS and RHS.
Defines rule #1.
Referenced by [8], [10], [14], [15].
Overlap of [7] cc=bb with [7] cc=bb:
Critical pair: cbb=bbc.
Defines rule #2.
Referenced by [12].
Overlap of [1] aba=b with [6] aca=c:
Critical pair: abc=bca.
Flip LHS and RHS.
Overlap of [5] ba=ac with [6] aca=c:
Critical pair: bc=acca.
Reduce RHS:
| [7] | a(cc)a |
| [4] | ⇒ a(bba) |
| ⇒ aabb |
Flip LHS and RHS.
Referenced by [12].
Overlap of [2] bbbbb=b with [5] ba=ac:
Critical pair: bbbbac=ba.
Reduce LHS:
| [4] | bb(bba)c |
| [4] | ⇒ (bba)bbc |
| ⇒ abbbbc |
Reduce RHS:
| [5] | (ba) |
| ⇒ ac |
Referenced by [14].
Overlap of [10] aabb=bc with [2] bbbbb=b:
Critical pair: aab=bcbbb.
Reduce RHS:
| [8] | b(cbb)b |
| ⇒ bbbcb |
Defines rule #7.
Overlap of [1] aba=b with [5] ba=ac:
Critical pair: aac=b.
Defines rule #8.
Referenced by [14].
Overlap of [11] abbbbc=ac with [9] bca=abc:
Critical pair: abbbabc=aca.
Reduce LHS:
| [5] | abb(ba)bc |
| [5] | ⇒ ab(ba)cbc |
| [5] | ⇒ a(ba)ccbc |
| [13] | ⇒ (aac)ccbc |
| [7] | ⇒ b(cc)bc |
| ⇒ bbbbc |
Reduce RHS:
| [6] | (aca) |
| ⇒ c |
Defines rule #4.
Referenced by [15].
Overlap of [14] bbbbc=c with [9] bca=abc:
Critical pair: bbbabc=ca.
Reduce LHS:
| [5] | bb(ba)bc |
| [5] | ⇒ b(ba)cbc |
| [5] | ⇒ (ba)ccbc |
| [7] | ⇒ a(cc)cbc |
| ⇒ abbcbc |
Flip LHS and RHS.
Defines rule #6.