Certificate for #4510 ⟨a, b, c | abc=1, abab=a⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #3.

Referenced by [3].

[2] abab=a

Axiom: abab=a.

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

[3] ac=ab

Overlap of [2] abab=a with [1] abc=1:

ab ab abc

Critical pair: ab=ac.

Flip LHS and RHS.

Defines rule #1.

[4] aba=aab

Overlap of [2] abab=a with [2] abab=a:

ab ab abab

Critical pair: aba=aab.

Defines rule #2.

Referenced by [5].

[5] aabb=a

Overlap of [2] abab=a with [4] aba=aab:

abab aba

Critical pair: aabb=a.

Defines rule #4.