Certificate for #13272 ⟨a, b | bba=abb, bbb=bb⟩

Completion settings:

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

[1] bba=abb

Axiom: bba=abb.

Referenced by [4].

[2] bbb=bb

Axiom: bbb=bb.

Defines rule #7.

Referenced by [6], [7].

[3] abb=c

Axiom: abb=c.

Defines rule #5.

Referenced by [4], [5], [7].

[4] bba=c

Simplify [1] bba=abb.

Reduce RHS:

[3]	(abb)
	⇒ c

Defines rule #6.

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

[5] ac=ca

Overlap of [3] abb=c with [4] bba=c:

a bb bba

Critical pair: ac=ca.

Referenced by [9].

[6] bc=c

Overlap of [2] bbb=bb with [4] bba=c:

b bb bba

Critical pair: bc=bba.

Reduce RHS:

[4]	(bba)
	⇒ c

Defines rule #4.

[7] cb=c

Overlap of [3] abb=c with [2] bbb=bb:

a bb bbb

Critical pair: abb=cb.

Reduce LHS:

[3]	(abb)
	⇒ c

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[8] ca=cc

Overlap of [7] cb=c with [4] bba=c:

c b bba

Critical pair: cc=cba.

Reduce RHS:

[7]	(cb)a
	⇒ ca

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

[9] ac=cc

Simplify [5] ac=ca.

Reduce RHS:

[8]	(ca)
	⇒ cc

Defines rule #3.