| Back: | ⟨a, b | aba=bb, aaaa=a⟩ |
|---|
Completion settings:
Axiom: aba=bb.
Defines rule #5.
Referenced by [3], [4], [5], [6], [7], [8], [11].
Axiom: aaaa=a.
Defines rule #11.
Overlap of [1] aba=bb with [1] aba=bb:
Critical pair: abbb=bbba.
Flip LHS and RHS.
Defines rule #3.
Referenced by [7], [8], [9], [10].
Overlap of [1] aba=bb with [2] aaaa=a:
Critical pair: aba=bbaaa.
Reduce LHS:
| [1] | (aba) |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #10.
Overlap of [2] aaaa=a with [1] aba=bb:
Critical pair: aaabb=aba.
Reduce RHS:
| [1] | (aba) |
| ⇒ bb |
Defines rule #9.
Overlap of [1] aba=bb with [5] aaabb=bb:
Critical pair: abbb=bbaabb.
Flip LHS and RHS.
Defines rule #8.
Overlap of [5] aaabb=bb with [3] bbba=abbb:
Critical pair: aaababbb=bbbba.
Reduce LHS:
| [1] | aa(aba)bbb |
| ⇒ aabbbbb |
Reduce RHS:
| [3] | b(bbba) |
| ⇒ babbb |
Overlap of [6] bbaabb=abbb with [3] bbba=abbb:
Critical pair: bbaababbb=abbbbba.
Reduce LHS:
| [1] | bba(aba)bbb |
| ⇒ bbabbbbb |
Reduce RHS:
| [3] | abb(bbba) |
| ⇒ abbabbb |
Flip LHS and RHS.
Defines rule #6.
Overlap of [7] aabbbbb=babbb with [3] bbba=abbb:
Critical pair: aabbabbb=babbba.
Reduce LHS:
| [8] | a(abbabbb) |
| [8] | ⇒ (abbabbb)bb |
| ⇒ bbabbbbbbb |
Reduce RHS:
| [3] | ba(bbba) |
| ⇒ baabbb |
Flip LHS and RHS.
Defines rule #7.
Overlap of [8] abbabbb=bbabbbbb with [3] bbba=abbb:
Critical pair: abbaabbb=bbabbbbba.
Reduce LHS:
| [6] | a(bbaabb)b |
| ⇒ aabbbb |
Reduce RHS:
| [3] | bbabb(bbba) |
| [8] | ⇒ bb(abbabbb) |
| [3] | ⇒ b(bbba)bbbbb |
| ⇒ babbbbbbbb |
Defines rule #4.
Overlap of [5] aaabb=bb with [10] aabbbb=babbbbbbbb:
Critical pair: ababbbbbbbb=bbbb.
Reduce LHS:
| [1] | (aba)bbbbbbbb |
| ⇒ bbbbbbbbbb |
Defines rule #1.
Overlap of [7] aabbbbb=babbb with [10] aabbbb=babbbbbbbb:
Critical pair: babbbbbbbbb=babbb.
Defines rule #2.