| Back: | ⟨a, b, c | aba=b, bccb=1⟩ |
|---|
Completion settings:
Axiom: aba=b.
Defines rule #5.
Referenced by [5].
Axiom: bccb=1.
Referenced by [6], [7], [8], [9], [11].
Axiom: bb=d.
Defines rule #1.
Referenced by [4], [5], [7], [8].
Overlap of [3] bb=d with [3] bb=d:
Critical pair: bd=db.
Flip LHS and RHS.
Defines rule #3.
Referenced by [8].
Overlap of [1] aba=b with [1] aba=b:
Critical pair: abb=bba.
Reduce LHS:
| [3] | a(bb) |
| ⇒ ad |
Reduce RHS:
| [3] | (bb)a |
| ⇒ da |
Flip LHS and RHS.
Defines rule #2.
Referenced by [10].
Overlap of [2] bccb=1 with [2] bccb=1:
Critical pair: bcc=ccb.
Flip LHS and RHS.
Defines rule #7.
Referenced by [8].
Overlap of [2] bccb=1 with [3] bb=d:
Critical pair: bccd=b.
Referenced by [9].
Overlap of [3] bb=d with [2] bccb=1:
Critical pair: b=dccb.
Reduce RHS:
| [6] | d(ccb) |
| [4] | ⇒ (db)cc |
| ⇒ bdcc |
Flip LHS and RHS.
Referenced by [11].
Overlap of [2] bccb=1 with [7] bccd=b:
Critical pair: bccb=ccd.
Reduce LHS:
| [2] | (bccb) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #8.
Referenced by [10], [12], [14].
Overlap of [9] ccd=1 with [5] da=ad:
Critical pair: ccad=a.
Referenced by [13].
Overlap of [2] bccb=1 with [8] bdcc=b:
Critical pair: bccb=dcc.
Reduce LHS:
| [2] | (bccb) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [12].
Overlap of [11] dcc=1 with [9] ccd=1:
Critical pair: dc=cd.
Defines rule #4.
Overlap of [10] ccad=a with [12] dc=cd:
Critical pair: ccacd=ac.
Referenced by [14].
Overlap of [13] ccacd=ac with [12] dc=cd:
Critical pair: ccaccd=acc.
Reduce LHS:
| [9] | cca(ccd) |
| ⇒ cca |
Defines rule #6.