| Back: | ⟨a, b | aa=1, ababbb=bab⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #3.
Referenced by [3], [4], [7], [10], [11], [13], [15], [16].
Axiom: ababbb=bab.
Overlap of [1] aa=1 with [2] ababbb=bab:
Critical pair: abab=babbb.
Defines rule #4.
Referenced by [4], [5], [6], [7], [9], [12], [15].
Overlap of [1] aa=1 with [3] abab=babbb:
Critical pair: ababbb=bab.
Reduce LHS:
| [3] | (abab)bb |
| ⇒ babbbbb |
Defines rule #1.
Referenced by [6], [7], [8], [9], [12], [14], [15].
Overlap of [3] abab=babbb with [3] abab=babbb:
Critical pair: abbabbb=babbbab.
Flip LHS and RHS.
Defines rule #6.
Referenced by [6], [7], [9], [10], [12], [13].
Overlap of [5] babbbab=abbabbb with [5] babbbab=abbabbb:
Critical pair: babbabbabbb=abbabbbbbab.
Reduce RHS:
| [4] | ab(babbbbb)ab |
| [3] | ⇒ abb(abab) |
| ⇒ abbbabbb |
Overlap of [2] ababbb=bab with [6] babbabbabbb=abbbabbb:
Critical pair: ababbabbbabbb=bababbabbabbb.
Reduce LHS:
| [5] | abab(babbbab)bb |
| [4] | ⇒ ababab(babbbbb) |
| [3] | ⇒ (abab)abbab |
| [5] | ⇒ (babbbab)bab |
| ⇒ abbabbbbab |
Reduce RHS:
| [6] | ba(babbabbabbb) |
| [1] | ⇒ b(aa)bbbabbb |
| ⇒ bbbbabbb |
Referenced by [13].
Overlap of [6] babbabbabbb=abbbabbb with [4] babbbbb=bab:
Critical pair: babbabbab=abbbabbbbb.
Reduce RHS:
| [4] | abb(babbbbb) |
| ⇒ abbbab |
Referenced by [9], [10], [13].
Overlap of [8] babbabbab=abbbab with [3] abab=babbb:
Critical pair: babbabbbabbb=abbbabab.
Reduce LHS:
| [5] | bab(babbbab)bb |
| [4] | ⇒ babab(babbbbb) |
| [3] | ⇒ b(abab)bab |
| ⇒ bbabbbbab |
Reduce RHS:
| [3] | abbb(abab) |
| ⇒ abbbbabbb |
Defines rule #7.
Referenced by [15].
Overlap of [8] babbabbab=abbbab with [8] babbabbab=abbbab:
Critical pair: bababbbab=abbbabbab.
Reduce LHS:
| [5] | ba(babbbab) |
| [1] | ⇒ b(aa)bbabbb |
| ⇒ bbbabbb |
Flip LHS and RHS.
Overlap of [1] aa=1 with [10] abbbabbab=bbbabbb:
Critical pair: abbbabbb=bbbabbab.
Flip LHS and RHS.
Defines rule #8.
Overlap of [10] abbbabbab=bbbabbb with [3] abab=babbb:
Critical pair: abbbabbbabbb=bbbabbbab.
Reduce LHS:
| [5] | abb(babbbab)bb |
| [4] | ⇒ abbab(babbbbb) |
| ⇒ abbabbab |
Reduce RHS:
| [5] | bb(babbbab) |
| ⇒ bbabbabbb |
Defines rule #9.
Referenced by [13].
Overlap of [12] abbabbab=bbabbabbb with [8] babbabbab=abbbab:
Critical pair: ababbbab=bbabbabbbbab.
Reduce LHS:
| [5] | a(babbbab) |
| [1] | ⇒ (aa)bbabbb |
| ⇒ bbabbb |
Reduce RHS:
| [7] | bb(abbabbbbab) |
| ⇒ bbbbbbabbb |
Flip LHS and RHS.
Referenced by [14].
Overlap of [13] bbbbbbabbb=bbabbb with [4] babbbbb=bab:
Critical pair: bbbbbbab=bbabbbbb.
Reduce RHS:
| [4] | b(babbbbb) |
| ⇒ bbab |
Defines rule #2.
Overlap of [3] abab=babbb with [9] bbabbbbab=abbbbabbb:
Critical pair: abaabbbbabbb=babbbbabbbbab.
Reduce LHS:
| [1] | ab(aa)bbbbabbb |
| ⇒ abbbbbabbb |
Reduce RHS:
| [9] | babb(bbabbbbab) |
| [9] | ⇒ ba(bbabbbbab)bb |
| [1] | ⇒ b(aa)bbbbabbbbb |
| [4] | ⇒ bbbb(babbbbb) |
| ⇒ bbbbbab |
Referenced by [16].
Overlap of [1] aa=1 with [15] abbbbbabbb=bbbbbab:
Critical pair: abbbbbab=bbbbbabbb.
Defines rule #5.