Certificate for #13146 ⟨a, b | aba=aaa, abb=ba⟩

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

Completion settings:

[1] aaa=aba

Axiom: aba=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] ba=abb

Axiom: abb=ba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3], [4].

[3] aaa=aabb

Simplify [1] aaa=aba.

Reduce RHS:

[2]a(ba)
⇒ aabb

Defines rule #3.

Referenced by [4].

[4] aabbbbbb=aabbbb

Overlap of [3] aaa=aabb with [3] aaa=aabb:

a aa aaa

Critical pair: aaabb=aabba.

Reduce LHS:

[3](aaa)bb
⇒ aabbbb

Reduce RHS:

[2]aab(ba)
[2]⇒ aa(ba)bb
[3]⇒ (aaa)bbbb
⇒ aabbbbbb

Flip LHS and RHS.

Defines rule #2.