Certificate for #13220 ⟨a, b | abb=aba, bbb=ba

Completion settings:

[1] aba=abb

Axiom: abb=aba.

Flip LHS and RHS.

Referenced by [3].

[2] ba=bbb

Axiom: bbb=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] abbb=abb

Overlap of [1] aba=abb with [2] ba=bbb:

a ba ba

Critical pair: abbb=abb.

Defines rule #2.

Referenced by [4].

[4] bbbbbb=bbbbb

Overlap of [2] ba=bbb with [3] abbb=abb:

b a abbb

Critical pair: babb=bbbbbb.

Reduce LHS:

[2](ba)bb
bbbbb

Flip LHS and RHS.

Defines rule #1.