| Back: | ⟨a, b | aa=1, ababbbb=bb⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #1.
Axiom: ababbbb=bb.
Referenced by [3], [4], [7], [9].
Overlap of [1] aa=1 with [2] ababbbb=bb:
Critical pair: abb=babbbb.
Flip LHS and RHS.
Referenced by [4], [5], [6], [7], [8], [10].
Overlap of [2] ababbbb=bb with [3] babbbb=abb:
Critical pair: ababbbabb=bbabbbb.
Reduce RHS:
| [3] | b(babbbb) |
| ⇒ babb |
Referenced by [10].
Overlap of [3] babbbb=abb with [3] babbbb=abb:
Critical pair: babbbabb=abbabbbb.
Reduce RHS:
| [3] | ab(babbbb) |
| ⇒ ababb |
Referenced by [6], [7], [8], [9], [10].
Overlap of [3] babbbb=abb with [5] babbbabb=ababb:
Critical pair: babbbababb=abbabbbabb.
Reduce RHS:
| [5] | ab(babbbabb) |
| ⇒ abababb |
Referenced by [8].
Overlap of [5] babbbabb=ababb with [3] babbbb=abb:
Critical pair: babbabb=ababbbb.
Reduce RHS:
| [2] | (ababbbb) |
| ⇒ bb |
Overlap of [5] babbbabb=ababb with [3] babbbb=abb:
Critical pair: babbbababb=ababbabbbb.
Reduce LHS:
| [6] | (babbbababb) |
| ⇒ abababb |
Reduce RHS:
| [7] | a(babbabb)bb |
| ⇒ abbbb |
Referenced by [9].
Overlap of [5] babbbabb=ababb with [5] babbbabb=ababb:
Critical pair: babbbabababb=ababbabbbabb.
Reduce LHS:
| [8] | babbb(abababb) |
| [5] | ⇒ (babbbabb)bb |
| [2] | ⇒ (ababbbb) |
| ⇒ bb |
Reduce RHS:
| [7] | a(babbabb)babb |
| ⇒ abbbabb |
Flip LHS and RHS.
Overlap of [5] babbbabb=ababb with [9] abbbabb=bb:
Critical pair: babbbbb=ababbbabb.
Reduce LHS:
| [3] | (babbbb)b |
| ⇒ abbb |
Reduce RHS:
| [4] | (ababbbabb) |
| ⇒ babb |
Flip LHS and RHS.
Defines rule #2.
Referenced by [11].
Overlap of [10] babb=abbb with [10] babb=abbb:
Critical pair: bababbb=abbbabb.
Reduce LHS:
| [10] | ba(babb)b |
| [1] | ⇒ b(aa)bbbb |
| ⇒ bbbbb |
Reduce RHS:
| [9] | (abbbabb) |
| ⇒ bb |
Defines rule #3.