Certificate for #13186 ⟨a, b | abb=aaa, bba=aa⟩

Back:⟨a, b | abb=aaa, bba=aa⟩

Completion settings:

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] aa=bba

Axiom: bba=aa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] abb=bbbba

Overlap of [1] aaa=abb with [2] aa=bba:

aaa aa

Critical pair: bbaa=abb.

Reduce LHS:

[2]bb(aa)
⇒ bbbba

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] bbbbbba=bbbba

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

a a aa

Critical pair: abba=bbaa.

Reduce LHS:

[3](abb)a
[2]⇒ bbbb(aa)
⇒ bbbbbba

Reduce RHS:

[2]bb(aa)
⇒ bbbba

Defines rule #1.