Certificate for #15365 ⟨a, b | aba=bb, aaaaaa=1⟩

Completion settings:

Auxiliary generators:
1. c = aaaa
2. d = cbbc
3. e = dbdbd
Reduction order:
- Left-to-right recursive path with deg(b) = 0; deg(e) = 1; deg(c) = deg(d) = deg(a) = 2, c < d < a

[1] aba=bb

Axiom: aba=bb.

Defines rule #38.

Referenced by [8], [9], [10], [14].

[2] aaaaaa=1

Axiom: aaaaaa=1.

Referenced by [6].

[3] aaaa=c

Axiom: aaaa=c.

Referenced by [6], [10], [11], [12].

[4] cbbc=d

Axiom: cbbc=d.

Defines rule #18.

Referenced by [7], [13], [16], [17], [21], [23], [26], [29], [33], [38], [42], [81], [86].

[5] dbdbd=e

Axiom: dbdbd=e.

Referenced by [19], [28], [37], [49].

[6] caa=1

Overlap of [2] aaaaaa=1 with [3] aaaa=c:

aaaaaa aaaa

Critical pair: caa=1.

Referenced by [9], [12], [15].

[7] dbbc=cbbd

Overlap of [4] cbbc=d with [4] cbbc=d:

cbb c cbbc

Critical pair: cbbd=dbbc.

Flip LHS and RHS.

Referenced by [34].

[8] bbba=abbb

Overlap of [1] aba=bb with [1] aba=bb:

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #13.

Referenced by [100].

[9] cabb=ba

Overlap of [6] caa=1 with [1] aba=bb:

ca a aba

Critical pair: cabb=ba.

Referenced by [13], [23], [27], [40], [51].

[10] bbaaa=abc

Overlap of [1] aba=bb with [3] aaaa=c:

ab a aaaa

Critical pair: abc=bbaaa.

Flip LHS and RHS.

Referenced by [18].

[11] ac=ca

Overlap of [3] aaaa=c with [3] aaaa=c:

a aaa aaaa

Critical pair: ac=ca.

Defines rule #31.

Referenced by [13], [15], [22], [23], [27], [31], [40], [66], [78], [82], [83].

[12] aa=cc

Overlap of [6] caa=1 with [3] aaaa=c:

c aa aaaa

Critical pair: cc=aa.

Flip LHS and RHS.

Defines rule #37.

Referenced by [14], [15], [18], [20], [22], [57], [82], [84], [94].

[13] ad=bca

Overlap of [11] ac=ca with [4] cbbc=d:

a c cbbc

Critical pair: ad=cabbc.

Reduce RHS:

[9]	(cabb)c
[11]	⇒ b(ac)
	⇒ bca

Referenced by [21], [22], [23], [27], [30], [59], [66], [68].

[14] ccba=abb

Overlap of [12] aa=cc with [1] aba=bb:

a a aba

Critical pair: abb=ccba.

Flip LHS and RHS.

Referenced by [20], [21].

[15] ccc=1

Overlap of [12] aa=cc with [11] ac=ca:

a a ac

Critical pair: aca=ccc.

Reduce LHS:

[11]	(ac)a
[6]	⇒ (caa)
	⇒ 1

Flip LHS and RHS.

Defines rule #40.

Referenced by [16], [17], [22], [24], [25], [32], [41], [74], [82], [95].

[16] dcc=cbb

Overlap of [4] cbbc=d with [15] ccc=1:

cbb c ccc

Critical pair: cbb=dcc.

Flip LHS and RHS.

Referenced by [26], [29], [36].

[17] ccd=bbc

Overlap of [15] ccc=1 with [4] cbbc=d:

cc c cbbc

Critical pair: ccd=bbc.

Defines rule #41.

Referenced by [95].

[18] bbcca=abc

Overlap of [10] bbaaa=abc with [12] aa=cc:

bb aaa aa

Critical pair: bbcca=abc.

Referenced by [35].

[19] ebd=dbe

Overlap of [5] dbdbd=e with [5] dbdbd=e:

db dbd dbdbd

Critical pair: dbe=ebd.

Flip LHS and RHS.

Referenced by [48], [52].

[20] ccbcc=abba

Overlap of [14] ccba=abb with [12] aa=cc:

ccb a aa

Critical pair: ccbcc=abba.

Referenced by [36].

[21] cda=abbd

Overlap of [14] ccba=abb with [13] ad=bca:

ccb a ad

Critical pair: ccbbca=abbd.

Reduce LHS:

[4]	c(cbbc)a
	⇒ cda

Referenced by [22].

[22] ccbbd=cb

Overlap of [11] ac=ca with [21] cda=abbd:

a c cda

Critical pair: aabbd=cada.

Reduce LHS:

[12]	(aa)bbd
	⇒ ccbbd

Reduce RHS:

[13]	c(ad)a
[12]	⇒ cbc(aa)
[15]	⇒ cb(ccc)
	⇒ cb

Referenced by [23], [24], [25], [26].

[23] da=cab

Overlap of [11] ac=ca with [22] ccbbd=cb:

a c ccbbd

Critical pair: acb=cacbbd.

Reduce LHS:

[11]	(ac)b
	⇒ cab

Reduce RHS:

[11]	c(ac)bbd
[9]	⇒ c(cabb)d
[13]	⇒ cb(ad)
[4]	⇒ (cbbc)a
	⇒ da

Flip LHS and RHS.

Referenced by [30], [53].

[24] ccb=bbd

Overlap of [15] ccc=1 with [22] ccbbd=cb:

c cc ccbbd

Critical pair: ccb=bbd.

Defines rule #16.

Referenced by [31], [32], [33], [36], [47], [63], [66], [76].

[25] cbbd=b

Overlap of [15] ccc=1 with [22] ccbbd=cb:

cc c ccbbd

Critical pair: cccb=cbbd.

Reduce LHS:

[15]	(ccc)b
	⇒ b

Flip LHS and RHS.

Defines rule #20.

Referenced by [27], [28], [29], [34], [39], [44], [77].

[26] dbbd=cbbb

Overlap of [16] dcc=cbb with [22] ccbbd=cb:

dc c ccbbd

Critical pair: dccb=cbbcbbd.

Reduce LHS:

[16]	(dcc)b
	⇒ cbbb

Reduce RHS:

[4]	(cbbc)bbd
	⇒ dbbd

Flip LHS and RHS.

Defines rule #28.

Referenced by [38].

[27] bbca=ab

Overlap of [11] ac=ca with [25] cbbd=b:

a c cbbd

Critical pair: ab=cabbd.

Reduce RHS:

[9]	(cabb)d
[13]	⇒ b(ad)
	⇒ bbca

Flip LHS and RHS.

Referenced by [59], [60], [61], [66].

[28] bbdbd=cbbe

Overlap of [25] cbbd=b with [5] dbdbd=e:

cbb d dbdbd

Critical pair: cbbe=bbdbd.

Flip LHS and RHS.

Referenced by [32].

[29] bcc=dbb

Overlap of [25] cbbd=b with [16] dcc=cbb:

cbb d dcc

Critical pair: cbbcbb=bcc.

Reduce LHS:

[4]	(cbbc)bb
	⇒ dbb

Flip LHS and RHS.

Defines rule #19.

Referenced by [35], [42], [43], [50], [58].

[30] dbca=cabd

Overlap of [23] da=cab with [13] ad=bca:

d a ad

Critical pair: dbca=cabd.

Referenced by [54].

[31] ccab=abbd

Overlap of [11] ac=ca with [24] ccb=bbd:

a c ccb

Critical pair: abbd=cacb.

Reduce RHS:

[11]	c(ac)b
	⇒ ccab

Flip LHS and RHS.

Referenced by [55].

[32] cbbe=cb

Overlap of [15] ccc=1 with [24] ccb=bbd:

cc c ccb

Critical pair: ccbbd=cb.

Reduce LHS:

[24]	(ccb)bd
[28]	⇒ (bbdbd)
	⇒ cbbe

Referenced by [40], [41].

[33] bbdbc=cd

Overlap of [24] ccb=bbd with [4] cbbc=d:

c cb cbbc

Critical pair: cd=bbdbc.

Flip LHS and RHS.

Referenced by [66], [67].

[34] dbbc=b

Simplify [7] dbbc=cbbd.

Reduce RHS:

[25]	(cbbd)
	⇒ b

Defines rule #26.

Referenced by [37], [38], [39], [43], [86].

[35] abc=bdbba

Overlap of [18] bbcca=abc with [29] bcc=dbb:

b bcca bcc

Critical pair: bdbba=abc.

Flip LHS and RHS.

Referenced by [100], [101].

[36] abba=bbcbb

Overlap of [20] ccbcc=abba with [24] ccb=bbd:

ccbcc ccb

Critical pair: bbdcc=abba.

Reduce LHS:

[16]	bb(dcc)
	⇒ bbcbb

Flip LHS and RHS.

Defines rule #39.

[37] dbdbb=ebbc

Overlap of [5] dbdbd=e with [34] dbbc=b:

dbdb d dbbc

Critical pair: dbdbb=ebbc.

Referenced by [43].

[38] bbbc=cbbb

Overlap of [34] dbbc=b with [4] cbbc=d:

dbb c cbbc

Critical pair: dbbd=bbbc.

Reduce LHS:

[26]	(dbbd)
	⇒ cbbb

Flip LHS and RHS.

Defines rule #5.

[39] bbbd=dbbb

Overlap of [34] dbbc=b with [25] cbbd=b:

dbb c cbbd

Critical pair: dbbb=bbbd.

Flip LHS and RHS.

Defines rule #9.

Referenced by [100].

[40] cab=bae

Overlap of [11] ac=ca with [32] cbbe=cb:

a c cbbe

Critical pair: acb=cabbe.

Reduce LHS:

[11]	(ac)b
	⇒ cab

Reduce RHS:

[9]	(cabb)e
	⇒ bae

Defines rule #21.

Referenced by [51], [53], [54], [55], [58], [66], [78], [79].

[41] bbe=b

Overlap of [15] ccc=1 with [32] cbbe=cb:

cc c cbbe

Critical pair: cccb=bbe.

Reduce LHS:

[15]	(ccc)b
	⇒ b

Flip LHS and RHS.

Referenced by [45], [46].

[42] dc=cbdbb

Overlap of [4] cbbc=d with [29] bcc=dbb:

cb bc bcc

Critical pair: cbdbb=dc.

Flip LHS and RHS.

Defines rule #24.

Referenced by [63], [64], [66].

[43] ebbc=bc

Overlap of [34] dbbc=b with [29] bcc=dbb:

db bc bcc

Critical pair: dbdbb=bc.

Reduce LHS:

[37]	(dbdbb)
	⇒ ebbc

Referenced by [44].

[44] ebbb=bb

Overlap of [43] ebbc=bc with [25] cbbd=b:

ebb c cbbd

Critical pair: ebbb=bcbbd.

Reduce RHS:

[25]	b(cbbd)
	⇒ bb

Referenced by [45].

[45] ebb=b

Overlap of [44] ebbb=bb with [41] bbe=b:

eb bb bbe

Critical pair: ebb=bbe.

Reduce RHS:

[41]	(bbe)
	⇒ b

Defines rule #1.

Referenced by [46], [48], [57], [60], [61], [67], [80], [81], [96], [98].

[46] be=eb

Overlap of [45] ebb=b with [41] bbe=b:

e bb bbe

Critical pair: eb=be.

Flip LHS and RHS.

Defines rule #2.

Referenced by [47], [48], [52], [62], [75], [77], [78], [80], [84], [99], [100].

[47] cceb=bbde

Overlap of [24] ccb=bbd with [46] be=eb:

cc b be

Critical pair: cceb=bbde.

Referenced by [57].

[48] bdeb=bd

Overlap of [46] be=eb with [19] ebd=dbe:

b e ebd

Critical pair: bdbe=ebbd.

Reduce LHS:

[46]	bd(be)
	⇒ bdeb

Reduce RHS:

[45]	(ebb)d
	⇒ bd

Referenced by [49], [64], [79].

[49] eeb=e

Overlap of [5] dbdbd=e with [48] bdeb=bd:

dbd bd bdeb

Critical pair: dbdbd=eeb.

Reduce LHS:

[5]	(dbdbd)
	⇒ e

Flip LHS and RHS.

Defines rule #3.

Referenced by [50], [56], [65], [67], [75], [83], [84], [90], [96], [98], [100].

[50] ecc=eedbb

Overlap of [49] eeb=e with [29] bcc=dbb:

ee b bcc

Critical pair: eedbb=ecc.

Flip LHS and RHS.

Referenced by [57], [70].

[51] baeb=ba

Overlap of [9] cabb=ba with [40] cab=bae:

cabb cab

Critical pair: baeb=ba.

Defines rule #12.

Referenced by [56], [57], [62], [66], [100].

[52] ebd=deb

Simplify [19] ebd=dbe.

Reduce RHS:

[46]	d(be)
	⇒ deb

Referenced by [67], [75], [81], [88].

[53] da=bae

Simplify [23] da=cab.

Reduce RHS:

[40]	(cab)
	⇒ bae

Defines rule #29.

Referenced by [79], [93].

[54] dbca=baed

Simplify [30] dbca=cabd.

Reduce RHS:

[40]	(cab)d
	⇒ baed

Referenced by [69].

[55] abbd=cbae

Overlap of [31] ccab=abbd with [40] cab=bae:

c cab cab

Critical pair: cbae=abbd.

Flip LHS and RHS.

Defines rule #36.

[56] eaeb=ea

Overlap of [49] eeb=e with [51] baeb=ba:

ee b baeb

Critical pair: eeba=eaeb.

Reduce LHS:

[49]	(eeb)a
	⇒ ea

Flip LHS and RHS.

Referenced by [57], [78], [99].

[57] eedbb=bde

Overlap of [56] eaeb=ea with [51] baeb=ba:

eae b baeb

Critical pair: eaeba=eaaeb.

Reduce LHS:

[56]	(eaeb)a
[12]	⇒ e(aa)
[50]	⇒ (ecc)
	⇒ eedbb

Reduce RHS:

[12]	e(aa)eb
[47]	⇒ e(cceb)
[45]	⇒ (ebb)de
	⇒ bde

Referenced by [70].

[58] dbbab=bcbae

Overlap of [29] bcc=dbb with [40] cab=bae:

bc c cab

Critical pair: bcbae=dbbab.

Flip LHS and RHS.

Referenced by [100].

[59] bbcbca=abd

Overlap of [27] bbca=ab with [13] ad=bca:

bbc a ad

Critical pair: bbcbca=abd.

Referenced by [71].

[60] bca=eab

Overlap of [45] ebb=b with [27] bbca=ab:

e bb bbca

Critical pair: eab=bca.

Flip LHS and RHS.

Referenced by [63], [64], [65], [68], [69], [71], [89].

[61] ebab=ab

Overlap of [45] ebb=b with [27] bbca=ab:

eb b bbca

Critical pair: ebab=bbca.

Reduce RHS:

[27]	(bbca)
	⇒ ab

Referenced by [62].

[62] eba=aeb

Overlap of [61] ebab=ab with [46] be=eb:

eba b be

Critical pair: ebaeb=abe.

Reduce LHS:

[51]	e(baeb)
	⇒ eba

Reduce RHS:

[46]	a(be)
	⇒ aeb

Defines rule #15.

Referenced by [84].

[63] bbcbdbba=cceab

Overlap of [24] ccb=bbd with [60] bca=eab:

cc b bca

Critical pair: cceab=bbdca.

Reduce RHS:

[42]	bb(dc)a
	⇒ bbcbdbba

Flip LHS and RHS.

Referenced by [66], [72].

[64] bcbdbba=bdeeab

Overlap of [48] bdeb=bd with [60] bca=eab:

bde b bca

Critical pair: bdeeab=bdca.

Reduce RHS:

[42]	b(dc)a
	⇒ bcbdbba

Flip LHS and RHS.

Referenced by [73].

[65] eca=eeeab

Overlap of [49] eeb=e with [60] bca=eab:

ee b bca

Critical pair: eeeab=eca.

Flip LHS and RHS.

Referenced by [83], [90].

[66] cceab=abbc

Overlap of [40] cab=bae with [33] bbdbc=cd:

ca b bbdbc

Critical pair: cacd=baebdbc.

Reduce LHS:

[11]	c(ac)d
[13]	⇒ cc(ad)
[24]	⇒ (ccb)ca
[42]	⇒ bb(dc)a
[63]	⇒ (bbcbdbba)
	⇒ cceab

Reduce RHS:

[51]	(baeb)dbc
[13]	⇒ b(ad)bc
[27]	⇒ (bbca)bc
	⇒ abbc

Referenced by [72].

[67] dbc=eecd

Overlap of [49] eeb=e with [33] bbdbc=cd:

ee b bbdbc

Critical pair: eecd=ebdbc.

Reduce RHS:

[52]	(ebd)bc
[45]	⇒ d(ebb)c
	⇒ dbc

Flip LHS and RHS.

Referenced by [86], [96].

[68] ad=eab

Simplify [13] ad=bca.

Reduce RHS:

[60]	(bca)
	⇒ eab

Referenced by [84], [87].

[69] baed=deab

Overlap of [54] dbca=baed with [60] bca=eab:

d bca bca

Critical pair: deab=baed.

Flip LHS and RHS.

Referenced by [78].

[70] ecc=bde

Simplify [50] ecc=eedbb.

Reduce RHS:

[57]	(eedbb)
	⇒ bde

Referenced by [74], [94].

[71] abd=bbceab

Overlap of [59] bbcbca=abd with [60] bca=eab:

bbc bca bca

Critical pair: bbceab=abd.

Flip LHS and RHS.

Referenced by [91].

[72] bbcbdbba=abbc

Simplify [63] bbcbdbba=cceab.

Reduce RHS:

[66]	(cceab)
	⇒ abbc

Referenced by [73].

[73] abbc=bbdeeab

Overlap of [72] bbcbdbba=abbc with [64] bcbdbba=bdeeab:

b bcbdbba bcbdbba

Critical pair: bbdeeab=abbc.

Flip LHS and RHS.

Referenced by [92].

[74] bdec=e

Overlap of [70] ecc=bde with [15] ccc=1:

e cc ccc

Critical pair: e=bdec.

Flip LHS and RHS.

Referenced by [75], [76], [77], [78], [79].

[75] dec=ee

Overlap of [52] ebd=deb with [74] bdec=e:

e bd bdec

Critical pair: ee=debec.

Reduce RHS:

[46]	de(be)c
[49]	⇒ d(eeb)c
	⇒ dec

Flip LHS and RHS.

Referenced by [76], [78], [93].

[76] cce=bbdee

Overlap of [24] ccb=bbd with [74] bdec=e:

cc b bdec

Critical pair: cce=bbddec.

Reduce RHS:

[75]	bbd(dec)
	⇒ bbdee

Defines rule #17.

Referenced by [84].

[77] ebc=ceb

Overlap of [25] cbbd=b with [74] bdec=e:

cb bd bdec

Critical pair: cbe=bec.

Reduce LHS:

[46]	c(be)
	⇒ ceb

Reduce RHS:

[46]	(be)c
	⇒ ebc

Flip LHS and RHS.

Defines rule #7.

Referenced by [80], [81].

[78] cae=eea

Overlap of [40] cab=bae with [74] bdec=e:

ca b bdec

Critical pair: cae=baedec.

Reduce RHS:

[69]	(baed)ec
[46]	⇒ dea(be)c
[56]	⇒ d(eaeb)c
[11]	⇒ de(ac)
[75]	⇒ (dec)a
	⇒ eea

Referenced by [82], [94], [97].

[79] eab=bbaee

Overlap of [74] bdec=e with [40] cab=bae:

bde c cab

Critical pair: bdebae=eab.

Reduce LHS:

[48]	(bdeb)ae
[53]	⇒ b(da)e
	⇒ bbaee

Flip LHS and RHS.

Referenced by [83], [84], [87], [89], [91], [92], [99], [100].

[80] bceb=bc

Overlap of [46] be=eb with [77] ebc=ceb:

b e ebc

Critical pair: bceb=ebbc.

Reduce RHS:

[45]	(ebb)c
	⇒ bc

Defines rule #4.

Referenced by [96], [100].

[81] deb=d

Overlap of [77] ebc=ceb with [4] cbbc=d:

eb c cbbc

Critical pair: ebd=cebbbc.

Reduce LHS:

[52]	(ebd)
	⇒ deb

Reduce RHS:

[45]	c(ebb)bc
[4]	⇒ (cbbc)
	⇒ d

Defines rule #8.

Referenced by [88], [92].

[82] aeea=e

Overlap of [11] ac=ca with [78] cae=eea:

a c cae

Critical pair: aeea=caae.

Reduce RHS:

[12]	c(aa)e
[15]	⇒ (ccc)e
	⇒ e

Referenced by [83], [84], [85].

[83] aeaee=ec

Overlap of [82] aeea=e with [11] ac=ca:

aee a ac

Critical pair: aeeca=ec.

Reduce LHS:

[65]	ae(eca)
[79]	⇒ aeee(eab)
[49]	⇒ ae(eeb)baee
[49]	⇒ a(eeb)aee
	⇒ aeaee

Referenced by [94].

[84] ed=bbdeee

Overlap of [82] aeea=e with [68] ad=eab:

aee a ad

Critical pair: aeeeab=ed.

Reduce LHS:

[79]	aee(eab)
[49]	⇒ a(eeb)baee
[62]	⇒ a(eba)ee
[12]	⇒ (aa)ebee
[46]	⇒ cce(be)e
[49]	⇒ cc(eeb)e
[76]	⇒ (cce)e
	⇒ bbdeee

Flip LHS and RHS.

Defines rule #10.

Referenced by [96].

[85] eeea=aeee

Overlap of [82] aeea=e with [82] aeea=e:

aee a aeea

Critical pair: aeee=eeea.

Flip LHS and RHS.

Referenced by [90].

[86] dbd=eecb

Overlap of [67] dbc=eecd with [4] cbbc=d:

db c cbbc

Critical pair: dbd=eecdbbc.

Reduce RHS:

[34]	eec(dbbc)
	⇒ eecb

Referenced by [98].

[87] ad=bbaee

Simplify [68] ad=eab.

Reduce RHS:

[79]	(eab)
	⇒ bbaee

Defines rule #34.

[88] ebd=d

Simplify [52] ebd=deb.

Reduce RHS:

[81]	(deb)
	⇒ d

Defines rule #11.

Referenced by [94], [100].

[89] bca=bbaee

Simplify [60] bca=eab.

Reduce RHS:

[79]	(eab)
	⇒ bbaee

Defines rule #23.

[90] eca=aee

Simplify [65] eca=eeeab.

Reduce RHS:

[85]	(eeea)b
[49]	⇒ ae(eeb)
	⇒ aee

Referenced by [93].

[91] abd=bbcbbaee

Simplify [71] abd=bbceab.

Reduce RHS:

[79]	bbc(eab)
	⇒ bbcbbaee

Defines rule #35.

[92] abbc=bbdbaee

Simplify [73] abbc=bbdeeab.

Reduce RHS:

[79]	bbde(eab)
[81]	⇒ bb(deb)baee
	⇒ bbdbaee

Defines rule #33.

[93] eea=baeee

Overlap of [75] dec=ee with [90] eca=aee:

d ec eca

Critical pair: daee=eea.

Reduce LHS:

[53]	(da)ee
	⇒ baeee

Flip LHS and RHS.

Referenced by [97].

[94] cec=deee

Overlap of [78] cae=eea with [83] aeaee=ec:

c ae aeaee

Critical pair: cec=eeaaee.

Reduce RHS:

[12]	ee(aa)ee
[70]	⇒ e(ecc)ee
[88]	⇒ (ebd)eee
	⇒ deee

Referenced by [95].

[95] ec=bbceee

Overlap of [15] ccc=1 with [94] cec=deee:

cc c cec

Critical pair: ccdeee=ec.

Reduce LHS:

[17]	(ccd)eee
	⇒ bbceee

Flip LHS and RHS.

Defines rule #6.

Referenced by [96], [98], [100].

[96] dbc=bcdeee

Simplify [67] dbc=eecd.

Reduce RHS:

[95]	e(ec)d
[45]	⇒ (ebb)ceeed
[84]	⇒ bcee(ed)
[49]	⇒ bc(eeb)bdeee
[80]	⇒ (bceb)deee
	⇒ bcdeee

Defines rule #25.

[97] cae=baeee

Simplify [78] cae=eea.

Reduce RHS:

[93]	(eea)
	⇒ baeee

Defines rule #22.

[98] dbd=bcee

Simplify [86] dbd=eecb.

Reduce RHS:

[95]	e(ec)b
[45]	⇒ (ebb)ceeeb
[49]	⇒ bce(eeb)
	⇒ bcee

Defines rule #27.

[99] ea=bbaeee

Overlap of [79] eab=bbaee with [46] be=eb:

ea b be

Critical pair: eaeb=bbaeee.

Reduce LHS:

[56]	(eaeb)
	⇒ ea

Defines rule #14.

[100] dbba=bcbaee

Overlap of [79] eab=bbaee with [80] bceb=bc:

ea b bceb

Critical pair: eabc=bbaeeceb.

Reduce LHS:

[35]	e(abc)
[88]	⇒ (ebd)bba
	⇒ dbba

Reduce RHS:

[95]	bbae(ec)eb
[51]	⇒ b(baeb)bceeeeb
[49]	⇒ bbabcee(eeb)
[35]	⇒ bb(abc)eee
[39]	⇒ (bbbd)bbaeee
[8]	⇒ dbb(bbba)eee
[58]	⇒ (dbbab)bbeee
[51]	⇒ bc(baeb)beee
[46]	⇒ bcba(be)ee
[51]	⇒ bc(baeb)ee
	⇒ bcbaee

Defines rule #30.

Referenced by [101].

[101] abc=bbcbaee

Simplify [35] abc=bdbba.

Reduce RHS:

[100]	b(dbba)
	⇒ bbcbaee

Defines rule #32.