Certificate for #21739 ⟨a, b | aaa=1, abbabba=b⟩

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

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #18.

Referenced by [5], [11], [12], [17], [20], [25], [26], [31], [44], [55], [59].

[2] abbabba=b

Axiom: abbabba=b.

Referenced by [11], [12], [13], [14], [15].

[3] bbaba=c

Axiom: bbaba=c.

Referenced by [6], [10], [14], [15], [16], [18], [22], [23], [24], [37], [43], [48].

[4] abacc=d

Axiom: abacc=d.

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

[5] bacc=aad

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

aa a abacc

Critical pair: aad=bacc.

Flip LHS and RHS.

Referenced by [9], [15], [25], [27], [55].

[6] ccc=bbd

Overlap of [3] bbaba=c with [4] abacc=d:

bb aba abacc

Critical pair: bbd=ccc.

Flip LHS and RHS.

Defines rule #23.

Referenced by [7], [8], [9], [19], [27], [55].

[7] ababbd=dc

Overlap of [4] abacc=d with [6] ccc=bbd:

aba cc ccc

Critical pair: ababbd=dc.

Referenced by [10], [36].

[8] bbdc=cbbd

Overlap of [6] ccc=bbd with [6] ccc=bbd:

c cc ccc

Critical pair: cbbd=bbdc.

Flip LHS and RHS.

Referenced by [35].

[9] aadc=babbd

Overlap of [5] bacc=aad with [6] ccc=bbd:

ba cc ccc

Critical pair: babbd=aadc.

Flip LHS and RHS.

Referenced by [29].

[10] cbabbd=bbabdc

Overlap of [3] bbaba=c with [7] ababbd=dc:

bbab a ababbd

Critical pair: bbabdc=cbabbd.

Flip LHS and RHS.

Referenced by [39].

[11] bbabba=aab

Overlap of [1] aaa=1 with [2] abbabba=b:

aa a abbabba

Critical pair: aab=bbabba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [24], [26], [30].

[12] baa=abbabb

Overlap of [2] abbabba=b with [1] aaa=1:

abbabb a aaa

Critical pair: abbabb=baa.

Flip LHS and RHS.

Defines rule #11.

Referenced by [21], [22], [23], [24], [25], [29], [61], [62].

[13] bbba=abbb

Overlap of [2] abbabba=b with [2] abbabba=b:

abb abba abbabba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [16], [22], [23], [37], [45], [46], [53], [56], [58], [62].

[14] abbac=bba

Overlap of [2] abbabba=b with [3] bbaba=c:

abba bba bbaba

Critical pair: abbac=bba.

Defines rule #21.

Referenced by [20], [21], [23], [29].

[15] acad=bcc

Overlap of [2] abbabba=b with [5] bacc=aad:

abbab ba bacc

Critical pair: abbabaad=bcc.

Reduce LHS:

[3]a(bbaba)ad
⇒ acad

Referenced by [21].

[16] ababbb=bc

Overlap of [13] bbba=abbb with [3] bbaba=c:

b bba bbaba

Critical pair: bc=abbbba.

Reduce RHS:

[13]ab(bbba)
⇒ ababbb

Flip LHS and RHS.

Referenced by [17], [18], [32], [33], [34].

[17] aabc=babbb

Overlap of [1] aaa=1 with [16] ababbb=bc:

aa a ababbb

Critical pair: aabc=babbb.

Defines rule #20.

Referenced by [27].

[18] bbbc=cbbb

Overlap of [3] bbaba=c with [16] ababbb=bc:

bb aba ababbb

Critical pair: bbbc=cbbb.

Defines rule #9.

Referenced by [19], [21], [22], [23], [27], [38], [43], [58], [62].

[19] bbdbbb=bbbbbd

Overlap of [18] bbbc=cbbb with [6] ccc=bbd:

bbb c ccc

Critical pair: bbbbbd=cbbbcc.

Reduce RHS:

[18]c(bbbc)c
[18]⇒ cc(bbbc)
[6]⇒ (ccc)bbb
⇒ bbdbbb

Flip LHS and RHS.

Referenced by [40].

[20] aabba=bbac

Overlap of [1] aaa=1 with [14] abbac=bba:

aa a abbac

Critical pair: aabba=bbac.

Defines rule #19.

Referenced by [22], [25], [26].

[21] accbbb=babbabbd

Overlap of [14] abbac=bba with [15] acad=bcc:

abb ac acad

Critical pair: abbbcc=bbaad.

Reduce LHS:

[18]a(bbbc)c
[18]⇒ ac(bbbc)
⇒ accbbb

Reduce RHS:

[12]b(baa)d
⇒ babbabbd

Referenced by [23], [28].

[22] ca=bacbbbbb

Overlap of [3] bbaba=c with [12] baa=abbabb:

bba ba baa

Critical pair: bbaabbabb=ca.

Reduce LHS:

[20]bb(aabba)bb
[13]⇒ b(bbba)cbb
[18]⇒ ba(bbbc)bb
⇒ bacbbbbb

Flip LHS and RHS.

Defines rule #13.

Referenced by [37], [62].

[23] babbabbd=babba

Overlap of [12] baa=abbabb with [14] abbac=bba:

ba a abbac

Critical pair: babba=abbabbbbac.

Reduce RHS:

[13]abbab(bbba)c
[3]⇒ a(bbaba)bbbc
[18]⇒ ac(bbbc)
[21]⇒ (accbbb)
⇒ babbabbd

Flip LHS and RHS.

Referenced by [28].

[24] aaba=cbbabb

Overlap of [11] bbabba=aab with [12] baa=abbabb:

bbab ba baa

Critical pair: bbababbabb=aaba.

Reduce LHS:

[3](bbaba)bbabb
⇒ cbbabb

Flip LHS and RHS.

Referenced by [45], [59].

[25] abbabbd=abba

Overlap of [1] aaa=1 with [20] aabba=bbac:

aa a aabba

Critical pair: aabbac=abba.

Reduce LHS:

[20](aabba)c
[5]⇒ b(bacc)
[12]⇒ (baa)d
⇒ abbabbd

Referenced by [29].

[26] bbacbba=ab

Overlap of [20] aabba=bbac with [11] bbabba=aab:

aa bba bbabba

Critical pair: aaaab=bbacbba.

Reduce LHS:

[1](aaa)ab
⇒ ab

Flip LHS and RHS.

Referenced by [58].

[27] aadbbb=aabbbd

Overlap of [17] aabc=babbb with [6] ccc=bbd:

aab c ccc

Critical pair: aabbbd=babbbcc.

Reduce RHS:

[18]ba(bbbc)c
[18]⇒ bac(bbbc)
[5]⇒ (bacc)bbb
⇒ aadbbb

Flip LHS and RHS.

Referenced by [41].

[28] accbbb=babba

Simplify [21] accbbb=babbabbd.

Reduce RHS:

[23](babbabbd)
⇒ babba

Referenced by [60].

[29] bbabbd=bba

Overlap of [12] baa=abbabb with [9] aadc=babbd:

b aa aadc

Critical pair: bbabbd=abbabbdc.

Reduce RHS:

[25](abbabbd)c
[14]⇒ (abbac)
⇒ bba

Referenced by [30].

[30] aabbbd=aab

Overlap of [11] bbabba=aab with [29] bbabbd=bba:

bba bba bbabbd

Critical pair: bbabba=aabbbd.

Reduce LHS:

[11](bbabba)
⇒ aab

Flip LHS and RHS.

Referenced by [31], [41].

[31] bbbd=b

Overlap of [1] aaa=1 with [30] aabbbd=aab:

a aa aabbbd

Critical pair: aaab=bbbd.

Reduce LHS:

[1](aaa)b
⇒ b

Flip LHS and RHS.

Defines rule #2.

Referenced by [32], [33], [34], [35], [40], [42], [43], [47], [49], [53], [55], [56], [58], [60], [62].

[32] abab=bcd

Overlap of [16] ababbb=bc with [31] bbbd=b:

aba bbb bbbd

Critical pair: abab=bcd.

Referenced by [33], [34], [36], [52].

[33] bcdb=bcbd

Overlap of [16] ababbb=bc with [31] bbbd=b:

abab bb bbbd

Critical pair: ababb=bcbd.

Reduce LHS:

[32](abab)b
⇒ bcdb

Referenced by [34], [36], [37], [38].

[34] bcbdb=bcbbd

Overlap of [16] ababbb=bc with [31] bbbd=b:

ababb b bbbd

Critical pair: ababbb=bcbbd.

Reduce LHS:

[32](abab)bb
[33]⇒ (bcdb)b
⇒ bcbdb

Referenced by [37], [38].

[35] bcbbd=bc

Overlap of [31] bbbd=b with [8] bbdc=cbbd:

b bbd bbdc

Critical pair: bcbbd=bc.

Referenced by [37], [38].

[36] dc=bcbdd

Overlap of [7] ababbd=dc with [32] abab=bcd:

ababbd abab

Critical pair: bcdbd=dc.

Reduce LHS:

[33](bcdb)d
⇒ bcbdd

Flip LHS and RHS.

Defines rule #8.

Referenced by [37], [38], [39], [43], [48], [55], [58], [62].

[37] bcbcbdd=ccbbbbbbbbbbb

Overlap of [33] bcdb=bcbd with [3] bbaba=c:

bcd b bbaba

Critical pair: bcdc=bcbdbaba.

Reduce LHS:

[36]bc(dc)
⇒ bcbcbdd

Reduce RHS:

[34](bcbdb)aba
[35]⇒ (bcbbd)aba
[22]⇒ b(ca)ba
[13]⇒ bbacbbb(bbba)
[13]⇒ bbac(bbba)bbb
[22]⇒ bba(ca)bbbbbb
[3]⇒ (bbaba)cbbbbbbbbbbb
⇒ ccbbbbbbbbbbb

Referenced by [38].

[38] bcbc=ccbbbbbbbbbbbbbb

Overlap of [33] bcdb=bcbd with [18] bbbc=cbbb:

bcd b bbbc

Critical pair: bcdcbbb=bcbdbbc.

Reduce LHS:

[36]bc(dc)bbb
[37]⇒ (bcbcbdd)bbb
⇒ ccbbbbbbbbbbbbbb

Reduce RHS:

[34](bcbdb)bc
[35]⇒ (bcbbd)bc
⇒ bcbc

Flip LHS and RHS.

Defines rule #16.

[39] cbabbd=bbabbcbdd

Simplify [10] cbabbd=bbabdc.

Reduce RHS:

[36]bbab(dc)
⇒ bbabbcbdd

Referenced by [51].

[40] bbdbbb=bbb

Simplify [19] bbdbbb=bbbbbd.

Reduce RHS:

[31]bb(bbbd)
⇒ bbb

Referenced by [42].

[41] aadbbb=aab

Simplify [27] aadbbb=aabbbd.

Reduce RHS:

[30](aabbbd)
⇒ aab

Referenced by [44], [45].

[42] bbdb=b

Overlap of [40] bbdbbb=bbb with [31] bbbd=b:

bbd bbb bbbd

Critical pair: bbdb=bbbd.

Reduce RHS:

[31](bbbd)
⇒ b

Referenced by [43].

[43] cbbd=c

Overlap of [42] bbdb=b with [3] bbaba=c:

bbd b bbaba

Critical pair: bbdc=bbaba.

Reduce LHS:

[36]bb(dc)
[18]⇒ (bbbc)bdd
[31]⇒ cb(bbbd)d
⇒ cbbd

Reduce RHS:

[3](bbaba)
⇒ c

Defines rule #7.

Referenced by [55], [58], [61], [62], [63], [64].

[44] dbbb=b

Overlap of [1] aaa=1 with [41] aadbbb=aab:

a aa aadbbb

Critical pair: aaab=dbbb.

Reduce LHS:

[1](aaa)b
⇒ b

Flip LHS and RHS.

Referenced by [46], [47].

[45] aadabbb=cbbabb

Overlap of [41] aadbbb=aab with [13] bbba=abbb:

aad bbb bbba

Critical pair: aadabbb=aaba.

Reduce RHS:

[24](aaba)
⇒ cbbabb

Referenced by [52].

[46] dabbb=ba

Overlap of [44] dbbb=b with [13] bbba=abbb:

d bbb bbba

Critical pair: dabbb=ba.

Referenced by [49], [50].

[47] db=bd

Overlap of [44] dbbb=b with [31] bbbd=b:

d bbb bbbd

Critical pair: db=bd.

Defines rule #1.

Referenced by [48], [50], [52], [54], [55], [56], [58], [61], [62], [63], [64].

[48] bbdaba=bcbdd

Overlap of [47] db=bd with [3] bbaba=c:

d b bbaba

Critical pair: dc=bdbaba.

Reduce LHS:

[36](dc)
⇒ bcbdd

Reduce RHS:

[47]b(db)aba
⇒ bbdaba

Flip LHS and RHS.

Referenced by [53].

[49] dab=bad

Overlap of [46] dabbb=ba with [31] bbbd=b:

da bbb bbbd

Critical pair: dab=bad.

Referenced by [50], [52], [53], [54], [56].

[50] babbd=ba

Overlap of [46] dabbb=ba with [49] dab=bad:

dabbb dab

Critical pair: badbb=ba.

Reduce LHS:

[47]ba(db)b
[47]⇒ bab(db)
⇒ babbd

Defines rule #4.

Referenced by [51], [54], [58], [62].

[51] cba=bbabbcbdd

Overlap of [39] cbabbd=bbabbcbdd with [50] babbd=ba:

c babbd babbd

Critical pair: cba=bbabbcbdd.

Defines rule #14.

Referenced by [62].

[52] cbbabb=abcbdd

Overlap of [45] aadabbb=cbbabb with [49] dab=bad:

aa dabbb dab

Critical pair: aabadbb=cbbabb.

Reduce LHS:

[47]aaba(db)b
[32]⇒ a(abab)db
[47]⇒ abcd(db)
[47]⇒ abc(db)d
⇒ abcbdd

Flip LHS and RHS.

Referenced by [59].

[53] aba=bcbdd

Overlap of [48] bbdaba=bcbdd with [49] dab=bad:

bb daba dab

Critical pair: bbbada=bcbdd.

Reduce LHS:

[13](bbba)da
[31]⇒ a(bbbd)a
⇒ aba

Defines rule #10.

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

[54] bda=bbabdd

Overlap of [47] db=bd with [50] babbd=ba:

d b babbd

Critical pair: dba=bdabbd.

Reduce LHS:

[47](db)a
⇒ bda

Reduce RHS:

[49]b(dab)bd
[47]⇒ bba(db)d
⇒ bbabdd

Referenced by [56], [58].

[55] bbdd=d

Overlap of [53] aba=bcbdd with [5] bacc=aad:

a ba bacc

Critical pair: aaad=bcbddcc.

Reduce LHS:

[1](aaa)d
⇒ d

Reduce RHS:

[36]bcbd(dc)c
[47]⇒ bcb(db)cbddc
[43]⇒ b(cbbd)cbddc
[36]⇒ bccbd(dc)
[47]⇒ bccb(db)cbdd
[43]⇒ bc(cbbd)cbdd
[6]⇒ b(ccc)bdd
[31]⇒ (bbbd)bdd
⇒ bbdd

Flip LHS and RHS.

Defines rule #3.

Referenced by [57], [62].

[56] bdda=abdd

Overlap of [47] db=bd with [54] bda=bbabdd:

d b bda

Critical pair: dbbabdd=bdda.

Reduce LHS:

[47](db)babdd
[47]⇒ b(db)abdd
[49]⇒ bb(dab)dd
[13]⇒ (bbba)ddd
[31]⇒ a(bbbd)dd
⇒ abdd

Flip LHS and RHS.

Referenced by [57].

[57] da=babdd

Overlap of [55] bbdd=d with [56] bdda=abdd:

b bdd bdda

Critical pair: babdd=da.

Flip LHS and RHS.

Defines rule #5.

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

[58] acbba=bad

Overlap of [47] db=bd with [26] bbacbba=ab:

d b bbacbba

Critical pair: dab=bdbacbba.

Reduce LHS:

[57](da)b
[47]⇒ babd(db)
[47]⇒ bab(db)d
[50]⇒ (babbd)d
⇒ bad

Reduce RHS:

[47]b(db)acbba
[54]⇒ b(bda)cbba
[13]⇒ (bbba)bddcbba
[31]⇒ ab(bbbd)dcbba
[36]⇒ abb(dc)bba
[18]⇒ a(bbbc)bddbba
[31]⇒ acb(bbbd)dbba
[43]⇒ a(cbbd)bba
⇒ acbba

Flip LHS and RHS.

Referenced by [59].

[59] cbba=abcbddd

Overlap of [1] aaa=1 with [58] acbba=bad:

aa a acbba

Critical pair: aabad=cbba.

Reduce LHS:

[24](aaba)d
[52]⇒ (cbbabb)d
⇒ abcbddd

Flip LHS and RHS.

Defines rule #15.

Referenced by [61], [62].

[60] accb=babbad

Overlap of [28] accbbb=babba with [31] bbbd=b:

acc bbb bbbd

Critical pair: accb=babbad.

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

[61] abbabbccb=bbabcddddd

Overlap of [12] baa=abbabb with [60] accb=babbad:

ba a accb

Critical pair: bababbad=abbabbccb.

Reduce LHS:

[53]b(aba)bbad
[47]⇒ bbcbd(db)bad
[47]⇒ bbcb(db)dbad
[43]⇒ bb(cbbd)dbad
[47]⇒ bbc(db)ad
[57]⇒ bbcb(da)d
[59]⇒ bb(cbba)bddd
[47]⇒ bbabcbdd(db)ddd
[47]⇒ bbabcbd(db)dddd
[47]⇒ bbabcb(db)ddddd
[43]⇒ bbab(cbbd)ddddd
⇒ bbabcddddd

Flip LHS and RHS.

Referenced by [62].

[62] bbccbd=cbcdddddd

Overlap of [60] accb=babbad with [12] baa=abbabb:

acc b baa

Critical pair: accabbabb=babbadaa.

Reduce LHS:

[22]ac(ca)bbabb
[13]⇒ acbacbbbb(bbba)bb
[13]⇒ acbacb(bbba)bbbbb
[51]⇒ a(cba)cbabbbbbbbb
[36]⇒ abbabbcbd(dc)babbbbbbbb
[47]⇒ abbabbcb(db)cbddbabbbbbbbb
[43]⇒ abbabb(cbbd)cbddbabbbbbbbb
[47]⇒ abbabbccbd(db)abbbbbbbb
[47]⇒ abbabbccb(db)dabbbbbbbb
[43]⇒ abbabbc(cbbd)dabbbbbbbb
[57]⇒ abbabbcc(da)bbbbbbbb
[47]⇒ abbabbccbabd(db)bbbbbbb
[47]⇒ abbabbccbab(db)dbbbbbbb
[50]⇒ abbabbcc(babbd)dbbbbbbb
[47]⇒ abbabbccba(db)bbbbbb
[47]⇒ abbabbccbab(db)bbbbb
[50]⇒ abbabbcc(babbd)bbbbb
[61]⇒ (abbabbccb)abbbbb
[57]⇒ bbabcdddd(da)bbbbb
[47]⇒ bbabcddd(db)abddbbbbb
[47]⇒ bbabcdd(db)dabddbbbbb
[47]⇒ bbabcd(db)ddabddbbbbb
[47]⇒ bbabc(db)dddabddbbbbb
[47]⇒ bbabcbddddabd(db)bbbb
[47]⇒ bbabcbddddab(db)dbbbb
[55]⇒ bbabcbdddda(bbdd)bbbb
[47]⇒ bbabcbdddda(db)bbb
[47]⇒ bbabcbddddab(db)bb
[47]⇒ bbabcbddddabb(db)b
[31]⇒ bbabcbdddda(bbbd)b
[57]⇒ bbabcbddd(da)bb
[47]⇒ bbabcbdd(db)abddbb
[47]⇒ bbabcbd(db)dabddbb
[47]⇒ bbabcb(db)ddabddbb
[43]⇒ bbab(cbbd)ddabddbb
[47]⇒ bbabcddabd(db)b
[47]⇒ bbabcddab(db)db
[55]⇒ bbabcdda(bbdd)b
[47]⇒ bbabcdda(db)
[57]⇒ bbabcd(da)bd
[47]⇒ bbabc(db)abddbd
[47]⇒ bbabcbdabd(db)d
[47]⇒ bbabcbdab(db)dd
[55]⇒ bbabcbda(bbdd)d
[57]⇒ bbabcb(da)dd
[59]⇒ bbab(cbba)bdddd
[47]⇒ bbababcbdd(db)dddd
[47]⇒ bbababcbd(db)ddddd
[47]⇒ bbababcb(db)dddddd
[43]⇒ bbabab(cbbd)dddddd
[53]⇒ bb(aba)bcdddddd
[18]⇒ (bbbc)bddbcdddddd
[31]⇒ cb(bbbd)dbcdddddd
[43]⇒ (cbbd)bcdddddd
⇒ cbcdddddd

Reduce RHS:

[57]babba(da)a
[53]⇒ babb(aba)bdda
[18]⇒ ba(bbbc)bddbdda
[31]⇒ bacb(bbbd)dbdda
[43]⇒ ba(cbbd)bdda
[57]⇒ bacbd(da)
[47]⇒ bacb(db)abdd
[43]⇒ ba(cbbd)abdd
[22]⇒ ba(ca)bdd
[31]⇒ babacbbb(bbbd)d
[31]⇒ babacb(bbbd)
[53]⇒ b(aba)cbb
[36]⇒ bbcbd(dc)bb
[47]⇒ bbcb(db)cbddbb
[43]⇒ bb(cbbd)cbddbb
[47]⇒ bbccbd(db)b
[47]⇒ bbccb(db)db
[43]⇒ bbc(cbbd)db
[47]⇒ bbcc(db)
⇒ bbccbd

Flip LHS and RHS.

Referenced by [64].

[63] acc=babbabdd

Overlap of [60] accb=babbad with [43] cbbd=c:

ac cb cbbd

Critical pair: acc=babbadbd.

Reduce RHS:

[47]babba(db)d
⇒ babbabdd

Defines rule #22.

[64] bbcc=cbcbdddddd

Overlap of [62] bbccbd=cbcdddddd with [47] db=bd:

bbccb d db

Critical pair: bbccbbd=cbcddddddb.

Reduce LHS:

[43]bbc(cbbd)
⇒ bbcc

Reduce RHS:

[47]cbcddddd(db)
[47]⇒ cbcdddd(db)d
[47]⇒ cbcddd(db)dd
[47]⇒ cbcdd(db)ddd
[47]⇒ cbcd(db)dddd
[47]⇒ cbc(db)ddddd
⇒ cbcbdddddd

Defines rule #17.