Certificate for #3151 ⟨a, b | aabbbabbbba=1⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(c) = deg(d) = deg(a) = 0, c < d < a; deg(b) = 1
Auxiliary generators:
1. aaa=c
2. bbbabbbb=d

[1] aabbbabbbba=1

Axiom: aabbbabbbba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [16], [17], [20], [22], [27].

[3] bbbabbbb=d

Axiom: bbbabbbb=d.

Defines rule #19.

Referenced by [4], [11], [12], [13], [17], [20], [26].

[4] aada=1

Overlap of [1] aabbbabbbba=1 with [3] bbbabbbb=d:

aa bbbabbbba bbbabbbb

Critical pair: aada=1.

Referenced by [6], [7], [8], [9], [10].

[5] ca=ac

Overlap of [2] aaa=c with [2] aaa=c:

a aa aaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [18], [21].

[6] cda=a

Overlap of [2] aaa=c with [4] aada=1:

a aa aada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

[7] ada=aad

Overlap of [4] aada=1 with [4] aada=1:

aad a aada

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [9], [10].

[8] cd=1

Overlap of [6] cda=a with [4] aada=1:

cd a aada

Critical pair: cd=aada.

Reduce RHS:

[4]	(aada)
	⇒ 1

Defines rule #2.

Referenced by [16], [23], [26], [32].

[9] da=ad

Overlap of [4] aada=1 with [7] ada=aad:

aad a ada

Critical pair: aadaad=da.

Reduce LHS:

[4]	(aada)ad
	⇒ ad

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [14], [20], [30], [35].

[10] dc=1

Overlap of [9] da=ad with [2] aaa=c:

d a aaa

Critical pair: dc=adaa.

Reduce RHS:

[7]	(ada)a
[4]	⇒ (aada)
	⇒ 1

Defines rule #1.

Referenced by [15], [17], [20], [28], [33], [36].

[11] bbbabd=adbbbb

Overlap of [3] bbbabbbb=d with [3] bbbabbbb=d:

bbbab bbb bbbabbbb

Critical pair: bbbabd=dabbbb.

Reduce RHS:

[9]	(da)bbbb
	⇒ adbbbb

Defines rule #7.

Referenced by [14], [15].

[12] bbbabbd=dbabbbb

Overlap of [3] bbbabbbb=d with [3] bbbabbbb=d:

bbbabb bb bbbabbbb

Critical pair: bbbabbd=dbabbbb.

Defines rule #13.

Referenced by [30].

[13] bbbabbbd=dbbabbbb

Overlap of [3] bbbabbbb=d with [3] bbbabbbb=d:

bbbabbb b bbbabbbb

Critical pair: bbbabbbd=dbbabbbb.

Defines rule #16.

Referenced by [35].

[14] bbbabad=adbbbba

Overlap of [11] bbbabd=adbbbb with [9] da=ad:

bbbab d da

Critical pair: bbbabad=adbbbba.

Defines rule #10.

[15] adbbbbc=bbbab

Overlap of [11] bbbabd=adbbbb with [10] dc=1:

bbbab d dc

Critical pair: bbbab=adbbbbc.

Flip LHS and RHS.

Referenced by [16].

[16] bbbbc=aabbbab

Overlap of [2] aaa=c with [15] adbbbbc=bbbab:

aa a adbbbbc

Critical pair: aabbbab=cdbbbbc.

Reduce RHS:

[8]	(cd)bbbbc
	⇒ bbbbc

Flip LHS and RHS.

Defines rule #6.

Referenced by [17], [18].

[17] bbbcbbbab=1

Overlap of [3] bbbabbbb=d with [16] bbbbc=aabbbab:

bbba bbbb bbbbc

Critical pair: bbbaaabbbab=dc.

Reduce LHS:

[2]	bbb(aaa)bbbab
	⇒ bbbcbbbab

Reduce RHS:

[10]	(dc)
	⇒ 1

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

[18] bbbbac=aabbbaba

Overlap of [16] bbbbc=aabbbab with [5] ca=ac:

bbbb c ca

Critical pair: bbbbac=aabbbaba.

Defines rule #9.

Referenced by [20], [21].

[19] bbbcbbba=bbcbbbab

Overlap of [17] bbbcbbbab=1 with [17] bbbcbbbab=1:

bbbcbbba b bbbcbbbab

Critical pair: bbbcbbba=bbcbbbab.

Referenced by [20].

[20] bbcbbbabba=a

Overlap of [3] bbbabbbb=d with [18] bbbbac=aabbbaba:

bbba bbbb bbbbac

Critical pair: bbbaaabbbaba=dac.

Reduce LHS:

[2]	bbb(aaa)bbbaba
[19]	⇒ (bbbcbbba)ba
	⇒ bbcbbbabba

Reduce RHS:

[9]	(da)c
[10]	⇒ a(dc)
	⇒ a

Referenced by [22].

[21] bbbbaac=aabbbabaa

Overlap of [18] bbbbac=aabbbaba with [5] ca=ac:

bbbba c ca

Critical pair: bbbbaac=aabbbabaa.

Referenced by [31].

[22] bbcbbbabbc=c

Overlap of [20] bbcbbbabba=a with [2] aaa=c:

bbcbbbabb a aaa

Critical pair: bbcbbbabbc=aaa.

Reduce RHS:

[2]	(aaa)
	⇒ c

Referenced by [23], [24].

[23] bbcbbbabb=1

Overlap of [22] bbcbbbabbc=c with [8] cd=1:

bbcbbbabb c cd

Critical pair: bbcbbbabb=cd.

Reduce RHS:

[8]	(cd)
	⇒ 1

Referenced by [24], [25].

[24] bbcbbba=cbbbabb

Overlap of [22] bbcbbbabbc=c with [23] bbcbbbabb=1:

bbcbbba bbc bbcbbbabb

Critical pair: bbcbbba=cbbbabb.

Referenced by [25].

[25] bcbbbab=cbbbabb

Overlap of [23] bbcbbbabb=1 with [17] bbbcbbbab=1:

bbcbbba bb bbbcbbbab

Critical pair: bbcbbba=bcbbbab.

Reduce LHS:

[24]	(bbcbbba)
	⇒ cbbbabb

Flip LHS and RHS.

Referenced by [26].

[26] bcbbba=cbbbab

Overlap of [25] bcbbbab=cbbbabb with [17] bbbcbbbab=1:

bcbbba b bbbcbbbab

Critical pair: bcbbba=cbbbabbbbcbbbab.

Reduce RHS:

[3]	c(bbbabbbb)cbbbab
[8]	⇒ (cd)cbbbab
	⇒ cbbbab

Defines rule #8.

Referenced by [27], [29], [34].

[27] cbbbabaa=bcbbbc

Overlap of [26] bcbbba=cbbbab with [2] aaa=c:

bcbbb a aaa

Critical pair: bcbbbc=cbbbabaa.

Flip LHS and RHS.

Referenced by [28], [29].

[28] bbbabaa=dbcbbbc

Overlap of [10] dc=1 with [27] cbbbabaa=bcbbbc:

d c cbbbabaa

Critical pair: dbcbbbc=bbbabaa.

Flip LHS and RHS.

Defines rule #12.

Referenced by [31].

[29] cbbbabbaa=bbcbbbc

Overlap of [26] bcbbba=cbbbab with [27] cbbbabaa=bcbbbc:

b cbbba cbbbabaa

Critical pair: bbcbbbc=cbbbabbaa.

Flip LHS and RHS.

Referenced by [33], [34].

[30] bbbabbad=dbabbbba

Overlap of [12] bbbabbd=dbabbbb with [9] da=ad:

bbbabb d da

Critical pair: bbbabbad=dbabbbba.

Defines rule #14.

[31] bbbbaac=aadbcbbbc

Simplify [21] bbbbaac=aabbbabaa.

Reduce RHS:

[28]	aa(bbbabaa)
	⇒ aadbcbbbc

Referenced by [32].

[32] bbbbaa=aadbcbbb

Overlap of [31] bbbbaac=aadbcbbbc with [8] cd=1:

bbbbaa c cd

Critical pair: bbbbaa=aadbcbbbcd.

Reduce RHS:

[8]	aadbcbbb(cd)
	⇒ aadbcbbb

Defines rule #11.

[33] bbbabbaa=dbbcbbbc

Overlap of [10] dc=1 with [29] cbbbabbaa=bbcbbbc:

d c cbbbabbaa

Critical pair: dbbcbbbc=bbbabbaa.

Flip LHS and RHS.

Defines rule #15.

[34] cbbbabbbaa=bbbcbbbc

Overlap of [26] bcbbba=cbbbab with [29] cbbbabbaa=bbcbbbc:

b cbbba cbbbabbaa

Critical pair: bbbcbbbc=cbbbabbbaa.

Flip LHS and RHS.

Referenced by [36].

[35] bbbabbbad=dbbabbbba

Overlap of [13] bbbabbbd=dbbabbbb with [9] da=ad:

bbbabbb d da

Critical pair: bbbabbbad=dbbabbbba.

Defines rule #17.

[36] bbbabbbaa=dbbbcbbbc

Overlap of [10] dc=1 with [34] cbbbabbbaa=bbbcbbbc:

d c cbbbabbbaa

Critical pair: dbbbcbbbc=bbbabbbaa.

Flip LHS and RHS.

Defines rule #18.