Certificate for #4678 ⟨a, b | aaab=b, aabb=b⟩

Back:⟨a, b | aaab=b, aabb=b⟩

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Referenced by [3].

[2] aabb=b

Axiom: aabb=b.

Referenced by [3], [4].

[3] ab=bb

Overlap of [1] aaab=b with [2] aabb=b:

a aab aabb

Critical pair: ab=bb.

Defines rule #1.

Referenced by [4].

[4] bbbb=b

Overlap of [2] aabb=b with [3] ab=bb:

a abb ab

Critical pair: abbb=b.

Reduce LHS:

[3](ab)bb
⇒ bbbb

Defines rule #2.