| Back: | ⟨a, b | aaa=1, babb=abab⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #1.
Referenced by [3].
Axiom: babb=abab.
Flip LHS and RHS.
Defines rule #2.
Referenced by [3], [4], [5], [6], [7], [9], [10], [12].
Overlap of [1] aaa=1 with [2] abab=babb:
Critical pair: aababb=bab.
Reduce LHS:
| [2] | a(abab)b |
| [2] | ⇒ (abab)bb |
| ⇒ babbbb |
Defines rule #3.
Referenced by [7], [8], [9], [10], [11], [12], [13], [15].
Overlap of [2] abab=babb with [2] abab=babb:
Critical pair: abbabb=babbab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [5], [6], [7], [10].
Overlap of [2] abab=babb with [4] babbab=abbabb:
Critical pair: aabbabb=babbbab.
Flip LHS and RHS.
Defines rule #7.
Referenced by [6], [7], [9], [12].
Overlap of [4] babbab=abbabb with [4] babbab=abbabb:
Critical pair: bababbabb=abbabbbab.
Reduce LHS:
| [2] | b(abab)babb |
| [5] | ⇒ b(babbbab)b |
| ⇒ baabbabbb |
Reduce RHS:
| [5] | ab(babbbab) |
| ⇒ abaabbabb |
Flip LHS and RHS.
Overlap of [4] babbab=abbabb with [5] babbbab=aabbabb:
Critical pair: babaabbabb=abbabbbbab.
Reduce LHS:
| [6] | b(abaabbabb) |
| ⇒ bbaabbabbb |
Reduce RHS:
| [3] | ab(babbbb)ab |
| [2] | ⇒ abb(abab) |
| ⇒ abbbabb |
Referenced by [8].
Overlap of [7] bbaabbabbb=abbbabb with [3] babbbb=bab:
Critical pair: bbaabbab=abbbabbb.
Defines rule #9.
Referenced by [9], [10], [12], [14].
Overlap of [8] bbaabbab=abbbabbb with [2] abab=babb:
Critical pair: bbaabbbabb=abbbabbbab.
Reduce RHS:
| [5] | abb(babbbab) |
| [8] | ⇒ a(bbaabbab)b |
| [3] | ⇒ aabb(babbbb) |
| ⇒ aabbbab |
Referenced by [14].
Overlap of [8] bbaabbab=abbbabbb with [4] babbab=abbabb:
Critical pair: bbaababbabb=abbbabbbbab.
Reduce LHS:
| [2] | bba(abab)babb |
| [2] | ⇒ bb(abab)bbabb |
| [3] | ⇒ bb(babbbb)abb |
| [2] | ⇒ bbb(abab)b |
| ⇒ bbbbabbb |
Reduce RHS:
| [3] | abb(babbbb)ab |
| [2] | ⇒ abbb(abab) |
| ⇒ abbbbabb |
Flip LHS and RHS.
Overlap of [10] abbbbabb=bbbbabbb with [3] babbbb=bab:
Critical pair: abbbbab=bbbbabbbbb.
Reduce RHS:
| [3] | bbb(babbbb)b |
| ⇒ bbbbabb |
Defines rule #6.
Overlap of [10] abbbbabb=bbbbabbb with [5] babbbab=aabbabb:
Critical pair: abbbaabbabb=bbbbabbbbab.
Reduce LHS:
| [8] | ab(bbaabbab)b |
| [2] | ⇒ (abab)bbabbbb |
| [3] | ⇒ (babbbb)abbbb |
| [2] | ⇒ b(abab)bbb |
| [3] | ⇒ b(babbbb)b |
| ⇒ bbabb |
Reduce RHS:
| [3] | bbb(babbbb)ab |
| [2] | ⇒ bbbb(abab) |
| ⇒ bbbbbabb |
Flip LHS and RHS.
Overlap of [12] bbbbbabb=bbabb with [3] babbbb=bab:
Critical pair: bbbbbab=bbabbbb.
Reduce RHS:
| [3] | b(babbbb) |
| ⇒ bbab |
Defines rule #5.
Overlap of [12] bbbbbabb=bbabb with [8] bbaabbab=abbbabbb:
Critical pair: bbbbbaabbbabbb=bbabbaabbab.
Reduce LHS:
| [9] | bbb(bbaabbbabb)b |
| [9] | ⇒ b(bbaabbbabb) |
| ⇒ baabbbab |
Reduce RHS:
| [8] | bba(bbaabbab) |
| [9] | ⇒ (bbaabbbabb)b |
| ⇒ aabbbabb |
Defines rule #8.
Overlap of [6] abaabbabb=baabbabbb with [3] babbbb=bab:
Critical pair: abaabbab=baabbabbbbb.
Reduce RHS:
| [3] | baab(babbbb)b |
| ⇒ baabbabb |
Defines rule #10.