Certificate for #13147 ⟨a, b | aba=aaa, abb=bb⟩

Back:⟨a, b | aba=aaa, abb=bb⟩

Completion settings:

[1] aba=aaa

Axiom: aba=aaa.

Defines rule #1.

Referenced by [3].

[2] abb=bb

Axiom: abb=bb.

Defines rule #2.

Referenced by [3].

[3] bbb=bb

Overlap of [1] aba=aaa with [2] abb=bb:

ab a abb

Critical pair: abbb=aaabb.

Reduce LHS:

[2](abb)b
⇒ bbb

Reduce RHS:

[2]aa(abb)
[2]⇒ a(abb)
[2]⇒ (abb)
⇒ bb

Defines rule #3.