| Back: | ⟨a, b | aa=a, babbb=bba⟩ |
|---|
Completion settings:
Axiom: aa=a.
Defines rule #3.
Referenced by [3].
Axiom: babbb=bba.
Flip LHS and RHS.
Defines rule #2.
Overlap of [2] bba=babbb with [1] aa=a:
Critical pair: bba=babbba.
Reduce LHS:
| [2] | (bba) |
| ⇒ babbb |
Reduce RHS:
| [2] | bab(bba) |
| [2] | ⇒ ba(bba)bbb |
| ⇒ bababbbbbb |
Flip LHS and RHS.
Overlap of [2] bba=babbb with [3] bababbbbbb=babbb:
Critical pair: bbabbb=babbbbabbbbbb.
Reduce LHS:
| [2] | (bba)bbb |
| ⇒ babbbbbb |
Reduce RHS:
| [2] | babb(bba)bbbbbb |
| [2] | ⇒ bab(bba)bbbbbbbbb |
| [2] | ⇒ ba(bba)bbbbbbbbbbbb |
| [3] | ⇒ (bababbbbbb)bbbbbbbbb |
| ⇒ babbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [5].
Overlap of [3] bababbbbbb=babbb with [4] babbbbbbbbbbbb=babbbbbb:
Critical pair: bababbbbbb=babbbbbbbbb.
Reduce LHS:
| [3] | (bababbbbbb) |
| ⇒ babbb |
Flip LHS and RHS.
Defines rule #1.
Referenced by [6].
Overlap of [3] bababbbbbb=babbb with [5] babbbbbbbbb=babbb:
Critical pair: bababbb=babbbbbb.
Defines rule #4.