| Back: | ⟨a, b, c | ab=1, bbcaa=c⟩ |
|---|
Completion settings:
Axiom: ab=1.
Defines rule #1.
Referenced by [4], [5], [6], [7], [8], [11].
Axiom: bbcaa=c.
Axiom: cbb=d.
Defines rule #6.
Referenced by [8], [11], [12], [14], [16].
Overlap of [1] ab=1 with [2] bbcaa=c:
Critical pair: ac=bcaa.
Flip LHS and RHS.
Overlap of [2] bbcaa=c with [1] ab=1:
Critical pair: bbca=cb.
Overlap of [1] ab=1 with [4] bcaa=ac:
Critical pair: aac=caa.
Defines rule #7.
Referenced by [8].
Overlap of [4] bcaa=ac with [1] ab=1:
Critical pair: bca=acb.
Referenced by [10], [11], [13].
Overlap of [6] aac=caa with [3] cbb=d:
Critical pair: aad=caabb.
Reduce RHS:
| [1] | ca(ab)b |
| [1] | ⇒ c(ab) |
| ⇒ c |
Defines rule #8.
Overlap of [2] bbcaa=c with [5] bbca=cb:
Critical pair: cba=c.
Defines rule #5.
Referenced by [12], [15], [17].
Overlap of [5] bbca=cb with [7] bca=acb:
Critical pair: bacb=cb.
Overlap of [7] bca=acb with [1] ab=1:
Critical pair: bc=acbb.
Reduce RHS:
| [3] | a(cbb) |
| ⇒ ad |
Defines rule #2.
Referenced by [12], [13], [14], [15].
Overlap of [3] cbb=d with [11] bc=ad:
Critical pair: cbad=dc.
Reduce LHS:
| [9] | (cba)d |
| ⇒ cd |
Flip LHS and RHS.
Defines rule #3.
Overlap of [7] bca=acb with [11] bc=ad:
Critical pair: ada=acb.
Referenced by [18].
Overlap of [11] bc=ad with [3] cbb=d:
Critical pair: bd=adbb.
Flip LHS and RHS.
Referenced by [19].
Overlap of [11] bc=ad with [9] cba=c:
Critical pair: bc=adba.
Reduce LHS:
| [11] | (bc) |
| ⇒ ad |
Flip LHS and RHS.
Referenced by [20].
Overlap of [10] bacb=cb with [3] cbb=d:
Critical pair: bad=cbb.
Reduce RHS:
| [3] | (cbb) |
| ⇒ d |
Defines rule #10.
Referenced by [18], [19], [20].
Overlap of [10] bacb=cb with [9] cba=c:
Critical pair: bac=cba.
Reduce RHS:
| [9] | (cba) |
| ⇒ c |
Defines rule #9.
Referenced by [18].
Overlap of [16] bad=d with [13] ada=acb:
Critical pair: bacb=da.
Reduce LHS:
| [17] | (bac)b |
| ⇒ cb |
Flip LHS and RHS.
Defines rule #4.
Overlap of [16] bad=d with [14] adbb=bd:
Critical pair: bbd=dbb.
Flip LHS and RHS.
Defines rule #12.
Overlap of [16] bad=d with [15] adba=ad:
Critical pair: bad=dba.
Reduce LHS:
| [16] | (bad) |
| ⇒ d |
Flip LHS and RHS.
Defines rule #11.