Certificate for #3017 ⟨a, b | aa=a, abab=ba⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [5].

[2] abab=ba

Axiom: abab=ba.

Referenced by [3], [4].

[3] aba=ba

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

a a abab

Critical pair: aba=abab.

Reduce RHS:

[2](abab)
⇒ ba

Defines rule #2.

Referenced by [4], [5].

[4] bab=ba

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

abab aba

Critical pair: bab=ba.

Defines rule #3.

Referenced by [5].

[5] bba=ba

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

b ab aba

Critical pair: bba=baa.

Reduce RHS:

[1]b(aa)
⇒ ba

Defines rule #4.