Certificate for #4681 ⟨a, b | aabbaaab=aba⟩

Back:⟨a, b | aabbaaab=aba⟩

Completion settings:

[1] aabbaaab=aba

Axiom: aabbaaab=aba.

Referenced by [5].

[2] ab=c

Axiom: ab=c.

Defines rule #36.

Referenced by [5], [6], [8], [14], [21], [86].

[3] caca=d

Axiom: caca=d.

Referenced by [7].

[4] acbaa=e

Axiom: acbaa=e.

Defines rule #88.

Referenced by [6], [14], [15], [16], [18], [22], [25], [41], [87].

[5] aabbaaab=ca

Simplify [1] aabbaaab=aba.

Reduce RHS:

[2](ab)a
⇒ ca

Referenced by [6].

[6] ca=ec

Overlap of [5] aabbaaab=ca with [2] ab=c:

a abbaaab ab

Critical pair: acbaaab=ca.

Reduce LHS:

[4](acbaa)ab
[2]⇒ e(ab)
⇒ ec

Flip LHS and RHS.

Defines rule #37.

Referenced by [7], [8], [9], [13], [15], [16], [17], [19], [25], [27], [28], [32], [36], [41], [87].

[7] ecec=d

Overlap of [3] caca=d with [6] ca=ec:

caca ca

Critical pair: ecca=d.

Reduce LHS:

[6]ec(ca)
⇒ ecec

Defines rule #7.

Referenced by [9], [10], [11], [24], [29], [31], [32], [34], [35], [38], [43], [44], [46], [50], [56], [61], [62], [64], [66], [72], [74], [77], [79], [81], [84], [89].

[8] ecb=cc

Overlap of [6] ca=ec with [2] ab=c:

c a ab

Critical pair: cc=ecb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [11], [12], [15], [25], [30], [39], [41], [48], [53], [54], [55], [58], [59], [60], [68], [87].

[9] da=eceec

Overlap of [7] ecec=d with [6] ca=ec:

ece c ca

Critical pair: eceec=da.

Flip LHS and RHS.

Defines rule #42.

Referenced by [36].

[10] dec=ecd

Overlap of [7] ecec=d with [7] ecec=d:

ec ec ecec

Critical pair: ecd=dec.

Flip LHS and RHS.

Defines rule #4.

Referenced by [12].

[11] eccc=db

Overlap of [7] ecec=d with [8] ecb=cc:

ec ec ecb

Critical pair: eccc=db.

Defines rule #6.

Referenced by [13], [22], [23], [26], [31], [40], [41], [42], [45], [47], [51], [52], [61], [65], [67], [73], [78], [80], [85], [88], [90], [91].

[12] dcc=ecdb

Overlap of [10] dec=ecd with [8] ecb=cc:

d ec ecb

Critical pair: dcc=ecdb.

Defines rule #3.

[13] dba=eccec

Overlap of [11] eccc=db with [6] ca=ec:

ecc c ca

Critical pair: eccec=dba.

Flip LHS and RHS.

Defines rule #43.

Referenced by [32], [35].

[14] acbac=eb

Overlap of [4] acbaa=e with [2] ab=c:

acba a ab

Critical pair: acbac=eb.

Defines rule #75.

Referenced by [17], [18], [19], [20], [23], [37], [39], [48], [58], [68].

[15] acbae=ceec

Overlap of [4] acbaa=e with [4] acbaa=e:

acba a acbaa

Critical pair: acbae=ecbaa.

Reduce RHS:

[8](ecb)aa
[6]⇒ c(ca)a
[6]⇒ ce(ca)
⇒ ceec

Defines rule #76.

Referenced by [19], [36], [37], [38], [39], [40], [48], [58], [68].

[16] eccbaa=ce

Overlap of [6] ca=ec with [4] acbaa=e:

c a acbaa

Critical pair: ce=eccbaa.

Flip LHS and RHS.

Defines rule #81.

Referenced by [24], [25], [27], [32], [51].

[17] eccbac=ceb

Overlap of [6] ca=ec with [14] acbac=eb:

c a acbac

Critical pair: ceb=eccbac.

Flip LHS and RHS.

Defines rule #51.

Referenced by [34], [35], [52].

[18] ebbaa=acbe

Overlap of [14] acbac=eb with [4] acbaa=e:

acb ac acbaa

Critical pair: acbe=ebbaa.

Flip LHS and RHS.

Defines rule #78.

[19] eba=ceecc

Overlap of [14] acbac=eb with [6] ca=ec:

acba c ca

Critical pair: acbaec=eba.

Reduce LHS:

[15](acbae)c
⇒ ceecc

Flip LHS and RHS.

Defines rule #38.

Referenced by [21], [22], [23], [40], [73].

[20] ebbac=acbeb

Overlap of [14] acbac=eb with [14] acbac=eb:

acb ac acbac

Critical pair: acbeb=ebbac.

Flip LHS and RHS.

Defines rule #39.

[21] ceeccb=ebc

Overlap of [19] eba=ceecc with [2] ab=c:

eb a ab

Critical pair: ebc=ceeccb.

Flip LHS and RHS.

Defines rule #14.

Referenced by [26], [27], [33], [36], [43], [49], [69].

[22] cedbbaa=ebe

Overlap of [19] eba=ceecc with [4] acbaa=e:

eb a acbaa

Critical pair: ebe=ceecccbaa.

Reduce RHS:

[11]ce(eccc)baa
⇒ cedbbaa

Flip LHS and RHS.

Defines rule #80.

Referenced by [56], [57], [70].

[23] cedbbac=ebeb

Overlap of [19] eba=ceecc with [14] acbac=eb:

eb a acbac

Critical pair: ebeb=ceecccbac.

Reduce RHS:

[11]ce(eccc)bac
⇒ cedbbac

Flip LHS and RHS.

Defines rule #48.

Referenced by [62], [63], [71].

[24] dcbaa=ecce

Overlap of [7] ecec=d with [16] eccbaa=ce:

ec ec eccbaa

Critical pair: ecce=dcbaa.

Flip LHS and RHS.

Defines rule #79.

Referenced by [41].

[25] eccbae=cceec

Overlap of [16] eccbaa=ce with [4] acbaa=e:

eccba a acbaa

Critical pair: eccbae=cecbaa.

Reduce RHS:

[8]c(ecb)aa
[6]⇒ cc(ca)a
[6]⇒ cce(ca)
⇒ cceec

Defines rule #52.

Referenced by [64], [65].

[26] dbeeccb=eccebc

Overlap of [11] eccc=db with [21] ceeccb=ebc:

ecc c ceeccb

Critical pair: eccebc=dbeeccb.

Flip LHS and RHS.

Defines rule #20.

[27] ebeec=cece

Overlap of [21] ceeccb=ebc with [16] eccbaa=ce:

ce eccb eccbaa

Critical pair: cece=ebcaa.

Reduce RHS:

[6]eb(ca)a
[6]⇒ ebe(ca)
⇒ ebeec

Flip LHS and RHS.

Defines rule #9.

Referenced by [28], [29], [30], [31], [32], [33], [35], [43], [53], [57], [63], [75], [82].

[28] cecea=ebeeec

Overlap of [27] ebeec=cece with [6] ca=ec:

ebee c ca

Critical pair: ebeeec=cecea.

Flip LHS and RHS.

Defines rule #60.

Referenced by [66], [67], [68].

[29] ceceec=ebed

Overlap of [27] ebeec=cece with [7] ecec=d:

ebe ec ecec

Critical pair: ebed=ceceec.

Flip LHS and RHS.

Defines rule #22.

Referenced by [46], [47], [48], [49].

[30] ebecc=ceceb

Overlap of [27] ebeec=cece with [8] ecb=cc:

ebe ec ecb

Critical pair: ebecc=ceceb.

Defines rule #8.

Referenced by [42], [43], [54].

[31] ebedb=cdc

Overlap of [27] ebeec=cece with [11] eccc=db:

ebe ec eccc

Critical pair: ebedb=cececc.

Reduce RHS:

[7]c(ecec)c
⇒ cdc

Defines rule #2.

Referenced by [39], [55].

[32] cecceec=ebece

Overlap of [27] ebeec=cece with [16] eccbaa=ce:

ebe ec eccbaa

Critical pair: ebece=cececbaa.

Reduce RHS:

[7]c(ecec)baa
[13]⇒ c(dba)a
[6]⇒ cecce(ca)
⇒ cecceec

Flip LHS and RHS.

Defines rule #28.

Referenced by [69], [70], [71], [76], [83].

[33] ceceeeccb=ebeeebc

Overlap of [27] ebeec=cece with [21] ceeccb=ebc:

ebee c ceeccb

Critical pair: ebeeebc=ceceeeccb.

Flip LHS and RHS.

Defines rule #33.

Referenced by [79], [80].

[34] dcbac=ecceb

Overlap of [7] ecec=d with [17] eccbac=ceb:

ec ec eccbac

Critical pair: ecceb=dcbac.

Flip LHS and RHS.

Defines rule #44.

Referenced by [51], [52], [53], [54], [55], [59], [65], [78].

[35] ceccecc=ebeceb

Overlap of [27] ebeec=cece with [17] eccbac=ceb:

ebe ec eccbac

Critical pair: ebeceb=cececbac.

Reduce RHS:

[7]c(ecec)bac
[13]⇒ c(dba)c
⇒ ceccecc

Flip LHS and RHS.

Defines rule #27.

[36] dceec=eebece

Overlap of [9] da=eceec with [15] acbae=ceec:

d a acbae

Critical pair: dceec=eceeccbae.

Reduce RHS:

[21]e(ceeccb)ae
[6]⇒ eeb(ca)e
⇒ eebece

Defines rule #17.

Referenced by [60], [61].

[37] ebbae=acbceec

Overlap of [14] acbac=eb with [15] acbae=ceec:

acb ac acbae

Critical pair: acbceec=ebbae.

Flip LHS and RHS.

Defines rule #40.

Referenced by [72].

[38] acbad=ceeccec

Overlap of [15] acbae=ceec with [7] ecec=d:

acba e ecec

Critical pair: acbad=ceeccec.

Defines rule #77.

Referenced by [73].

[39] ceccedb=ebdc

Overlap of [15] acbae=ceec with [31] ebedb=cdc:

acba e ebedb

Critical pair: acbacdc=ceecbedb.

Reduce LHS:

[14](acbac)dc
⇒ ebdc

Reduce RHS:

[8]ce(ecb)edb
⇒ ceccedb

Flip LHS and RHS.

Defines rule #21.

[40] cedbbae=ebceec

Overlap of [19] eba=ceecc with [15] acbae=ceec:

eb a acbae

Critical pair: ebceec=ceecccbae.

Reduce RHS:

[11]ce(eccc)bae
⇒ cedbbae

Flip LHS and RHS.

Defines rule #49.

Referenced by [74], [75], [76].

[41] dcbae=dbeec

Overlap of [24] dcbaa=ecce with [4] acbaa=e:

dcba a acbaa

Critical pair: dcbae=eccecbaa.

Reduce RHS:

[8]ecc(ecb)aa
[11]⇒ (eccc)caa
[6]⇒ db(ca)a
[6]⇒ dbe(ca)
⇒ dbeec

Defines rule #45.

Referenced by [50], [51], [52], [53], [54], [55], [59], [65], [78].

[42] cecebc=ebdb

Overlap of [30] ebecc=ceceb with [11] eccc=db:

eb ecc eccc

Critical pair: ebdb=cecebc.

Flip LHS and RHS.

Defines rule #13.

Referenced by [44], [45].

[43] ebecebc=ceccdb

Overlap of [30] ebecc=ceceb with [21] ceeccb=ebc:

ebec c ceeccb

Critical pair: ebecebc=cecebeeccb.

Reduce RHS:

[27]cec(ebeec)cb
[7]⇒ cecc(ecec)b
⇒ ceccdb

Defines rule #15.

[44] debc=eebdb

Overlap of [7] ecec=d with [42] cecebc=ebdb:

e cec cecebc

Critical pair: eebdb=debc.

Flip LHS and RHS.

Defines rule #5.

[45] dbecebc=eccebdb

Overlap of [11] eccc=db with [42] cecebc=ebdb:

ecc c cecebc

Critical pair: eccebdb=dbecebc.

Flip LHS and RHS.

Defines rule #19.

[46] deec=eebed

Overlap of [7] ecec=d with [29] ceceec=ebed:

e cec ceceec

Critical pair: eebed=deec.

Flip LHS and RHS.

Defines rule #12.

[47] dbeceec=eccebed

Overlap of [11] eccc=db with [29] ceceec=ebed:

ecc c ceceec

Critical pair: eccebed=dbeceec.

Flip LHS and RHS.

Defines rule #25.

[48] ebeceec=cecced

Overlap of [14] acbac=eb with [29] ceceec=ebed:

acba c ceceec

Critical pair: acbaebed=ebeceec.

Reduce LHS:

[15](acbae)bed
[8]⇒ ce(ecb)ed
⇒ cecced

Flip LHS and RHS.

Defines rule #23.

[49] ebedcb=ceebc

Overlap of [29] ceceec=ebed with [21] ceeccb=ebc:

ce ceec ceeccb

Critical pair: ceebc=ebedcb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [58], [59].

[50] dcbad=dbeeccec

Overlap of [41] dcbae=dbeec with [7] ecec=d:

dcba e ecec

Critical pair: dcbad=dbeeccec.

Defines rule #46.

[51] dbedbbaa=eccebe

Overlap of [41] dcbae=dbeec with [16] eccbaa=ce:

dcba e eccbaa

Critical pair: dcbace=dbeecccbaa.

Reduce LHS:

[34](dcbac)e
⇒ eccebe

Reduce RHS:

[11]dbe(eccc)baa
⇒ dbedbbaa

Flip LHS and RHS.

Defines rule #83.

[52] dbedbbac=eccebeb

Overlap of [41] dcbae=dbeec with [17] eccbac=ceb:

dcba e eccbac

Critical pair: dcbaceb=dbeecccbac.

Reduce LHS:

[34](dcbac)eb
⇒ eccebeb

Reduce RHS:

[11]dbe(eccc)bac
⇒ dbedbbac

Flip LHS and RHS.

Defines rule #57.

[53] dbecceec=eccebece

Overlap of [41] dcbae=dbeec with [27] ebeec=cece:

dcba e ebeec

Critical pair: dcbacece=dbeecbeec.

Reduce LHS:

[34](dcbac)ece
⇒ eccebece

Reduce RHS:

[8]dbe(ecb)eec
⇒ dbecceec

Flip LHS and RHS.

Defines rule #31.

[54] dbeccecc=eccebeceb

Overlap of [41] dcbae=dbeec with [30] ebecc=ceceb:

dcba e ebecc

Critical pair: dcbaceceb=dbeecbecc.

Reduce LHS:

[34](dcbac)eceb
⇒ eccebeceb

Reduce RHS:

[8]dbe(ecb)ecc
⇒ dbeccecc

Flip LHS and RHS.

Defines rule #30.

[55] dbeccedb=eccebdc

Overlap of [41] dcbae=dbeec with [31] ebedb=cdc:

dcba e ebedb

Critical pair: dcbacdc=dbeecbedb.

Reduce LHS:

[34](dcbac)dc
⇒ eccebdc

Reduce RHS:

[8]dbe(ecb)edb
⇒ dbeccedb

Flip LHS and RHS.

Defines rule #24.

[56] dedbbaa=eceebe

Overlap of [7] ecec=d with [22] cedbbaa=ebe:

ece c cedbbaa

Critical pair: eceebe=dedbbaa.

Flip LHS and RHS.

Defines rule #82.

[57] ceceedbbaa=ebeeebe

Overlap of [27] ebeec=cece with [22] cedbbaa=ebe:

ebee c cedbbaa

Critical pair: ebeeebe=ceceedbbaa.

Flip LHS and RHS.

Defines rule #85.

Referenced by [84], [85].

[58] ceccedcb=ebeebc

Overlap of [15] acbae=ceec with [49] ebedcb=ceebc:

acba e ebedcb

Critical pair: acbaceebc=ceecbedcb.

Reduce LHS:

[14](acbac)eebc
⇒ ebeebc

Reduce RHS:

[8]ce(ecb)edcb
⇒ ceccedcb

Flip LHS and RHS.

Defines rule #29.

Referenced by [77].

[59] dbeccedcb=eccebeebc

Overlap of [41] dcbae=dbeec with [49] ebedcb=ceebc:

dcba e ebedcb

Critical pair: dcbaceebc=dbeecbedcb.

Reduce LHS:

[34](dcbac)eebc
⇒ eccebeebc

Reduce RHS:

[8]dbe(ecb)edcb
⇒ dbeccedcb

Flip LHS and RHS.

Defines rule #32.

[60] dcecc=eebeceb

Overlap of [36] dceec=eebece with [8] ecb=cc:

dce ec ecb

Critical pair: dcecc=eebeceb.

Defines rule #16.

[61] dcedb=eebdc

Overlap of [36] dceec=eebece with [11] eccc=db:

dce ec eccc

Critical pair: dcedb=eebececc.

Reduce RHS:

[7]eeb(ecec)c
⇒ eebdc

Defines rule #11.

[62] dedbbac=eceebeb

Overlap of [7] ecec=d with [23] cedbbac=ebeb:

ece c cedbbac

Critical pair: eceebeb=dedbbac.

Flip LHS and RHS.

Defines rule #54.

[63] ceceedbbac=ebeeebeb

Overlap of [27] ebeec=cece with [23] cedbbac=ebeb:

ebee c cedbbac

Critical pair: ebeeebeb=ceceedbbac.

Flip LHS and RHS.

Defines rule #66.

Referenced by [88].

[64] eccbad=cceeccec

Overlap of [25] eccbae=cceec with [7] ecec=d:

eccba e ecec

Critical pair: eccbad=cceeccec.

Defines rule #53.

Referenced by [78].

[65] dbedbbae=eccebceec

Overlap of [41] dcbae=dbeec with [25] eccbae=cceec:

dcba e eccbae

Critical pair: dcbacceec=dbeecccbae.

Reduce LHS:

[34](dcbac)ceec
⇒ eccebceec

Reduce RHS:

[11]dbe(eccc)bae
⇒ dbedbbae

Flip LHS and RHS.

Defines rule #58.

[66] dea=eebeeec

Overlap of [7] ecec=d with [28] cecea=ebeeec:

e cec cecea

Critical pair: eebeeec=dea.

Flip LHS and RHS.

Defines rule #47.

[67] dbecea=eccebeeec

Overlap of [11] eccc=db with [28] cecea=ebeeec:

ecc c cecea

Critical pair: eccebeeec=dbecea.

Flip LHS and RHS.

Defines rule #62.

[68] ebecea=cecceeec

Overlap of [14] acbac=eb with [28] cecea=ebeeec:

acba c cecea

Critical pair: acbaebeeec=ebecea.

Reduce LHS:

[15](acbae)beeec
[8]⇒ ce(ecb)eeec
⇒ cecceeec

Flip LHS and RHS.

Defines rule #61.

[69] ebeceeeccb=cecceeebc

Overlap of [32] cecceec=ebece with [21] ceeccb=ebc:

ceccee c ceeccb

Critical pair: cecceeebc=ebeceeeccb.

Flip LHS and RHS.

Defines rule #34.

[70] ebeceedbbaa=cecceeebe

Overlap of [32] cecceec=ebece with [22] cedbbaa=ebe:

ceccee c cedbbaa

Critical pair: cecceeebe=ebeceedbbaa.

Flip LHS and RHS.

Defines rule #86.

[71] ebeceedbbac=cecceeebeb

Overlap of [32] cecceec=ebece with [23] cedbbac=ebeb:

ceccee c cedbbac

Critical pair: cecceeebeb=ebeceedbbac.

Flip LHS and RHS.

Defines rule #69.

[72] ebbad=acbceeccec

Overlap of [37] ebbae=acbceec with [7] ecec=d:

ebba e ecec

Critical pair: ebbad=acbceeccec.

Defines rule #41.

[73] cedbbad=ebceeccec

Overlap of [19] eba=ceecc with [38] acbad=ceeccec:

eb a acbad

Critical pair: ebceeccec=ceecccbad.

Reduce RHS:

[11]ce(eccc)bad
⇒ cedbbad

Flip LHS and RHS.

Defines rule #50.

Referenced by [81], [82], [83].

[74] dedbbae=eceebceec

Overlap of [7] ecec=d with [40] cedbbae=ebceec:

ece c cedbbae

Critical pair: eceebceec=dedbbae.

Flip LHS and RHS.

Defines rule #55.

[75] ceceedbbae=ebeeebceec

Overlap of [27] ebeec=cece with [40] cedbbae=ebceec:

ebee c cedbbae

Critical pair: ebeeebceec=ceceedbbae.

Flip LHS and RHS.

Defines rule #67.

Referenced by [90].

[76] ebeceedbbae=cecceeebceec

Overlap of [32] cecceec=ebece with [40] cedbbae=ebceec:

ceccee c cedbbae

Critical pair: cecceeebceec=ebeceedbbae.

Flip LHS and RHS.

Defines rule #70.

[77] dcedcb=eebeebc

Overlap of [7] ecec=d with [58] ceccedcb=ebeebc:

e cec ceccedcb

Critical pair: eebeebc=dcedcb.

Flip LHS and RHS.

Defines rule #18.

[78] dbedbbad=eccebceeccec

Overlap of [41] dcbae=dbeec with [64] eccbad=cceeccec:

dcba e eccbad

Critical pair: dcbacceeccec=dbeecccbad.

Reduce LHS:

[34](dcbac)ceeccec
⇒ eccebceeccec

Reduce RHS:

[11]dbe(eccc)bad
⇒ dbedbbad

Flip LHS and RHS.

Defines rule #59.

[79] deeeccb=eebeeebc

Overlap of [7] ecec=d with [33] ceceeeccb=ebeeebc:

e cec ceceeeccb

Critical pair: eebeeebc=deeeccb.

Flip LHS and RHS.

Defines rule #26.

[80] dbeceeeccb=eccebeeebc

Overlap of [11] eccc=db with [33] ceceeeccb=ebeeebc:

ecc c ceceeeccb

Critical pair: eccebeeebc=dbeceeeccb.

Flip LHS and RHS.

Defines rule #35.

[81] dedbbad=eceebceeccec

Overlap of [7] ecec=d with [73] cedbbad=ebceeccec:

ece c cedbbad

Critical pair: eceebceeccec=dedbbad.

Flip LHS and RHS.

Defines rule #56.

[82] ceceedbbad=ebeeebceeccec

Overlap of [27] ebeec=cece with [73] cedbbad=ebceeccec:

ebee c cedbbad

Critical pair: ebeeebceeccec=ceceedbbad.

Flip LHS and RHS.

Defines rule #68.

Referenced by [91].

[83] ebeceedbbad=cecceeebceeccec

Overlap of [32] cecceec=ebece with [73] cedbbad=ebceeccec:

ceccee c cedbbad

Critical pair: cecceeebceeccec=ebeceedbbad.

Flip LHS and RHS.

Defines rule #71.

[84] deedbbaa=eebeeebe

Overlap of [7] ecec=d with [57] ceceedbbaa=ebeeebe:

e cec ceceedbbaa

Critical pair: eebeeebe=deedbbaa.

Flip LHS and RHS.

Defines rule #84.

Referenced by [86], [87].

[85] dbeceedbbaa=eccebeeebe

Overlap of [11] eccc=db with [57] ceceedbbaa=ebeeebe:

ecc c ceceedbbaa

Critical pair: eccebeeebe=dbeceedbbaa.

Flip LHS and RHS.

Defines rule #87.

[86] deedbbac=eebeeebeb

Overlap of [84] deedbbaa=eebeeebe with [2] ab=c:

deedbba a ab

Critical pair: deedbbac=eebeeebeb.

Defines rule #63.

[87] deedbbae=eebeeebceec

Overlap of [84] deedbbaa=eebeeebe with [4] acbaa=e:

deedbba a acbaa

Critical pair: deedbbae=eebeeebecbaa.

Reduce RHS:

[8]eebeeeb(ecb)aa
[6]⇒ eebeeebc(ca)a
[6]⇒ eebeeebce(ca)
⇒ eebeeebceec

Defines rule #64.

Referenced by [89].

[88] dbeceedbbac=eccebeeebeb

Overlap of [11] eccc=db with [63] ceceedbbac=ebeeebeb:

ecc c ceceedbbac

Critical pair: eccebeeebeb=dbeceedbbac.

Flip LHS and RHS.

Defines rule #72.

[89] deedbbad=eebeeebceeccec

Overlap of [87] deedbbae=eebeeebceec with [7] ecec=d:

deedbba e ecec

Critical pair: deedbbad=eebeeebceeccec.

Defines rule #65.

[90] dbeceedbbae=eccebeeebceec

Overlap of [11] eccc=db with [75] ceceedbbae=ebeeebceec:

ecc c ceceedbbae

Critical pair: eccebeeebceec=dbeceedbbae.

Flip LHS and RHS.

Defines rule #73.

[91] dbeceedbbad=eccebeeebceeccec

Overlap of [11] eccc=db with [82] ceceedbbad=ebeeebceeccec:

ecc c ceceedbbad

Critical pair: eccebeeebceeccec=dbeceedbbad.

Flip LHS and RHS.

Defines rule #74.