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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [3].

[2] ba=bbbb

Axiom: bbbb=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbb=bb

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

b a aab

Critical pair: bb=bbbbab.

Reduce RHS:

[2]bbb(ba)b
bbbbbbbb

Flip LHS and RHS.

Defines rule #1.