Certificate for #6073 ⟨a, b, c | ab=c, bac=cc⟩

Completion settings:

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

[1] ab=c

Axiom: ab=c.

Defines rule #10.

Referenced by [5].

[2] bac=cc

Axiom: bac=cc.

Defines rule #9.

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

[3] cac=d

Axiom: cac=d.

Defines rule #3.

Referenced by [4], [5], [6], [8], [9], [11].

[4] cad=dac

Overlap of [3] cac=d with [3] cac=d:

ca c cac

Critical pair: cad=dac.

Defines rule #2.

[5] acc=d

Overlap of [1] ab=c with [2] bac=cc:

a b bac

Critical pair: acc=cac.

Reduce RHS:

[3]	(cac)
	⇒ d

Defines rule #6.

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

[6] bad=cd

Overlap of [2] bac=cc with [3] cac=d:

ba c cac

Critical pair: bad=ccac.

Reduce RHS:

[3]	c(cac)
	⇒ cd

Referenced by [10].

[7] bd=ccc

Overlap of [2] bac=cc with [5] acc=d:

b ac acc

Critical pair: bd=ccc.

Defines rule #7.

[8] cd=dc

Overlap of [3] cac=d with [5] acc=d:

c ac acc

Critical pair: cd=dc.

Defines rule #1.

Referenced by [9], [10].

[9] adc=dac

Overlap of [5] acc=d with [3] cac=d:

ac c cac

Critical pair: acd=dac.

Reduce LHS:

[8]	a(cd)
	⇒ adc

Defines rule #5.

Referenced by [11].

[10] bad=dc

Simplify [6] bad=cd.

Reduce RHS:

[8]	(cd)
	⇒ dc

Defines rule #8.

[11] add=dad

Overlap of [9] adc=dac with [3] cac=d:

ad c cac

Critical pair: add=dacac.

Reduce RHS:

[3]	da(cac)
	⇒ dad

Defines rule #4.