Certificate for #13203 ⟨a, b | abb=aab, bbb=ab⟩

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

Completion settings:

[1] aab=abb

Axiom: abb=aab.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bbb

Axiom: bbb=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] aab=bbbb

Simplify [1] aab=abb.

Reduce RHS:

[2](ab)b
⇒ bbbb

Referenced by [4].

[4] bbbbb=bbbb

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

a ab ab

Critical pair: abbb=bbbb.

Reduce LHS:

[2](ab)bb
⇒ bbbbb

Defines rule #1.