Certificate for #6035 ⟨a, b, c | ab=c, aca=ba⟩

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

Completion settings:

[1] ab=c

Axiom: ab=c.

Defines rule #5.

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

[2] ba=aca

Axiom: aca=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aaca=ca

Overlap of [1] ab=c with [2] ba=aca:

a b ba

Critical pair: aaca=ca.

Defines rule #1.

[4] bc=acc

Overlap of [2] ba=aca with [1] ab=c:

b a ab

Critical pair: bc=acab.

Reduce RHS:

[1]ac(ab)
⇒ acc

Defines rule #4.

Referenced by [5].

[5] aacc=cc

Overlap of [1] ab=c with [4] bc=acc:

a b bc

Critical pair: aacc=cc.

Defines rule #2.