Certificate for #6688 ⟨a, b | aab=b, abba=ba⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] abba=ba

Axiom: abba=ba.

Referenced by [3], [6].

[3] aba=bba

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

a ab abba

Critical pair: aba=bba.

Defines rule #2.

Referenced by [4].

[4] abb=bbb

Overlap of [3] aba=bba with [1] aab=b:

ab a aab

Critical pair: abb=bbaab.

Reduce RHS:

[1]bb(aab)
⇒ bbb

Defines rule #1.

Referenced by [5], [6].

[5] bbbb=bb

Overlap of [1] aab=b with [4] abb=bbb:

a ab abb

Critical pair: abbb=bb.

Reduce LHS:

[4](abb)b
⇒ bbbb

Defines rule #4.

[6] bbba=ba

Overlap of [2] abba=ba with [4] abb=bbb:

abba abb

Critical pair: bbba=ba.

Defines rule #5.