Certificate for #4517 ⟨a, b, c | abc=1, abba=b⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #1.

Referenced by [3].

[2] abba=b

Axiom: abba=b.

Defines rule #3.

Referenced by [3], [4].

[3] bbc=abb

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

abb a abc

Critical pair: abb=bbc.

Flip LHS and RHS.

Defines rule #2.

[4] bbba=abbb

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

abb a abba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #4.