Average Error: 30.1 → 0.3
Time: 12.8s
Precision: 64
$\cos x - \cos \left(x + 1\right)$
$\left(\sqrt{1 - \cos 1} \cdot \sqrt{1 - \cos 1}\right) \cdot \cos x + \sin x \cdot \sin 1$
\cos x - \cos \left(x + 1\right)
\left(\sqrt{1 - \cos 1} \cdot \sqrt{1 - \cos 1}\right) \cdot \cos x + \sin x \cdot \sin 1
double f(double x) {
double r1723852 = x;
double r1723853 = cos(r1723852);
double r1723854 = 1.0;
double r1723855 = r1723852 + r1723854;
double r1723856 = cos(r1723855);
double r1723857 = r1723853 - r1723856;
return r1723857;
}


double f(double x) {
double r1723858 = 1.0;
double r1723859 = 1.0;
double r1723860 = cos(r1723859);
double r1723861 = r1723858 - r1723860;
double r1723862 = sqrt(r1723861);
double r1723863 = r1723862 * r1723862;
double r1723864 = x;
double r1723865 = cos(r1723864);
double r1723866 = r1723863 * r1723865;
double r1723867 = sin(r1723864);
double r1723868 = sin(r1723859);
double r1723869 = r1723867 * r1723868;
double r1723870 = r1723866 + r1723869;
return r1723870;
}



# Try it out

Your Program's Arguments

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 30.1

$\cos x - \cos \left(x + 1\right)$
2. Using strategy rm
3. Applied cos-sum0.9

$\leadsto \cos x - \color{blue}{\left(\cos x \cdot \cos 1 - \sin x \cdot \sin 1\right)}$
4. Applied associate--r-0.9

$\leadsto \color{blue}{\left(\cos x - \cos x \cdot \cos 1\right) + \sin x \cdot \sin 1}$
5. Simplified0.9

$\leadsto \color{blue}{\left(1 - \cos 1\right) \cdot \cos x} + \sin x \cdot \sin 1$
6. Using strategy rm
7. Applied add-sqr-sqrt0.3

$\leadsto \color{blue}{\left(\sqrt{1 - \cos 1} \cdot \sqrt{1 - \cos 1}\right)} \cdot \cos x + \sin x \cdot \sin 1$
8. Final simplification0.3

$\leadsto \left(\sqrt{1 - \cos 1} \cdot \sqrt{1 - \cos 1}\right) \cdot \cos x + \sin x \cdot \sin 1$

# Reproduce

herbie shell --seed 1
(FPCore (x)
:name "cos(x)-cos(x+1)"
:precision binary64
(- (cos x) (cos (+ x 1))))