Certificate for #13233 ⟨a, b | baa=abb, bab=ab⟩

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

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Defines rule #1.

Referenced by [3], [4].

[2] bab=ab

Axiom: bab=ab.

Defines rule #2.

Referenced by [3], [4].

[3] abbb=aab

Overlap of [2] bab=ab with [2] bab=ab:

ba b bab

Critical pair: baab=abab.

Reduce LHS:

[1](baa)b
⇒ abbb

Reduce RHS:

[2]a(bab)
⇒ aab

Defines rule #4.

Referenced by [4].

[4] aaab=aab

Overlap of [1] baa=abb with [3] abbb=aab:

ba a abbb

Critical pair: baaab=abbbbb.

Reduce LHS:

[1](baa)ab
[2]⇒ ab(bab)
[2]⇒ a(bab)
⇒ aab

Reduce RHS:

[3](abbb)bb
[3]⇒ a(abbb)
⇒ aaab

Flip LHS and RHS.

Defines rule #3.