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

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

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Defines rule #1.

Referenced by [3].

[2] bab=b

Axiom: bab=b.

Defines rule #2.

Referenced by [3], [4].

[3] abbbb=abb

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

ba b baa

Critical pair: baabb=baa.

Reduce LHS:

[1](baa)bb
⇒ abbbb

Reduce RHS:

[1](baa)
⇒ abb

Referenced by [4].

[4] bbbb=bb

Overlap of [2] bab=b with [3] abbbb=abb:

b ab abbbb

Critical pair: babb=bbbb.

Reduce LHS:

[2](bab)b
⇒ bb

Flip LHS and RHS.

Defines rule #3.