Certificate for #21749 ⟨a, b | aaa=1, abbbbba=b⟩

Back:⟨a, b | aaa=1, abbbbba=b⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #27.

Referenced by [7], [8], [16], [59], [63].

[2] abbbbba=b

Axiom: abbbbba=b.

Referenced by [5].

[3] bbb=c

Axiom: bbb=c.

Defines rule #2.

Referenced by [5], [6], [9], [11], [12], [13], [20], [22], [24], [26], [28], [29], [32], [40], [43], [44], [46], [50], [52], [54], [57], [58], [62], [63], [64], [66], [67], [71], [73].

[4] acbacba=d

Axiom: acbacba=d.

Referenced by [16], [17], [18], [19], [20], [21], [22].

[5] acbba=b

Overlap of [2] abbbbba=b with [3] bbb=c:

a bbbbba bbb

Critical pair: acbba=b.

Defines rule #22.

Referenced by [7], [8], [9], [11], [14], [18], [21], [22], [24], [46], [50], [63].

[6] bc=cb

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

b bb bbb

Critical pair: bc=cb.

Defines rule #1.

Referenced by [9], [10], [11], [15], [20], [21], [22], [23], [30], [45], [50], [53], [57], [58], [60], [62], [63], [64], [65].

[7] aab=cbba

Overlap of [1] aaa=1 with [5] acbba=b:

aa a acbba

Critical pair: aab=cbba.

Defines rule #19.

Referenced by [11], [12], [41].

[8] baa=acbb

Overlap of [5] acbba=b with [1] aaa=1:

acbb a aaa

Critical pair: acbb=baa.

Flip LHS and RHS.

Defines rule #24.

Referenced by [13], [14], [19], [20], [57], [60], [63].

[9] cca=acc

Overlap of [5] acbba=b with [5] acbba=b:

acbb a acbba

Critical pair: acbbb=bcbba.

Reduce LHS:

[3]ac(bbb)
⇒ acc

Reduce RHS:

[6](bc)bba
[3]⇒ c(bbb)a
⇒ cca

Flip LHS and RHS.

Defines rule #10.

Referenced by [10], [20], [21], [25], [57], [66].

[10] ccba=bacc

Overlap of [6] bc=cb with [9] cca=acc:

b c cca

Critical pair: bacc=cbca.

Reduce RHS:

[6]c(bc)a
⇒ ccba

Flip LHS and RHS.

Defines rule #11.

Referenced by [11], [15], [20], [21], [22], [26].

[11] acbacc=bab

Overlap of [5] acbba=b with [7] aab=cbba:

acbb a aab

Critical pair: acbbcbba=bab.

Reduce LHS:

[6]acb(bc)bba
[6]⇒ ac(bc)bbba
[3]⇒ acc(bbb)ba
[10]⇒ ac(ccba)
⇒ acbacc

Referenced by [20], [21], [22].

[12] aac=cbbabb

Overlap of [7] aab=cbba with [3] bbb=c:

aa b bbb

Critical pair: aac=cbbabb.

Defines rule #18.

[13] caa=bbacbb

Overlap of [3] bbb=c with [8] baa=acbb:

bb b baa

Critical pair: bbacbb=caa.

Flip LHS and RHS.

Defines rule #23.

[14] acbacbb=ba

Overlap of [5] acbba=b with [8] baa=acbb:

acb ba baa

Critical pair: acbacbb=ba.

Referenced by [18].

[15] ccbba=bbacc

Overlap of [6] bc=cb with [10] ccba=bacc:

b c ccba

Critical pair: bbacc=cbcba.

Reduce RHS:

[6]c(bc)ba
⇒ ccbba

Flip LHS and RHS.

Defines rule #12.

[16] cbacba=aad

Overlap of [1] aaa=1 with [4] acbacba=d:

aa a acbacba

Critical pair: aad=cbacba.

Flip LHS and RHS.

Referenced by [61].

[17] dcba=acbd

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

acb acba acbacba

Critical pair: acbd=dcba.

Flip LHS and RHS.

Referenced by [37].

[18] dcbba=ba

Overlap of [4] acbacba=d with [5] acbba=b:

acbacb a acbba

Critical pair: acbacbb=dcbba.

Reduce LHS:

[14](acbacbb)
⇒ ba

Flip LHS and RHS.

Referenced by [24], [40].

[19] acbacacbb=da

Overlap of [4] acbacba=d with [8] baa=acbb:

acbac ba baa

Critical pair: acbacacbb=da.

Referenced by [62].

[20] acbab=bad

Overlap of [8] baa=acbb with [4] acbacba=d:

ba a acbacba

Critical pair: bad=acbbcbacba.

Reduce RHS:

[6]acb(bc)bacba
[6]⇒ ac(bc)bbacba
[3]⇒ acc(bbb)acba
[9]⇒ ac(cca)cba
[10]⇒ acac(ccba)
[11]⇒ ac(acbacc)
⇒ acbab

Flip LHS and RHS.

Referenced by [57].

[21] ccd=bb

Overlap of [9] cca=acc with [4] acbacba=d:

cc a acbacba

Critical pair: ccd=acccbacba.

Reduce RHS:

[10]ac(ccba)cba
[11]⇒ (acbacc)cba
[6]⇒ ba(bc)ba
[5]⇒ b(acbba)
⇒ bb

Referenced by [27], [34].

[22] ccbd=c

Overlap of [10] ccba=bacc with [4] acbacba=d:

ccb a acbacba

Critical pair: ccbd=bacccbacba.

Reduce RHS:

[10]bac(ccba)cba
[11]⇒ b(acbacc)cba
[6]⇒ bba(bc)ba
[5]⇒ bb(acbba)
[3]⇒ (bbb)
⇒ c

Referenced by [23], [28], [35].

[23] ccbbd=cb

Overlap of [6] bc=cb with [22] ccbd=c:

b c ccbd

Critical pair: bc=cbcbd.

Reduce LHS:

[6](bc)
⇒ cb

Reduce RHS:

[6]c(bc)bd
⇒ ccbbd

Flip LHS and RHS.

Referenced by [29].

[24] dcc=bb

Overlap of [18] dcbba=ba with [5] acbba=b:

dcbb a acbba

Critical pair: dcbbb=bacbba.

Reduce LHS:

[3]dc(bbb)
⇒ dcc

Reduce RHS:

[5]b(acbba)
⇒ bb

Defines rule #3.

Referenced by [25], [26], [27], [28], [29], [36], [39], [40], [50], [58], [62], [70].

[25] dacc=bba

Overlap of [24] dcc=bb with [9] cca=acc:

d cc cca

Critical pair: dacc=bba.

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

[26] dbacc=ca

Overlap of [24] dcc=bb with [10] ccba=bacc:

d cc ccba

Critical pair: dbacc=bbba.

Reduce RHS:

[3](bbb)a
⇒ ca

Referenced by [39], [45].

[27] bbd=dbb

Overlap of [24] dcc=bb with [21] ccd=bb:

d cc ccd

Critical pair: dbb=bbd.

Flip LHS and RHS.

Referenced by [32], [33], [43], [48], [55], [60].

[28] cd=dc

Overlap of [24] dcc=bb with [22] ccbd=c:

d cc ccbd

Critical pair: dc=bbbd.

Reduce RHS:

[3](bbb)d
⇒ cd

Flip LHS and RHS.

Defines rule #5.

Referenced by [30], [31], [32], [33], [36], [39], [42], [47], [55], [60], [62], [63], [66], [68], [70], [72].

[29] cbd=dcb

Overlap of [24] dcc=bb with [23] ccbbd=cb:

d cc ccbbd

Critical pair: dcb=bbbbd.

Reduce RHS:

[3](bbb)bd
⇒ cbd

Flip LHS and RHS.

Referenced by [30], [31], [36], [37], [48], [49], [56], [58].

[30] bdc=dcb

Overlap of [6] bc=cb with [28] cd=dc:

b c cd

Critical pair: bdc=cbd.

Reduce RHS:

[29](cbd)
⇒ dcb

Referenced by [31], [51], [58].

[31] bddc=ddcb

Overlap of [30] bdc=dcb with [28] cd=dc:

bd c cd

Critical pair: bddc=dcbd.

Reduce RHS:

[29]d(cbd)
⇒ ddcb

Referenced by [40], [52].

[32] bdbb=dc

Overlap of [3] bbb=c with [27] bbd=dbb:

b bb bbd

Critical pair: bdbb=cd.

Reduce RHS:

[28](cd)
⇒ dc

Referenced by [33].

[33] bddbb=ddc

Overlap of [32] bdbb=dc with [27] bbd=dbb:

bd bb bbd

Critical pair: bddbb=dcd.

Reduce RHS:

[28]d(cd)
⇒ ddc

Referenced by [41].

[34] dabb=bbad

Overlap of [25] dacc=bba with [21] ccd=bb:

da cc ccd

Critical pair: dabb=bbad.

Referenced by [36], [43].

[35] dac=bbabd

Overlap of [25] dacc=bba with [22] ccbd=c:

da cc ccbd

Critical pair: dac=bbabd.

Referenced by [38].

[36] bbabd=bbadb

Overlap of [25] dacc=bba with [29] cbd=dcb:

dac c cbd

Critical pair: dacdcb=bbabd.

Reduce LHS:

[28]da(cd)cb
[24]⇒ da(dcc)b
[34]⇒ (dabb)b
⇒ bbadb

Flip LHS and RHS.

Referenced by [38].

[37] dcba=adcb

Simplify [17] dcba=acbd.

Reduce RHS:

[29]a(cbd)
⇒ adcb

Defines rule #16.

Referenced by [50], [51], [52], [58].

[38] dac=bbadb

Simplify [35] dac=bbabd.

Reduce RHS:

[36](bbabd)
⇒ bbadb

Referenced by [42].

[39] dbabb=cad

Overlap of [26] dbacc=ca with [28] cd=dc:

dbac c cd

Critical pair: dbacdc=cad.

Reduce LHS:

[28]dba(cd)c
[24]⇒ dba(dcc)
⇒ dbabb

Referenced by [44].

[40] bdba=dbba

Overlap of [31] bddc=ddcb with [18] dcbba=ba:

bd dc dcbba

Critical pair: bdba=ddcbbba.

Reduce RHS:

[3]ddc(bbb)a
[24]⇒ d(dcc)a
⇒ dbba

Referenced by [53].

[41] aaddc=cbbaddbb

Overlap of [7] aab=cbba with [33] bddbb=ddc:

aa b bddbb

Critical pair: aaddc=cbbaddbb.

Referenced by [59].

[42] dadc=bbadbd

Overlap of [38] dac=bbadb with [28] cd=dc:

da c cd

Critical pair: dadc=bbadbd.

Referenced by [52].

[43] dbbabb=cbad

Overlap of [27] bbd=dbb with [34] dabb=bbad:

bb d dabb

Critical pair: bbbbad=dbbabb.

Reduce LHS:

[3](bbb)bad
⇒ cbad

Flip LHS and RHS.

Referenced by [54].

[44] dbac=cadb

Overlap of [39] dbabb=cad with [3] bbb=c:

dba bb bbb

Critical pair: dbac=cadb.

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

[45] cadcb=ca

Overlap of [26] dbacc=ca with [44] dbac=cadb:

dbacc dbac

Critical pair: cadbc=ca.

Reduce LHS:

[6]cad(bc)
⇒ cadcb

Defines rule #8.

Referenced by [49], [64], [69], [73].

[46] cadca=dbb

Overlap of [44] dbac=cadb with [5] acbba=b:

db ac acbba

Critical pair: dbb=cadbbba.

Reduce RHS:

[3]cad(bbb)a
⇒ cadca

Flip LHS and RHS.

Referenced by [58].

[47] dbadc=cadbd

Overlap of [44] dbac=cadb with [28] cd=dc:

dba c cd

Critical pair: dbadc=cadbd.

Referenced by [48].

[48] cadbdb=caddbb

Overlap of [44] dbac=cadb with [29] cbd=dcb:

dba c cbd

Critical pair: dbadcb=cadbbd.

Reduce LHS:

[47](dbadc)b
⇒ cadbdb

Reduce RHS:

[27]cad(bbd)
⇒ caddbb

Referenced by [52].

[49] caddcb=cad

Overlap of [45] cadcb=ca with [29] cbd=dcb:

cad cb cbd

Critical pair: caddcb=cad.

Referenced by [63], [64].

[50] dcbb=b

Overlap of [37] dcba=adcb with [5] acbba=b:

dcb a acbba

Critical pair: dcbb=adcbcbba.

Reduce RHS:

[6]adc(bc)bba
[24]⇒ a(dcc)bbba
[3]⇒ a(bbb)bba
[5]⇒ (acbba)
⇒ b

Defines rule #4.

Referenced by [51], [52], [55], [60], [63].

[51] badcb=ba

Overlap of [30] bdc=dcb with [37] dcba=adcb:

b dc dcba

Critical pair: badcb=dcbba.

Reduce RHS:

[50](dcbb)a
⇒ ba

Defines rule #9.

Referenced by [56], [65].

[52] dba=caddbb

Overlap of [31] bddc=ddcb with [37] dcba=adcb:

bd dc dcba

Critical pair: bdadcb=ddcbba.

Reduce LHS:

[42]b(dadc)b
[3]⇒ (bbb)adbdb
[48]⇒ (cadbdb)
⇒ caddbb

Reduce RHS:

[50]d(dcbb)a
⇒ dba

Flip LHS and RHS.

Defines rule #15.

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

[53] dbba=cbaddbb

Overlap of [40] bdba=dbba with [52] dba=caddbb:

b dba dba

Critical pair: bcaddbb=dbba.

Reduce LHS:

[6](bc)addbb
⇒ cbaddbb

Flip LHS and RHS.

Defines rule #17.

Referenced by [54], [62], [66].

[54] cbaddcb=cbad

Overlap of [43] dbbabb=cbad with [53] dbba=cbaddbb:

dbbabb dbba

Critical pair: cbaddbbbb=cbad.

Reduce LHS:

[3]cbadd(bbb)b
⇒ cbaddcb

Referenced by [62].

[55] bd=db

Overlap of [50] dcbb=b with [27] bbd=dbb:

dc bb bbd

Critical pair: dcdbb=bd.

Reduce LHS:

[28]d(cd)bb
[50]⇒ d(dcbb)
⇒ db

Flip LHS and RHS.

Defines rule #6.

Referenced by [58], [63], [64], [70], [72].

[56] baddcb=bad

Overlap of [51] badcb=ba with [29] cbd=dcb:

bad cb cbd

Critical pair: baddcb=bad.

Referenced by [64].

[57] babad=acaccb

Overlap of [8] baa=acbb with [20] acbab=bad:

ba a acbab

Critical pair: babad=acbbcbab.

Reduce RHS:

[6]acb(bc)bab
[6]⇒ ac(bc)bbab
[3]⇒ acc(bbb)ab
[9]⇒ ac(cca)b
⇒ acaccb

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

[58] adca=ddc

Overlap of [30] bdc=dcb with [46] cadca=dbb:

bd c cadca

Critical pair: bddbb=dcbadca.

Reduce LHS:

[55](bd)dbb
[55]⇒ d(bd)bb
[3]⇒ dd(bbb)
⇒ ddc

Reduce RHS:

[37](dcba)dca
[29]⇒ ad(cbd)ca
[6]⇒ addc(bc)a
[24]⇒ ad(dcc)ba
[3]⇒ ad(bbb)a
⇒ adca

Flip LHS and RHS.

Referenced by [59], [60].

[59] dca=cbbaddbb

Overlap of [1] aaa=1 with [58] adca=ddc:

aa a adca

Critical pair: aaddc=dca.

Reduce LHS:

[41](aaddc)
⇒ cbbaddbb

Flip LHS and RHS.

Defines rule #14.

Referenced by [63], [64].

[60] acba=baddc

Overlap of [8] baa=acbb with [58] adca=ddc:

ba a adca

Critical pair: baddc=acbbdca.

Reduce RHS:

[27]ac(bbd)ca
[28]⇒ a(cd)bbca
[50]⇒ a(dcbb)ca
[6]⇒ a(bc)a
⇒ acba

Flip LHS and RHS.

Defines rule #21.

Referenced by [61], [62], [66].

[61] aad=cbbaddc

Overlap of [16] cbacba=aad with [60] acba=baddc:

cb acba acba

Critical pair: cbbaddc=aad.

Flip LHS and RHS.

Defines rule #20.

[62] da=bbaddbb

Overlap of [19] acbacacbb=da with [60] acba=baddc:

acbacacbb acba

Critical pair: baddccacbb=da.

Reduce LHS:

[24]bad(dcc)acbb
[53]⇒ ba(dbba)cbb
[6]⇒ bacbaddb(bc)bb
[6]⇒ bacbadd(bc)bbb
[54]⇒ ba(cbaddcb)bbb
[3]⇒ bacbad(bbb)
[60]⇒ b(acba)dc
[28]⇒ bbadd(cd)c
[24]⇒ bbadd(dcc)
⇒ bbaddbb

Flip LHS and RHS.

Defines rule #13.

Referenced by [63], [64].

[63] ddcb=d

Overlap of [62] da=bbaddbb with [1] aaa=1:

d a aaa

Critical pair: d=bbaddbbaa.

Reduce RHS:

[8]bbaddb(baa)
[52]⇒ bbad(dba)cbb
[6]⇒ bbadcaddb(bc)bb
[6]⇒ bbadcadd(bc)bbb
[49]⇒ bbad(caddcb)bbb
[3]⇒ bbadcad(bbb)
[59]⇒ bba(dca)dc
[5]⇒ bb(acbba)ddbbdc
[3]⇒ (bbb)ddbbdc
[28]⇒ (cd)dbbdc
[28]⇒ d(cd)bbdc
[50]⇒ d(dcbb)dc
[55]⇒ d(bd)c
[6]⇒ dd(bc)
⇒ ddcb

Flip LHS and RHS.

Defines rule #7.

Referenced by [66], [67].

[64] bbacab=cabadddbb

Overlap of [52] dba=caddbb with [57] babad=acaccb:

d ba babad

Critical pair: dacaccb=caddbbbad.

Reduce LHS:

[62](da)caccb
[6]⇒ bbaddb(bc)accb
[6]⇒ bbadd(bc)baccb
[56]⇒ b(baddcb)baccb
[52]⇒ bba(dba)ccb
[6]⇒ bbacaddb(bc)cb
[6]⇒ bbacadd(bc)bcb
[49]⇒ bba(caddcb)bcb
[6]⇒ bbacad(bc)b
[45]⇒ bba(cadcb)b
⇒ bbacab

Reduce RHS:

[3]cadd(bbb)ad
[59]⇒ cad(dca)d
[45]⇒ (cadcb)baddbbd
[55]⇒ cabaddb(bd)
[55]⇒ cabadd(bd)b
⇒ cabadddbb

Referenced by [67].

[65] baba=acacccbb

Overlap of [57] babad=acaccb with [51] badcb=ba:

ba bad badcb

Critical pair: baba=acaccbcb.

Reduce RHS:

[6]acacc(bc)b
⇒ acacccbb

Defines rule #25.

[66] acacacc=babbadddb

Overlap of [57] babad=acaccb with [53] dbba=cbaddbb:

baba d dbba

Critical pair: babacbaddbb=acaccbbba.

Reduce LHS:

[60]bab(acba)ddbb
[28]⇒ babbadd(cd)dbb
[28]⇒ babbaddd(cd)bb
[63]⇒ babbadd(ddcb)b
⇒ babbadddb

Reduce RHS:

[3]acacc(bbb)a
[9]⇒ acac(cca)
⇒ acacacc

Flip LHS and RHS.

Referenced by [70].

[67] bbacac=cabadd

Overlap of [64] bbacab=cabadddbb with [3] bbb=c:

bbaca b bbb

Critical pair: bbacac=cabadddbbbb.

Reduce RHS:

[3]cabaddd(bbb)b
[63]⇒ cabad(ddcb)
⇒ cabadd

Referenced by [68].

[68] bbacadc=cabaddd

Overlap of [67] bbacac=cabadd with [28] cd=dc:

bbaca c cd

Critical pair: bbacadc=cabaddd.

Referenced by [69].

[69] bbaca=cabadddb

Overlap of [68] bbacadc=cabaddd with [45] cadcb=ca:

bba cadc cadcb

Critical pair: bbaca=cabadddb.

Defines rule #26.

[70] acacabb=babbaddddb

Overlap of [66] acacacc=babbadddb with [28] cd=dc:

acacac c cd

Critical pair: acacacdc=babbadddbd.

Reduce LHS:

[28]acaca(cd)c
[24]⇒ acaca(dcc)
⇒ acacabb

Reduce RHS:

[55]babbaddd(bd)
⇒ babbaddddb

Referenced by [71].

[71] acacac=babbaddddbb

Overlap of [70] acacabb=babbaddddb with [3] bbb=c:

acaca bb bbb

Critical pair: acacac=babbaddddbb.

Referenced by [72].

[72] acacadc=babbadddddbb

Overlap of [71] acacac=babbaddddbb with [28] cd=dc:

acaca c cd

Critical pair: acacadc=babbaddddbbd.

Reduce RHS:

[55]babbaddddb(bd)
[55]⇒ babbadddd(bd)b
⇒ babbadddddbb

Referenced by [73].

[73] acaca=babbadddddc

Overlap of [72] acacadc=babbadddddbb with [45] cadcb=ca:

aca cadc cadcb

Critical pair: acaca=babbadddddbbb.

Reduce RHS:

[3]babbaddddd(bbb)
⇒ babbadddddc

Defines rule #28.