Certificate for #4886 ⟨a, b | aab=ba, aaaaa=1⟩

Back:⟨a, b | aab=ba, aaaaa=1⟩

Completion settings:

[1] aab=ba

Axiom: aab=ba.

Referenced by [3].

[2] aaaaa=1

Axiom: aaaaa=1.

Defines rule #1.

Referenced by [3].

[3] ab=baaa

Overlap of [2] aaaaa=1 with [1] aab=ba:

aaaa a aab

Critical pair: aaaaba=ab.

Reduce LHS:

[1]aa(aab)a
[1]⇒ (aab)aa
⇒ baaa

Flip LHS and RHS.

Defines rule #2.