Certificate for #2886 ⟨a, b | aaaabbbaaba=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. aaaaa=c
2. bbbaab=d

[1] aaaabbbaaba=1

Axiom: aaaabbbaaba=1.

Referenced by [4].

[2] aaaaa=c

Axiom: aaaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [10], [15], [17], [19], [24], [26], [29], [35].

[3] bbbaab=d

Axiom: bbbaab=d.

Defines rule #16.

Referenced by [4], [11], [26].

[4] aaaada=1

Overlap of [1] aaaabbbaaba=1 with [3] bbbaab=d:

aaaa bbbaaba bbbaab

Critical pair: aaaada=1.

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

[5] ac=ca

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

a aaaa aaaaa

Critical pair: ac=ca.

Defines rule #3.

Referenced by [25], [32].

[6] cda=a

Overlap of [2] aaaaa=c with [4] aaaada=1:

a aaaa aaaada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10].

[7] cada=aa

Overlap of [2] aaaaa=c with [4] aaaada=1:

aa aaa aaaada

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [10].

[8] aaaad=aaada

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

aaaad a aaaada

Critical pair: aaaad=aaada.

Referenced by [9], [12], [19].

[9] aaadaa=cd

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

cd a aaaada

Critical pair: cd=aaaada.

Reduce RHS:

[8]	(aaaad)a
	⇒ aaadaa

Flip LHS and RHS.

Referenced by [12], [13].

[10] cad=a

Overlap of [7] cada=aa with [4] aaaada=1:

cad a aaaada

Critical pair: cad=aaaaada.

Reduce RHS:

[2]	(aaaaa)da
[6]	⇒ (cda)
	⇒ a

Referenced by [18].

[11] dbbaab=bbbaad

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

bbbaa b bbbaab

Critical pair: bbbaad=dbbaab.

Flip LHS and RHS.

Referenced by [20].

[12] cd=1

Overlap of [4] aaaada=1 with [8] aaaad=aaada:

aaaada aaaad

Critical pair: aaadaa=1.

Reduce LHS:

[9]	(aaadaa)
	⇒ cd

Defines rule #1.

Referenced by [13], [15], [19], [21], [26], [30], [33].

[13] aaadaa=1

Simplify [9] aaadaa=cd.

Reduce RHS:

[12]	(cd)
	⇒ 1

Referenced by [14], [16].

[14] aaad=adaa

Overlap of [13] aaadaa=1 with [13] aaadaa=1:

aaad aa aaadaa

Critical pair: aaad=adaa.

Referenced by [15], [16], [19].

[15] adaaaa=1

Overlap of [2] aaaaa=c with [14] aaad=adaa:

aa aaa aaad

Critical pair: aaadaa=cd.

Reduce LHS:

[14]	(aaad)aa
	⇒ adaaaa

Reduce RHS:

[12]	(cd)
	⇒ 1

Referenced by [16], [17].

[16] aad=daa

Overlap of [13] aaadaa=1 with [14] aaad=adaa:

aaada a aaad

Critical pair: aaadaadaa=aad.

Reduce LHS:

[14]	(aaad)aadaa
[15]	⇒ (adaaaa)daa
	⇒ daa

Flip LHS and RHS.

Referenced by [17], [20], [22].

[17] dca=a

Overlap of [16] aad=daa with [15] adaaaa=1:

a ad adaaaa

Critical pair: a=daaaaaa.

Reduce RHS:

[2]	d(aaaaa)a
	⇒ dca

Flip LHS and RHS.

Referenced by [18].

[18] ad=da

Overlap of [17] dca=a with [10] cad=a:

d ca cad

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [19], [23], [34].

[19] dc=1

Overlap of [2] aaaaa=c with [18] ad=da:

aaaa a ad

Critical pair: aaaada=cd.

Reduce LHS:

[8]	(aaaad)a
[14]	⇒ (aaad)aa
[18]	⇒ (ad)aaaa
[2]	⇒ d(aaaaa)
	⇒ dc

Reduce RHS:

[12]	(cd)
	⇒ 1

Defines rule #2.

Referenced by [24], [34], [35].

[20] dbbaab=bbbdaa

Simplify [11] dbbaab=bbbaad.

Reduce RHS:

[16]	bbb(aad)
	⇒ bbbdaa

Defines rule #9.

Referenced by [21], [22], [23].

[21] cbbbdaa=bbaab

Overlap of [12] cd=1 with [20] dbbaab=bbbdaa:

c d dbbaab

Critical pair: cbbbdaa=bbaab.

Referenced by [24].

[22] daabbaab=aabbbdaa

Overlap of [16] aad=daa with [20] dbbaab=bbbdaa:

aa d dbbaab

Critical pair: aabbbdaa=daabbaab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [34].

[23] dabbaab=abbbdaa

Overlap of [18] ad=da with [20] dbbaab=bbbdaa:

a d dbbaab

Critical pair: abbbdaa=dabbaab.

Flip LHS and RHS.

Defines rule #11.

[24] cbbb=bbaabaaa

Overlap of [21] cbbbdaa=bbaab with [2] aaaaa=c:

cbbbd aa aaaaa

Critical pair: cbbbdc=bbaabaaa.

Reduce LHS:

[19]	cbbb(dc)
	⇒ cbbb

Defines rule #8.

Referenced by [25], [26].

[25] cabbb=abbaabaaa

Overlap of [5] ac=ca with [24] cbbb=bbaabaaa:

a c cbbb

Critical pair: abbaabaaa=cabbb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [32].

[26] bbaabcb=1

Overlap of [24] cbbb=bbaabaaa with [3] bbbaab=d:

c bbb bbbaab

Critical pair: cd=bbaabaaaaab.

Reduce LHS:

[12]	(cd)
	⇒ 1

Reduce RHS:

[2]	bbaab(aaaaa)b
	⇒ bbaabcb

Flip LHS and RHS.

Referenced by [27], [28].

[27] baabcb=bbaabc

Overlap of [26] bbaabcb=1 with [26] bbaabcb=1:

bbaabc b bbaabcb

Critical pair: bbaabc=baabcb.

Flip LHS and RHS.

Referenced by [28], [31].

[28] aabcb=baabc

Overlap of [26] bbaabcb=1 with [27] baabcb=bbaabc:

bbaabc b baabcb

Critical pair: bbaabcbbaabc=aabcb.

Reduce LHS:

[26]	(bbaabcb)baabc
	⇒ baabc

Flip LHS and RHS.

Defines rule #6.

Referenced by [29].

[29] aaabaabc=cbcb

Overlap of [2] aaaaa=c with [28] aabcb=baabc:

aaa aa aabcb

Critical pair: aaabaabc=cbcb.

Referenced by [30], [31].

[30] aaabaab=cbcbd

Overlap of [29] aaabaabc=cbcb with [12] cd=1:

aaabaab c cd

Critical pair: aaabaab=cbcbd.

Defines rule #7.

[31] aaabbaabc=cbcbb

Overlap of [29] aaabaabc=cbcb with [27] baabcb=bbaabc:

aaa baabc baabcb

Critical pair: aaabbaabc=cbcbb.

Referenced by [33].

[32] caabbb=aabbaabaaa

Overlap of [5] ac=ca with [25] cabbb=abbaabaaa:

a c cabbb

Critical pair: aabbaabaaa=caabbb.

Flip LHS and RHS.

Defines rule #12.

[33] aaabbaab=cbcbbd

Overlap of [31] aaabbaabc=cbcbb with [12] cd=1:

aaabbaab c cd

Critical pair: aaabbaab=cbcbbd.

Defines rule #15.

Referenced by [34].

[34] aaabbbdaa=bcbbd

Overlap of [18] ad=da with [22] daabbaab=aabbbdaa:

a d daabbaab

Critical pair: aaabbbdaa=daaabbaab.

Reduce RHS:

[33]	d(aaabbaab)
[19]	⇒ (dc)bcbbd
	⇒ bcbbd

Referenced by [35].

[35] aaabbb=bcbbdaaa

Overlap of [34] aaabbbdaa=bcbbd with [2] aaaaa=c:

aaabbbd aa aaaaa

Critical pair: aaabbbdc=bcbbdaaa.

Reduce LHS:

[19]	aaabbb(dc)
	⇒ aaabbb

Defines rule #14.