Certificate for #7000 ⟨a, b, c | ab=1, bacca=c⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

Referenced by [3], [4].

[2] bacca=c

Axiom: bacca=c.

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

[3] acca=ac

Overlap of [1] ab=1 with [2] bacca=c:

a b bacca

Critical pair: ac=acca.

Flip LHS and RHS.

Referenced by [6].

[4] bacc=cb

Overlap of [2] bacca=c with [1] ab=1:

bacc a ab

Critical pair: bacc=cb.

Referenced by [5], [6], [8].

[5] cba=c

Overlap of [2] bacca=c with [4] bacc=cb:

bacca bacc

Critical pair: cba=c.

Referenced by [6].

[6] bac=c

Overlap of [4] bacc=cb with [3] acca=ac:

b acc acca

Critical pair: bac=cba.

Reduce RHS:

[5](cba)
⇒ c

Defines rule #4.

Referenced by [7], [8].

[7] cca=c

Overlap of [2] bacca=c with [6] bac=c:

bacca bac

Critical pair: cca=c.

Defines rule #3.

[8] cb=cc

Overlap of [4] bacc=cb with [6] bac=c:

bacc bac

Critical pair: cc=cb.

Flip LHS and RHS.

Defines rule #2.