| Back: | ⟨a, b | aaa=1, babab=abb⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #9.
Referenced by [5], [6], [7], [14].
Axiom: babab=abb.
Defines rule #7.
Referenced by [3], [4], [5], [6], [8], [9], [10], [11], [12].
Overlap of [2] babab=abb with [2] babab=abb:
Critical pair: baabb=abbab.
Defines rule #6.
Referenced by [4], [5], [9], [12].
Overlap of [3] baabb=abbab with [2] babab=abb:
Critical pair: baababb=abbababab.
Reduce RHS:
| [2] | ab(babab)ab |
| ⇒ ababbab |
Defines rule #12.
Overlap of [3] baabb=abbab with [4] baababb=ababbab:
Critical pair: baabababbab=abbabaababb.
Reduce LHS:
| [2] | baa(babab)bab |
| [1] | ⇒ b(aaa)bbbab |
| ⇒ bbbbab |
Reduce RHS:
| [4] | abba(baababb) |
| [4] | ⇒ ab(baababb)ab |
| [2] | ⇒ a(babab)babab |
| [2] | ⇒ aabb(babab) |
| ⇒ aabbabb |
Flip LHS and RHS.
Overlap of [4] baababb=ababbab with [2] babab=abb:
Critical pair: baabababb=ababbababab.
Reduce LHS:
| [2] | baa(babab)b |
| [1] | ⇒ b(aaa)bbb |
| ⇒ bbbb |
Reduce RHS:
| [2] | abab(babab)ab |
| [2] | ⇒ a(babab)bab |
| ⇒ aabbbab |
Flip LHS and RHS.
Referenced by [7].
Overlap of [1] aaa=1 with [6] aabbbab=bbbb:
Critical pair: abbbb=bbbab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [8], [9], [10], [15].
Overlap of [7] bbbab=abbbb with [2] babab=abb:
Critical pair: bbabb=abbbbab.
Reduce RHS:
| [7] | ab(bbbab) |
| ⇒ ababbbb |
Flip LHS and RHS.
Referenced by [10], [12], [13].
Overlap of [7] bbbab=abbbb with [3] baabb=abbab:
Critical pair: bbbaabbab=abbbbaabb.
Reduce LHS:
| [3] | bb(baabb)ab |
| [2] | ⇒ bbab(babab) |
| [2] | ⇒ b(babab)b |
| ⇒ babbb |
Reduce RHS:
| [3] | abbb(baabb) |
| [7] | ⇒ a(bbbab)bab |
| [7] | ⇒ aabb(bbbab) |
| [5] | ⇒ (aabbabb)bb |
| [7] | ⇒ b(bbbab)bb |
| ⇒ babbbbbb |
Flip LHS and RHS.
Defines rule #2.
Referenced by [11], [12], [13].
Overlap of [8] ababbbb=bbabb with [7] bbbab=abbbb:
Critical pair: abababbbb=bbabbab.
Reduce LHS:
| [2] | a(babab)bbb |
| ⇒ aabbbbb |
Flip LHS and RHS.
Defines rule #8.
Overlap of [2] babab=abb with [9] babbbbbb=babbb:
Critical pair: bababbb=abbbbbbb.
Reduce LHS:
| [2] | (babab)bb |
| ⇒ abbbb |
Flip LHS and RHS.
Referenced by [14].
Overlap of [3] baabb=abbab with [9] babbbbbb=babbb:
Critical pair: baabbabbb=abbababbbbbb.
Reduce LHS:
| [3] | (baabb)abbb |
| [2] | ⇒ ab(babab)bb |
| [8] | ⇒ (ababbbb) |
| ⇒ bbabb |
Reduce RHS:
| [2] | ab(babab)bbbbb |
| [8] | ⇒ (ababbbb)bbb |
| ⇒ bbabbbbb |
Flip LHS and RHS.
Defines rule #3.
Overlap of [8] ababbbb=bbabb with [9] babbbbbb=babbb:
Critical pair: ababbb=bbabbbb.
Defines rule #5.
Referenced by [16].
Overlap of [1] aaa=1 with [11] abbbbbbb=abbbb:
Critical pair: aaabbbb=bbbbbbb.
Reduce LHS:
| [1] | (aaa)bbbb |
| ⇒ bbbb |
Flip LHS and RHS.
Defines rule #1.
Simplify [5] aabbabb=bbbbab.
Reduce RHS:
| [7] | b(bbbab) |
| ⇒ babbbb |
Defines rule #10.
Overlap of [4] baababb=ababbab with [13] ababbb=bbabbbb:
Critical pair: babbabbbb=ababbabb.
Flip LHS and RHS.
Defines rule #11.