Certificate for #16019 ⟨a, b | aaa=ab, baab=ba⟩

Back:⟨a, b | aaa=ab, baab=ba⟩

Completion settings:

[1] ab=aaa

Axiom: aaa=ab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [2], [3].

[2] baaaa=ba

Axiom: baab=ba.

Reduce LHS:

[1]ba(ab)
⇒ baaaa

Defines rule #2.

Referenced by [3].

[3] aaaaaaa=aaaa

Overlap of [1] ab=aaa with [2] baaaa=ba:

a b baaaa

Critical pair: aba=aaaaaaa.

Reduce LHS:

[1](ab)a
⇒ aaaa

Flip LHS and RHS.

Defines rule #1.