Certificate for #1636 ⟨a, b | aab=ba, abb=a⟩

Back:⟨a, b | aab=ba, abb=a⟩

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] abb=a

Axiom: abb=a.

Defines rule #3.

Referenced by [3].

[3] aaaaa=aa

Overlap of [2] abb=a with [1] ba=aab:

ab b ba

Critical pair: abaab=aa.

Reduce LHS:

[1]a(ba)ab
[1]⇒ aaa(ba)b
[2]⇒ aaaa(abb)
⇒ aaaaa

Defines rule #1.