Certificate for #1615 ⟨a, b, c | aab=ab, aca=1⟩

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

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Referenced by [4], [5].

[2] aca=1

Axiom: aca=1.

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

[3] ca=ac

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

ac a aca

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #2.

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

[4] ab=b

Overlap of [2] aca=1 with [1] aab=ab:

ac a aab

Critical pair: acab=ab.

Reduce LHS:

[2](aca)b
⇒ b

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

[5] acb=b

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

c a aab

Critical pair: cab=acab.

Reduce LHS:

[3](ca)b
⇒ acb

Reduce RHS:

[2](aca)b
⇒ b

Referenced by [6].

[6] cb=b

Overlap of [3] ca=ac with [4] ab=b:

c a ab

Critical pair: cb=acb.

Reduce RHS:

[5](acb)
⇒ b

Defines rule #3.

[7] aac=1

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

a ca ca

Critical pair: aac=1.

Defines rule #4.