Certificate for #4557 ⟨a, b, c | abc=1, baba=b⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #1.

Referenced by [3].

[2] baba=b

Axiom: baba=b.

Defines rule #4.

Referenced by [3], [4].

[3] bbc=bab

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

bab a abc

Critical pair: bab=bbc.

Flip LHS and RHS.

Defines rule #3.

[4] bba=bab

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

ba ba baba

Critical pair: bab=bba.

Flip LHS and RHS.

Defines rule #2.