| Back: | ⟨a, b | aba=b, aaaa=bbb⟩ |
|---|
Completion settings:
Axiom: aba=b.
Referenced by [3], [4], [5], [6], [7], [8], [9], [10], [11].
Axiom: aaaa=bbb.
Defines rule #3.
Referenced by [4], [5], [6], [7].
Overlap of [1] aba=b with [1] aba=b:
Critical pair: abb=bba.
Flip LHS and RHS.
Referenced by [5].
Overlap of [1] aba=b with [2] aaaa=bbb:
Critical pair: abbbb=baaa.
Referenced by [5].
Overlap of [2] aaaa=bbb with [1] aba=b:
Critical pair: aaab=bbbba.
Reduce RHS:
| [3] | bb(bba) |
| [3] | ⇒ (bba)bb |
| [4] | ⇒ (abbbb) |
| ⇒ baaa |
Flip LHS and RHS.
Overlap of [1] aba=b with [5] baaa=aaab:
Critical pair: aaaab=baa.
Reduce LHS:
| [2] | (aaaa)b |
| ⇒ bbbb |
Overlap of [5] baaa=aaab with [2] aaaa=bbb:
Critical pair: bbbb=aaaba.
Reduce LHS:
| [6] | (bbbb) |
| ⇒ baa |
Reduce RHS:
| [1] | aa(aba) |
| ⇒ aab |
Overlap of [1] aba=b with [7] baa=aab:
Critical pair: aaab=ba.
Referenced by [9].
Overlap of [5] baaa=aaab with [7] baa=aab:
Critical pair: aaba=aaab.
Reduce LHS:
| [1] | a(aba) |
| ⇒ ab |
Reduce RHS:
| [8] | (aaab) |
| ⇒ ba |
Flip LHS and RHS.
Defines rule #1.
Overlap of [7] baa=aab with [9] ba=ab:
Critical pair: aba=aab.
Reduce LHS:
| [1] | (aba) |
| ⇒ b |
Flip LHS and RHS.
Defines rule #2.
Simplify [6] bbbb=baa.
Reduce RHS:
| [9] | (ba)a |
| [1] | ⇒ (aba) |
| ⇒ b |
Defines rule #4.