Certificate for #16455 ⟨a, b | aba=bb, abab=bb⟩

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

Completion settings:

[1] aba=bb

Axiom: aba=bb.

Defines rule #1.

Referenced by [2], [3], [5].

[2] bbb=bb

Axiom: abab=bb.

Reduce LHS:

[1](aba)b
⇒ bbb

Defines rule #3.

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

[3] bba=abb

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

ab a aba

Critical pair: abbb=bbba.

Reduce LHS:

[2]a(bbb)
⇒ abb

Reduce RHS:

[2](bbb)a
⇒ bba

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] babb=abb

Overlap of [2] bbb=bb with [3] bba=abb:

b bb bba

Critical pair: babb=bba.

Reduce RHS:

[3](bba)
⇒ abb

Defines rule #5.

[5] aabb=bb

Overlap of [3] bba=abb with [1] aba=bb:

bb a aba

Critical pair: bbbb=abbba.

Reduce LHS:

[2](bbb)b
[2]⇒ (bbb)
⇒ bb

Reduce RHS:

[2]a(bbb)a
[3]⇒ a(bba)
⇒ aabb

Flip LHS and RHS.

Defines rule #4.