Certificate for #4159 ⟨a, b | abb=aab, baa=b⟩

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

Completion settings:

[1] aab=abb

Axiom: abb=aab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[2] baa=b

Axiom: baa=b.

Defines rule #2.

Referenced by [3], [4].

[3] babb=bb

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

b aa aab

Critical pair: babb=bb.

Referenced by [5].

[4] bab=bbb

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

ba a aab

Critical pair: baabb=bab.

Reduce LHS:

[2](baa)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] bbbb=bb

Simplify [3] babb=bb.

Reduce LHS:

[4](bab)b
⇒ bbbb

Defines rule #4.