Certificate for #13192 ⟨a, b | abb=aaa, bbb=ba⟩

Back:⟨a, b | abb=aaa, bbb=ba⟩

Completion settings:

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Defines rule #5.

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

[2] ba=bbb

Axiom: bbb=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aabb=abbbb

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

a aa aaa

Critical pair: aabb=abba.

Reduce RHS:

[2]ab(ba)
⇒ abbbb

Defines rule #4.

Referenced by [5].

[4] bbbbbbb=bbbbb

Overlap of [2] ba=bbb with [1] aaa=abb:

b a aaa

Critical pair: babb=bbbaa.

Reduce LHS:

[2](ba)bb
⇒ bbbbb

Reduce RHS:

[2]bb(ba)a
[2]⇒ bbbb(ba)
⇒ bbbbbbb

Flip LHS and RHS.

Defines rule #1.

[5] abbbbbb=abbbb

Overlap of [1] aaa=abb with [3] aabb=abbbb:

a aa aabb

Critical pair: aabbbb=abbbb.

Reduce LHS:

[3](aabb)bb
⇒ abbbbbb

Defines rule #2.