Certificate for #3303 ⟨a, b, c | bb=ac, caca=1⟩

Back:⟨a, b, c | bb=ac, caca=1⟩

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Defines rule #1.

Referenced by [3].

[2] caca=1

Axiom: caca=1.

Defines rule #3.

Referenced by [4].

[3] bac=acb

Overlap of [1] bb=ac with [1] bb=ac:

b b bb

Critical pair: bac=acb.

Defines rule #2.

Referenced by [4].

[4] acacba=ba

Overlap of [3] bac=acb with [2] caca=1:

ba c caca

Critical pair: ba=acbaca.

Reduce RHS:

[3]ac(bac)a
⇒ acacba

Flip LHS and RHS.

Defines rule #4.