Certificate for #13181 ⟨a, b | abb=aaa, baa=bb⟩

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

Completion settings:

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Defines rule #5.

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

[2] baa=bb

Axiom: baa=bb.

Defines rule #4.

Referenced by [4], [5].

[3] abba=aabb

Overlap of [1] aaa=abb with [1] aaa=abb:

a aa aaa

Critical pair: aabb=abba.

Flip LHS and RHS.

Referenced by [6].

[4] bba=babb

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

b aa aaa

Critical pair: babb=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[5] bbbb=bbb

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

ba a aaa

Critical pair: baabb=bbaa.

Reduce LHS:

[2](baa)bb
⇒ bbbb

Reduce RHS:

[2]b(baa)
⇒ bbb

Defines rule #1.

[6] ababb=aabb

Simplify [3] abba=aabb.

Reduce LHS:

[4]a(bba)
⇒ ababb

Defines rule #3.