Certificate for #16362 ⟨a, b | aba=aa, abbb=bb⟩

Back:⟨a, b | aba=aa, abbb=bb⟩

Completion settings:

[1] aba=aa

Axiom: aba=aa.

Defines rule #1.

Referenced by [3], [4].

[2] abbb=bb

Axiom: abbb=bb.

Referenced by [3].

[3] abb=bb

Overlap of [1] aba=aa with [2] abbb=bb:

ab a abbb

Critical pair: abbb=aabbb.

Reduce LHS:

[2](abbb)
⇒ bb

Reduce RHS:

[2]a(abbb)
⇒ abb

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] bbb=bb

Overlap of [1] aba=aa with [3] abb=bb:

ab a abb

Critical pair: abbb=aabb.

Reduce LHS:

[3](abb)b
⇒ bbb

Reduce RHS:

[3]a(abb)
[3]⇒ (abb)
⇒ bb

Defines rule #3.