Certificate for #16332 ⟨a, b | aab=bb, bbba=bb

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

Referenced by [3], [4].

[2] bbba=bb

Axiom: bbba=bb.

Referenced by [3], [4], [5], [6].

[3] bbab=bbbbb

Overlap of [2] bbba=bb with [1] aab=bb:

bbb a aab

Critical pair: bbbbb=bbab.

Flip LHS and RHS.

Referenced by [4].

[4] bbbbbb=bbb

Overlap of [1] aab=bb with [3] bbab=bbbbb:

aa b bbab

Critical pair: aabbbbb=bbbab.

Reduce LHS:

[1](aab)bbbb
bbbbbb

Reduce RHS:

[2](bbba)b
bbb

Referenced by [5].

[5] bbbbb=bb

Overlap of [4] bbbbbb=bbb with [2] bbba=bb:

bbb bbb bbba

Critical pair: bbbbb=bbba.

Reduce RHS:

[2](bbba)
bb

Defines rule #1.

Referenced by [6].

[6] bba=bbbb

Overlap of [5] bbbbb=bb with [2] bbba=bb:

bb bbb bbba

Critical pair: bbbb=bba.

Flip LHS and RHS.

Defines rule #2.