Certificate for #12553 ⟨a, b | abab=bb, bbbb=b⟩

Back:⟨a, b | abab=bb, bbbb=b⟩

Completion settings:

[1] abab=bb

Axiom: abab=bb.

Referenced by [3], [5].

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #3.

Referenced by [4], [6].

[3] bbab=abbb

Overlap of [1] abab=bb with [1] abab=bb:

ab ab abab

Critical pair: abbb=bbab.

Flip LHS and RHS.

Referenced by [4], [5].

[4] bab=abb

Overlap of [2] bbbb=b with [3] bbab=abbb:

bb bb bbab

Critical pair: bbabbb=bab.

Reduce LHS:

[3](bbab)bb
[2]⇒ a(bbbb)b
⇒ abb

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] aabbb=bbb

Overlap of [4] bab=abb with [1] abab=bb:

b ab abab

Critical pair: bbb=abbab.

Reduce RHS:

[3]a(bbab)
⇒ aabbb

Flip LHS and RHS.

Referenced by [6].

[6] aab=b

Overlap of [5] aabbb=bbb with [2] bbbb=b:

aa bbb bbbb

Critical pair: aab=bbbb.

Reduce RHS:

[2](bbbb)
⇒ b

Defines rule #1.