| Back: | ⟨a, b | abbbba=bab⟩ |
|---|
Completion settings:
Axiom: abbbba=bab.
Referenced by [6].
Axiom: ab=c.
Defines rule #1.
Referenced by [6], [7], [8], [12].
Axiom: cb=d.
Defines rule #2.
Referenced by [7], [8], [9], [13].
Axiom: db=e.
Defines rule #3.
Referenced by [7], [9], [10], [14].
Axiom: eb=f.
Defines rule #4.
Referenced by [7], [10], [11], [15].
Simplify [1] abbbba=bab.
Reduce RHS:
| [2] | b(ab) |
| ⇒ bc |
Referenced by [7].
Overlap of [6] abbbba=bc with [2] ab=c:
Critical pair: cbbba=bc.
Reduce LHS:
| [3] | (cb)bba |
| [4] | ⇒ (db)ba |
| [5] | ⇒ (eb)a |
| ⇒ fa |
Defines rule #5.
Referenced by [8].
Overlap of [7] fa=bc with [2] ab=c:
Critical pair: fc=bcb.
Reduce RHS:
| [3] | b(cb) |
| ⇒ bd |
Defines rule #6.
Referenced by [9].
Overlap of [8] fc=bd with [3] cb=d:
Critical pair: fd=bdb.
Reduce RHS:
| [4] | b(db) |
| ⇒ be |
Defines rule #7.
Referenced by [10].
Overlap of [9] fd=be with [4] db=e:
Critical pair: fe=beb.
Reduce RHS:
| [5] | b(eb) |
| ⇒ bf |
Defines rule #8.
Referenced by [11].
Overlap of [10] fe=bf with [5] eb=f:
Critical pair: ff=bfb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [12], [13], [14], [15].
Overlap of [2] ab=c with [11] bfb=ff:
Critical pair: aff=cfb.
Flip LHS and RHS.
Defines rule #10.
Overlap of [3] cb=d with [11] bfb=ff:
Critical pair: cff=dfb.
Flip LHS and RHS.
Defines rule #11.
Overlap of [4] db=e with [11] bfb=ff:
Critical pair: dff=efb.
Flip LHS and RHS.
Defines rule #12.
Overlap of [5] eb=f with [11] bfb=ff:
Critical pair: eff=ffb.
Flip LHS and RHS.
Defines rule #13.