Certificate for #4327 ⟨a, b | abbaaaaab=ba

Completion settings:

[1] abbaaaaab=ba

Axiom: abbaaaaab=ba.

Referenced by [4].

[2] baaaaa=c

Axiom: baaaaa=c.

Referenced by [4], [5].

[3] ab=d

Axiom: ab=d.

Defines rule #28.

Referenced by [4], [6], [7], [10].

[4] ba=dcb

Overlap of [1] abbaaaaab=ba with [3] ab=d:

abbaaaaab ab

Critical pair: dbaaaaab=ba.

Reduce LHS:

[2]d(baaaaa)b
dcb

Flip LHS and RHS.

Defines rule #31.

Referenced by [5], [6], [7], [8].

[5] dcdcdcdcdcb=c

Overlap of [2] baaaaa=c with [4] ba=dcb:

baaaaa ba

Critical pair: dcbaaaa=c.

Reduce LHS:

[4]dc(ba)aaa
[4]dcdc(ba)aa
[4]dcdcdc(ba)a
[4]dcdcdcdc(ba)
dcdcdcdcdcb

Defines rule #3.

Referenced by [8], [9], [11], [15], [16], [21], [28].

[6] da=adcb

Overlap of [3] ab=d with [4] ba=dcb:

a b ba

Critical pair: adcb=da.

Flip LHS and RHS.

Defines rule #30.

[7] dcbb=bd

Overlap of [4] ba=dcb with [3] ab=d:

b a ab

Critical pair: bd=dcbb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [9], [12], [22], [33].

[8] ca=dcc

Overlap of [5] dcdcdcdcdcb=c with [4] ba=dcb:

dcdcdcdcdc b ba

Critical pair: dcdcdcdcdcdcb=ca.

Reduce LHS:

[5]dc(dcdcdcdcdcb)
dcc

Flip LHS and RHS.

Defines rule #29.

Referenced by [10].

[9] dcdcdcdcbd=cb

Overlap of [5] dcdcdcdcdcb=c with [7] dcbb=bd:

dcdcdcdc dcb dcbb

Critical pair: dcdcdcdcbd=cb.

Defines rule #2.

Referenced by [11], [12], [13], [14], [23], [29], [30].

[10] dccb=cd

Overlap of [8] ca=dcc with [3] ab=d:

c a ab

Critical pair: cd=dccb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [19], [24].

[11] cbcdcdcdcdcb=dcdcdcdcbc

Overlap of [9] dcdcdcdcbd=cb with [5] dcdcdcdcdcb=c:

dcdcdcdcb d dcdcdcdcdcb

Critical pair: dcdcdcdcbc=cbcdcdcdcdcb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [16], [17], [18], [29].

[12] cbcbb=dcdcdcbdd

Overlap of [9] dcdcdcdcbd=cb with [7] dcbb=bd:

dcdcdcdcb d dcbb

Critical pair: dcdcdcdcbbd=cbcbb.

Reduce LHS:

[7]dcdcdc(dcbb)d
dcdcdcbdd

Flip LHS and RHS.

Defines rule #23.

Referenced by [15], [27].

[13] dcdcdcdcbcb=cbcdcdcdcbd

Overlap of [9] dcdcdcdcbd=cb with [9] dcdcdcdcbd=cb:

dcdcdcdcb d dcdcdcdcbd

Critical pair: dcdcdcdcbcb=cbcdcdcdcbd.

Defines rule #14.

Referenced by [27].

[14] cbccb=dcdcdcdcbcd

Overlap of [9] dcdcdcdcbd=cb with [10] dccb=cd:

dcdcdcdcb d dccb

Critical pair: dcdcdcdcbcd=cbccb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [18], [20], [32].

[15] ccbb=dcdcdcdcddcdcdcbdd

Overlap of [5] dcdcdcdcdcb=c with [12] cbcbb=dcdcdcbdd:

dcdcdcdcd cb cbcbb

Critical pair: dcdcdcdcddcdcdcbdd=ccbb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [19], [20].

[16] dcdcdcdcddcdcdcdcbc=ccdcdcdcdcb

Overlap of [5] dcdcdcdcdcb=c with [11] cbcdcdcdcdcb=dcdcdcdcbc:

dcdcdcdcd cb cbcdcdcdcdcb

Critical pair: dcdcdcdcddcdcdcdcbc=ccdcdcdcdcb.

Defines rule #5.

Referenced by [29], [30], [31].

[17] dcdcdcdcbccdcdcdcdcb=cbcdcdcdcddcdcdcdcbc

Overlap of [11] cbcdcdcdcdcb=dcdcdcdcbc with [11] cbcdcdcdcdcb=dcdcdcdcbc:

cbcdcdcdcd cb cbcdcdcdcdcb

Critical pair: cbcdcdcdcddcdcdcdcbc=dcdcdcdcbccdcdcdcdcb.

Flip LHS and RHS.

Defines rule #17.

[18] dcdcdcdcbcccb=cbcdcdcdcddcdcdcdcbcd

Overlap of [11] cbcdcdcdcdcb=dcdcdcdcbc with [14] cbccb=dcdcdcdcbcd:

cbcdcdcdcd cb cbccb

Critical pair: cbcdcdcdcddcdcdcdcbcd=dcdcdcdcbcccb.

Flip LHS and RHS.

Defines rule #16.

[19] ddcdcdcdcddcdcdcbdd=cdb

Overlap of [10] dccb=cd with [15] ccbb=dcdcdcdcddcdcdcbdd:

d ccb ccbb

Critical pair: ddcdcdcdcddcdcdcbdd=cdb.

Defines rule #4.

Referenced by [21], [22], [23], [24], [25], [26], [31].

[20] dcdcdcdcbcdb=cbdcdcdcdcddcdcdcbdd

Overlap of [14] cbccb=dcdcdcdcbcd with [15] ccbb=dcdcdcdcddcdcdcbdd:

cb ccb ccbb

Critical pair: cbdcdcdcdcddcdcdcbdd=dcdcdcdcbcdb.

Flip LHS and RHS.

Defines rule #15.

[21] cdbcdcdcdcdcb=ddcdcdcdcddcdcdcbdc

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [5] dcdcdcdcdcb=c:

ddcdcdcdcddcdcdcbd d dcdcdcdcdcb

Critical pair: ddcdcdcdcddcdcdcbdc=cdbcdcdcdcdcb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [32].

[22] cdbcbb=ddcdcdcdcddcdcdcbdbd

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [7] dcbb=bd:

ddcdcdcdcddcdcdcbd d dcbb

Critical pair: ddcdcdcdcddcdcdcbdbd=cdbcbb.

Flip LHS and RHS.

Defines rule #25.

[23] ddcdcdcdcddcdcdcbdcb=cdbcdcdcdcbd

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [9] dcdcdcdcbd=cb:

ddcdcdcdcddcdcdcbd d dcdcdcdcbd

Critical pair: ddcdcdcdcddcdcdcbdcb=cdbcdcdcdcbd.

Defines rule #19.

Referenced by [33].

[24] cdbccb=ddcdcdcdcddcdcdcbdcd

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [10] dccb=cd:

ddcdcdcdcddcdcdcbd d dccb

Critical pair: ddcdcdcdcddcdcdcbdcd=cdbccb.

Flip LHS and RHS.

Defines rule #9.

[25] ddcdcdcdcddcdcdcbcdb=cdbcdcdcdcddcdcdcbdd

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [19] ddcdcdcdcddcdcdcbdd=cdb:

ddcdcdcdcddcdcdcb dd ddcdcdcdcddcdcdcbdd

Critical pair: ddcdcdcdcddcdcdcbcdb=cdbcdcdcdcddcdcdcbdd.

Defines rule #18.

[26] ddcdcdcdcddcdcdcbdcdb=cdbdcdcdcdcddcdcdcbdd

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [19] ddcdcdcdcddcdcdcbdd=cdb:

ddcdcdcdcddcdcdcbd d ddcdcdcdcddcdcdcbdd

Critical pair: ddcdcdcdcddcdcdcbdcdb=cdbdcdcdcdcddcdcdcbdd.

Defines rule #20.

[27] cbcdcdcdcbdb=dcdcdcddcdcdcbdd

Overlap of [13] dcdcdcdcbcb=cbcdcdcdcbd with [12] cbcbb=dcdcdcbdd:

dcdcdcd cbcb cbcbb

Critical pair: dcdcdcddcdcdcbdd=cbcdcdcdcbdb.

Flip LHS and RHS.

Defines rule #24.

Referenced by [28], [30].

[28] ccdcdcdcbdb=dcdcdcdcddcdcdcddcdcdcbdd

Overlap of [5] dcdcdcdcdcb=c with [27] cbcdcdcdcbdb=dcdcdcddcdcdcbdd:

dcdcdcdcd cb cbcdcdcdcbdb

Critical pair: dcdcdcdcddcdcdcddcdcdcbdd=ccdcdcdcbdb.

Flip LHS and RHS.

Defines rule #13.

[29] cccbcdcdcdcb=dcdcdcdcddcdcdcddcdcdcdcbc

Overlap of [16] dcdcdcdcddcdcdcdcbc=ccdcdcdcdcb with [11] cbcdcdcdcdcb=dcdcdcdcbc:

dcdcdcdcddcdcdcd cbc cbcdcdcdcdcb

Critical pair: dcdcdcdcddcdcdcddcdcdcdcbc=ccdcdcdcdcbdcdcdcdcb.

Reduce RHS:

[9]cc(dcdcdcdcbd)cdcdcdcb
cccbcdcdcdcb

Flip LHS and RHS.

Defines rule #12.

[30] cccbcdcdcbdb=dcdcdcdcddcdcdcddcdcdcddcdcdcbdd

Overlap of [16] dcdcdcdcddcdcdcdcbc=ccdcdcdcdcb with [27] cbcdcdcdcbdb=dcdcdcddcdcdcbdd:

dcdcdcdcddcdcdcd cbc cbcdcdcdcbdb

Critical pair: dcdcdcdcddcdcdcddcdcdcddcdcdcbdd=ccdcdcdcdcbdcdcdcbdb.

Reduce RHS:

[9]cc(dcdcdcdcbd)cdcdcbdb
cccbcdcdcbdb

Flip LHS and RHS.

Defines rule #27.

[31] ddcdcdcdcddcdcdcbdccdcdcdcdcb=cdbcdcdcdcddcdcdcdcbc

Overlap of [19] ddcdcdcdcddcdcdcbdd=cdb with [16] dcdcdcdcddcdcdcdcbc=ccdcdcdcdcb:

ddcdcdcdcddcdcdcbd d dcdcdcdcddcdcdcdcbc

Critical pair: ddcdcdcdcddcdcdcbdccdcdcdcdcb=cdbcdcdcdcddcdcdcdcbc.

Defines rule #22.

[32] ddcdcdcdcddcdcdcbdcccb=cdbcdcdcdcddcdcdcdcbcd

Overlap of [21] cdbcdcdcdcdcb=ddcdcdcdcddcdcdcbdc with [14] cbccb=dcdcdcdcbcd:

cdbcdcdcdcd cb cbccb

Critical pair: cdbcdcdcdcddcdcdcdcbcd=ddcdcdcdcddcdcdcbdcccb.

Flip LHS and RHS.

Defines rule #21.

[33] cdbcdcdcdcbdb=ddcdcdcdcddcdcbdd

Overlap of [23] ddcdcdcdcddcdcdcbdcb=cdbcdcdcdcbd with [7] dcbb=bd:

ddcdcdcdcddcdcdcb dcb dcbb

Critical pair: ddcdcdcdcddcdcdcbbd=cdbcdcdcdcbdb.

Reduce LHS:

[7]ddcdcdcdcddcdc(dcbb)d
ddcdcdcdcddcdcbdd

Flip LHS and RHS.

Defines rule #26.