Certificate for #3042 ⟨a, b | aabaabbaaba=1⟩

Completion settings:

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

[1] aabaabbaaba=1

Axiom: aabaabbaaba=1.

Referenced by [4].

[2] baab=c

Axiom: baab=c.

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

[3] aaa=d

Axiom: aaa=d.

Defines rule #5.

Referenced by [5], [6], [7], [8], [12], [16], [21].

[4] aacca=1

Overlap of [1] aabaabbaaba=1 with [2] baab=c:

aa baabbaaba baab

Critical pair: aacbaaba=1.

Reduce LHS:

[2]	aac(baab)a
	⇒ aacca

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

[5] ad=da

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

a aa aaa

Critical pair: ad=da.

Defines rule #2.

Referenced by [13], [22], [25].

[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 [10], [12], [14].

[7] dacca=aa

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

aa a aacca

Critical pair: aa=dacca.

Flip LHS and RHS.

Referenced by [12].

[8] aaccd=aa

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

aacc a aaa

Critical pair: aaccd=aa.

Referenced by [13].

[9] aacc=acca

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

aacc a aacca

Critical pair: aacc=acca.

Referenced by [10], [13], [14], [15].

[10] accaa=dcc

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

dcc a aacca

Critical pair: dcc=aacca.

Reduce RHS:

[9]	(aacc)a
	⇒ accaa

Flip LHS and RHS.

Referenced by [14], [15].

[11] caab=baac

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

baa b baab

Critical pair: baac=caab.

Flip LHS and RHS.

Referenced by [20], [21].

[12] dacc=a

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

dacc a aacca

Critical pair: dacc=aaacca.

Reduce RHS:

[3]	(aaa)cca
[6]	⇒ (dcca)
	⇒ a

Referenced by [17], [23].

[13] accda=aa

Simplify [8] aaccd=aa.

Reduce LHS:

[9]	(aacc)d
[5]	⇒ acc(ad)
	⇒ accda

Referenced by [14].

[14] ccda=a

Overlap of [4] aacca=1 with [13] accda=aa:

aacc a accda

Critical pair: aaccaa=ccda.

Reduce LHS:

[9]	(aacc)aa
[10]	⇒ (accaa)a
[6]	⇒ (dcca)
	⇒ a

Flip LHS and RHS.

Referenced by [16], [17].

[15] dcc=1

Overlap of [4] aacca=1 with [9] aacc=acca:

aacca aacc

Critical pair: accaa=1.

Reduce LHS:

[10]	(accaa)
	⇒ dcc

Defines rule #3.

Referenced by [18], [19], [20], [25].

[16] ccdd=d

Overlap of [14] ccda=a with [3] aaa=d:

ccd a aaa

Critical pair: ccdd=aaa.

Reduce RHS:

[3]	(aaa)
	⇒ d

Referenced by [18].

[17] acc=cca

Overlap of [14] ccda=a with [12] dacc=a:

cc da dacc

Critical pair: cca=acc.

Flip LHS and RHS.

Defines rule #4.

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

[18] ccd=1

Overlap of [16] ccdd=d with [15] dcc=1:

ccd d dcc

Critical pair: ccd=dcc.

Reduce RHS:

[15]	(dcc)
	⇒ 1

Referenced by [19], [21].

[19] cd=dc

Overlap of [15] dcc=1 with [18] ccd=1:

dc c ccd

Critical pair: dc=cd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [22], [25].

[20] aab=dcbaac

Overlap of [15] dcc=1 with [11] caab=baac:

dc c caab

Critical pair: dcbaac=aab.

Flip LHS and RHS.

Defines rule #7.

[21] acbaac=b

Overlap of [17] acc=cca with [11] caab=baac:

ac c caab

Critical pair: acbaac=ccaaab.

Reduce RHS:

[3]	cc(aaa)b
[18]	⇒ (ccd)b
	⇒ b

Referenced by [22].

[22] acbdaac=bd

Overlap of [21] acbaac=b with [19] cd=dc:

acbaa c cd

Critical pair: acbaadc=bd.

Reduce LHS:

[5]	acba(ad)c
[5]	⇒ acb(ad)ac
	⇒ acbdaac

Referenced by [23].

[23] acbaa=bdc

Overlap of [22] acbdaac=bd with [17] acc=cca:

acbda ac acc

Critical pair: acbdacca=bdc.

Reduce LHS:

[12]	acb(dacc)a
	⇒ acbaa

Referenced by [24].

[24] bdcb=cca

Overlap of [23] acbaa=bdc with [2] baab=c:

ac baa baab

Critical pair: acc=bdcb.

Reduce LHS:

[17]	(acc)
	⇒ cca

Flip LHS and RHS.

Defines rule #8.

Referenced by [25].

[25] acb=bca

Overlap of [24] bdcb=cca with [24] bdcb=cca:

bdc b bdcb

Critical pair: bdccca=ccadcb.

Reduce LHS:

[15]	b(dcc)ca
	⇒ bca

Reduce RHS:

[5]	cc(ad)cb
[19]	⇒ c(cd)acb
[19]	⇒ (cd)cacb
[15]	⇒ (dcc)acb
	⇒ acb

Flip LHS and RHS.

Defines rule #6.