| Back: | ⟨a, b | aa=a, bbabbb=ba⟩ |
|---|
Completion settings:
Axiom: aa=a.
Defines rule #3.
Referenced by [3], [4], [5], [6].
Axiom: bbabbb=ba.
Referenced by [3], [4], [5], [8], [11].
Overlap of [2] bbabbb=ba with [2] bbabbb=ba:
Critical pair: bbabba=baabbb.
Reduce RHS:
| [1] | b(aa)bbb |
| ⇒ babbb |
Referenced by [5], [6], [7], [8].
Overlap of [2] bbabbb=ba with [2] bbabbb=ba:
Critical pair: bbabbba=bababbb.
Reduce LHS:
| [2] | (bbabbb)a |
| [1] | ⇒ b(aa) |
| ⇒ ba |
Flip LHS and RHS.
Referenced by [7].
Overlap of [2] bbabbb=ba with [3] bbabba=babbb:
Critical pair: bbabbabbb=baabba.
Reduce LHS:
| [3] | (bbabba)bbb |
| ⇒ babbbbbb |
Reduce RHS:
| [1] | b(aa)bba |
| ⇒ babba |
Flip LHS and RHS.
Referenced by [9].
Overlap of [3] bbabba=babbb with [1] aa=a:
Critical pair: bbabba=babbba.
Reduce LHS:
| [3] | (bbabba) |
| ⇒ babbb |
Flip LHS and RHS.
Overlap of [3] bbabba=babbb with [3] bbabba=babbb:
Critical pair: bbababbb=babbbbba.
Reduce LHS:
| [4] | b(bababbb) |
| ⇒ bba |
Flip LHS and RHS.
Overlap of [6] babbba=babbb with [3] bbabba=babbb:
Critical pair: babbabbb=babbbbba.
Reduce LHS:
| [2] | ba(bbabbb) |
| ⇒ baba |
Reduce RHS:
| [7] | (babbbbba) |
| ⇒ bba |
Overlap of [8] baba=bba with [8] baba=bba:
Critical pair: babba=bbaba.
Reduce LHS:
| [5] | (babba) |
| ⇒ babbbbbb |
Reduce RHS:
| [8] | b(baba) |
| ⇒ bbba |
Flip LHS and RHS.
Referenced by [10].
Simplify [7] babbbbba=bba.
Reduce LHS:
| [9] | babb(bbba) |
| [6] | ⇒ (babbba)bbbbbb |
| ⇒ babbbbbbbbb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [2] bbabbb=ba with [10] bba=babbbbbbbbb:
Critical pair: babbbbbbbbbbbb=ba.
Defines rule #1.
Simplify [8] baba=bba.
Reduce RHS:
| [10] | (bba) |
| ⇒ babbbbbbbbb |
Defines rule #4.