Certificate for #6260 ⟨a, b, c | aa=1, bbcccb=1⟩

Completion settings:

Auxiliary generators:
1. d = ccc
Reduction order:
- Left-to-right shortlex with a < d < b < c

[1] aa=1

Axiom: aa=1.

Defines rule #1.

[2] bbcccb=1

Axiom: bbcccb=1.

Referenced by [4].

[3] ccc=d

Axiom: ccc=d.

Defines rule #4.

Referenced by [4], [5].

[4] bbdb=1

Overlap of [2] bbcccb=1 with [3] ccc=d:

bb cccb ccc

Critical pair: bbdb=1.

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

[5] cd=dc

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

c cc ccc

Critical pair: cd=dc.

Defines rule #3.

Referenced by [10].

[6] bbd=bdb

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

bbd b bbdb

Critical pair: bbd=bdb.

Referenced by [7], [8].

[7] bdbb=1

Overlap of [4] bbdb=1 with [6] bbd=bdb:

bbdb bbd

Critical pair: bdbb=1.

Referenced by [8], [9].

[8] bd=db

Overlap of [4] bbdb=1 with [6] bbd=bdb:

bbd b bbd

Critical pair: bbdbdb=bd.

Reduce LHS:

[6]	(bbd)bdb
[7]	⇒ (bdbb)db
	⇒ db

Flip LHS and RHS.

Defines rule #2.

Referenced by [9], [11].

[9] dbbb=1

Simplify [7] bdbb=1.

Reduce LHS:

[8]	(bd)bb
	⇒ dbbb

Defines rule #5.

Referenced by [10].

[10] dcbbb=c

Overlap of [5] cd=dc with [9] dbbb=1:

c d dbbb

Critical pair: c=dcbbb.

Flip LHS and RHS.

Referenced by [11].

[11] dbcbbb=bc

Overlap of [8] bd=db with [10] dcbbb=c:

b d dcbbb

Critical pair: bc=dbcbbb.

Flip LHS and RHS.

Referenced by [12].

[12] cbbb=bbbc

Overlap of [4] bbdb=1 with [11] dbcbbb=bc:

bb db dbcbbb

Critical pair: bbbc=cbbb.

Flip LHS and RHS.

Defines rule #6.