Certificate for #19562 ⟨a, b | aab=b, abbba=ba⟩

Back:⟨a, b | aab=b, abbba=ba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #4.

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

[2] abbba=ba

Axiom: abbba=ba.

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

[3] aba=bbba

Overlap of [1] aab=b with [2] abbba=ba:

a ab abbba

Critical pair: aba=bbba.

Defines rule #5.

[4] abbbb=bb

Overlap of [2] abbba=ba with [1] aab=b:

abbb a aab

Critical pair: abbbb=baab.

Reduce RHS:

[1]b(aab)
⇒ bb

Referenced by [5].

[5] abb=bbbb

Overlap of [1] aab=b with [4] abbbb=bb:

a ab abbbb

Critical pair: abb=bbbb.

Defines rule #2.

Referenced by [6], [7].

[6] bbbbbb=bb

Overlap of [1] aab=b with [5] abb=bbbb:

a ab abb

Critical pair: abbbb=bb.

Reduce LHS:

[5](abb)bb
⇒ bbbbbb

Defines rule #1.

[7] bbbbba=ba

Overlap of [2] abbba=ba with [5] abb=bbbb:

abbba abb

Critical pair: bbbbba=ba.

Defines rule #3.