Certificate for #6017 ⟨a, b, c | ab=c, aba=ba⟩

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

Completion settings:

[1] ab=c

Axiom: ab=c.

Defines rule #1.

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

[2] ba=ca

Axiom: aba=ba.

Reduce LHS:

[1](ab)a
⇒ ca

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] aca=ca

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

a b ba

Critical pair: aca=ca.

Defines rule #4.

[4] bc=cc

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

b a ab

Critical pair: bc=cab.

Reduce RHS:

[1]c(ab)
⇒ cc

Defines rule #3.

Referenced by [5].

[5] acc=cc

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

a b bc

Critical pair: acc=cc.

Defines rule #5.