Certificate for #13236 ⟨a, b | baa=abb, bba=aa⟩

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

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Referenced by [3].

[2] aa=bba

Axiom: bba=aa.

Flip LHS and RHS.

Defines rule #3.

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

[3] abb=bbba

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

b aa aa

Critical pair: bbba=abb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] bbbbba=bbbba

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

a a aa

Critical pair: abba=bbaa.

Reduce LHS:

[3](abb)a
[2]⇒ bbb(aa)
⇒ bbbbba

Reduce RHS:

[2]bb(aa)
⇒ bbbba

Defines rule #1.

Referenced by [5].

[5] bbbaba=bbbba

Overlap of [2] aa=bba with [3] abb=bbba:

a a abb

Critical pair: abbba=bbabb.

Reduce LHS:

[3](abb)ba
⇒ bbbaba

Reduce RHS:

[3]bb(abb)
[4]⇒ (bbbbba)
⇒ bbbba

Defines rule #4.