Certificate for #13219 ⟨a, b | abb=aba, bbb=ab⟩

Back:⟨a, b | abb=aba, bbb=ab⟩

Completion settings:

[1] aba=abb

Axiom: abb=aba.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bbb

Axiom: bbb=ab.

Flip LHS and RHS.

Defines rule #2.

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

[3] aba=bbbb

Simplify [1] aba=abb.

Reduce RHS:

[2](ab)b
⇒ bbbb

Referenced by [4].

[4] bbba=bbbb

Overlap of [3] aba=bbbb with [2] ab=bbb:

aba ab

Critical pair: bbba=bbbb.

Defines rule #3.

Referenced by [5].

[5] bbbbbb=bbbbb

Overlap of [4] bbba=bbbb with [2] ab=bbb:

bbb a ab

Critical pair: bbbbbb=bbbbb.

Defines rule #1.