Certificate for #3165 ⟨a, b | aabbbbbbaba=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. bbbbbbab=d

[1] aabbbbbbaba=1

Axiom: aabbbbbbaba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

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

[3] bbbbbbab=d

Axiom: bbbbbbab=d.

Defines rule #17.

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

[4] aada=1

Overlap of [1] aabbbbbbaba=1 with [3] bbbbbbab=d:

aa bbbbbbaba bbbbbbab

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], [20], [29].

[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], [25], [27], [30].

[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], [21], [22], [23], [24], [32].

[12] dbbbbbab=bbbbbbda

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

bbbbbba b bbbbbbab

Critical pair: bbbbbbad=dbbbbbab.

Reduce LHS:

[10]	bbbbbb(ad)
	⇒ bbbbbbda

Flip LHS and RHS.

Defines rule #12.

Referenced by [13], [14].

[13] cbbbbbbda=bbbbbab

Overlap of [9] cd=1 with [12] dbbbbbab=bbbbbbda:

c d dbbbbbab

Critical pair: cbbbbbbda=bbbbbab.

Referenced by [15].

[14] dabbbbbab=abbbbbbda

Overlap of [10] ad=da with [12] dbbbbbab=bbbbbbda:

a d dbbbbbab

Critical pair: abbbbbbda=dabbbbbab.

Flip LHS and RHS.

Defines rule #14.

[15] cbbbbbb=bbbbbabaa

Overlap of [13] cbbbbbbda=bbbbbab with [2] aaa=c:

cbbbbbbd a aaa

Critical pair: cbbbbbbdc=bbbbbabaa.

Reduce LHS:

[11]	cbbbbbb(dc)
	⇒ cbbbbbb

Defines rule #11.

Referenced by [16], [17], [18], [19].

[16] cabbbbbb=abbbbbabaa

Overlap of [5] ac=ca with [15] cbbbbbb=bbbbbabaa:

a c cbbbbbb

Critical pair: abbbbbabaa=cabbbbbb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [29].

[17] bbbbbabcb=1

Overlap of [15] cbbbbbb=bbbbbabaa with [3] bbbbbbab=d:

c bbbbbb bbbbbbab

Critical pair: cd=bbbbbabaaab.

Reduce LHS:

[9]	(cd)
	⇒ 1

Reduce RHS:

[2]	bbbbbab(aaa)b
	⇒ bbbbbabcb

Flip LHS and RHS.

Referenced by [19].

[18] bbbbbabaabab=cbd

Overlap of [15] cbbbbbb=bbbbbabaa with [3] bbbbbbab=d:

cb bbbbb bbbbbbab

Critical pair: cbd=bbbbbabaabab.

Flip LHS and RHS.

Referenced by [19].

[19] aabab=cbcbd

Overlap of [15] cbbbbbb=bbbbbabaa with [18] bbbbbabaabab=cbd:

cb bbbbb bbbbbabaabab

Critical pair: cbcbd=bbbbbabaaabaabab.

Reduce RHS:

[2]	bbbbbab(aaa)baabab
[17]	⇒ (bbbbbabcb)aabab
	⇒ aabab

Flip LHS and RHS.

Defines rule #7.

Referenced by [20], [22].

[20] cabcbd=cbab

Overlap of [2] aaa=c with [19] aabab=cbcbd:

a aa aabab

Critical pair: acbcbd=cbab.

Reduce LHS:

[5]	(ac)bcbd
	⇒ cabcbd

Referenced by [21].

[21] abcbd=bab

Overlap of [11] dc=1 with [20] cabcbd=cbab:

d c cabcbd

Critical pair: dcbab=abcbd.

Reduce LHS:

[11]	(dc)bab
	⇒ bab

Flip LHS and RHS.

Referenced by [22], [23].

[22] aabbab=cbcbbd

Overlap of [19] aabab=cbcbd with [21] abcbd=bab:

aab ab abcbd

Critical pair: aabbab=cbcbdcbd.

Reduce RHS:

[11]	cbcb(dc)bd
	⇒ cbcbbd

Defines rule #8.

Referenced by [24].

[23] abcb=babc

Overlap of [21] abcbd=bab with [11] dc=1:

abcb d dc

Critical pair: abcb=babc.

Defines rule #6.

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

[24] aabbbabc=cbcbbb

Overlap of [22] aabbab=cbcbbd with [23] abcb=babc:

aabb ab abcb

Critical pair: aabbbabc=cbcbbdcb.

Reduce RHS:

[11]	cbcbb(dc)b
	⇒ cbcbbb

Referenced by [25], [26].

[25] aabbbab=cbcbbbd

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

aabbbab c cd

Critical pair: aabbbab=cbcbbbd.

Defines rule #9.

[26] aabbbbabc=cbcbbbb

Overlap of [24] aabbbabc=cbcbbb with [23] abcb=babc:

aabbb abc abcb

Critical pair: aabbbbabc=cbcbbbb.

Referenced by [27], [28].

[27] aabbbbab=cbcbbbbd

Overlap of [26] aabbbbabc=cbcbbbb with [9] cd=1:

aabbbbab c cd

Critical pair: aabbbbab=cbcbbbbd.

Defines rule #10.

[28] aabbbbbabc=cbcbbbbb

Overlap of [26] aabbbbabc=cbcbbbb with [23] abcb=babc:

aabbbb abc abcb

Critical pair: aabbbbbabc=cbcbbbbb.

Referenced by [30].

[29] caabbbbbb=aabbbbbabaa

Overlap of [5] ac=ca with [16] cabbbbbb=abbbbbabaa:

a c cabbbbbb

Critical pair: aabbbbbabaa=caabbbbbb.

Flip LHS and RHS.

Referenced by [31].

[30] aabbbbbab=cbcbbbbbd

Overlap of [28] aabbbbbabc=cbcbbbbb with [9] cd=1:

aabbbbbab c cd

Critical pair: aabbbbbab=cbcbbbbbd.

Defines rule #16.

Referenced by [31].

[31] caabbbbbb=cbcbbbbbdaa

Simplify [29] caabbbbbb=aabbbbbabaa.

Reduce RHS:

[30]	(aabbbbbab)aa
	⇒ cbcbbbbbdaa

Referenced by [32].

[32] aabbbbbb=bcbbbbbdaa

Overlap of [11] dc=1 with [31] caabbbbbb=cbcbbbbbdaa:

d c caabbbbbb

Critical pair: dcbcbbbbbdaa=aabbbbbb.

Reduce LHS:

[11]	(dc)bcbbbbbdaa
	⇒ bcbbbbbdaa

Flip LHS and RHS.

Defines rule #15.