Certificate for #1669 ⟨a, b, c | aab=ba, cac=1⟩

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

Completion settings:

[1] aab=ba

Axiom: aab=ba.

Defines rule #4.

Referenced by [5].

[2] cac=1

Axiom: cac=1.

Referenced by [3], [4].

[3] ac=ca

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

ca c cac

Critical pair: ca=ac.

Flip LHS and RHS.

Defines rule #1.

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

[4] cca=1

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

c ac ac

Critical pair: cca=1.

Defines rule #2.

Referenced by [5], [7].

[5] ccba=ab

Overlap of [4] cca=1 with [1] aab=ba:

cc a aab

Critical pair: ccba=ab.

Referenced by [6].

[6] ccbca=abc

Overlap of [5] ccba=ab with [3] ac=ca:

ccb a ac

Critical pair: ccbca=abc.

Referenced by [7].

[7] ccb=abcc

Overlap of [6] ccbca=abc with [3] ac=ca:

ccbc a ac

Critical pair: ccbcca=abcc.

Reduce LHS:

[4]ccb(cca)
⇒ ccb

Defines rule #3.