Certificate for #13267 ⟨a, b | bab=baa, bba=ab⟩

Back:⟨a, b | bab=baa, bba=ab⟩

Completion settings:

[1] baa=bab

Axiom: bab=baa.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bba

Axiom: bba=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] baa=bbba

Simplify [1] baa=bab.

Reduce RHS:

[2]b(ab)
⇒ bbba

Defines rule #3.

Referenced by [4].

[4] bbbbbbba=bbbbba

Overlap of [3] baa=bbba with [2] ab=bba:

ba a ab

Critical pair: babba=bbbab.

Reduce LHS:

[2]b(ab)ba
[2]⇒ bbb(ab)a
[3]⇒ bbbb(baa)
⇒ bbbbbbba

Reduce RHS:

[2]bbb(ab)
⇒ bbbbba

Defines rule #1.