Certificate for #4508 ⟨a, b, c | abc=1, abaa=b⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #1.

Referenced by [3].

[2] abaa=b

Axiom: abaa=b.

Defines rule #3.

Referenced by [3], [4].

[3] bbc=aba

Overlap of [2] abaa=b with [1] abc=1:

aba a abc

Critical pair: aba=bbc.

Flip LHS and RHS.

Defines rule #2.

[4] bbaa=abab

Overlap of [2] abaa=b with [2] abaa=b:

aba a abaa

Critical pair: abab=bbaa.

Flip LHS and RHS.

Defines rule #4.