2cos (problem 3.3.5)

Percentage Accurate: 52.9% → 99.8%
Time: 18.0s
Alternatives: 9
Speedup: 1.9×

Specification

?
\[\left(\left(-10000 \leq x \land x \leq 10000\right) \land 10^{-16} \cdot \left|x\right| < \varepsilon\right) \land \varepsilon < \left|x\right|\]
\[\begin{array}{l} \\ \cos \left(x + \varepsilon\right) - \cos x \end{array} \]
(FPCore (x eps) :precision binary64 (- (cos (+ x eps)) (cos x)))
double code(double x, double eps) {
	return cos((x + eps)) - cos(x);
}
real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = cos((x + eps)) - cos(x)
end function
public static double code(double x, double eps) {
	return Math.cos((x + eps)) - Math.cos(x);
}
def code(x, eps):
	return math.cos((x + eps)) - math.cos(x)
function code(x, eps)
	return Float64(cos(Float64(x + eps)) - cos(x))
end
function tmp = code(x, eps)
	tmp = cos((x + eps)) - cos(x);
end
code[x_, eps_] := N[(N[Cos[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Cos[x], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\cos \left(x + \varepsilon\right) - \cos x
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 9 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 52.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \cos \left(x + \varepsilon\right) - \cos x \end{array} \]
(FPCore (x eps) :precision binary64 (- (cos (+ x eps)) (cos x)))
double code(double x, double eps) {
	return cos((x + eps)) - cos(x);
}
real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = cos((x + eps)) - cos(x)
end function
public static double code(double x, double eps) {
	return Math.cos((x + eps)) - Math.cos(x);
}
def code(x, eps):
	return math.cos((x + eps)) - math.cos(x)
function code(x, eps)
	return Float64(cos(Float64(x + eps)) - cos(x))
end
function tmp = code(x, eps)
	tmp = cos((x + eps)) - cos(x);
end
code[x_, eps_] := N[(N[Cos[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Cos[x], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\cos \left(x + \varepsilon\right) - \cos x
\end{array}

Alternative 1: 99.8% accurate, 0.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \sin \left(\varepsilon \cdot 0.5\right)\\ \left(t\_0 \cdot \mathsf{fma}\left(\sin x, \cos \left(\varepsilon \cdot 0.5\right), t\_0 \cdot \cos x\right)\right) \cdot -2 \end{array} \end{array} \]
(FPCore (x eps)
 :precision binary64
 (let* ((t_0 (sin (* eps 0.5))))
   (* (* t_0 (fma (sin x) (cos (* eps 0.5)) (* t_0 (cos x)))) -2.0)))
double code(double x, double eps) {
	double t_0 = sin((eps * 0.5));
	return (t_0 * fma(sin(x), cos((eps * 0.5)), (t_0 * cos(x)))) * -2.0;
}
function code(x, eps)
	t_0 = sin(Float64(eps * 0.5))
	return Float64(Float64(t_0 * fma(sin(x), cos(Float64(eps * 0.5)), Float64(t_0 * cos(x)))) * -2.0)
end
code[x_, eps_] := Block[{t$95$0 = N[Sin[N[(eps * 0.5), $MachinePrecision]], $MachinePrecision]}, N[(N[(t$95$0 * N[(N[Sin[x], $MachinePrecision] * N[Cos[N[(eps * 0.5), $MachinePrecision]], $MachinePrecision] + N[(t$95$0 * N[Cos[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * -2.0), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \sin \left(\varepsilon \cdot 0.5\right)\\
\left(t\_0 \cdot \mathsf{fma}\left(\sin x, \cos \left(\varepsilon \cdot 0.5\right), t\_0 \cdot \cos x\right)\right) \cdot -2
\end{array}
\end{array}
Derivation
  1. Initial program 54.8%

    \[\cos \left(x + \varepsilon\right) - \cos x \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right) - \cos x} \]
    2. lift-cos.f64N/A

      \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right)} - \cos x \]
    3. lift-cos.f64N/A

      \[\leadsto \cos \left(x + \varepsilon\right) - \color{blue}{\cos x} \]
    4. diff-cosN/A

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)} \]
    5. *-commutativeN/A

      \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
    6. lower-*.f64N/A

      \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
  4. Applied rewrites99.6%

    \[\leadsto \color{blue}{\left(\sin \left(\left(\varepsilon + 0\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \cdot -2} \]
  5. Taylor expanded in eps around inf

    \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + 2 \cdot x\right)\right)\right)} \cdot -2 \]
  6. Step-by-step derivation
    1. metadata-evalN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot x\right)\right)\right) \cdot -2 \]
    2. cancel-sign-sub-invN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon - -2 \cdot x\right)}\right)\right) \cdot -2 \]
    3. lower-*.f64N/A

      \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right)} \cdot -2 \]
    4. lower-sin.f64N/A

      \[\leadsto \left(\color{blue}{\sin \left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
    5. lower-*.f64N/A

      \[\leadsto \left(\sin \color{blue}{\left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
    6. lower-sin.f64N/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \color{blue}{\sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)}\right) \cdot -2 \]
    7. cancel-sign-sub-invN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon + \left(\mathsf{neg}\left(-2\right)\right) \cdot x\right)}\right)\right) \cdot -2 \]
    8. metadata-evalN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{2} \cdot x\right)\right)\right) \cdot -2 \]
    9. distribute-rgt-inN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\varepsilon \cdot \frac{1}{2} + \left(2 \cdot x\right) \cdot \frac{1}{2}\right)}\right) \cdot -2 \]
    10. *-commutativeN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{\left(x \cdot 2\right)} \cdot \frac{1}{2}\right)\right) \cdot -2 \]
    11. associate-*l*N/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x \cdot \left(2 \cdot \frac{1}{2}\right)}\right)\right) \cdot -2 \]
    12. metadata-evalN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + x \cdot \color{blue}{1}\right)\right) \cdot -2 \]
    13. *-rgt-identityN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x}\right)\right) \cdot -2 \]
    14. *-commutativeN/A

      \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\color{blue}{\frac{1}{2} \cdot \varepsilon} + x\right)\right) \cdot -2 \]
    15. lower-fma.f6499.7

      \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
  7. Applied rewrites99.7%

    \[\leadsto \color{blue}{\left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)} \cdot -2 \]
  8. Step-by-step derivation
    1. Applied rewrites99.8%

      \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \mathsf{fma}\left(\sin x, \color{blue}{\cos \left(\varepsilon \cdot 0.5\right)}, \sin \left(\varepsilon \cdot 0.5\right) \cdot \cos x\right)\right) \cdot -2 \]
    2. Final simplification99.8%

      \[\leadsto \left(\sin \left(\varepsilon \cdot 0.5\right) \cdot \mathsf{fma}\left(\sin x, \cos \left(\varepsilon \cdot 0.5\right), \sin \left(\varepsilon \cdot 0.5\right) \cdot \cos x\right)\right) \cdot -2 \]
    3. Add Preprocessing

    Alternative 2: 99.7% accurate, 0.9× speedup?

    \[\begin{array}{l} \\ -2 \cdot \left(\sin \left(\varepsilon \cdot 0.5\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right) \end{array} \]
    (FPCore (x eps)
     :precision binary64
     (* -2.0 (* (sin (* eps 0.5)) (sin (fma 0.5 eps x)))))
    double code(double x, double eps) {
    	return -2.0 * (sin((eps * 0.5)) * sin(fma(0.5, eps, x)));
    }
    
    function code(x, eps)
    	return Float64(-2.0 * Float64(sin(Float64(eps * 0.5)) * sin(fma(0.5, eps, x))))
    end
    
    code[x_, eps_] := N[(-2.0 * N[(N[Sin[N[(eps * 0.5), $MachinePrecision]], $MachinePrecision] * N[Sin[N[(0.5 * eps + x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
    
    \begin{array}{l}
    
    \\
    -2 \cdot \left(\sin \left(\varepsilon \cdot 0.5\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)
    \end{array}
    
    Derivation
    1. Initial program 54.8%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right) - \cos x} \]
      2. lift-cos.f64N/A

        \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right)} - \cos x \]
      3. lift-cos.f64N/A

        \[\leadsto \cos \left(x + \varepsilon\right) - \color{blue}{\cos x} \]
      4. diff-cosN/A

        \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)} \]
      5. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
      6. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
    4. Applied rewrites99.6%

      \[\leadsto \color{blue}{\left(\sin \left(\left(\varepsilon + 0\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \cdot -2} \]
    5. Taylor expanded in eps around inf

      \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + 2 \cdot x\right)\right)\right)} \cdot -2 \]
    6. Step-by-step derivation
      1. metadata-evalN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot x\right)\right)\right) \cdot -2 \]
      2. cancel-sign-sub-invN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon - -2 \cdot x\right)}\right)\right) \cdot -2 \]
      3. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right)} \cdot -2 \]
      4. lower-sin.f64N/A

        \[\leadsto \left(\color{blue}{\sin \left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
      5. lower-*.f64N/A

        \[\leadsto \left(\sin \color{blue}{\left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
      6. lower-sin.f64N/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \color{blue}{\sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)}\right) \cdot -2 \]
      7. cancel-sign-sub-invN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon + \left(\mathsf{neg}\left(-2\right)\right) \cdot x\right)}\right)\right) \cdot -2 \]
      8. metadata-evalN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{2} \cdot x\right)\right)\right) \cdot -2 \]
      9. distribute-rgt-inN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\varepsilon \cdot \frac{1}{2} + \left(2 \cdot x\right) \cdot \frac{1}{2}\right)}\right) \cdot -2 \]
      10. *-commutativeN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{\left(x \cdot 2\right)} \cdot \frac{1}{2}\right)\right) \cdot -2 \]
      11. associate-*l*N/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x \cdot \left(2 \cdot \frac{1}{2}\right)}\right)\right) \cdot -2 \]
      12. metadata-evalN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + x \cdot \color{blue}{1}\right)\right) \cdot -2 \]
      13. *-rgt-identityN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x}\right)\right) \cdot -2 \]
      14. *-commutativeN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\color{blue}{\frac{1}{2} \cdot \varepsilon} + x\right)\right) \cdot -2 \]
      15. lower-fma.f6499.7

        \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
    7. Applied rewrites99.7%

      \[\leadsto \color{blue}{\left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)} \cdot -2 \]
    8. Final simplification99.7%

      \[\leadsto -2 \cdot \left(\sin \left(\varepsilon \cdot 0.5\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right) \]
    9. Add Preprocessing

    Alternative 3: 99.6% accurate, 1.3× speedup?

    \[\begin{array}{l} \\ -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon \cdot \varepsilon, \mathsf{fma}\left(\varepsilon \cdot \varepsilon, -1.5500992063492063 \cdot 10^{-6}, 0.00026041666666666666\right), -0.020833333333333332\right), 0.5\right)\right)\right) \end{array} \]
    (FPCore (x eps)
     :precision binary64
     (*
      -2.0
      (*
       (sin (fma 0.5 eps x))
       (*
        eps
        (fma
         eps
         (*
          eps
          (fma
           (* eps eps)
           (fma (* eps eps) -1.5500992063492063e-6 0.00026041666666666666)
           -0.020833333333333332))
         0.5)))))
    double code(double x, double eps) {
    	return -2.0 * (sin(fma(0.5, eps, x)) * (eps * fma(eps, (eps * fma((eps * eps), fma((eps * eps), -1.5500992063492063e-6, 0.00026041666666666666), -0.020833333333333332)), 0.5)));
    }
    
    function code(x, eps)
    	return Float64(-2.0 * Float64(sin(fma(0.5, eps, x)) * Float64(eps * fma(eps, Float64(eps * fma(Float64(eps * eps), fma(Float64(eps * eps), -1.5500992063492063e-6, 0.00026041666666666666), -0.020833333333333332)), 0.5))))
    end
    
    code[x_, eps_] := N[(-2.0 * N[(N[Sin[N[(0.5 * eps + x), $MachinePrecision]], $MachinePrecision] * N[(eps * N[(eps * N[(eps * N[(N[(eps * eps), $MachinePrecision] * N[(N[(eps * eps), $MachinePrecision] * -1.5500992063492063e-6 + 0.00026041666666666666), $MachinePrecision] + -0.020833333333333332), $MachinePrecision]), $MachinePrecision] + 0.5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
    
    \begin{array}{l}
    
    \\
    -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon \cdot \varepsilon, \mathsf{fma}\left(\varepsilon \cdot \varepsilon, -1.5500992063492063 \cdot 10^{-6}, 0.00026041666666666666\right), -0.020833333333333332\right), 0.5\right)\right)\right)
    \end{array}
    
    Derivation
    1. Initial program 54.8%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right) - \cos x} \]
      2. lift-cos.f64N/A

        \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right)} - \cos x \]
      3. lift-cos.f64N/A

        \[\leadsto \cos \left(x + \varepsilon\right) - \color{blue}{\cos x} \]
      4. diff-cosN/A

        \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)} \]
      5. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
      6. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
    4. Applied rewrites99.6%

      \[\leadsto \color{blue}{\left(\sin \left(\left(\varepsilon + 0\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \cdot -2} \]
    5. Taylor expanded in eps around inf

      \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + 2 \cdot x\right)\right)\right)} \cdot -2 \]
    6. Step-by-step derivation
      1. metadata-evalN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot x\right)\right)\right) \cdot -2 \]
      2. cancel-sign-sub-invN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon - -2 \cdot x\right)}\right)\right) \cdot -2 \]
      3. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right)} \cdot -2 \]
      4. lower-sin.f64N/A

        \[\leadsto \left(\color{blue}{\sin \left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
      5. lower-*.f64N/A

        \[\leadsto \left(\sin \color{blue}{\left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
      6. lower-sin.f64N/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \color{blue}{\sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)}\right) \cdot -2 \]
      7. cancel-sign-sub-invN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon + \left(\mathsf{neg}\left(-2\right)\right) \cdot x\right)}\right)\right) \cdot -2 \]
      8. metadata-evalN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{2} \cdot x\right)\right)\right) \cdot -2 \]
      9. distribute-rgt-inN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\varepsilon \cdot \frac{1}{2} + \left(2 \cdot x\right) \cdot \frac{1}{2}\right)}\right) \cdot -2 \]
      10. *-commutativeN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{\left(x \cdot 2\right)} \cdot \frac{1}{2}\right)\right) \cdot -2 \]
      11. associate-*l*N/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x \cdot \left(2 \cdot \frac{1}{2}\right)}\right)\right) \cdot -2 \]
      12. metadata-evalN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + x \cdot \color{blue}{1}\right)\right) \cdot -2 \]
      13. *-rgt-identityN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x}\right)\right) \cdot -2 \]
      14. *-commutativeN/A

        \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\color{blue}{\frac{1}{2} \cdot \varepsilon} + x\right)\right) \cdot -2 \]
      15. lower-fma.f6499.7

        \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
    7. Applied rewrites99.7%

      \[\leadsto \color{blue}{\left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)} \cdot -2 \]
    8. Taylor expanded in eps around 0

      \[\leadsto \left(\left(\varepsilon \cdot \left(\frac{1}{2} + {\varepsilon}^{2} \cdot \left({\varepsilon}^{2} \cdot \left(\frac{1}{3840} + \frac{-1}{645120} \cdot {\varepsilon}^{2}\right) - \frac{1}{48}\right)\right)\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)}\right) \cdot -2 \]
    9. Step-by-step derivation
      1. Applied rewrites99.3%

        \[\leadsto \left(\left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon \cdot \varepsilon, \mathsf{fma}\left(\varepsilon \cdot \varepsilon, -1.5500992063492063 \cdot 10^{-6}, 0.00026041666666666666\right), -0.020833333333333332\right), 0.5\right)\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
      2. Final simplification99.3%

        \[\leadsto -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon \cdot \varepsilon, \mathsf{fma}\left(\varepsilon \cdot \varepsilon, -1.5500992063492063 \cdot 10^{-6}, 0.00026041666666666666\right), -0.020833333333333332\right), 0.5\right)\right)\right) \]
      3. Add Preprocessing

      Alternative 4: 99.5% accurate, 1.4× speedup?

      \[\begin{array}{l} \\ -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot 0.00026041666666666666, -0.020833333333333332\right), 0.5\right)\right)\right) \end{array} \]
      (FPCore (x eps)
       :precision binary64
       (*
        -2.0
        (*
         (sin (fma 0.5 eps x))
         (*
          eps
          (fma
           eps
           (* eps (fma eps (* eps 0.00026041666666666666) -0.020833333333333332))
           0.5)))))
      double code(double x, double eps) {
      	return -2.0 * (sin(fma(0.5, eps, x)) * (eps * fma(eps, (eps * fma(eps, (eps * 0.00026041666666666666), -0.020833333333333332)), 0.5)));
      }
      
      function code(x, eps)
      	return Float64(-2.0 * Float64(sin(fma(0.5, eps, x)) * Float64(eps * fma(eps, Float64(eps * fma(eps, Float64(eps * 0.00026041666666666666), -0.020833333333333332)), 0.5))))
      end
      
      code[x_, eps_] := N[(-2.0 * N[(N[Sin[N[(0.5 * eps + x), $MachinePrecision]], $MachinePrecision] * N[(eps * N[(eps * N[(eps * N[(eps * N[(eps * 0.00026041666666666666), $MachinePrecision] + -0.020833333333333332), $MachinePrecision]), $MachinePrecision] + 0.5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
      
      \begin{array}{l}
      
      \\
      -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot 0.00026041666666666666, -0.020833333333333332\right), 0.5\right)\right)\right)
      \end{array}
      
      Derivation
      1. Initial program 54.8%

        \[\cos \left(x + \varepsilon\right) - \cos x \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift--.f64N/A

          \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right) - \cos x} \]
        2. lift-cos.f64N/A

          \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right)} - \cos x \]
        3. lift-cos.f64N/A

          \[\leadsto \cos \left(x + \varepsilon\right) - \color{blue}{\cos x} \]
        4. diff-cosN/A

          \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)} \]
        5. *-commutativeN/A

          \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
        6. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
      4. Applied rewrites99.6%

        \[\leadsto \color{blue}{\left(\sin \left(\left(\varepsilon + 0\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \cdot -2} \]
      5. Taylor expanded in eps around inf

        \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + 2 \cdot x\right)\right)\right)} \cdot -2 \]
      6. Step-by-step derivation
        1. metadata-evalN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot x\right)\right)\right) \cdot -2 \]
        2. cancel-sign-sub-invN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon - -2 \cdot x\right)}\right)\right) \cdot -2 \]
        3. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right)} \cdot -2 \]
        4. lower-sin.f64N/A

          \[\leadsto \left(\color{blue}{\sin \left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
        5. lower-*.f64N/A

          \[\leadsto \left(\sin \color{blue}{\left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
        6. lower-sin.f64N/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \color{blue}{\sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)}\right) \cdot -2 \]
        7. cancel-sign-sub-invN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon + \left(\mathsf{neg}\left(-2\right)\right) \cdot x\right)}\right)\right) \cdot -2 \]
        8. metadata-evalN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{2} \cdot x\right)\right)\right) \cdot -2 \]
        9. distribute-rgt-inN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\varepsilon \cdot \frac{1}{2} + \left(2 \cdot x\right) \cdot \frac{1}{2}\right)}\right) \cdot -2 \]
        10. *-commutativeN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{\left(x \cdot 2\right)} \cdot \frac{1}{2}\right)\right) \cdot -2 \]
        11. associate-*l*N/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x \cdot \left(2 \cdot \frac{1}{2}\right)}\right)\right) \cdot -2 \]
        12. metadata-evalN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + x \cdot \color{blue}{1}\right)\right) \cdot -2 \]
        13. *-rgt-identityN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x}\right)\right) \cdot -2 \]
        14. *-commutativeN/A

          \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\color{blue}{\frac{1}{2} \cdot \varepsilon} + x\right)\right) \cdot -2 \]
        15. lower-fma.f6499.7

          \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
      7. Applied rewrites99.7%

        \[\leadsto \color{blue}{\left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)} \cdot -2 \]
      8. Taylor expanded in eps around 0

        \[\leadsto \left(\left(\varepsilon \cdot \left(\frac{1}{2} + {\varepsilon}^{2} \cdot \left(\frac{1}{3840} \cdot {\varepsilon}^{2} - \frac{1}{48}\right)\right)\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)}\right) \cdot -2 \]
      9. Step-by-step derivation
        1. Applied rewrites99.2%

          \[\leadsto \left(\left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot 0.00026041666666666666, -0.020833333333333332\right), 0.5\right)\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
        2. Final simplification99.2%

          \[\leadsto -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot \mathsf{fma}\left(\varepsilon, \varepsilon \cdot 0.00026041666666666666, -0.020833333333333332\right), 0.5\right)\right)\right) \]
        3. Add Preprocessing

        Alternative 5: 99.5% accurate, 1.6× speedup?

        \[\begin{array}{l} \\ -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(-0.020833333333333332, \varepsilon \cdot \varepsilon, 0.5\right)\right)\right) \end{array} \]
        (FPCore (x eps)
         :precision binary64
         (*
          -2.0
          (*
           (sin (fma 0.5 eps x))
           (* eps (fma -0.020833333333333332 (* eps eps) 0.5)))))
        double code(double x, double eps) {
        	return -2.0 * (sin(fma(0.5, eps, x)) * (eps * fma(-0.020833333333333332, (eps * eps), 0.5)));
        }
        
        function code(x, eps)
        	return Float64(-2.0 * Float64(sin(fma(0.5, eps, x)) * Float64(eps * fma(-0.020833333333333332, Float64(eps * eps), 0.5))))
        end
        
        code[x_, eps_] := N[(-2.0 * N[(N[Sin[N[(0.5 * eps + x), $MachinePrecision]], $MachinePrecision] * N[(eps * N[(-0.020833333333333332 * N[(eps * eps), $MachinePrecision] + 0.5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        
        \\
        -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(-0.020833333333333332, \varepsilon \cdot \varepsilon, 0.5\right)\right)\right)
        \end{array}
        
        Derivation
        1. Initial program 54.8%

          \[\cos \left(x + \varepsilon\right) - \cos x \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift--.f64N/A

            \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right) - \cos x} \]
          2. lift-cos.f64N/A

            \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right)} - \cos x \]
          3. lift-cos.f64N/A

            \[\leadsto \cos \left(x + \varepsilon\right) - \color{blue}{\cos x} \]
          4. diff-cosN/A

            \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)} \]
          5. *-commutativeN/A

            \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
          6. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
        4. Applied rewrites99.6%

          \[\leadsto \color{blue}{\left(\sin \left(\left(\varepsilon + 0\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \cdot -2} \]
        5. Taylor expanded in eps around inf

          \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + 2 \cdot x\right)\right)\right)} \cdot -2 \]
        6. Step-by-step derivation
          1. metadata-evalN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot x\right)\right)\right) \cdot -2 \]
          2. cancel-sign-sub-invN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon - -2 \cdot x\right)}\right)\right) \cdot -2 \]
          3. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right)} \cdot -2 \]
          4. lower-sin.f64N/A

            \[\leadsto \left(\color{blue}{\sin \left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
          5. lower-*.f64N/A

            \[\leadsto \left(\sin \color{blue}{\left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
          6. lower-sin.f64N/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \color{blue}{\sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)}\right) \cdot -2 \]
          7. cancel-sign-sub-invN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon + \left(\mathsf{neg}\left(-2\right)\right) \cdot x\right)}\right)\right) \cdot -2 \]
          8. metadata-evalN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{2} \cdot x\right)\right)\right) \cdot -2 \]
          9. distribute-rgt-inN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\varepsilon \cdot \frac{1}{2} + \left(2 \cdot x\right) \cdot \frac{1}{2}\right)}\right) \cdot -2 \]
          10. *-commutativeN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{\left(x \cdot 2\right)} \cdot \frac{1}{2}\right)\right) \cdot -2 \]
          11. associate-*l*N/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x \cdot \left(2 \cdot \frac{1}{2}\right)}\right)\right) \cdot -2 \]
          12. metadata-evalN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + x \cdot \color{blue}{1}\right)\right) \cdot -2 \]
          13. *-rgt-identityN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x}\right)\right) \cdot -2 \]
          14. *-commutativeN/A

            \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\color{blue}{\frac{1}{2} \cdot \varepsilon} + x\right)\right) \cdot -2 \]
          15. lower-fma.f6499.7

            \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
        7. Applied rewrites99.7%

          \[\leadsto \color{blue}{\left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)} \cdot -2 \]
        8. Taylor expanded in eps around 0

          \[\leadsto \left(\left(\varepsilon \cdot \left(\frac{1}{2} + \frac{-1}{48} \cdot {\varepsilon}^{2}\right)\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)}\right) \cdot -2 \]
        9. Step-by-step derivation
          1. Applied rewrites99.1%

            \[\leadsto \left(\left(\varepsilon \cdot \mathsf{fma}\left(-0.020833333333333332, \varepsilon \cdot \varepsilon, 0.5\right)\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
          2. Final simplification99.1%

            \[\leadsto -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot \mathsf{fma}\left(-0.020833333333333332, \varepsilon \cdot \varepsilon, 0.5\right)\right)\right) \]
          3. Add Preprocessing

          Alternative 6: 99.2% accurate, 1.7× speedup?

          \[\begin{array}{l} \\ -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot 0.5\right)\right) \end{array} \]
          (FPCore (x eps)
           :precision binary64
           (* -2.0 (* (sin (fma 0.5 eps x)) (* eps 0.5))))
          double code(double x, double eps) {
          	return -2.0 * (sin(fma(0.5, eps, x)) * (eps * 0.5));
          }
          
          function code(x, eps)
          	return Float64(-2.0 * Float64(sin(fma(0.5, eps, x)) * Float64(eps * 0.5)))
          end
          
          code[x_, eps_] := N[(-2.0 * N[(N[Sin[N[(0.5 * eps + x), $MachinePrecision]], $MachinePrecision] * N[(eps * 0.5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot 0.5\right)\right)
          \end{array}
          
          Derivation
          1. Initial program 54.8%

            \[\cos \left(x + \varepsilon\right) - \cos x \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift--.f64N/A

              \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right) - \cos x} \]
            2. lift-cos.f64N/A

              \[\leadsto \color{blue}{\cos \left(x + \varepsilon\right)} - \cos x \]
            3. lift-cos.f64N/A

              \[\leadsto \cos \left(x + \varepsilon\right) - \color{blue}{\cos x} \]
            4. diff-cosN/A

              \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right)} \]
            5. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
            6. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\sin \left(\frac{\left(x + \varepsilon\right) - x}{2}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \cdot -2} \]
          4. Applied rewrites99.6%

            \[\leadsto \color{blue}{\left(\sin \left(\left(\varepsilon + 0\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \cdot -2} \]
          5. Taylor expanded in eps around inf

            \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + 2 \cdot x\right)\right)\right)} \cdot -2 \]
          6. Step-by-step derivation
            1. metadata-evalN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \cdot x\right)\right)\right) \cdot -2 \]
            2. cancel-sign-sub-invN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon - -2 \cdot x\right)}\right)\right) \cdot -2 \]
            3. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right)} \cdot -2 \]
            4. lower-sin.f64N/A

              \[\leadsto \left(\color{blue}{\sin \left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
            5. lower-*.f64N/A

              \[\leadsto \left(\sin \color{blue}{\left(\frac{1}{2} \cdot \varepsilon\right)} \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)\right) \cdot -2 \]
            6. lower-sin.f64N/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \color{blue}{\sin \left(\frac{1}{2} \cdot \left(\varepsilon - -2 \cdot x\right)\right)}\right) \cdot -2 \]
            7. cancel-sign-sub-invN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\left(\varepsilon + \left(\mathsf{neg}\left(-2\right)\right) \cdot x\right)}\right)\right) \cdot -2 \]
            8. metadata-evalN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\frac{1}{2} \cdot \left(\varepsilon + \color{blue}{2} \cdot x\right)\right)\right) \cdot -2 \]
            9. distribute-rgt-inN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\varepsilon \cdot \frac{1}{2} + \left(2 \cdot x\right) \cdot \frac{1}{2}\right)}\right) \cdot -2 \]
            10. *-commutativeN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{\left(x \cdot 2\right)} \cdot \frac{1}{2}\right)\right) \cdot -2 \]
            11. associate-*l*N/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x \cdot \left(2 \cdot \frac{1}{2}\right)}\right)\right) \cdot -2 \]
            12. metadata-evalN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + x \cdot \color{blue}{1}\right)\right) \cdot -2 \]
            13. *-rgt-identityN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\varepsilon \cdot \frac{1}{2} + \color{blue}{x}\right)\right) \cdot -2 \]
            14. *-commutativeN/A

              \[\leadsto \left(\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \left(\color{blue}{\frac{1}{2} \cdot \varepsilon} + x\right)\right) \cdot -2 \]
            15. lower-fma.f6499.7

              \[\leadsto \left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
          7. Applied rewrites99.7%

            \[\leadsto \color{blue}{\left(\sin \left(0.5 \cdot \varepsilon\right) \cdot \sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)\right)} \cdot -2 \]
          8. Taylor expanded in eps around 0

            \[\leadsto \left(\left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)}\right) \cdot -2 \]
          9. Step-by-step derivation
            1. Applied rewrites98.9%

              \[\leadsto \left(\left(\varepsilon \cdot 0.5\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right)}\right) \cdot -2 \]
            2. Final simplification98.9%

              \[\leadsto -2 \cdot \left(\sin \left(\mathsf{fma}\left(0.5, \varepsilon, x\right)\right) \cdot \left(\varepsilon \cdot 0.5\right)\right) \]
            3. Add Preprocessing

            Alternative 7: 79.6% accurate, 1.9× speedup?

            \[\begin{array}{l} \\ \sin x \cdot \left(-\varepsilon\right) \end{array} \]
            (FPCore (x eps) :precision binary64 (* (sin x) (- eps)))
            double code(double x, double eps) {
            	return sin(x) * -eps;
            }
            
            real(8) function code(x, eps)
                real(8), intent (in) :: x
                real(8), intent (in) :: eps
                code = sin(x) * -eps
            end function
            
            public static double code(double x, double eps) {
            	return Math.sin(x) * -eps;
            }
            
            def code(x, eps):
            	return math.sin(x) * -eps
            
            function code(x, eps)
            	return Float64(sin(x) * Float64(-eps))
            end
            
            function tmp = code(x, eps)
            	tmp = sin(x) * -eps;
            end
            
            code[x_, eps_] := N[(N[Sin[x], $MachinePrecision] * (-eps)), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \sin x \cdot \left(-\varepsilon\right)
            \end{array}
            
            Derivation
            1. Initial program 54.8%

              \[\cos \left(x + \varepsilon\right) - \cos x \]
            2. Add Preprocessing
            3. Taylor expanded in eps around 0

              \[\leadsto \color{blue}{-1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
            4. Step-by-step derivation
              1. associate-*r*N/A

                \[\leadsto \color{blue}{\left(-1 \cdot \varepsilon\right) \cdot \sin x} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\sin x \cdot \left(-1 \cdot \varepsilon\right)} \]
              3. lower-*.f64N/A

                \[\leadsto \color{blue}{\sin x \cdot \left(-1 \cdot \varepsilon\right)} \]
              4. lower-sin.f64N/A

                \[\leadsto \color{blue}{\sin x} \cdot \left(-1 \cdot \varepsilon\right) \]
              5. mul-1-negN/A

                \[\leadsto \sin x \cdot \color{blue}{\left(\mathsf{neg}\left(\varepsilon\right)\right)} \]
              6. lower-neg.f6479.9

                \[\leadsto \sin x \cdot \color{blue}{\left(-\varepsilon\right)} \]
            5. Applied rewrites79.9%

              \[\leadsto \color{blue}{\sin x \cdot \left(-\varepsilon\right)} \]
            6. Add Preprocessing

            Alternative 8: 52.7% accurate, 18.8× speedup?

            \[\begin{array}{l} \\ \varepsilon \cdot \left(\varepsilon \cdot -0.5\right) \end{array} \]
            (FPCore (x eps) :precision binary64 (* eps (* eps -0.5)))
            double code(double x, double eps) {
            	return eps * (eps * -0.5);
            }
            
            real(8) function code(x, eps)
                real(8), intent (in) :: x
                real(8), intent (in) :: eps
                code = eps * (eps * (-0.5d0))
            end function
            
            public static double code(double x, double eps) {
            	return eps * (eps * -0.5);
            }
            
            def code(x, eps):
            	return eps * (eps * -0.5)
            
            function code(x, eps)
            	return Float64(eps * Float64(eps * -0.5))
            end
            
            function tmp = code(x, eps)
            	tmp = eps * (eps * -0.5);
            end
            
            code[x_, eps_] := N[(eps * N[(eps * -0.5), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \varepsilon \cdot \left(\varepsilon \cdot -0.5\right)
            \end{array}
            
            Derivation
            1. Initial program 54.8%

              \[\cos \left(x + \varepsilon\right) - \cos x \]
            2. Add Preprocessing
            3. Taylor expanded in x around 0

              \[\leadsto \color{blue}{\cos \varepsilon - 1} \]
            4. Step-by-step derivation
              1. sub-negN/A

                \[\leadsto \color{blue}{\cos \varepsilon + \left(\mathsf{neg}\left(1\right)\right)} \]
              2. metadata-evalN/A

                \[\leadsto \cos \varepsilon + \color{blue}{-1} \]
              3. lower-+.f64N/A

                \[\leadsto \color{blue}{\cos \varepsilon + -1} \]
              4. lower-cos.f6453.1

                \[\leadsto \color{blue}{\cos \varepsilon} + -1 \]
            5. Applied rewrites53.1%

              \[\leadsto \color{blue}{\cos \varepsilon + -1} \]
            6. Taylor expanded in eps around 0

              \[\leadsto \frac{-1}{2} \cdot \color{blue}{{\varepsilon}^{2}} \]
            7. Step-by-step derivation
              1. Applied rewrites54.4%

                \[\leadsto \varepsilon \cdot \color{blue}{\left(\varepsilon \cdot -0.5\right)} \]
              2. Add Preprocessing

              Alternative 9: 51.4% accurate, 51.8× speedup?

              \[\begin{array}{l} \\ -1 + 1 \end{array} \]
              (FPCore (x eps) :precision binary64 (+ -1.0 1.0))
              double code(double x, double eps) {
              	return -1.0 + 1.0;
              }
              
              real(8) function code(x, eps)
                  real(8), intent (in) :: x
                  real(8), intent (in) :: eps
                  code = (-1.0d0) + 1.0d0
              end function
              
              public static double code(double x, double eps) {
              	return -1.0 + 1.0;
              }
              
              def code(x, eps):
              	return -1.0 + 1.0
              
              function code(x, eps)
              	return Float64(-1.0 + 1.0)
              end
              
              function tmp = code(x, eps)
              	tmp = -1.0 + 1.0;
              end
              
              code[x_, eps_] := N[(-1.0 + 1.0), $MachinePrecision]
              
              \begin{array}{l}
              
              \\
              -1 + 1
              \end{array}
              
              Derivation
              1. Initial program 54.8%

                \[\cos \left(x + \varepsilon\right) - \cos x \]
              2. Add Preprocessing
              3. Taylor expanded in x around 0

                \[\leadsto \color{blue}{\cos \varepsilon - 1} \]
              4. Step-by-step derivation
                1. sub-negN/A

                  \[\leadsto \color{blue}{\cos \varepsilon + \left(\mathsf{neg}\left(1\right)\right)} \]
                2. metadata-evalN/A

                  \[\leadsto \cos \varepsilon + \color{blue}{-1} \]
                3. lower-+.f64N/A

                  \[\leadsto \color{blue}{\cos \varepsilon + -1} \]
                4. lower-cos.f6453.1

                  \[\leadsto \color{blue}{\cos \varepsilon} + -1 \]
              5. Applied rewrites53.1%

                \[\leadsto \color{blue}{\cos \varepsilon + -1} \]
              6. Taylor expanded in eps around 0

                \[\leadsto 1 + -1 \]
              7. Step-by-step derivation
                1. Applied rewrites53.0%

                  \[\leadsto 1 + -1 \]
                2. Final simplification53.0%

                  \[\leadsto -1 + 1 \]
                3. Add Preprocessing

                Developer Target 1: 99.7% accurate, 0.9× speedup?

                \[\begin{array}{l} \\ \left(-2 \cdot \sin \left(x + \frac{\varepsilon}{2}\right)\right) \cdot \sin \left(\frac{\varepsilon}{2}\right) \end{array} \]
                (FPCore (x eps)
                 :precision binary64
                 (* (* -2.0 (sin (+ x (/ eps 2.0)))) (sin (/ eps 2.0))))
                double code(double x, double eps) {
                	return (-2.0 * sin((x + (eps / 2.0)))) * sin((eps / 2.0));
                }
                
                real(8) function code(x, eps)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: eps
                    code = ((-2.0d0) * sin((x + (eps / 2.0d0)))) * sin((eps / 2.0d0))
                end function
                
                public static double code(double x, double eps) {
                	return (-2.0 * Math.sin((x + (eps / 2.0)))) * Math.sin((eps / 2.0));
                }
                
                def code(x, eps):
                	return (-2.0 * math.sin((x + (eps / 2.0)))) * math.sin((eps / 2.0))
                
                function code(x, eps)
                	return Float64(Float64(-2.0 * sin(Float64(x + Float64(eps / 2.0)))) * sin(Float64(eps / 2.0)))
                end
                
                function tmp = code(x, eps)
                	tmp = (-2.0 * sin((x + (eps / 2.0)))) * sin((eps / 2.0));
                end
                
                code[x_, eps_] := N[(N[(-2.0 * N[Sin[N[(x + N[(eps / 2.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Sin[N[(eps / 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
                
                \begin{array}{l}
                
                \\
                \left(-2 \cdot \sin \left(x + \frac{\varepsilon}{2}\right)\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)
                \end{array}
                

                Developer Target 2: 98.8% accurate, 0.5× speedup?

                \[\begin{array}{l} \\ {\left(\sqrt[3]{\left(-2 \cdot \sin \left(0.5 \cdot \mathsf{fma}\left(2, x, \varepsilon\right)\right)\right) \cdot \sin \left(0.5 \cdot \varepsilon\right)}\right)}^{3} \end{array} \]
                (FPCore (x eps)
                 :precision binary64
                 (pow (cbrt (* (* -2.0 (sin (* 0.5 (fma 2.0 x eps)))) (sin (* 0.5 eps)))) 3.0))
                double code(double x, double eps) {
                	return pow(cbrt(((-2.0 * sin((0.5 * fma(2.0, x, eps)))) * sin((0.5 * eps)))), 3.0);
                }
                
                function code(x, eps)
                	return cbrt(Float64(Float64(-2.0 * sin(Float64(0.5 * fma(2.0, x, eps)))) * sin(Float64(0.5 * eps)))) ^ 3.0
                end
                
                code[x_, eps_] := N[Power[N[Power[N[(N[(-2.0 * N[Sin[N[(0.5 * N[(2.0 * x + eps), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Sin[N[(0.5 * eps), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], 1/3], $MachinePrecision], 3.0], $MachinePrecision]
                
                \begin{array}{l}
                
                \\
                {\left(\sqrt[3]{\left(-2 \cdot \sin \left(0.5 \cdot \mathsf{fma}\left(2, x, \varepsilon\right)\right)\right) \cdot \sin \left(0.5 \cdot \varepsilon\right)}\right)}^{3}
                \end{array}
                

                Reproduce

                ?
                herbie shell --seed 2024219 
                (FPCore (x eps)
                  :name "2cos (problem 3.3.5)"
                  :precision binary64
                  :pre (and (and (and (<= -10000.0 x) (<= x 10000.0)) (< (* 1e-16 (fabs x)) eps)) (< eps (fabs x)))
                
                  :alt
                  (! :herbie-platform default (* -2 (sin (+ x (/ eps 2))) (sin (/ eps 2))))
                
                  :alt
                  (! :herbie-platform default (pow (cbrt (* -2 (sin (* 1/2 (fma 2 x eps))) (sin (* 1/2 eps)))) 3))
                
                  (- (cos (+ x eps)) (cos x)))