Certificate for #8884 ⟨a, b | aa=a, abbab=bb⟩

Back:⟨a, b | aa=a, abbab=bb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abbab=bb

Axiom: abbab=bb.

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

[3] abb=bb

Overlap of [1] aa=a with [2] abbab=bb:

a a abbab

Critical pair: abb=abbab.

Reduce RHS:

[2](abbab)
⇒ bb

Defines rule #2.

Referenced by [4], [5].

[4] bbab=bb

Overlap of [2] abbab=bb with [3] abb=bb:

abbab abb

Critical pair: bbab=bb.

Defines rule #3.

[5] bbbb=bbb

Overlap of [2] abbab=bb with [3] abb=bb:

abb ab abb

Critical pair: abbbb=bbb.

Reduce LHS:

[3](abb)bb
⇒ bbbb

Defines rule #4.