| Back: | ⟨a, b | abbaabaab=ba⟩ |
|---|
Completion settings:
Axiom: abbaabaab=ba.
Referenced by [4].
Axiom: baa=c.
Axiom: ab=d.
Defines rule #26.
Referenced by [4], [6], [7], [10].
Overlap of [1] abbaabaab=ba with [3] ab=d:
Critical pair: dbaabaab=ba.
Reduce LHS:
| [2] | d(baa)baab |
| [2] | ⇒ dc(baa)b |
| ⇒ dccb |
Flip LHS and RHS.
Defines rule #29.
Referenced by [5], [6], [7], [8].
Overlap of [2] baa=c with [4] ba=dccb:
Critical pair: dccba=c.
Reduce LHS:
| [4] | dcc(ba) |
| ⇒ dccdccb |
Defines rule #3.
Referenced by [8], [9], [11], [15], [16], [21].
Overlap of [3] ab=d with [4] ba=dccb:
Critical pair: adccb=da.
Flip LHS and RHS.
Defines rule #28.
Overlap of [4] ba=dccb with [3] ab=d:
Critical pair: bd=dccbb.
Flip LHS and RHS.
Defines rule #11.
Referenced by [9], [12], [22].
Overlap of [5] dccdccb=c with [4] ba=dccb:
Critical pair: dccdccdccb=ca.
Reduce LHS:
| [5] | dcc(dccdccb) |
| ⇒ dccc |
Flip LHS and RHS.
Defines rule #27.
Referenced by [10].
Overlap of [5] dccdccb=c with [7] dccbb=bd:
Critical pair: dccbd=cb.
Defines rule #1.
Referenced by [11], [12], [13], [14], [23].
Overlap of [8] ca=dccc with [3] ab=d:
Critical pair: cd=dcccb.
Flip LHS and RHS.
Defines rule #2.
Referenced by [14], [19], [24].
Overlap of [9] dccbd=cb with [5] dccdccb=c:
Critical pair: dccbc=cbccdccb.
Flip LHS and RHS.
Defines rule #7.
Referenced by [16], [17], [18], [27].
Overlap of [9] dccbd=cb with [7] dccbb=bd:
Critical pair: dccbbd=cbccbb.
Reduce LHS:
| [7] | (dccbb)d |
| ⇒ bdd |
Flip LHS and RHS.
Defines rule #23.
Overlap of [9] dccbd=cb with [9] dccbd=cb:
Critical pair: dccbcb=cbccbd.
Defines rule #12.
Referenced by [28].
Overlap of [9] dccbd=cb with [10] dcccb=cd:
Critical pair: dccbcd=cbcccb.
Flip LHS and RHS.
Defines rule #6.
Referenced by [18], [20], [29], [31].
Overlap of [5] dccdccb=c with [12] cbccbb=bdd:
Critical pair: dccdcbdd=cccbb.
Flip LHS and RHS.
Defines rule #10.
Overlap of [5] dccdccb=c with [11] cbccdccb=dccbc:
Critical pair: dccdcdccbc=cccdccb.
Defines rule #5.
Referenced by [27], [28], [29], [30].
Overlap of [11] cbccdccb=dccbc with [11] cbccdccb=dccbc:
Critical pair: cbccdcdccbc=dccbcccdccb.
Flip LHS and RHS.
Defines rule #15.
Overlap of [11] cbccdccb=dccbc with [14] cbcccb=dccbcd:
Critical pair: cbccdcdccbcd=dccbccccb.
Flip LHS and RHS.
Defines rule #14.
Overlap of [10] dcccb=cd with [15] cccbb=dccdcbdd:
Critical pair: ddccdcbdd=cdb.
Defines rule #4.
Referenced by [21], [22], [23], [24], [25], [26], [30].
Overlap of [14] cbcccb=dccbcd with [15] cccbb=dccdcbdd:
Critical pair: cbdccdcbdd=dccbcdb.
Flip LHS and RHS.
Defines rule #13.
Overlap of [19] ddccdcbdd=cdb with [5] dccdccb=c:
Critical pair: ddccdcbdc=cdbccdccb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [31].
Overlap of [19] ddccdcbdd=cdb with [7] dccbb=bd:
Critical pair: ddccdcbdbd=cdbccbb.
Flip LHS and RHS.
Defines rule #24.
Overlap of [19] ddccdcbdd=cdb with [9] dccbd=cb:
Critical pair: ddccdcbdcb=cdbccbd.
Defines rule #19.
Overlap of [19] ddccdcbdd=cdb with [10] dcccb=cd:
Critical pair: ddccdcbdcd=cdbcccb.
Flip LHS and RHS.
Defines rule #8.
Overlap of [19] ddccdcbdd=cdb with [19] ddccdcbdd=cdb:
Critical pair: ddccdcbcdb=cdbccdcbdd.
Defines rule #18.
Overlap of [19] ddccdcbdd=cdb with [19] ddccdcbdd=cdb:
Critical pair: ddccdcbdcdb=cdbdccdcbdd.
Defines rule #20.
Overlap of [16] dccdcdccbc=cccdccb with [11] cbccdccb=dccbc:
Critical pair: dccdcdcdccbc=cccdccbcdccb.
Flip LHS and RHS.
Defines rule #17.
Overlap of [16] dccdcdccbc=cccdccb with [12] cbccbb=bdd:
Critical pair: dccdcdcbdd=cccdccbcbb.
Reduce RHS:
| [13] | ccc(dccbcb)b |
| ⇒ ccccbccbdb |
Flip LHS and RHS.
Defines rule #25.
Overlap of [16] dccdcdccbc=cccdccb with [14] cbcccb=dccbcd:
Critical pair: dccdcdcdccbcd=cccdccbccb.
Flip LHS and RHS.
Defines rule #16.
Overlap of [19] ddccdcbdd=cdb with [16] dccdcdccbc=cccdccb:
Critical pair: ddccdcbdcccdccb=cdbccdcdccbc.
Defines rule #22.
Overlap of [21] cdbccdccb=ddccdcbdc with [14] cbcccb=dccbcd:
Critical pair: cdbccdcdccbcd=ddccdcbdccccb.
Flip LHS and RHS.
Defines rule #21.