Certificate for #13202 ⟨a, b | abb=aab, bbb=aa⟩

Back:⟨a, b | abb=aab, bbb=aa⟩

Completion settings:

[1] aab=abb

Axiom: abb=aab.

Flip LHS and RHS.

Referenced by [3].

[2] aa=bbb

Axiom: bbb=aa.

Flip LHS and RHS.

Defines rule #4.

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

[3] abb=bbbb

Overlap of [1] aab=abb with [2] aa=bbb:

aab aa

Critical pair: bbbb=abb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] bbba=bbbbb

Overlap of [2] aa=bbb with [2] aa=bbb:

a a aa

Critical pair: abbb=bbba.

Reduce LHS:

[3](abb)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbbbb=bbbbb

Overlap of [2] aa=bbb with [3] abb=bbbb:

a a abb

Critical pair: abbbb=bbbbb.

Reduce LHS:

[3](abb)bb
⇒ bbbbbb

Defines rule #1.