Certificate for #13169 ⟨a, b | aba=aab, bab=bb⟩

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

Completion settings:

[1] aab=aba

Axiom: aba=aab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bab=bb

Axiom: bab=bb.

Defines rule #1.

Referenced by [3], [4].

[3] abba=abb

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

aa b bab

Critical pair: aabb=abaab.

Reduce LHS:

[1](aab)b
[2]⇒ a(bab)
⇒ abb

Reduce RHS:

[1]ab(aab)
[2]⇒ a(bab)a
⇒ abba

Flip LHS and RHS.

Defines rule #4.

Referenced by [4].

[4] bbba=bbb

Overlap of [2] bab=bb with [3] abba=abb:

b ab abba

Critical pair: babb=bbba.

Reduce LHS:

[2](bab)b
⇒ bbb

Flip LHS and RHS.

Defines rule #3.