Certificate for #25242 ⟨a, b | aa=a, babbb=aba⟩

Back:⟨a, b | aa=a, babbb=aba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] babbb=aba

Axiom: babbb=aba.

Defines rule #2.

Referenced by [3].

[3] babbaba=aba

Overlap of [2] babbb=aba with [2] babbb=aba:

babb b babbb

Critical pair: babbaba=abaabbb.

Reduce RHS:

[1]ab(aa)bbb
[2]⇒ a(babbb)
[1]⇒ (aa)ba
⇒ aba

Defines rule #3.