Certificate for #13206 ⟨a, b | abb=aba, baa=aa⟩

Back:⟨a, b | abb=aba, baa=aa⟩

Completion settings:

[1] abb=aba

Axiom: abb=aba.

Defines rule #1.

Referenced by [3].

[2] baa=aa

Axiom: baa=aa.

Defines rule #2.

Referenced by [3].

[3] aaaa=aaa

Overlap of [1] abb=aba with [2] baa=aa:

ab b baa

Critical pair: abaa=abaaa.

Reduce LHS:

[2]a(baa)
⇒ aaa

Reduce RHS:

[2]a(baa)a
⇒ aaaa

Flip LHS and RHS.

Defines rule #3.