Certificate for #2073 ⟨a, b | abbaaaab=ba

Completion settings:

[1] abbaaaab=ba

Axiom: abbaaaab=ba.

Referenced by [4].

[2] baaaa=c

Axiom: baaaa=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] abbaaaab=ba with [3] ab=d:

abbaaaab ab

Critical pair: dbaaaab=ba.

Reduce LHS:

[2]d(baaaa)b
dcb

Flip LHS and RHS.

Defines rule #31.

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

[5] dcdcdcdcb=c

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

baaaa ba

Critical pair: dcbaaa=c.

Reduce LHS:

[4]dc(ba)aa
[4]dcdc(ba)a
[4]dcdcdc(ba)
dcdcdcdcb

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] dcdcdcdcb=c with [4] ba=dcb:

dcdcdcdc b ba

Critical pair: dcdcdcdcdcb=ca.

Reduce LHS:

[5]dc(dcdcdcdcb)
dcc

Flip LHS and RHS.

Defines rule #29.

Referenced by [10].

[9] dcdcdcbd=cb

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

dcdcdc dcb dcbb

Critical pair: dcdcdcbd=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] cbcdcdcdcb=dcdcdcbc

Overlap of [9] dcdcdcbd=cb with [5] dcdcdcdcb=c:

dcdcdcb d dcdcdcdcb

Critical pair: dcdcdcbc=cbcdcdcdcb.

Flip LHS and RHS.

Defines rule #7.

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

[12] cbcbb=dcdcbdd

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

dcdcdcb d dcbb

Critical pair: dcdcdcbbd=cbcbb.

Reduce LHS:

[7]dcdc(dcbb)d
dcdcbdd

Flip LHS and RHS.

Defines rule #23.

Referenced by [15], [27].

[13] dcdcdcbcb=cbcdcdcbd

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

dcdcdcb d dcdcdcbd

Critical pair: dcdcdcbcb=cbcdcdcbd.

Defines rule #14.

Referenced by [27].

[14] cbccb=dcdcdcbcd

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

dcdcdcb d dccb

Critical pair: dcdcdcbcd=cbccb.

Flip LHS and RHS.

Defines rule #6.

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

[15] ccbb=dcdcdcddcdcbdd

Overlap of [5] dcdcdcdcb=c with [12] cbcbb=dcdcbdd:

dcdcdcd cb cbcbb

Critical pair: dcdcdcddcdcbdd=ccbb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [19], [20].

[16] dcdcdcddcdcdcbc=ccdcdcdcb

Overlap of [5] dcdcdcdcb=c with [11] cbcdcdcdcb=dcdcdcbc:

dcdcdcd cb cbcdcdcdcb

Critical pair: dcdcdcddcdcdcbc=ccdcdcdcb.

Defines rule #5.

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

[17] dcdcdcbccdcdcdcb=cbcdcdcddcdcdcbc

Overlap of [11] cbcdcdcdcb=dcdcdcbc with [11] cbcdcdcdcb=dcdcdcbc:

cbcdcdcd cb cbcdcdcdcb

Critical pair: cbcdcdcddcdcdcbc=dcdcdcbccdcdcdcb.

Flip LHS and RHS.

Defines rule #17.

[18] dcdcdcbcccb=cbcdcdcddcdcdcbcd

Overlap of [11] cbcdcdcdcb=dcdcdcbc with [14] cbccb=dcdcdcbcd:

cbcdcdcd cb cbccb

Critical pair: cbcdcdcddcdcdcbcd=dcdcdcbcccb.

Flip LHS and RHS.

Defines rule #16.

[19] ddcdcdcddcdcbdd=cdb

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

d ccb ccbb

Critical pair: ddcdcdcddcdcbdd=cdb.

Defines rule #4.

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

[20] dcdcdcbcdb=cbdcdcdcddcdcbdd

Overlap of [14] cbccb=dcdcdcbcd with [15] ccbb=dcdcdcddcdcbdd:

cb ccb ccbb

Critical pair: cbdcdcdcddcdcbdd=dcdcdcbcdb.

Flip LHS and RHS.

Defines rule #15.

[21] cdbcdcdcdcb=ddcdcdcddcdcbdc

Overlap of [19] ddcdcdcddcdcbdd=cdb with [5] dcdcdcdcb=c:

ddcdcdcddcdcbd d dcdcdcdcb

Critical pair: ddcdcdcddcdcbdc=cdbcdcdcdcb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [32].

[22] cdbcbb=ddcdcdcddcdcbdbd

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

ddcdcdcddcdcbd d dcbb

Critical pair: ddcdcdcddcdcbdbd=cdbcbb.

Flip LHS and RHS.

Defines rule #25.

[23] ddcdcdcddcdcbdcb=cdbcdcdcbd

Overlap of [19] ddcdcdcddcdcbdd=cdb with [9] dcdcdcbd=cb:

ddcdcdcddcdcbd d dcdcdcbd

Critical pair: ddcdcdcddcdcbdcb=cdbcdcdcbd.

Defines rule #19.

Referenced by [33].

[24] cdbccb=ddcdcdcddcdcbdcd

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

ddcdcdcddcdcbd d dccb

Critical pair: ddcdcdcddcdcbdcd=cdbccb.

Flip LHS and RHS.

Defines rule #9.

[25] ddcdcdcddcdcbcdb=cdbcdcdcddcdcbdd

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

ddcdcdcddcdcb dd ddcdcdcddcdcbdd

Critical pair: ddcdcdcddcdcbcdb=cdbcdcdcddcdcbdd.

Defines rule #18.

[26] ddcdcdcddcdcbdcdb=cdbdcdcdcddcdcbdd

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

ddcdcdcddcdcbd d ddcdcdcddcdcbdd

Critical pair: ddcdcdcddcdcbdcdb=cdbdcdcdcddcdcbdd.

Defines rule #20.

[27] cbcdcdcbdb=dcdcddcdcbdd

Overlap of [13] dcdcdcbcb=cbcdcdcbd with [12] cbcbb=dcdcbdd:

dcdcd cbcb cbcbb

Critical pair: dcdcddcdcbdd=cbcdcdcbdb.

Flip LHS and RHS.

Defines rule #24.

Referenced by [28], [30].

[28] ccdcdcbdb=dcdcdcddcdcddcdcbdd

Overlap of [5] dcdcdcdcb=c with [27] cbcdcdcbdb=dcdcddcdcbdd:

dcdcdcd cb cbcdcdcbdb

Critical pair: dcdcdcddcdcddcdcbdd=ccdcdcbdb.

Flip LHS and RHS.

Defines rule #13.

[29] cccbcdcdcb=dcdcdcddcdcddcdcdcbc

Overlap of [16] dcdcdcddcdcdcbc=ccdcdcdcb with [11] cbcdcdcdcb=dcdcdcbc:

dcdcdcddcdcd cbc cbcdcdcdcb

Critical pair: dcdcdcddcdcddcdcdcbc=ccdcdcdcbdcdcdcb.

Reduce RHS:

[9]cc(dcdcdcbd)cdcdcb
cccbcdcdcb

Flip LHS and RHS.

Defines rule #12.

[30] cccbcdcbdb=dcdcdcddcdcddcdcddcdcbdd

Overlap of [16] dcdcdcddcdcdcbc=ccdcdcdcb with [27] cbcdcdcbdb=dcdcddcdcbdd:

dcdcdcddcdcd cbc cbcdcdcbdb

Critical pair: dcdcdcddcdcddcdcddcdcbdd=ccdcdcdcbdcdcbdb.

Reduce RHS:

[9]cc(dcdcdcbd)cdcbdb
cccbcdcbdb

Flip LHS and RHS.

Defines rule #27.

[31] ddcdcdcddcdcbdccdcdcdcb=cdbcdcdcddcdcdcbc

Overlap of [19] ddcdcdcddcdcbdd=cdb with [16] dcdcdcddcdcdcbc=ccdcdcdcb:

ddcdcdcddcdcbd d dcdcdcddcdcdcbc

Critical pair: ddcdcdcddcdcbdccdcdcdcb=cdbcdcdcddcdcdcbc.

Defines rule #22.

[32] ddcdcdcddcdcbdcccb=cdbcdcdcddcdcdcbcd

Overlap of [21] cdbcdcdcdcb=ddcdcdcddcdcbdc with [14] cbccb=dcdcdcbcd:

cdbcdcdcd cb cbccb

Critical pair: cdbcdcdcddcdcdcbcd=ddcdcdcddcdcbdcccb.

Flip LHS and RHS.

Defines rule #21.

[33] cdbcdcdcbdb=ddcdcdcddcbdd

Overlap of [23] ddcdcdcddcdcbdcb=cdbcdcdcbd with [7] dcbb=bd:

ddcdcdcddcdcb dcb dcbb

Critical pair: ddcdcdcddcdcbbd=cdbcdcdcbdb.

Reduce LHS:

[7]ddcdcdcddc(dcbb)d
ddcdcdcddcbdd

Flip LHS and RHS.

Defines rule #26.