Certificate for #13235 ⟨a, b | baa=abb, bab=bb⟩

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

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Defines rule #1.

Referenced by [3], [4].

[2] bab=bb

Axiom: bab=bb.

Defines rule #2.

Referenced by [3], [4].

[3] abbbb=bbb

Overlap of [2] bab=bb with [1] baa=abb:

ba b baa

Critical pair: baabb=bbaa.

Reduce LHS:

[1](baa)bb
⇒ abbbb

Reduce RHS:

[1]b(baa)
[2]⇒ (bab)b
⇒ bbb

Referenced by [4], [5], [6].

[4] bbbbb=bbbb

Overlap of [1] baa=abb with [3] abbbb=bbb:

ba a abbbb

Critical pair: babbb=abbbbbb.

Reduce LHS:

[2](bab)bb
⇒ bbbb

Reduce RHS:

[3](abbbb)bb
⇒ bbbbb

Flip LHS and RHS.

Referenced by [5].

[5] bbbb=bbb

Overlap of [3] abbbb=bbb with [4] bbbbb=bbbb:

a bbbb bbbbb

Critical pair: abbbb=bbbb.

Reduce LHS:

[3](abbbb)
⇒ bbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] abbb=bbb

Overlap of [3] abbbb=bbb with [5] bbbb=bbb:

a bbbb bbbb

Critical pair: abbb=bbb.

Defines rule #3.