Certificate for #2979 ⟨a, b | aaabbabbbba=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. aaaa=c
2. bbabbbb=d

[1] aaabbabbbba=1

Axiom: aaabbabbbba=1.

Referenced by [4].

[2] aaaa=c

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [16], [17], [22], [23], [31].

[3] bbabbbb=d

Axiom: bbabbbb=d.

Defines rule #20.

Referenced by [4], [12], [13], [17], [21].

[4] aaada=1

Overlap of [1] aaabbabbbba=1 with [3] bbabbbb=d:

aaa bbabbbba bbabbbb

Critical pair: aaada=1.

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

[5] ca=ac

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

a aaa aaaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [18], [28].

[6] cda=a

Overlap of [2] aaaa=c with [4] aaada=1:

a aaa aaada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

[7] aada=aaad

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

aaad a aaada

Critical pair: aaad=aada.

Flip LHS and RHS.

Referenced by [9], [10], [11].

[8] cd=1

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

cd a aaada

Critical pair: cd=aaada.

Reduce RHS:

[4]	(aaada)
	⇒ 1

Defines rule #2.

Referenced by [16], [21], [30], [31].

[9] ada=aad

Overlap of [4] aaada=1 with [7] aada=aaad:

aaad a aada

Critical pair: aaadaaad=ada.

Reduce LHS:

[4]	(aaada)aad
	⇒ aad

Flip LHS and RHS.

Referenced by [11].

[10] da=ad

Overlap of [7] aada=aaad with [7] aada=aaad:

aad a aada

Critical pair: aadaaad=aaadada.

Reduce LHS:

[7]	(aada)aad
[4]	⇒ (aaada)ad
	⇒ ad

Reduce RHS:

[4]	(aaada)da
	⇒ da

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [12], [14], [26], [27], [30], [32].

[11] dc=1

Overlap of [10] da=ad with [2] aaaa=c:

d a aaaa

Critical pair: dc=adaaa.

Reduce RHS:

[9]	(ada)aa
[7]	⇒ (aada)a
[4]	⇒ (aaada)
	⇒ 1

Defines rule #1.

Referenced by [15], [17], [24], [29], [33].

[12] bbabbd=adbbbb

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

bbabb bb bbabbbb

Critical pair: bbabbd=dabbbb.

Reduce RHS:

[10]	(da)bbbb
	⇒ adbbbb

Defines rule #9.

Referenced by [14], [15].

[13] bbabbbd=dbabbbb

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

bbabbb b bbabbbb

Critical pair: bbabbbd=dbabbbb.

Defines rule #16.

Referenced by [27].

[14] bbabbad=adbbbba

Overlap of [12] bbabbd=adbbbb with [10] da=ad:

bbabb d da

Critical pair: bbabbad=adbbbba.

Defines rule #11.

Referenced by [26].

[15] adbbbbc=bbabb

Overlap of [12] bbabbd=adbbbb with [11] dc=1:

bbabb d dc

Critical pair: bbabb=adbbbbc.

Flip LHS and RHS.

Referenced by [16].

[16] bbbbc=aaabbabb

Overlap of [2] aaaa=c with [15] adbbbbc=bbabb:

aaa a adbbbbc

Critical pair: aaabbabb=cdbbbbc.

Reduce RHS:

[8]	(cd)bbbbc
	⇒ bbbbc

Flip LHS and RHS.

Defines rule #8.

Referenced by [17], [18].

[17] bbcbbabb=1

Overlap of [3] bbabbbb=d with [16] bbbbc=aaabbabb:

bba bbbb bbbbc

Critical pair: bbaaaabbabb=dc.

Reduce LHS:

[2]	bb(aaaa)bbabb
	⇒ bbcbbabb

Reduce RHS:

[11]	(dc)
	⇒ 1

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

[18] bbbbac=aaabbabba

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

bbbb c ca

Critical pair: bbbbac=aaabbabba.

Defines rule #10.

Referenced by [28].

[19] bbcbba=cbbabb

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

bbcbba bb bbcbbabb

Critical pair: bbcbba=cbbabb.

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

[20] bcbbabb=cbbabbb

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

bbcbbab b bbcbbabb

Critical pair: bbcbbab=bcbbabb.

Reduce LHS:

[19]	(bbcbba)b
	⇒ cbbabbb

Flip LHS and RHS.

Referenced by [21].

[21] bcbba=cbbab

Overlap of [17] bbcbbabb=1 with [19] bbcbba=cbbabb:

bbcbbab b bbcbba

Critical pair: bbcbbabcbbabb=bcbba.

Reduce LHS:

[19]	(bbcbba)bcbbabb
[19]	⇒ cbbab(bbcbba)bb
[20]	⇒ cbba(bcbbabb)bb
[3]	⇒ cbbac(bbabbbb)b
[8]	⇒ cbba(cd)b
	⇒ cbbab

Flip LHS and RHS.

Defines rule #6.

Referenced by [23].

[22] cbbabbaaa=bbcbbc

Overlap of [19] bbcbba=cbbabb with [2] aaaa=c:

bbcbb a aaaa

Critical pair: bbcbbc=cbbabbaaa.

Flip LHS and RHS.

Referenced by [29].

[23] cbbabaaa=bcbbc

Overlap of [21] bcbba=cbbab with [2] aaaa=c:

bcbb a aaaa

Critical pair: bcbbc=cbbabaaa.

Flip LHS and RHS.

Referenced by [24], [25].

[24] bbabaaa=dbcbbc

Overlap of [11] dc=1 with [23] cbbabaaa=bcbbc:

d c cbbabaaa

Critical pair: dbcbbc=bbabaaa.

Flip LHS and RHS.

Defines rule #7.

[25] cbbabbbaaa=bbbcbbc

Overlap of [19] bbcbba=cbbabb with [23] cbbabaaa=bcbbc:

bb cbba cbbabaaa

Critical pair: bbbcbbc=cbbabbbaaa.

Flip LHS and RHS.

Referenced by [33].

[26] bbabbaad=adbbbbaa

Overlap of [14] bbabbad=adbbbba with [10] da=ad:

bbabba d da

Critical pair: bbabbaad=adbbbbaa.

Defines rule #13.

Referenced by [30].

[27] bbabbbad=dbabbbba

Overlap of [13] bbabbbd=dbabbbb with [10] da=ad:

bbabbb d da

Critical pair: bbabbbad=dbabbbba.

Defines rule #17.

Referenced by [32].

[28] bbbbaac=aaabbabbaa

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

bbbba c ca

Critical pair: bbbbaac=aaabbabbaa.

Defines rule #12.

[29] bbabbaaa=dbbcbbc

Overlap of [11] dc=1 with [22] cbbabbaaa=bbcbbc:

d c cbbabbaaa

Critical pair: dbbcbbc=bbabbaaa.

Flip LHS and RHS.

Defines rule #15.

Referenced by [30].

[30] adbbbbaaa=dbbcbb

Overlap of [26] bbabbaad=adbbbbaa with [10] da=ad:

bbabbaa d da

Critical pair: bbabbaaad=adbbbbaaa.

Reduce LHS:

[29]	(bbabbaaa)d
[8]	⇒ dbbcbb(cd)
	⇒ dbbcbb

Flip LHS and RHS.

Referenced by [31].

[31] bbbbaaa=aaadbbcbb

Overlap of [2] aaaa=c with [30] adbbbbaaa=dbbcbb:

aaa a adbbbbaaa

Critical pair: aaadbbcbb=cdbbbbaaa.

Reduce RHS:

[8]	(cd)bbbbaaa
	⇒ bbbbaaa

Flip LHS and RHS.

Defines rule #14.

[32] bbabbbaad=dbabbbbaa

Overlap of [27] bbabbbad=dbabbbba with [10] da=ad:

bbabbba d da

Critical pair: bbabbbaad=dbabbbbaa.

Defines rule #18.

[33] bbabbbaaa=dbbbcbbc

Overlap of [11] dc=1 with [25] cbbabbbaaa=bbbcbbc:

d c cbbabbbaaa

Critical pair: dbbbcbbc=bbabbbaaa.

Flip LHS and RHS.

Defines rule #19.