Certificate for #13270 ⟨a, b | bba=abb, bbb=aa⟩

Back:⟨a, b | bba=abb, bbb=aa⟩

Completion settings:

[1] bba=abb

Axiom: bba=abb.

Defines rule #2.

Referenced by [3].

[2] aa=bbb

Axiom: bbb=aa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[3] babb=abbb

Overlap of [2] aa=bbb with [2] aa=bbb:

a a aa

Critical pair: abbb=bbba.

Reduce RHS:

[1]b(bba)
⇒ babb

Flip LHS and RHS.

Defines rule #1.