Certificate for #16435 ⟨a, b | aba=ab, bbbb=ba⟩

Back:⟨a, b | aba=ab, bbbb=ba⟩

Completion settings:

[1] aba=ab

Axiom: aba=ab.

Referenced by [3].

[2] ba=bbbb

Axiom: bbbb=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] abbbb=ab

Overlap of [1] aba=ab with [2] ba=bbbb:

a ba ba

Critical pair: abbbb=ab.

Defines rule #2.

Referenced by [4].

[4] bbbbbbbb=bbbbb

Overlap of [2] ba=bbbb with [3] abbbb=ab:

b a abbbb

Critical pair: bab=bbbbbbbb.

Reduce LHS:

[2](ba)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #1.