Certificate for #2609 ⟨a, b, c | aba=b, accb=1⟩

Completion settings:

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

[1] aba=b

Axiom: aba=b.

Referenced by [4], [5].

[2] accb=1

Axiom: accb=1.

Referenced by [6].

[3] aab=d

Axiom: aab=d.

Referenced by [4], [7].

[4] ab=da

Overlap of [3] aab=d with [1] aba=b:

a ab aba

Critical pair: ab=da.

Referenced by [5], [7].

[5] b=daa

Overlap of [1] aba=b with [4] ab=da:

aba ab

Critical pair: daa=b.

Flip LHS and RHS.

Defines rule #14.

Referenced by [6].

[6] accdaa=1

Overlap of [2] accb=1 with [5] b=daa:

acc b b

Critical pair: accdaa=1.

Referenced by [9], [10], [11], [12], [13], [14], [19].

[7] ada=d

Overlap of [3] aab=d with [4] ab=da:

a ab ab

Critical pair: ada=d.

Defines rule #1.

Referenced by [8], [10], [11], [13], [16], [17], [18], [20], [23].

[8] add=dda

Overlap of [7] ada=d with [7] ada=d:

ad a ada

Critical pair: add=dda.

Defines rule #2.

[9] accda=ccdaa

Overlap of [6] accdaa=1 with [6] accdaa=1:

accda a accdaa

Critical pair: accda=ccdaa.

Referenced by [10], [14], [19], [21], [22].

[10] ccdaad=da

Overlap of [6] accdaa=1 with [7] ada=d:

accda a ada

Critical pair: accdad=da.

Reduce LHS:

[9]	(accda)d
	⇒ ccdaad

Defines rule #13.

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

[11] dccdaa=ad

Overlap of [7] ada=d with [6] accdaa=1:

ad a accdaa

Critical pair: ad=dccdaa.

Flip LHS and RHS.

Referenced by [12].

[12] dccda=aad

Overlap of [11] dccdaa=ad with [6] accdaa=1:

dccda a accdaa

Critical pair: dccda=adccdaa.

Reduce RHS:

[11]	a(dccdaa)
	⇒ aad

Defines rule #6.

Referenced by [13], [15], [17], [20].

[13] aaad=dccd

Overlap of [12] dccda=aad with [6] accdaa=1:

dccd a accdaa

Critical pair: dccd=aadccdaa.

Reduce RHS:

[12]	aa(dccda)a
[7]	⇒ aaa(ada)
	⇒ aaad

Flip LHS and RHS.

Defines rule #4.

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

[14] daccd=aad

Overlap of [6] accdaa=1 with [13] aaad=dccd:

accda a aaad

Critical pair: accdadccd=aad.

Reduce LHS:

[9]	(accda)dccd
[10]	⇒ (ccdaad)ccd
	⇒ daccd

Referenced by [17], [21].

[15] dccaad=aadccd

Overlap of [13] aaad=dccd with [12] dccda=aad:

aaa d dccda

Critical pair: aaaaad=dccdccda.

Reduce LHS:

[13]	aa(aaad)
	⇒ aadccd

Reduce RHS:

[12]	dcc(dccda)
	⇒ dccaad

Flip LHS and RHS.

Defines rule #12.

[16] ccdad=daa

Overlap of [10] ccdaad=da with [7] ada=d:

ccda ad ada

Critical pair: ccdad=daa.

Defines rule #9.

Referenced by [17], [18].

[17] daaccd=ad

Overlap of [10] ccdaad=da with [12] dccda=aad:

ccdaa d dccda

Critical pair: ccdaaaad=daccda.

Reduce LHS:

[13]	ccda(aaad)
[16]	⇒ (ccdad)ccd
	⇒ daaccd

Reduce RHS:

[14]	(daccd)a
[7]	⇒ a(ada)
	⇒ ad

Referenced by [20], [21], [22].

[18] ccdd=daaa

Overlap of [16] ccdad=daa with [7] ada=d:

ccd ad ada

Critical pair: ccdd=daaa.

Defines rule #5.

[19] ccdaaa=1

Overlap of [6] accdaa=1 with [9] accda=ccdaa:

accdaa accda

Critical pair: ccdaaa=1.

Defines rule #10.

Referenced by [22].

[20] dccad=adccd

Overlap of [12] dccda=aad with [17] daaccd=ad:

dcc da daaccd

Critical pair: dccad=aadaccd.

Reduce RHS:

[7]	a(ada)ccd
	⇒ adccd

Defines rule #8.

[21] accaad=ccad

Overlap of [9] accda=ccdaa with [14] daccd=aad:

acc da daccd

Critical pair: accaad=ccdaaccd.

Reduce RHS:

[17]	cc(daaccd)
	⇒ ccad

Defines rule #11.

[22] accad=ccd

Overlap of [9] accda=ccdaa with [17] daaccd=ad:

acc da daaccd

Critical pair: accad=ccdaaaccd.

Reduce RHS:

[19]	(ccdaaa)ccd
	⇒ ccd

Defines rule #7.

Referenced by [23].

[23] accd=ccda

Overlap of [22] accad=ccd with [7] ada=d:

acc ad ada

Critical pair: accd=ccda.

Defines rule #3.