Certificate for #16335 ⟨a, b | aab=bb, bbbb=ba

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

Referenced by [3].

[2] ba=bbbb

Axiom: bbbb=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbb=bbb

Overlap of [2] ba=bbbb with [1] aab=bb:

b a aab

Critical pair: bbb=bbbbab.

Reduce RHS:

[2]bbb(ba)b
bbbbbbbb

Flip LHS and RHS.

Defines rule #1.