Certificate for #3475 ⟨a, b, c | ba=ac, cbb=b⟩

Completion settings:

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

[1] ac=ba

Axiom: ba=ac.

Flip LHS and RHS.

Defines rule #6.

Referenced by [4].

[2] cbb=b

Axiom: cbb=b.

Defines rule #8.

Referenced by [4], [5].

[3] ab=d

Axiom: ab=d.

Defines rule #5.

Referenced by [4], [6].

[4] bdb=d

Overlap of [1] ac=ba with [2] cbb=b:

a c cbb

Critical pair: ab=babb.

Reduce LHS:

[3]	(ab)
	⇒ d

Reduce RHS:

[3]	b(ab)b
	⇒ bdb

Flip LHS and RHS.

Defines rule #4.

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

[5] cbd=d

Overlap of [2] cbb=b with [4] bdb=d:

cb b bdb

Critical pair: cbd=bdb.

Reduce RHS:

[4]	(bdb)
	⇒ d

Defines rule #7.

Referenced by [8].

[6] ad=ddb

Overlap of [3] ab=d with [4] bdb=d:

a b bdb

Critical pair: ad=ddb.

Referenced by [9].

[7] ddb=bdd

Overlap of [4] bdb=d with [4] bdb=d:

bd b bdb

Critical pair: bdd=ddb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

[8] cd=db

Overlap of [5] cbd=d with [4] bdb=d:

c bd bdb

Critical pair: cd=db.

Defines rule #3.

[9] ad=bdd

Simplify [6] ad=ddb.

Reduce RHS:

[7]	(ddb)
	⇒ bdd

Defines rule #2.