Certificate for #3221 ⟨a, b | abaabbbaaba=1⟩

Completion settings:

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

[1] abaabbbaaba=1

Axiom: abaabbbaaba=1.

Referenced by [4].

[2] bbb=c

Axiom: bbb=c.

Defines rule #2.

Referenced by [5], [15], [16], [19], [20], [21], [22], [23], [24], [27], [32].

[3] aab=d

Axiom: aab=d.

Referenced by [4], [6], [8], [17], [18].

[4] abdbbda=1

Overlap of [1] abaabbbaaba=1 with [3] aab=d:

ab aabbbaaba aab

Critical pair: abdbbaaba=1.

Reduce LHS:

[3]	abdbb(aab)a
	⇒ abdbbda

Referenced by [6], [7], [9].

[5] cb=bc

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

b bb bbb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [23], [32].

[6] ddbbda=a

Overlap of [3] aab=d with [4] abdbbda=1:

a ab abdbbda

Critical pair: a=ddbbda.

Flip LHS and RHS.

Referenced by [8], [9].

[7] bdbbda=abdbbd

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

abdbbd a abdbbda

Critical pair: abdbbd=bdbbda.

Flip LHS and RHS.

Referenced by [19].

[8] ddbbdd=d

Overlap of [6] ddbbda=a with [3] aab=d:

ddbbd a aab

Critical pair: ddbbdd=aab.

Reduce RHS:

[3]	(aab)
	⇒ d

Referenced by [11].

[9] ddbbd=1

Overlap of [6] ddbbda=a with [4] abdbbda=1:

ddbbd a abdbbda

Critical pair: ddbbd=abdbbda.

Reduce RHS:

[4]	(abdbbda)
	⇒ 1

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

[10] ddbb=dbbd

Overlap of [9] ddbbd=1 with [9] ddbbd=1:

ddbb d ddbbd

Critical pair: ddbb=dbbd.

Referenced by [11], [12], [13], [14], [15].

[11] dbbddd=d

Simplify [8] ddbbdd=d.

Reduce LHS:

[10]	(ddbb)dd
	⇒ dbbddd

Referenced by [12].

[12] dbbdd=bbddd

Overlap of [9] ddbbd=1 with [11] dbbddd=d:

ddbb d dbbddd

Critical pair: ddbbd=bbddd.

Reduce LHS:

[10]	(ddbb)d
	⇒ dbbdd

Referenced by [13], [14].

[13] bbddd=1

Overlap of [9] ddbbd=1 with [10] ddbb=dbbd:

ddbbd ddbb

Critical pair: dbbdd=1.

Reduce LHS:

[12]	(dbbdd)
	⇒ bbddd

Defines rule #13.

Referenced by [14], [16], [17], [25], [28], [33], [34], [36].

[14] dbb=bbd

Overlap of [9] ddbbd=1 with [10] ddbb=dbbd:

ddbb d ddbb

Critical pair: ddbbdbbd=dbb.

Reduce LHS:

[10]	(ddbb)dbbd
[12]	⇒ (dbbdd)bbd
[13]	⇒ (bbddd)bbd
	⇒ bbd

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [19], [20], [21], [23], [28].

[15] bbddb=ddc

Overlap of [10] ddbb=dbbd with [2] bbb=c:

dd bb bbb

Critical pair: ddc=dbbdb.

Reduce RHS:

[14]	(dbb)db
	⇒ bbddb

Flip LHS and RHS.

Defines rule #12.

Referenced by [27], [28].

[16] cddd=b

Overlap of [2] bbb=c with [13] bbddd=1:

b bb bbddd

Critical pair: b=cddd.

Flip LHS and RHS.

Defines rule #9.

Referenced by [29], [31], [35].

[17] aa=dbddd

Overlap of [3] aab=d with [13] bbddd=1:

aa b bbddd

Critical pair: aa=dbddd.

Defines rule #18.

Referenced by [18].

[18] dbdddb=d

Overlap of [3] aab=d with [17] aa=dbddd:

aab aa

Critical pair: dbdddb=d.

Referenced by [25], [26].

[19] bdbbda=acdd

Simplify [7] bdbbda=abdbbd.

Reduce RHS:

[14]	ab(dbb)d
[2]	⇒ a(bbb)dd
	⇒ acdd

Referenced by [20].

[20] cdda=acdd

Overlap of [19] bdbbda=acdd with [14] dbb=bbd:

b dbbda dbb

Critical pair: bbbdda=acdd.

Reduce LHS:

[2]	(bbb)dda
	⇒ cdda

Defines rule #16.

Referenced by [29], [30].

[21] bbdb=dc

Overlap of [14] dbb=bbd with [2] bbb=c:

d bb bbb

Critical pair: dc=bbdb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [22], [23], [24], [32].

[22] cdb=bdc

Overlap of [2] bbb=c with [21] bbdb=dc:

b bb bbdb

Critical pair: bdc=cdb.

Flip LHS and RHS.

Defines rule #3.

[23] dbc=bcd

Overlap of [21] bbdb=dc with [14] dbb=bbd:

bb db dbb

Critical pair: bbbbd=dcb.

Reduce LHS:

[2]	(bbb)bd
[5]	⇒ (cb)d
	⇒ bcd

Reduce RHS:

[5]	d(cb)
	⇒ dbc

Flip LHS and RHS.

Defines rule #5.

Referenced by [24], [29].

[24] dcc=ccd

Overlap of [21] bbdb=dc with [23] dbc=bcd:

bb db dbc

Critical pair: bbbcd=dcc.

Reduce LHS:

[2]	(bbb)cd
	⇒ ccd

Flip LHS and RHS.

Defines rule #6.

[25] bdddb=1

Overlap of [13] bbddd=1 with [18] dbdddb=d:

bbdd d dbdddb

Critical pair: bbddd=bdddb.

Reduce LHS:

[13]	(bbddd)
	⇒ 1

Flip LHS and RHS.

Referenced by [26].

[26] dddb=bddd

Overlap of [25] bdddb=1 with [18] dbdddb=d:

bdd db dbdddb

Critical pair: bddd=dddb.

Flip LHS and RHS.

Defines rule #10.

[27] cddb=bddc

Overlap of [2] bbb=c with [15] bbddb=ddc:

b bb bbddb

Critical pair: bddc=cddb.

Flip LHS and RHS.

Defines rule #8.

[28] dddc=b

Overlap of [14] dbb=bbd with [15] bbddb=ddc:

d bb bbddb

Critical pair: dddc=bbdddb.

Reduce RHS:

[13]	(bbddd)b
	⇒ b

Defines rule #11.

Referenced by [30].

[29] dbacdd=bba

Overlap of [23] dbc=bcd with [20] cdda=acdd:

db c cdda

Critical pair: dbacdd=bcddda.

Reduce RHS:

[16]	b(cddd)a
	⇒ bba

Referenced by [31].

[30] dddacdd=bdda

Overlap of [28] dddc=b with [20] cdda=acdd:

ddd c cdda

Critical pair: dddacdd=bdda.

Referenced by [35].

[31] dbab=bbad

Overlap of [29] dbacdd=bba with [16] cddd=b:

dba cdd cddd

Critical pair: dbab=bbad.

Referenced by [32], [33].

[32] dcab=bcad

Overlap of [21] bbdb=dc with [31] dbab=bbad:

bb db dbab

Critical pair: bbbbad=dcab.

Reduce LHS:

[2]	(bbb)bad
[5]	⇒ (cb)ad
	⇒ bcad

Flip LHS and RHS.

Referenced by [34].

[33] dba=bbadbddd

Overlap of [31] dbab=bbad with [13] bbddd=1:

dba b bbddd

Critical pair: dba=bbadbddd.

Defines rule #14.

[34] dca=bcadbddd

Overlap of [32] dcab=bcad with [13] bbddd=1:

dca b bbddd

Critical pair: dca=bcadbddd.

Defines rule #15.

[35] dddab=bddad

Overlap of [30] dddacdd=bdda with [16] cddd=b:

ddda cdd cddd

Critical pair: dddab=bddad.

Referenced by [36].

[36] ddda=bddadbddd

Overlap of [35] dddab=bddad with [13] bbddd=1:

ddda b bbddd

Critical pair: ddda=bddadbddd.

Defines rule #17.