Certificate for #13161 ⟨a, b | aba=aab, abb=bb⟩

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

Completion settings:

[1] aba=aab

Axiom: aba=aab.

Defines rule #1.

Referenced by [3].

[2] abb=bb

Axiom: abb=bb.

Defines rule #2.

Referenced by [3].

[3] bba=bb

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

ab a aba

Critical pair: abaab=aabba.

Reduce LHS:

[1](aba)ab
[1]⇒ a(aba)b
[2]⇒ aa(abb)
[2]⇒ a(abb)
[2]⇒ (abb)
⇒ bb

Reduce RHS:

[2]a(abb)a
[2]⇒ (abb)a
⇒ bba

Flip LHS and RHS.

Defines rule #3.