Certificate for #13217 ⟨a, b | abb=aba, bba=bb⟩

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

Completion settings:

[1] aba=abb

Axiom: abb=aba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bba=bb

Axiom: bba=bb.

Defines rule #1.

Referenced by [3].

[3] bbbb=bbb

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

bb a aba

Critical pair: bbabb=bbba.

Reduce LHS:

[2](bba)bb
⇒ bbbb

Reduce RHS:

[2]b(bba)
⇒ bbb

Defines rule #3.