Certificate for #24704 ⟨a, b | aa=a, bababb=ab⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

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

[2] bababb=ab

Axiom: bababb=ab.

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

[3] bababab=ab

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

babab b bababb

Critical pair: bababab=abababb.

Reduce RHS:

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

Referenced by [4].

[4] bab=abb

Overlap of [3] bababab=ab with [2] bababb=ab:

ba babab bababb

Critical pair: baab=abb.

Reduce LHS:

[1]b(aa)b
⇒ bab

Defines rule #2.

Referenced by [5].

[5] abbbb=ab

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

bababb bab

Critical pair: abbabb=ab.

Reduce LHS:

[4]ab(bab)b
[4]⇒ a(bab)bb
[1]⇒ (aa)bbbb
⇒ abbbb

Defines rule #3.