Certificate for #6906 ⟨a, b, c | ab=1, acaac=c⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

[2] acaac=c

Axiom: acaac=c.

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

[3] caac=acac

Overlap of [2] acaac=c with [2] acaac=c:

aca ac acaac

Critical pair: acac=caac.

Flip LHS and RHS.

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

[4] cac=acc

Overlap of [3] caac=acac with [2] acaac=c:

ca ac acaac

Critical pair: cac=acacaac.

Reduce RHS:

[2]ac(acaac)
⇒ acc

Defines rule #2.

Referenced by [5], [6].

[5] aaacc=c

Overlap of [2] acaac=c with [3] caac=acac:

a caac caac

Critical pair: aacac=c.

Reduce LHS:

[4]aa(cac)
⇒ aaacc

Defines rule #4.

[6] caac=aacc

Simplify [3] caac=acac.

Reduce RHS:

[4]a(cac)
⇒ aacc

Defines rule #3.