Certificate for #7831 ⟨a, b, c | ab=1, cac=aca⟩

Completion settings:

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

[1] ab=1

Axiom: ab=1.

Defines rule #1.

Referenced by [6].

[2] cac=aca

Axiom: cac=aca.

Referenced by [4].

[3] ac=d

Axiom: ac=d.

Defines rule #2.

Referenced by [4], [5], [7], [8], [9].

[4] cac=da

Simplify [2] cac=aca.

Reduce RHS:

[3]	(ac)a
	⇒ da

Referenced by [5].

[5] da=cd

Overlap of [4] cac=da with [3] ac=d:

c ac ac

Critical pair: cd=da.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] cdb=d

Overlap of [5] da=cd with [1] ab=1:

d a ab

Critical pair: d=cdb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[7] cdc=dd

Overlap of [5] da=cd with [3] ac=d:

d a ac

Critical pair: dd=cdc.

Flip LHS and RHS.

Defines rule #6.

Referenced by [9].

[8] ddb=ad

Overlap of [3] ac=d with [6] cdb=d:

a c cdb

Critical pair: ad=ddb.

Flip LHS and RHS.

Defines rule #5.

[9] ddc=add

Overlap of [3] ac=d with [7] cdc=dd:

a c cdc

Critical pair: add=ddc.

Flip LHS and RHS.

Defines rule #7.