Certificate for #691 ⟨a, b | aabbbbaba=1⟩

Completion settings:

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

[1] aabbbbaba=1

Axiom: aabbbbaba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [15], [17], [20].

[3] bbbbab=d

Axiom: bbbbab=d.

Defines rule #15.

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

[4] aada=1

Overlap of [1] aabbbbaba=1 with [3] bbbbab=d:

aa bbbbaba bbbbab

Critical pair: aada=1.

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

[5] ac=ca

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

a aa aaa

Critical pair: ac=ca.

Defines rule #3.

Referenced by [16], [25].

[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] aad=ada

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

aad a aada

Critical pair: aad=ada.

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

[8] adaa=cd

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

cd a aada

Critical pair: cd=aada.

Reduce RHS:

[7]	(aad)a
	⇒ adaa

Flip LHS and RHS.

Referenced by [9], [10].

[9] cd=1

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

aada aad

Critical pair: adaa=1.

Reduce LHS:

[8]	(adaa)
	⇒ cd

Defines rule #1.

Referenced by [10], [11], [13], [17], [21], [23], [26].

[10] ad=da

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

aad a aad

Critical pair: aadada=ad.

Reduce LHS:

[7]	(aad)ada
[8]	⇒ (adaa)da
[9]	⇒ (cd)da
	⇒ da

Flip LHS and RHS.

Defines rule #4.

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

[11] dc=1

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

aa a ad

Critical pair: aada=cd.

Reduce LHS:

[7]	(aad)a
[10]	⇒ (ad)aa
[2]	⇒ d(aaa)
	⇒ dc

Reduce RHS:

[9]	(cd)
	⇒ 1

Defines rule #2.

Referenced by [15], [28].

[12] dbbbab=bbbbda

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

bbbba b bbbbab

Critical pair: bbbbad=dbbbab.

Reduce LHS:

[10]	bbbb(ad)
	⇒ bbbbda

Flip LHS and RHS.

Defines rule #10.

Referenced by [13], [14].

[13] cbbbbda=bbbab

Overlap of [9] cd=1 with [12] dbbbab=bbbbda:

c d dbbbab

Critical pair: cbbbbda=bbbab.

Referenced by [15].

[14] dabbbab=abbbbda

Overlap of [10] ad=da with [12] dbbbab=bbbbda:

a d dbbbab

Critical pair: abbbbda=dabbbab.

Flip LHS and RHS.

Defines rule #12.

[15] cbbbb=bbbabaa

Overlap of [13] cbbbbda=bbbab with [2] aaa=c:

cbbbbd a aaa

Critical pair: cbbbbdc=bbbabaa.

Reduce LHS:

[11]	cbbbb(dc)
	⇒ cbbbb

Defines rule #9.

Referenced by [16], [17].

[16] cabbbb=abbbabaa

Overlap of [5] ac=ca with [15] cbbbb=bbbabaa:

a c cbbbb

Critical pair: abbbabaa=cabbbb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [25].

[17] bbbabcb=1

Overlap of [15] cbbbb=bbbabaa with [3] bbbbab=d:

c bbbb bbbbab

Critical pair: cd=bbbabaaab.

Reduce LHS:

[9]	(cd)
	⇒ 1

Reduce RHS:

[2]	bbbab(aaa)b
	⇒ bbbabcb

Flip LHS and RHS.

Referenced by [18], [19].

[18] bbabcb=bbbabc

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

bbbabc b bbbabcb

Critical pair: bbbabc=bbabcb.

Flip LHS and RHS.

Referenced by [19], [24].

[19] abcb=babc

Overlap of [18] bbabcb=bbbabc with [18] bbabcb=bbbabc:

bbabc b bbabcb

Critical pair: bbabcbbbabc=bbbabcbabcb.

Reduce LHS:

[18]	(bbabcb)bbabc
[17]	⇒ (bbbabcb)babc
	⇒ babc

Reduce RHS:

[17]	(bbbabcb)abcb
	⇒ abcb

Flip LHS and RHS.

Defines rule #6.

Referenced by [20], [22].

[20] aababc=cbcb

Overlap of [2] aaa=c with [19] abcb=babc:

aa a abcb

Critical pair: aababc=cbcb.

Referenced by [21], [22].

[21] aabab=cbcbd

Overlap of [20] aababc=cbcb with [9] cd=1:

aabab c cd

Critical pair: aabab=cbcbd.

Defines rule #7.

[22] aabbabc=cbcbb

Overlap of [20] aababc=cbcb with [19] abcb=babc:

aab abc abcb

Critical pair: aabbabc=cbcbb.

Referenced by [23], [24].

[23] aabbab=cbcbbd

Overlap of [22] aabbabc=cbcbb with [9] cd=1:

aabbab c cd

Critical pair: aabbab=cbcbbd.

Defines rule #8.

[24] aabbbabc=cbcbbb

Overlap of [22] aabbabc=cbcbb with [18] bbabcb=bbbabc:

aa bbabc bbabcb

Critical pair: aabbbabc=cbcbbb.

Referenced by [26].

[25] caabbbb=aabbbabaa

Overlap of [5] ac=ca with [16] cabbbb=abbbabaa:

a c cabbbb

Critical pair: aabbbabaa=caabbbb.

Flip LHS and RHS.

Referenced by [27].

[26] aabbbab=cbcbbbd

Overlap of [24] aabbbabc=cbcbbb with [9] cd=1:

aabbbab c cd

Critical pair: aabbbab=cbcbbbd.

Defines rule #14.

Referenced by [27].

[27] caabbbb=cbcbbbdaa

Simplify [25] caabbbb=aabbbabaa.

Reduce RHS:

[26]	(aabbbab)aa
	⇒ cbcbbbdaa

Referenced by [28].

[28] aabbbb=bcbbbdaa

Overlap of [11] dc=1 with [27] caabbbb=cbcbbbdaa:

d c caabbbb

Critical pair: dcbcbbbdaa=aabbbb.

Reduce LHS:

[11]	(dc)bcbbbdaa
	⇒ bcbbbdaa

Flip LHS and RHS.

Defines rule #13.