Certificate for #683 ⟨a, b | aabbabbaa=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. bba=c
2. aaa=d

[1] aabbabbaa=1

Axiom: aabbabbaa=1.

Referenced by [4].

[2] bba=c

Axiom: bba=c.

Referenced by [4], [6].

[3] aaa=d

Axiom: aaa=d.

Defines rule #7.

Referenced by [5], [7], [8], [20], [25].

[4] aacca=1

Overlap of [1] aabbabbaa=1 with [2] bba=c:

aa bbabbaa bba

Critical pair: aacbbaa=1.

Reduce LHS:

[2]	aac(bba)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], [20], [21].

[6] bb=cacca

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

bb a aacca

Critical pair: bb=cacca.

Referenced by [15].

[7] dcca=a

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

a aa aacca

Critical pair: a=dcca.

Flip LHS and RHS.

Referenced by [10].

[8] aaccd=aa

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

aacc a aaa

Critical pair: aaccd=aa.

Referenced by [11].

[9] acca=aacc

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

aacc a aacca

Critical pair: aacc=acca.

Flip LHS and RHS.

Referenced by [15].

[10] dcc=1

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

dcc a aacca

Critical pair: dcc=aacca.

Reduce RHS:

[4]	(aacca)
	⇒ 1

Referenced by [13].

[11] accd=a

Overlap of [4] aacca=1 with [8] 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], [17], [19], [21], [22], [23], [25].

[13] dc=cd

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

dc c ccd

Critical pair: dc=cd.

Defines rule #1.

Referenced by [16], [17], [21], [22], [23], [25].

[14] ccad=a

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

cc d da

Critical pair: ccad=a.

Referenced by [16].

[15] bb=caacc

Simplify [6] bb=cacca.

Reduce RHS:

[9]	c(acca)
	⇒ caacc

Defines rule #6.

Referenced by [18].

[16] ccacd=ac

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

cca d dc

Critical pair: ccacd=ac.

Referenced by [17].

[17] cca=acc

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

ccac d dc

Critical pair: ccaccd=acc.

Reduce LHS:

[12]	cca(ccd)
	⇒ cca

Defines rule #4.

Referenced by [24].

[18] bcaacc=caaccb

Overlap of [15] bb=caacc with [15] bb=caacc:

b b bb

Critical pair: bcaacc=caaccb.

Referenced by [19].

[19] bcaa=caaccbd

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

bcaa cc ccd

Critical pair: bcaa=caaccbd.

Defines rule #8.

Referenced by [20].

[20] caaccbad=bcd

Overlap of [19] 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 [21].

[21] caabad=dbcd

Overlap of [13] dc=cd with [20] 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 [22].

[22] caabacd=db

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

caaba d dc

Critical pair: caabacd=dbcdc.

Reduce RHS:

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

Referenced by [23].

[23] caaba=dbc

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

caabac d dc

Critical pair: caabaccd=dbc.

Reduce LHS:

[12]	caaba(ccd)
	⇒ caaba

Referenced by [24].

[24] aaccba=cdbc

Overlap of [17] cca=acc with [23] caaba=dbc:

c ca caaba

Critical pair: cdbc=accaba.

Reduce RHS:

[17]	a(cca)ba
	⇒ aaccba

Flip LHS and RHS.

Referenced by [25].

[25] ba=acdbc

Overlap of [3] aaa=d with [24] 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.