Certificate for #20164 ⟨a, b | aab=b, bbba=baa⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [3], [4].

[2] baa=bbba

Axiom: bbba=baa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] bbbab=bb

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

b aa aab

Critical pair: bb=bbbab.

Flip LHS and RHS.

Referenced by [5].

[4] bab=bbbb

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

ba a aab

Critical pair: bab=bbbaab.

Reduce RHS:

[1]bbb(aab)
⇒ bbbb

Defines rule #2.

Referenced by [5].

[5] bbbbbb=bb

Simplify [3] bbbab=bb.

Reduce LHS:

[4]bb(bab)
⇒ bbbbbb

Defines rule #1.