Certificate for #13126 ⟨a, b | aab=aaa, abb=ba⟩

Back:⟨a, b | aab=aaa, abb=ba⟩

Completion settings:

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[2] ba=abb

Axiom: abb=ba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3].

[3] aabbb=aabb

Overlap of [1] aaa=aab with [1] aaa=aab:

a aa aaa

Critical pair: aaab=aaba.

Reduce LHS:

[1](aaa)b
⇒ aabb

Reduce RHS:

[2]aa(ba)
[1]⇒ (aaa)bb
⇒ aabbb

Flip LHS and RHS.

Defines rule #2.