Certificate for #6753 ⟨a, b | aba=a, baab=ab

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #1.

Referenced by [3].

[2] baab=ab

Axiom: baab=ab.

Referenced by [3].

[3] baa=a

Overlap of [2] baab=ab with [1] aba=a:

ba ab aba

Critical pair: baa=aba.

Reduce RHS:

[1](aba)
a

Defines rule #2.