Certificate for #1818 ⟨a, b, c | aba=ab, cac=1⟩

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

Completion settings:

[1] aba=ab

Axiom: aba=ab.

Referenced by [5].

[2] cac=1

Axiom: cac=1.

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

[3] ca=ac

Overlap of [2] cac=1 with [2] cac=1:

ca c cac

Critical pair: ca=ac.

Defines rule #2.

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

[4] acc=1

Overlap of [2] cac=1 with [3] ca=ac:

cac ca

Critical pair: acc=1.

Defines rule #3.

Referenced by [6], [7].

[5] acba=acb

Overlap of [3] ca=ac with [1] aba=ab:

c a aba

Critical pair: cab=acba.

Reduce LHS:

[3](ca)b
⇒ acb

Flip LHS and RHS.

Referenced by [6].

[6] ba=b

Overlap of [2] cac=1 with [5] acba=acb:

c ac acba

Critical pair: cacb=ba.

Reduce LHS:

[3](ca)cb
[4]⇒ (acc)b
⇒ b

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] bcc=b

Overlap of [6] ba=b with [4] acc=1:

b a acc

Critical pair: b=bcc.

Flip LHS and RHS.

Defines rule #4.