Certificate for #23311 ⟨a, b | aaa=1, babb=abbb⟩

Back:⟨a, b | aaa=1, babb=abbb⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

[2] babb=abbb

Axiom: babb=abbb.

Defines rule #2.

Referenced by [3].

[3] baabbbb=aabbbbb

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

bab b babb

Critical pair: bababbb=abbbabb.

Reduce LHS:

[2]ba(babb)b
⇒ baabbbb

Reduce RHS:

[2]abb(babb)
[2]⇒ ab(babb)b
[2]⇒ a(babb)bb
⇒ aabbbbb

Defines rule #3.