Certificate for #7513 ⟨a, b, c | ab=1, bbac=cc⟩

Back:⟨a, b, c | ab=1, bbac=cc⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

Referenced by [3].

[2] bbac=cc

Axiom: bbac=cc.

Defines rule #4.

Referenced by [3], [4].

[3] acc=bac

Overlap of [1] ab=1 with [2] bbac=cc:

a b bbac

Critical pair: acc=bac.

Defines rule #3.

Referenced by [4].

[4] bcc=ccc

Overlap of [2] bbac=cc with [3] acc=bac:

bb ac acc

Critical pair: bbbac=ccc.

Reduce LHS:

[2]b(bbac)
⇒ bcc

Defines rule #2.