Certificate for #7601 ⟨a, b, c | ab=1, cbac=ba⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

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

[2] cbac=ba

Axiom: cbac=ba.

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

[3] cba=bac

Overlap of [2] cbac=ba with [2] cbac=ba:

cba c cbac

Critical pair: cbaba=babac.

Reduce LHS:

[1]cb(ab)a
⇒ cba

Reduce RHS:

[1]b(ab)ac
⇒ bac

Defines rule #3.

Referenced by [4], [5].

[4] bacc=ba

Overlap of [2] cbac=ba with [3] cba=bac:

cbac cba

Critical pair: bacc=ba.

Referenced by [7].

[5] bacb=cb

Overlap of [3] cba=bac with [1] ab=1:

cb a ab

Critical pair: cb=bacb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [6].

[6] ccb=b

Overlap of [2] cbac=ba with [5] bacb=cb:

c bac bacb

Critical pair: ccb=bab.

Reduce RHS:

[1]b(ab)
⇒ b

Defines rule #4.

[7] acc=a

Overlap of [1] ab=1 with [4] bacc=ba:

a b bacc

Critical pair: aba=acc.

Reduce LHS:

[1](ab)a
⇒ a

Flip LHS and RHS.

Defines rule #2.