Certificate for #13241 ⟨a, b | baa=abb, bbb=ab⟩

Back:⟨a, b | baa=abb, bbb=ab⟩

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Referenced by [3].

[2] ab=bbb

Axiom: bbb=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] baa=bbbb

Simplify [1] baa=abb.

Reduce RHS:

[2](ab)b
⇒ bbbb

Defines rule #3.

Referenced by [4].

[4] bbbbbb=bbbbb

Overlap of [3] baa=bbbb with [2] ab=bbb:

ba a ab

Critical pair: babbb=bbbbb.

Reduce LHS:

[2]b(ab)bb
⇒ bbbbbb

Defines rule #1.