| Back: | ⟨a, b | abaaab=baaba⟩ |
|---|
Completion settings:
Axiom: abaaab=baaba.
Flip LHS and RHS.
Referenced by [5].
Axiom: baa=c.
Defines rule #4.
Referenced by [6], [8], [9], [11], [13], [14].
Axiom: ab=d.
Defines rule #3.
Referenced by [5], [7], [8], [9], [11].
Axiom: da=e.
Defines rule #2.
Referenced by [5], [7], [9], [10], [11], [12], [13], [15].
Simplify [1] baaba=abaaab.
Reduce RHS:
| [3] | (ab)aaab |
| [4] | ⇒ (da)aab |
| [3] | ⇒ ea(ab) |
| ⇒ ead |
Referenced by [6].
Overlap of [5] baaba=ead with [2] baa=c:
Critical pair: cba=ead.
Referenced by [10].
Overlap of [4] da=e with [3] ab=d:
Critical pair: dd=eb.
Flip LHS and RHS.
Defines rule #9.
Overlap of [2] baa=c with [3] ab=d:
Critical pair: bad=cb.
Flip LHS and RHS.
Defines rule #8.
Referenced by [10].
Overlap of [3] ab=d with [2] baa=c:
Critical pair: ac=daa.
Reduce RHS:
| [4] | (da)a |
| ⇒ ea |
Flip LHS and RHS.
Defines rule #1.
Referenced by [10], [13], [16].
Simplify [6] cba=ead.
Reduce LHS:
| [8] | (cb)a |
| [4] | ⇒ ba(da) |
| ⇒ bae |
Reduce RHS:
| [9] | (ea)d |
| ⇒ acd |
Flip LHS and RHS.
Defines rule #7.
Referenced by [11], [12], [13].
Overlap of [2] baa=c with [10] acd=bae:
Critical pair: babae=ccd.
Reduce LHS:
| [3] | b(ab)ae |
| [4] | ⇒ b(da)e |
| ⇒ bee |
Flip LHS and RHS.
Defines rule #12.
Overlap of [4] da=e with [10] acd=bae:
Critical pair: dbae=ecd.
Flip LHS and RHS.
Defines rule #13.
Overlap of [10] acd=bae with [4] da=e:
Critical pair: ace=baea.
Reduce RHS:
| [9] | ba(ea) |
| [2] | ⇒ (baa)c |
| ⇒ cc |
Defines rule #6.
Referenced by [14], [15], [16].
Overlap of [2] baa=c with [13] ace=cc:
Critical pair: bacc=cce.
Flip LHS and RHS.
Defines rule #10.
Overlap of [4] da=e with [13] ace=cc:
Critical pair: dcc=ece.
Flip LHS and RHS.
Defines rule #11.
Overlap of [13] ace=cc with [9] ea=ac:
Critical pair: acac=cca.
Flip LHS and RHS.
Defines rule #5.