Certificate for #23327 ⟨a, b | aaa=1, bbbb=abbb⟩

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

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [3].

[2] abbb=bbbb

Axiom: bbbb=abbb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbb=bbb

Overlap of [1] aaa=1 with [2] abbb=bbbb:

aa a abbb

Critical pair: aabbbb=bbb.

Reduce LHS:

[2]a(abbb)b
[2]⇒ (abbb)bb
⇒ bbbbbb

Defines rule #3.