Certificate for #13209 ⟨a, b | abb=aba, baa=bb⟩

Back:⟨a, b | abb=aba, baa=bb⟩

Completion settings:

[1] abb=aba

Axiom: abb=aba.

Defines rule #1.

Referenced by [3], [4].

[2] baa=bb

Axiom: baa=bb.

Defines rule #2.

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

[3] abab=aba

Overlap of [1] abb=aba with [2] baa=bb:

ab b baa

Critical pair: abbb=abaaa.

Reduce LHS:

[1](abb)b
⇒ abab

Reduce RHS:

[2]a(baa)a
[1]⇒ (abb)a
[2]⇒ a(baa)
[1]⇒ (abb)
⇒ aba

Defines rule #3.

Referenced by [5].

[4] bbbb=bbba

Overlap of [2] baa=bb with [1] abb=aba:

ba a abb

Critical pair: baaba=bbbb.

Reduce LHS:

[2](baa)ba
⇒ bbba

Flip LHS and RHS.

Defines rule #4.

[5] bbbab=bbba

Overlap of [2] baa=bb with [3] abab=aba:

ba a abab

Critical pair: baaba=bbbab.

Reduce LHS:

[2](baa)ba
⇒ bbba

Flip LHS and RHS.

Defines rule #5.