| Back: | ⟨a, b | abbbbba=bab⟩ |
|---|
Completion settings:
Axiom: abbbbba=bab.
Referenced by [7].
Axiom: ab=c.
Defines rule #1.
Referenced by [7], [8], [9], [14].
Axiom: cb=d.
Defines rule #2.
Referenced by [8], [9], [10], [15].
Axiom: db=e.
Defines rule #3.
Referenced by [8], [10], [11], [16].
Axiom: eb=f.
Defines rule #4.
Referenced by [8], [11], [12], [17].
Axiom: fb=g.
Defines rule #5.
Referenced by [8], [12], [13], [18].
Simplify [1] abbbbba=bab.
Reduce RHS:
| [2] | b(ab) |
| ⇒ bc |
Referenced by [8].
Overlap of [7] abbbbba=bc with [2] ab=c:
Critical pair: cbbbba=bc.
Reduce LHS:
| [3] | (cb)bbba |
| [4] | ⇒ (db)bba |
| [5] | ⇒ (eb)ba |
| [6] | ⇒ (fb)a |
| ⇒ ga |
Defines rule #6.
Referenced by [9].
Overlap of [8] ga=bc with [2] ab=c:
Critical pair: gc=bcb.
Reduce RHS:
| [3] | b(cb) |
| ⇒ bd |
Defines rule #7.
Referenced by [10].
Overlap of [9] gc=bd with [3] cb=d:
Critical pair: gd=bdb.
Reduce RHS:
| [4] | b(db) |
| ⇒ be |
Defines rule #8.
Referenced by [11].
Overlap of [10] gd=be with [4] db=e:
Critical pair: ge=beb.
Reduce RHS:
| [5] | b(eb) |
| ⇒ bf |
Defines rule #9.
Referenced by [12].
Overlap of [11] ge=bf with [5] eb=f:
Critical pair: gf=bfb.
Reduce RHS:
| [6] | b(fb) |
| ⇒ bg |
Defines rule #10.
Referenced by [13].
Overlap of [12] gf=bg with [6] fb=g:
Critical pair: gg=bgb.
Flip LHS and RHS.
Defines rule #11.
Referenced by [14], [15], [16], [17], [18].
Overlap of [2] ab=c with [13] bgb=gg:
Critical pair: agg=cgb.
Flip LHS and RHS.
Defines rule #12.
Overlap of [3] cb=d with [13] bgb=gg:
Critical pair: cgg=dgb.
Flip LHS and RHS.
Defines rule #13.
Overlap of [4] db=e with [13] bgb=gg:
Critical pair: dgg=egb.
Flip LHS and RHS.
Defines rule #14.
Overlap of [5] eb=f with [13] bgb=gg:
Critical pair: egg=fgb.
Flip LHS and RHS.
Defines rule #15.
Overlap of [6] fb=g with [13] bgb=gg:
Critical pair: fgg=ggb.
Flip LHS and RHS.
Defines rule #16.