Certificate for #24718 ⟨a, b | aa=a, bbabbb=ab⟩

Back:⟨a, b | aa=a, bbabbb=ab⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] bbabbb=ab

Axiom: bbabbb=ab.

Referenced by [3], [4], [5].

[3] bbabbab=ab

Overlap of [2] bbabbb=ab with [2] bbabbb=ab:

bbabb b bbabbb

Critical pair: bbabbab=abbabbb.

Reduce RHS:

[2]a(bbabbb)
[1]⇒ (aa)b
⇒ ab

Referenced by [4].

[4] bbab=abbb

Overlap of [3] bbabbab=ab with [2] bbabbb=ab:

bba bbab bbabbb

Critical pair: bbaab=abbb.

Reduce LHS:

[1]bb(aa)b
⇒ bbab

Defines rule #2.

Referenced by [5].

[5] abbbbb=ab

Overlap of [2] bbabbb=ab with [4] bbab=abbb:

bbabbb bbab

Critical pair: abbbbb=ab.

Defines rule #3.