Certificate for #25218 ⟨a, b | aa=a, abbbb=bba⟩

Back:⟨a, b | aa=a, abbbb=bba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #3.

Referenced by [3].

[2] bba=abbbb

Axiom: abbbb=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] abbbbbbbb=abbbb

Overlap of [2] bba=abbbb with [1] aa=a:

bb a aa

Critical pair: bba=abbbba.

Reduce LHS:

[2](bba)
⇒ abbbb

Reduce RHS:

[2]abb(bba)
[2]⇒ a(bba)bbbb
[1]⇒ (aa)bbbbbbbb
⇒ abbbbbbbb

Flip LHS and RHS.

Defines rule #1.