Certificate for #2459 ⟨a, b, c | aab=b, cacc=1⟩

Back:⟨a, b, c | aab=b, cacc=1⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [6].

[2] cacc=1

Axiom: cacc=1.

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

[3] acc=cac

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

cac c cacc

Critical pair: cac=acc.

Flip LHS and RHS.

Referenced by [4].

[4] ac=ca

Overlap of [3] acc=cac with [2] cacc=1:

ac c cacc

Critical pair: ac=cacacc.

Reduce RHS:

[2]ca(cacc)
⇒ ca

Defines rule #1.

Referenced by [5].

[5] ccca=1

Overlap of [2] cacc=1 with [4] ac=ca:

c acc ac

Critical pair: ccac=1.

Reduce LHS:

[4]cc(ac)
⇒ ccca

Defines rule #3.

Referenced by [6].

[6] cccb=ab

Overlap of [5] ccca=1 with [1] aab=b:

ccc a aab

Critical pair: cccb=ab.

Defines rule #4.