| Back: | ⟨a, b | aaa=1, ababab=bb⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #6.
Axiom: ababab=bb.
Overlap of [1] aaa=1 with [2] ababab=bb:
Critical pair: aabb=babab.
Flip LHS and RHS.
Defines rule #5.
Overlap of [2] ababab=bb with [2] ababab=bb:
Critical pair: abbb=bbab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [5], [6], [7], [10].
Overlap of [3] babab=aabb with [4] bbab=abbb:
Critical pair: babaabbb=aabbbab.
Reduce RHS:
| [4] | aab(bbab) |
| ⇒ aababbb |
Referenced by [8].
Overlap of [4] bbab=abbb with [3] babab=aabb:
Critical pair: baabb=abbbab.
Reduce RHS:
| [4] | ab(bbab) |
| ⇒ ababbb |
Defines rule #4.
Overlap of [6] baabb=ababbb with [4] bbab=abbb:
Critical pair: baababbb=ababbbbab.
Reduce RHS:
| [4] | ababb(bbab) |
| [4] | ⇒ aba(bbab)bb |
| [6] | ⇒ a(baabb)bbb |
| ⇒ aababbbbbb |
Defines rule #7.
Referenced by [8].
Simplify [5] babaabbb=aababbb.
Reduce LHS:
| [6] | ba(baabb)b |
| [7] | ⇒ (baababbb)b |
| ⇒ aababbbbbbb |
Overlap of [1] aaa=1 with [8] aababbbbbbb=aababbb:
Critical pair: aaababbb=babbbbbbb.
Reduce LHS:
| [1] | (aaa)babbb |
| ⇒ babbb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [8] aababbbbbbb=aababbb with [4] bbab=abbb:
Critical pair: aababbbbbabbb=aababbbab.
Reduce LHS:
| [4] | aababbb(bbab)bb |
| [4] | ⇒ aabab(bbab)bbbb |
| [2] | ⇒ a(ababab)bbbbbb |
| ⇒ abbbbbbbb |
Reduce RHS:
| [4] | aabab(bbab) |
| [2] | ⇒ a(ababab)bb |
| ⇒ abbbb |
Referenced by [11].
Overlap of [1] aaa=1 with [10] abbbbbbbb=abbbb:
Critical pair: aaabbbb=bbbbbbbb.
Reduce LHS:
| [1] | (aaa)bbbb |
| ⇒ bbbb |
Flip LHS and RHS.
Defines rule #1.