Certificate for #1370 ⟨a, b | aaabbaabba=1⟩

Completion settings:

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

[1] aaabbaabba=1

Axiom: aaabbaabba=1.

Referenced by [4].

[2] aaaa=c

Axiom: aaaa=c.

Defines rule #9.

Referenced by [5], [6], [7], [16], [17], [24].

[3] bbaabb=d

Axiom: bbaabb=d.

Referenced by [4], [9], [16], [17], [21].

[4] aaada=1

Overlap of [1] aaabbaabba=1 with [3] bbaabb=d:

aaa bbaabba bbaabb

Critical pair: aaada=1.

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

[5] ca=ac

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

a aaa aaaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [13], [24].

[6] cda=a

Overlap of [2] aaaa=c with [4] aaada=1:

a aaa aaada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

[7] aaadc=aaa

Overlap of [4] aaada=1 with [2] aaaa=c:

aaad a aaaa

Critical pair: aaadc=aaa.

Referenced by [10].

[8] cd=1

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

cd a aaada

Critical pair: cd=aaada.

Reduce RHS:

[4]	(aaada)
	⇒ 1

Defines rule #2.

Referenced by [14], [16], [17], [19], [24], [27], [28], [29], [31].

[9] bbaad=daabb

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

bbaa bb bbaabb

Critical pair: bbaad=daabb.

Referenced by [15].

[10] aadc=aa

Overlap of [4] aaada=1 with [7] aaadc=aaa:

aaad a aaadc

Critical pair: aaadaaa=aadc.

Reduce LHS:

[4]	(aaada)aa
	⇒ aa

Flip LHS and RHS.

Referenced by [11].

[11] adc=a

Overlap of [4] aaada=1 with [10] aadc=aa:

aaad a aadc

Critical pair: aaadaa=adc.

Reduce LHS:

[4]	(aaada)a
	⇒ a

Flip LHS and RHS.

Referenced by [12].

[12] dc=1

Overlap of [4] aaada=1 with [11] adc=a:

aaad a adc

Critical pair: aaada=dc.

Reduce LHS:

[4]	(aaada)
	⇒ 1

Flip LHS and RHS.

Defines rule #1.

Referenced by [13], [20], [22], [23], [24], [26], [30].

[13] dac=a

Overlap of [12] dc=1 with [5] ca=ac:

d c ca

Critical pair: dac=a.

Referenced by [14].

[14] da=ad

Overlap of [13] dac=a with [8] cd=1:

da c cd

Critical pair: da=ad.

Defines rule #4.

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

[15] bbaad=aadbb

Simplify [9] bbaad=daabb.

Reduce RHS:

[14]	(da)abb
[14]	⇒ a(da)bb
	⇒ aadbb

Referenced by [16].

[16] bbbb=aadd

Overlap of [3] bbaabb=d with [15] bbaad=aadbb:

bbaa bb bbaad

Critical pair: bbaaaadbb=daad.

Reduce LHS:

[2]	bb(aaaa)dbb
[8]	⇒ bb(cd)bb
	⇒ bbbb

Reduce RHS:

[14]	(da)ad
[14]	⇒ a(da)d
	⇒ aadd

Defines rule #10.

Referenced by [17], [18], [24].

[17] dbb=bbd

Overlap of [16] bbbb=aadd with [3] bbaabb=d:

bb bb bbaabb

Critical pair: bbd=aaddaabb.

Reduce RHS:

[14]	aad(da)abb
[14]	⇒ aa(da)dabb
[14]	⇒ aaad(da)bb
[14]	⇒ aaa(da)dbb
[2]	⇒ (aaaa)ddbb
[8]	⇒ (cd)dbb
	⇒ dbb

Flip LHS and RHS.

Referenced by [19], [24].

[18] baadd=aaddb

Overlap of [16] bbbb=aadd with [16] bbbb=aadd:

b bbb bbbb

Critical pair: baadd=aaddb.

Referenced by [22].

[19] cbbd=bb

Overlap of [8] cd=1 with [17] dbb=bbd:

c d dbb

Critical pair: cbbd=bb.

Referenced by [20].

[20] cbb=bbc

Overlap of [19] cbbd=bb with [12] dc=1:

cbb d dc

Critical pair: cbb=bbc.

Defines rule #7.

Referenced by [21], [24].

[21] bbcbaabb=cbd

Overlap of [20] cbb=bbc with [3] bbaabb=d:

cb b bbaabb

Critical pair: cbd=bbcbaabb.

Flip LHS and RHS.

Referenced by [24].

[22] baad=aaddbc

Overlap of [18] baadd=aaddb with [12] dc=1:

baad d dc

Critical pair: baad=aaddbc.

Referenced by [23], [25].

[23] baa=aaddbcc

Overlap of [22] baad=aaddbc with [12] dc=1:

baa d dc

Critical pair: baa=aaddbcc.

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

[24] ddbcc=cbd

Overlap of [21] bbcbaabb=cbd with [23] baa=aaddbcc:

bbc baabb baa

Critical pair: bbcaaddbccbb=cbd.

Reduce LHS:

[5]	bb(ca)addbccbb
[5]	⇒ bba(ca)ddbccbb
[23]	⇒ b(baa)cddbccbb
[23]	⇒ (baa)ddbcccddbccbb
[8]	⇒ aaddbc(cd)dbcccddbccbb
[8]	⇒ aaddb(cd)bcccddbccbb
[17]	⇒ aad(dbb)cccddbccbb
[17]	⇒ aa(dbb)dcccddbccbb
[12]	⇒ aabbd(dc)ccddbccbb
[12]	⇒ aabb(dc)cddbccbb
[8]	⇒ aabb(cd)dbccbb
[20]	⇒ aabbdbc(cbb)
[20]	⇒ aabbdb(cbb)c
[17]	⇒ aabb(dbb)bcc
[16]	⇒ aa(bbbb)dbcc
[2]	⇒ (aaaa)dddbcc
[8]	⇒ (cd)ddbcc
	⇒ ddbcc