Certificate for #4011 ⟨a, b, c | abc=1, abaca=1⟩

Back:⟨a, b, c | abc=1, abaca=1⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #1.

Referenced by [3].

[2] abaca=1

Axiom: abaca=1.

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

[3] abac=bc

Overlap of [2] abaca=1 with [1] abc=1:

abac a abc

Critical pair: abac=bc.

Referenced by [4], [5].

[4] bca=1

Overlap of [2] abaca=1 with [3] abac=bc:

abaca abac

Critical pair: bca=1.

Defines rule #3.

[5] bac=bcbc

Overlap of [2] abaca=1 with [3] abac=bc:

abac a abac

Critical pair: abacbc=bac.

Reduce LHS:

[3](abac)bc
⇒ bcbc

Flip LHS and RHS.

Defines rule #2.