Certificate for #3030 ⟨a, b | aa=a, babb=ab⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] babb=ab

Axiom: babb=ab.

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

[3] babab=ab

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

bab b babb

Critical pair: babab=ababb.

Reduce RHS:

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

Referenced by [4].

[4] bab=abb

Overlap of [3] babab=ab with [2] babb=ab:

ba bab babb

Critical pair: baab=abb.

Reduce LHS:

[1]b(aa)b
⇒ bab

Defines rule #2.

Referenced by [5].

[5] abbb=ab

Overlap of [2] babb=ab with [4] bab=abb:

babb bab

Critical pair: abbb=ab.

Defines rule #3.