Certificate for #3149 ⟨a, b | aabbbabbbaa=1⟩

Completion settings:

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

[1] aabbbabbbaa=1

Axiom: aabbbabbbaa=1.

Referenced by [4].

[2] bbba=c

Axiom: bbba=c.

Referenced by [4], [10].

[3] aaa=d

Axiom: aaa=d.

Defines rule #6.

Referenced by [5], [6], [7], [19], [24].

[4] aacca=1

Overlap of [1] aabbbabbbaa=1 with [2] bbba=c:

aa bbbabbbaa bbba

Critical pair: aacbbbaa=1.

Reduce LHS:

[2]	aac(bbba)a
	⇒ aacca

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

[5] da=ad

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

a aa aaa

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #3.

Referenced by [14], [19], [20].

[6] dcca=a

Overlap of [3] aaa=d with [4] aacca=1:

a aa aacca

Critical pair: a=dcca.

Flip LHS and RHS.

Referenced by [9].

[7] aaccd=aa

Overlap of [4] aacca=1 with [3] aaa=d:

aacc a aaa

Critical pair: aaccd=aa.

Referenced by [11].

[8] acca=aacc

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

aacc a aacca

Critical pair: aacc=acca.

Flip LHS and RHS.

Referenced by [10].

[9] dcc=1

Overlap of [6] dcca=a with [4] aacca=1:

dcc a aacca

Critical pair: dcc=aacca.

Reduce RHS:

[4]	(aacca)
	⇒ 1

Referenced by [13].

[10] bbb=caacc

Overlap of [2] bbba=c with [4] aacca=1:

bbb a aacca

Critical pair: bbb=cacca.

Reduce RHS:

[8]	c(acca)
	⇒ caacc

Defines rule #8.

Referenced by [17].

[11] accd=a

Overlap of [4] aacca=1 with [7] aaccd=aa:

aacc a aaccd

Critical pair: aaccaa=accd.

Reduce LHS:

[4]	(aacca)a
	⇒ a

Flip LHS and RHS.

Referenced by [12].

[12] ccd=1

Overlap of [4] aacca=1 with [11] accd=a:

aacc a accd

Critical pair: aacca=ccd.

Reduce LHS:

[4]	(aacca)
	⇒ 1

Flip LHS and RHS.

Defines rule #2.

Referenced by [13], [14], [16], [18], [20], [21], [22], [24].

[13] dc=cd

Overlap of [9] dcc=1 with [12] ccd=1:

dc c ccd

Critical pair: dc=cd.

Defines rule #1.

Referenced by [15], [16], [20], [21], [22], [24].

[14] ccad=a

Overlap of [12] ccd=1 with [5] da=ad:

cc d da

Critical pair: ccad=a.

Referenced by [15].

[15] ccacd=ac

Overlap of [14] ccad=a with [13] dc=cd:

cca d dc

Critical pair: ccacd=ac.

Referenced by [16].

[16] cca=acc

Overlap of [15] ccacd=ac with [13] dc=cd:

ccac d dc

Critical pair: ccaccd=acc.

Reduce LHS:

[12]	cca(ccd)
	⇒ cca

Defines rule #4.

Referenced by [23].

[17] bcaacc=caaccb

Overlap of [10] bbb=caacc with [10] bbb=caacc:

b bb bbb

Critical pair: bcaacc=caaccb.

Referenced by [18].

[18] bcaa=caaccbd

Overlap of [17] bcaacc=caaccb with [12] ccd=1:

bcaa cc ccd

Critical pair: bcaa=caaccbd.

Defines rule #7.

Referenced by [19].

[19] caaccbad=bcd

Overlap of [18] bcaa=caaccbd with [3] aaa=d:

bc aa aaa

Critical pair: bcd=caaccbda.

Reduce RHS:

[5]	caaccb(da)
	⇒ caaccbad

Flip LHS and RHS.

Referenced by [20].

[20] caabad=dbcd

Overlap of [13] dc=cd with [19] caaccbad=bcd:

d c caaccbad

Critical pair: dbcd=cdaaccbad.

Reduce RHS:

[5]	c(da)accbad
[5]	⇒ ca(da)ccbad
[13]	⇒ caa(dc)cbad
[13]	⇒ caac(dc)bad
[12]	⇒ caa(ccd)bad
	⇒ caabad

Flip LHS and RHS.

Referenced by [21].

[21] caabacd=db

Overlap of [20] caabad=dbcd with [13] dc=cd:

caaba d dc

Critical pair: caabacd=dbcdc.

Reduce RHS:

[13]	dbc(dc)
[12]	⇒ db(ccd)
	⇒ db

Referenced by [22].

[22] caaba=dbc

Overlap of [21] caabacd=db with [13] dc=cd:

caabac d dc

Critical pair: caabaccd=dbc.

Reduce LHS:

[12]	caaba(ccd)
	⇒ caaba

Referenced by [23].

[23] aaccba=cdbc

Overlap of [16] cca=acc with [22] caaba=dbc:

c ca caaba

Critical pair: cdbc=accaba.

Reduce RHS:

[16]	a(cca)ba
	⇒ aaccba

Flip LHS and RHS.

Referenced by [24].

[24] ba=acdbc

Overlap of [3] aaa=d with [23] aaccba=cdbc:

a aa aaccba

Critical pair: acdbc=dccba.

Reduce RHS:

[13]	(dc)cba
[13]	⇒ c(dc)ba
[12]	⇒ (ccd)ba
	⇒ ba

Flip LHS and RHS.

Defines rule #5.