Certificate for #7492 ⟨a, b, c | ab=1, baca=cc⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

Referenced by [3], [4].

[2] baca=cc

Axiom: baca=cc.

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

[3] aca=acc

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

a b baca

Critical pair: acc=aca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[4] ccb=bac

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

bac a ab

Critical pair: bac=ccb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [7].

[5] ccca=cccc

Overlap of [4] ccb=bac with [2] baca=cc:

cc b baca

Critical pair: cccc=bacaca.

Reduce RHS:

[2](baca)ca
⇒ ccca

Flip LHS and RHS.

Defines rule #5.

[6] bacc=cc

Overlap of [2] baca=cc with [3] aca=acc:

b aca aca

Critical pair: bacc=cc.

Defines rule #4.

Referenced by [7].

[7] bacbac=cbac

Overlap of [6] bacc=cc with [4] ccb=bac:

bac c ccb

Critical pair: bacbac=cccb.

Reduce RHS:

[4]c(ccb)
⇒ cbac

Defines rule #6.