Certificate for #13213 ⟨a, b | abb=aba, bab=bb⟩

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

Completion settings:

[1] abb=aba

Axiom: abb=aba.

Defines rule #1.

Referenced by [3], [4].

[2] bab=bb

Axiom: bab=bb.

Defines rule #2.

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

[3] bbb=bba

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

b ab abb

Critical pair: baba=bbb.

Reduce LHS:

[2](bab)a
⇒ bba

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] abaa=aba

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

a bb bbb

Critical pair: abba=abab.

Reduce LHS:

[1](abb)a
⇒ abaa

Reduce RHS:

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

Defines rule #4.

[5] bbaa=bba

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

ba b bbb

Critical pair: babba=bbbb.

Reduce LHS:

[2](bab)ba
[3]⇒ (bbb)a
⇒ bbaa

Reduce RHS:

[3](bbb)b
[2]⇒ b(bab)
[3]⇒ (bbb)
⇒ bba

Defines rule #5.