Certificate for #333 ⟨a, b | ababbaba=1⟩

Completion settings:

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

[1] ababbaba=1

Axiom: ababbaba=1.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #5.

Referenced by [5], [6], [7], [14], [17].

[3] bab=d

Axiom: bab=d.

Referenced by [4], [9], [18].

[4] adda=1

Overlap of [1] ababbaba=1 with [3] bab=d:

a babbaba bab

Critical pair: adbaba=1.

Reduce LHS:

[3]	ad(bab)a
	⇒ adda

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

[5] ca=ac

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

a a aa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [11], [18].

[6] cdda=a

Overlap of [2] aa=c with [4] adda=1:

a a adda

Critical pair: a=cdda.

Flip LHS and RHS.

Referenced by [11].

[7] addc=a

Overlap of [4] adda=1 with [2] aa=c:

add a aa

Critical pair: addc=a.

Referenced by [10].

[8] dda=add

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

add a adda

Critical pair: add=dda.

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [14], [16], [18].

[9] bad=dab

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

ba b bab

Critical pair: bad=dab.

Referenced by [14], [15].

[10] ddc=1

Overlap of [4] adda=1 with [7] addc=a:

add a addc

Critical pair: adda=ddc.

Reduce LHS:

[4]	(adda)
	⇒ 1

Flip LHS and RHS.

Defines rule #2.

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

[11] acdd=a

Simplify [6] cdda=a.

Reduce LHS:

[8]	c(dda)
[5]	⇒ (ca)dd
	⇒ acdd

Referenced by [12].

[12] cdd=1

Overlap of [4] adda=1 with [11] acdd=a:

add a acdd

Critical pair: adda=cdd.

Reduce LHS:

[4]	(adda)
	⇒ 1

Flip LHS and RHS.

Referenced by [13].

[13] cd=dc

Overlap of [12] cdd=1 with [10] ddc=1:

cd d ddc

Critical pair: cd=dc.

Defines rule #1.

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

[14] dabda=b

Overlap of [9] bad=dab with [8] dda=add:

ba d dda

Critical pair: baadd=dabda.

Reduce LHS:

[2]	b(aa)dd
[13]	⇒ b(cd)d
[13]	⇒ bd(cd)
[10]	⇒ b(ddc)
	⇒ b

Flip LHS and RHS.

Referenced by [16], [18].

[15] ba=dabdc

Overlap of [9] bad=dab with [10] ddc=1:

ba d ddc

Critical pair: ba=dabdc.

Defines rule #6.

Referenced by [18].

[16] addbda=db

Overlap of [8] dda=add with [14] dabda=b:

d da dabda

Critical pair: db=addbda.

Flip LHS and RHS.

Referenced by [17].

[17] bda=adb

Overlap of [2] aa=c with [16] addbda=db:

a a addbda

Critical pair: adb=cddbda.

Reduce RHS:

[13]	(cd)dbda
[13]	⇒ d(cd)bda
[10]	⇒ (ddc)bda
	⇒ bda

Flip LHS and RHS.

Defines rule #7.

Referenced by [18].

[18] bdcb=add

Overlap of [3] bab=d with [17] bda=adb:

ba b bda

Critical pair: baadb=dda.

Reduce LHS:

[15]	(ba)adb
[5]	⇒ dabd(ca)db
[14]	⇒ (dabda)cdb
[13]	⇒ b(cd)b
	⇒ bdcb

Reduce RHS:

[8]	(dda)
	⇒ add

Defines rule #8.