Certificate for #2888 ⟨a, b | aa=a, babab=a⟩

Back:⟨a, b | aa=a, babab=a⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] babab=a

Axiom: babab=a.

Referenced by [3], [4].

[3] ba=ab

Overlap of [2] babab=a with [2] babab=a:

ba bab babab

Critical pair: baa=aab.

Reduce LHS:

[1]b(aa)
⇒ ba

Reduce RHS:

[1](aa)b
⇒ ab

Defines rule #2.

Referenced by [4].

[4] abbb=a

Overlap of [2] babab=a with [3] ba=ab:

babab ba

Critical pair: abbab=a.

Reduce LHS:

[3]ab(ba)b
[3]⇒ a(ba)bb
[1]⇒ (aa)bbb
⇒ abbb

Defines rule #3.