Certificate for #2578 ⟨a, b | aaa=1, abab=bb⟩

Back:⟨a, b | aaa=1, abab=bb⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [3].

[2] abab=bb

Axiom: abab=bb.

Referenced by [3], [4].

[3] bab=aabb

Overlap of [1] aaa=1 with [2] abab=bb:

aa a abab

Critical pair: aabb=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] baabb=abbb

Overlap of [2] abab=bb with [2] abab=bb:

ab ab abab

Critical pair: abbb=bbab.

Reduce RHS:

[3]b(bab)
⇒ baabb

Flip LHS and RHS.

Defines rule #3.