Certificate for #8879 ⟨a, b | aa=a, ababb=ba⟩

Back:⟨a, b | aa=a, ababb=ba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [6].

[2] ababb=ba

Axiom: ababb=ba.

Referenced by [3], [4].

[3] aba=ba

Overlap of [1] aa=a with [2] ababb=ba:

a a ababb

Critical pair: aba=ababb.

Reduce RHS:

[2](ababb)
⇒ ba

Defines rule #2.

Referenced by [4], [5].

[4] babb=ba

Overlap of [2] ababb=ba with [3] aba=ba:

ababb aba

Critical pair: babb=ba.

Defines rule #4.

Referenced by [6].

[5] abba=bba

Overlap of [3] aba=ba with [3] aba=ba:

ab a aba

Critical pair: abba=baba.

Reduce RHS:

[3]b(aba)
⇒ bba

Defines rule #3.

Referenced by [6].

[6] bbba=ba

Overlap of [4] babb=ba with [5] abba=bba:

b abb abba

Critical pair: bbba=baa.

Reduce RHS:

[1]b(aa)
⇒ ba

Defines rule #5.