Certificate for #13142 ⟨a, b | aab=aaa, bbb=ba⟩

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

Completion settings:

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[2] ba=bbb

Axiom: bbb=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] aabbb=aabb

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

a aa aaa

Critical pair: aaab=aaba.

Reduce LHS:

[1](aaa)b
⇒ aabb

Reduce RHS:

[2]aa(ba)
⇒ aabbb

Flip LHS and RHS.

Defines rule #3.

[4] bbbbbbb=bbbbbb

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

b a aaa

Critical pair: baab=bbbaa.

Reduce LHS:

[2](ba)ab
[2]⇒ bb(ba)b
⇒ bbbbbb

Reduce RHS:

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

Flip LHS and RHS.

Defines rule #1.