Certificate for #7580 ⟨a, b, c | ab=1, caac=ca⟩

Completion settings:

• Auxiliary generators:
  1. d = caa
• Reduction order:
  • Left-to-right recursive path with deg(b) = deg(d) = 0, b < d; deg(a) = deg(c) = 1, a < c

Axiom: ab=1.

Defines rule #2.

Referenced by [6], [8].

Axiom: caac=ca.

Referenced by [4].

Axiom: caa=d.

Referenced by [4], [5].

Overlap of [2] caac=ca with [3] caa=d:

Critical pair: dc=ca.

Flip LHS and RHS.

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

Overlap of [3] caa=d with [4] ca=dc:

Critical pair: dca=d.

Reduce LHS:

Referenced by [7], [9], [11].

Overlap of [4] ca=dc with [1] ab=1:

Critical pair: c=dcb.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [5] ddc=d with [4] ca=dc:

Critical pair: dddc=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

Overlap of [7] da=dd with [1] ab=1:

Critical pair: d=ddb.

Flip LHS and RHS.

Defines rule #1.

Overlap of [5] ddc=d with [6] dcb=c:

Critical pair: dc=db.

Referenced by [10], [11], [12].

Overlap of [6] dcb=c with [9] dc=db:

Critical pair: dbb=c.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12].

Overlap of [9] dc=db with [4] ca=dc:

Critical pair: ddc=dba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Overlap of [4] ca=dc with [10] c=dbb:

Critical pair: dbba=dc.

Reduce RHS:

Defines rule #5.