| Back: | ⟨a, b | aa=a, babbb=a⟩ |
|---|
Completion settings:
Axiom: aa=a.
Defines rule #3.
Referenced by [3], [4], [5], [6].
Axiom: babbb=a.
Referenced by [3], [4], [6], [7], [10].
Overlap of [2] babbb=a with [2] babbb=a:
Critical pair: babba=aabbb.
Reduce RHS:
| [1] | (aa)bbb |
| ⇒ abbb |
Referenced by [4], [5], [6], [7].
Overlap of [2] babbb=a with [3] babba=abbb:
Critical pair: babbabbb=aabba.
Reduce LHS:
| [3] | (babba)bbb |
| ⇒ abbbbbb |
Reduce RHS:
| [1] | (aa)bba |
| ⇒ abba |
Flip LHS and RHS.
Referenced by [8].
Overlap of [3] babba=abbb with [1] aa=a:
Critical pair: babba=abbba.
Reduce LHS:
| [3] | (babba) |
| ⇒ abbb |
Flip LHS and RHS.
Overlap of [3] babba=abbb with [3] babba=abbb:
Critical pair: bababbb=abbbbba.
Reduce LHS:
| [2] | ba(babbb) |
| [1] | ⇒ b(aa) |
| ⇒ ba |
Flip LHS and RHS.
Overlap of [5] abbba=abbb with [3] babba=abbb:
Critical pair: abbabbb=abbbbba.
Reduce LHS:
| [2] | ab(babbb) |
| ⇒ aba |
Reduce RHS:
| [6] | (abbbbba) |
| ⇒ ba |
Referenced by [8].
Overlap of [7] aba=ba with [7] aba=ba:
Critical pair: abba=baba.
Reduce LHS:
| [4] | (abba) |
| ⇒ abbbbbb |
Reduce RHS:
| [7] | b(aba) |
| ⇒ bba |
Flip LHS and RHS.
Referenced by [9].
Simplify [6] abbbbba=ba.
Reduce LHS:
| [8] | abbb(bba) |
| [5] | ⇒ (abbba)bbbbbb |
| ⇒ abbbbbbbbb |
Flip LHS and RHS.
Defines rule #2.
Referenced by [10].
Overlap of [2] babbb=a with [9] ba=abbbbbbbbb:
Critical pair: abbbbbbbbbbbb=a.
Defines rule #1.