Certificate for #13243 ⟨a, b | baa=abb, bbb=bb⟩

Completion settings:

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

[1] baa=abb

Axiom: baa=abb.

Referenced by [4].

[2] bbb=bb

Axiom: bbb=bb.

Referenced by [5].

[3] bb=c

Axiom: bb=c.

Defines rule #4.

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

[4] baa=ac

Simplify [1] baa=abb.

Reduce RHS:

[3]	a(bb)
	⇒ ac

Defines rule #7.

Referenced by [9], [10].

[5] bbb=c

Simplify [2] bbb=bb.

Reduce RHS:

[3]	(bb)
	⇒ c

Referenced by [6].

[6] cb=c

Overlap of [5] bbb=c with [3] bb=c:

bbb bb

Critical pair: cb=c.

Defines rule #2.

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

[7] bc=c

Overlap of [3] bb=c with [3] bb=c:

b b bb

Critical pair: bc=cb.

Reduce RHS:

[6]	(cb)
	⇒ c

Defines rule #3.

[8] cc=c

Overlap of [6] cb=c with [3] bb=c:

c b bb

Critical pair: cc=cb.

Reduce RHS:

[6]	(cb)
	⇒ c

Defines rule #1.

[9] bac=caa

Overlap of [3] bb=c with [4] baa=ac:

b b baa

Critical pair: bac=caa.

Referenced by [11].

[10] caa=cac

Overlap of [6] cb=c with [4] baa=ac:

c b baa

Critical pair: cac=caa.

Flip LHS and RHS.

Defines rule #5.

Referenced by [11].

[11] bac=cac

Simplify [9] bac=caa.

Reduce RHS:

[10]	(caa)
	⇒ cac

Defines rule #6.