Certificate for #1655 ⟨a, b | aab=bb, bba=b⟩

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

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

Referenced by [3], [4].

[2] bba=b

Axiom: bba=b.

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

[3] bab=bbbb

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

bb a aab

Critical pair: bbbb=bab.

Flip LHS and RHS.

Referenced by [4], [5].

[4] bbbbb=bb

Overlap of [1] aab=bb with [3] bab=bbbb:

aa b bab

Critical pair: aabbbb=bbab.

Reduce LHS:

[1](aab)bbb
⇒ bbbbb

Reduce RHS:

[2](bba)b
⇒ bb

Referenced by [5].

[5] bbbb=b

Overlap of [3] bab=bbbb with [2] bba=b:

ba b bba

Critical pair: bab=bbbbba.

Reduce LHS:

[3](bab)
⇒ bbbb

Reduce RHS:

[4](bbbbb)a
[2]⇒ (bba)
⇒ b

Defines rule #1.

Referenced by [6].

[6] ba=bbb

Overlap of [5] bbbb=b with [2] bba=b:

bb bb bba

Critical pair: bbb=ba.

Flip LHS and RHS.

Defines rule #2.