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

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] babab=aba

Axiom: babab=aba.

Referenced by [3], [4].

[3] baba=abab

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

ba bab babab

Critical pair: baaba=abaab.

Reduce LHS:

[1]b(aa)ba
⇒ baba

Reduce RHS:

[1]ab(aa)b
⇒ abab

Defines rule #2.

Referenced by [4].

[4] ababb=aba

Overlap of [2] babab=aba with [3] baba=abab:

babab baba

Critical pair: ababb=aba.

Defines rule #3.