Certificate for #13194 ⟨a, b | abb=aab, baa=aa⟩

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

Completion settings:

[1] abb=aab

Axiom: abb=aab.

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=aab with [2] baa=aa:

ab b baa

Critical pair: abaa=aabaa.

Reduce LHS:

[2]a(baa)
⇒ aaa

Reduce RHS:

[2]aa(baa)
⇒ aaaa

Flip LHS and RHS.

Defines rule #3.