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

Back:⟨a, b | aab=b, bbba=bb⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [3].

[2] bbba=bb

Axiom: bbba=bb.

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

[3] bbab=bbbb

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

bbb a aab

Critical pair: bbbb=bbab.

Flip LHS and RHS.

Referenced by [4].

[4] bbbbb=bbb

Overlap of [2] bbba=bb with [3] bbab=bbbb:

b bba bbab

Critical pair: bbbbb=bbb.

Referenced by [5].

[5] bbbb=bb

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

bb bbb bbba

Critical pair: bbbb=bbba.

Reduce RHS:

[2](bbba)
⇒ bb

Defines rule #3.

Referenced by [6].

[6] bba=bbb

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

b bbb bbba

Critical pair: bbb=bba.

Flip LHS and RHS.

Defines rule #1.