Certificate for #310 ⟨a, b | aababbba=1⟩

Completion settings:

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

[1] aababbba=1

Axiom: aababbba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [15], [20].

[3] babbb=d

Axiom: babbb=d.

Defines rule #14.

Referenced by [4], [11], [15], [18].

[4] aada=1

Overlap of [1] aababbba=1 with [3] babbb=d:

aa babbba babbb

Critical pair: aada=1.

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

[5] ca=ac

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

a aa aaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [23].

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

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

aad a aada

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [9], [10].

[8] cd=1

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

cd a aada

Critical pair: cd=aada.

Reduce RHS:

[4]	(aada)
	⇒ 1

Defines rule #2.

Referenced by [14], [26].

[9] da=ad

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

aad a ada

Critical pair: aadaad=da.

Reduce LHS:

[4]	(aada)ad
	⇒ ad

Flip LHS and RHS.

Defines rule #4.

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

[10] dc=1

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

d a aaa

Critical pair: dc=adaa.

Reduce RHS:

[7]	(ada)a
[4]	⇒ (aada)
	⇒ 1

Defines rule #1.

Referenced by [13], [15], [19], [21], [24].

[11] babbd=adbbb

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

babb b babbb

Critical pair: babbd=dabbb.

Reduce RHS:

[9]	(da)bbb
	⇒ adbbb

Defines rule #9.

Referenced by [12], [13].

[12] babbad=adbbba

Overlap of [11] babbd=adbbb with [9] da=ad:

babb d da

Critical pair: babbad=adbbba.

Defines rule #11.

[13] adbbbc=babb

Overlap of [11] babbd=adbbb with [10] dc=1:

babb d dc

Critical pair: babb=adbbbc.

Flip LHS and RHS.

Referenced by [14].

[14] bbbc=aababb

Overlap of [2] aaa=c with [13] adbbbc=babb:

aa a adbbbc

Critical pair: aababb=cdbbbc.

Reduce RHS:

[8]	(cd)bbbc
	⇒ bbbc

Flip LHS and RHS.

Defines rule #8.

Referenced by [15], [16].

[15] bcbabb=1

Overlap of [3] babbb=d with [14] bbbc=aababb:

ba bbb bbbc

Critical pair: baaababb=dc.

Reduce LHS:

[2]	b(aaa)babb
	⇒ bcbabb

Reduce RHS:

[10]	(dc)
	⇒ 1

Referenced by [17].

[16] bbbac=aababba

Overlap of [14] bbbc=aababb with [5] ca=ac:

bbb c ca

Critical pair: bbbac=aababba.

Defines rule #10.

Referenced by [23].

[17] bcbab=cbabb

Overlap of [15] bcbabb=1 with [15] bcbabb=1:

bcbab b bcbabb

Critical pair: bcbab=cbabb.

Referenced by [18], [22].

[18] bcbad=cbabd

Overlap of [17] bcbab=cbabb with [3] babbb=d:

bcba b babbb

Critical pair: bcbad=cbabbabbb.

Reduce RHS:

[3]	cbab(babbb)
	⇒ cbabd

Referenced by [19].

[19] bcba=cbab

Overlap of [18] bcbad=cbabd with [10] dc=1:

bcba d dc

Critical pair: bcba=cbabdc.

Reduce RHS:

[10]	cbab(dc)
	⇒ cbab

Defines rule #6.

Referenced by [20].

[20] cbabaa=bcbc

Overlap of [19] bcba=cbab with [2] aaa=c:

bcb a aaa

Critical pair: bcbc=cbabaa.

Flip LHS and RHS.

Referenced by [21], [22].

[21] babaa=dbcbc

Overlap of [10] dc=1 with [20] cbabaa=bcbc:

d c cbabaa

Critical pair: dbcbc=babaa.

Flip LHS and RHS.

Defines rule #7.

[22] cbabbaa=bbcbc

Overlap of [17] bcbab=cbabb with [20] cbabaa=bcbc:

b cbab cbabaa

Critical pair: bbcbc=cbabbaa.

Flip LHS and RHS.

Referenced by [24].

[23] bbbaac=aababbaa

Overlap of [16] bbbac=aababba with [5] ca=ac:

bbba c ca

Critical pair: bbbaac=aababbaa.

Referenced by [25].

[24] babbaa=dbbcbc

Overlap of [10] dc=1 with [22] cbabbaa=bbcbc:

d c cbabbaa

Critical pair: dbbcbc=babbaa.

Flip LHS and RHS.

Defines rule #13.

Referenced by [25].

[25] bbbaac=aadbbcbc

Simplify [23] bbbaac=aababbaa.

Reduce RHS:

[24]	aa(babbaa)
	⇒ aadbbcbc

Referenced by [26].

[26] bbbaa=aadbbcb

Overlap of [25] bbbaac=aadbbcbc with [8] cd=1:

bbbaa c cd

Critical pair: bbbaa=aadbbcbcd.

Reduce RHS:

[8]	aadbbcb(cd)
	⇒ aadbbcb

Defines rule #12.