Certificate for #3159 ⟨a, b | aabbbbabbba=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. bbbbabbb=d

[1] aabbbbabbba=1

Axiom: aabbbbabbba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [17], [19], [21], [24], [27].

[3] bbbbabbb=d

Axiom: bbbbabbb=d.

Defines rule #19.

Referenced by [4], [12], [13], [14], [19].

[4] aada=1

Overlap of [1] aabbbbabbba=1 with [3] bbbbabbb=d:

aa bbbbabbba bbbbabbb

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 [18].

[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], [15], [19], [21], [29], [32].

[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], [16], [20], [22], [31].

[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 [17], [25], [26], [27], [28].

[12] dbabbb=bbbbda

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

bbbba bbb bbbbabbb

Critical pair: bbbbad=dbabbb.

Reduce LHS:

[10]	bbbb(ad)
	⇒ bbbbda

Flip LHS and RHS.

Defines rule #7.

Referenced by [15], [16].

[13] dbbabbb=bbbbabd

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

bbbbab bb bbbbabbb

Critical pair: bbbbabd=dbbabbb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [21], [22].

[14] dbbbabbb=bbbbabbd

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

bbbbabb b bbbbabbb

Critical pair: bbbbabbd=dbbbabbb.

Flip LHS and RHS.

Defines rule #16.

Referenced by [31].

[15] cbbbbda=babbb

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

c d dbabbb

Critical pair: cbbbbda=babbb.

Referenced by [17].

[16] dababbb=abbbbda

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

a d dbabbb

Critical pair: abbbbda=dababbb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [20].

[17] cbbbb=babbbaa

Overlap of [15] cbbbbda=babbb with [2] aaa=c:

cbbbbd a aaa

Critical pair: cbbbbdc=babbbaa.

Reduce LHS:

[11]	cbbbb(dc)
	⇒ cbbbb

Defines rule #6.

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

[18] cabbbb=ababbbaa

Overlap of [5] ac=ca with [17] cbbbb=babbbaa:

a c cbbbb

Critical pair: ababbbaa=cabbbb.

Flip LHS and RHS.

Defines rule #9.

[19] babbbcbbb=1

Overlap of [17] cbbbb=babbbaa with [3] bbbbabbb=d:

c bbbb bbbbabbb

Critical pair: cd=babbbaaabbb.

Reduce LHS:

[9]	(cd)
	⇒ 1

Reduce RHS:

[2]	babbb(aaa)bbb
	⇒ babbbcbbb

Flip LHS and RHS.

Referenced by [23].

[20] daababbb=aabbbbda

Overlap of [10] ad=da with [16] dababbb=abbbbda:

a d dababbb

Critical pair: aabbbbda=daababbb.

Flip LHS and RHS.

Referenced by [26].

[21] babbbcbd=bbabbb

Overlap of [9] cd=1 with [13] dbbabbb=bbbbabd:

c d dbbabbb

Critical pair: cbbbbabd=bbabbb.

Reduce LHS:

[17]	(cbbbb)abd
[2]	⇒ babbb(aaa)bd
	⇒ babbbcbd

Referenced by [23].

[22] dabbabbb=abbbbabd

Overlap of [10] ad=da with [13] dbbabbb=bbbbabd:

a d dbbabbb

Critical pair: abbbbabd=dabbabbb.

Flip LHS and RHS.

Defines rule #14.

[23] abbbcbd=babbb

Overlap of [19] babbbcbbb=1 with [21] babbbcbd=bbabbb:

babbbcbb b babbbcbd

Critical pair: babbbcbbbbabbb=abbbcbd.

Reduce LHS:

[19]	(babbbcbbb)babbb
	⇒ babbb

Flip LHS and RHS.

Referenced by [24], [25].

[24] aababbb=cbbbcbd

Overlap of [2] aaa=c with [23] abbbcbd=babbb:

aa a abbbcbd

Critical pair: aababbb=cbbbcbd.

Defines rule #12.

Referenced by [26], [28].

[25] abbbcb=babbbc

Overlap of [23] abbbcbd=babbb with [11] dc=1:

abbbcb d dc

Critical pair: abbbcb=babbbc.

Defines rule #8.

Referenced by [28], [30].

[26] aabbbbda=bbbcbd

Overlap of [20] daababbb=aabbbbda with [24] aababbb=cbbbcbd:

d aababbb aababbb

Critical pair: dcbbbcbd=aabbbbda.

Reduce LHS:

[11]	(dc)bbbcbd
	⇒ bbbcbd

Flip LHS and RHS.

Referenced by [27].

[27] aabbbb=bbbcbdaa

Overlap of [26] aabbbbda=bbbcbd with [2] aaa=c:

aabbbbd a aaa

Critical pair: aabbbbdc=bbbcbdaa.

Reduce LHS:

[11]	aabbbb(dc)
	⇒ aabbbb

Defines rule #11.

[28] aabbabbbc=cbbbcbb

Overlap of [24] aababbb=cbbbcbd with [25] abbbcb=babbbc:

aab abbb abbbcb

Critical pair: aabbabbbc=cbbbcbdcb.

Reduce RHS:

[11]	cbbbcb(dc)b
	⇒ cbbbcbb

Referenced by [29], [30].

[29] aabbabbb=cbbbcbbd

Overlap of [28] aabbabbbc=cbbbcbb with [9] cd=1:

aabbabbb c cd

Critical pair: aabbabbb=cbbbcbbd.

Defines rule #15.

[30] aabbbabbbc=cbbbcbbb

Overlap of [28] aabbabbbc=cbbbcbb with [25] abbbcb=babbbc:

aabb abbbc abbbcb

Critical pair: aabbbabbbc=cbbbcbbb.

Referenced by [32].

[31] dabbbabbb=abbbbabbd

Overlap of [10] ad=da with [14] dbbbabbb=bbbbabbd:

a d dbbbabbb

Critical pair: abbbbabbd=dabbbabbb.

Flip LHS and RHS.

Defines rule #17.

[32] aabbbabbb=cbbbcbbbd

Overlap of [30] aabbbabbbc=cbbbcbbb with [9] cd=1:

aabbbabbb c cd

Critical pair: aabbbabbb=cbbbcbbbd.

Defines rule #18.