mixedcos

Percentage Accurate: 66.8% → 97.4%
Time: 8.3s
Alternatives: 7
Speedup: 9.0×

Specification

?
\[\begin{array}{l} \\ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \end{array} \]
(FPCore (x c s)
 :precision binary64
 (/ (cos (* 2.0 x)) (* (pow c 2.0) (* (* x (pow s 2.0)) x))))
double code(double x, double c, double s) {
	return cos((2.0 * x)) / (pow(c, 2.0) * ((x * pow(s, 2.0)) * x));
}
real(8) function code(x, c, s)
    real(8), intent (in) :: x
    real(8), intent (in) :: c
    real(8), intent (in) :: s
    code = cos((2.0d0 * x)) / ((c ** 2.0d0) * ((x * (s ** 2.0d0)) * x))
end function
public static double code(double x, double c, double s) {
	return Math.cos((2.0 * x)) / (Math.pow(c, 2.0) * ((x * Math.pow(s, 2.0)) * x));
}
def code(x, c, s):
	return math.cos((2.0 * x)) / (math.pow(c, 2.0) * ((x * math.pow(s, 2.0)) * x))
function code(x, c, s)
	return Float64(cos(Float64(2.0 * x)) / Float64((c ^ 2.0) * Float64(Float64(x * (s ^ 2.0)) * x)))
end
function tmp = code(x, c, s)
	tmp = cos((2.0 * x)) / ((c ^ 2.0) * ((x * (s ^ 2.0)) * x));
end
code[x_, c_, s_] := N[(N[Cos[N[(2.0 * x), $MachinePrecision]], $MachinePrecision] / N[(N[Power[c, 2.0], $MachinePrecision] * N[(N[(x * N[Power[s, 2.0], $MachinePrecision]), $MachinePrecision] * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)}
\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 7 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: 66.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \end{array} \]
(FPCore (x c s)
 :precision binary64
 (/ (cos (* 2.0 x)) (* (pow c 2.0) (* (* x (pow s 2.0)) x))))
double code(double x, double c, double s) {
	return cos((2.0 * x)) / (pow(c, 2.0) * ((x * pow(s, 2.0)) * x));
}
real(8) function code(x, c, s)
    real(8), intent (in) :: x
    real(8), intent (in) :: c
    real(8), intent (in) :: s
    code = cos((2.0d0 * x)) / ((c ** 2.0d0) * ((x * (s ** 2.0d0)) * x))
end function
public static double code(double x, double c, double s) {
	return Math.cos((2.0 * x)) / (Math.pow(c, 2.0) * ((x * Math.pow(s, 2.0)) * x));
}
def code(x, c, s):
	return math.cos((2.0 * x)) / (math.pow(c, 2.0) * ((x * math.pow(s, 2.0)) * x))
function code(x, c, s)
	return Float64(cos(Float64(2.0 * x)) / Float64((c ^ 2.0) * Float64(Float64(x * (s ^ 2.0)) * x)))
end
function tmp = code(x, c, s)
	tmp = cos((2.0 * x)) / ((c ^ 2.0) * ((x * (s ^ 2.0)) * x));
end
code[x_, c_, s_] := N[(N[Cos[N[(2.0 * x), $MachinePrecision]], $MachinePrecision] / N[(N[Power[c, 2.0], $MachinePrecision] * N[(N[(x * N[Power[s, 2.0], $MachinePrecision]), $MachinePrecision] * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)}
\end{array}

Alternative 1: 97.4% accurate, 2.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := s \cdot \left(x \cdot c\right)\\ \frac{\frac{\cos \left(x + x\right)}{t\_0}}{t\_0} \end{array} \end{array} \]
(FPCore (x c s)
 :precision binary64
 (let* ((t_0 (* s (* x c)))) (/ (/ (cos (+ x x)) t_0) t_0)))
double code(double x, double c, double s) {
	double t_0 = s * (x * c);
	return (cos((x + x)) / t_0) / t_0;
}
real(8) function code(x, c, s)
    real(8), intent (in) :: x
    real(8), intent (in) :: c
    real(8), intent (in) :: s
    real(8) :: t_0
    t_0 = s * (x * c)
    code = (cos((x + x)) / t_0) / t_0
end function
public static double code(double x, double c, double s) {
	double t_0 = s * (x * c);
	return (Math.cos((x + x)) / t_0) / t_0;
}
def code(x, c, s):
	t_0 = s * (x * c)
	return (math.cos((x + x)) / t_0) / t_0
function code(x, c, s)
	t_0 = Float64(s * Float64(x * c))
	return Float64(Float64(cos(Float64(x + x)) / t_0) / t_0)
end
function tmp = code(x, c, s)
	t_0 = s * (x * c);
	tmp = (cos((x + x)) / t_0) / t_0;
end
code[x_, c_, s_] := Block[{t$95$0 = N[(s * N[(x * c), $MachinePrecision]), $MachinePrecision]}, N[(N[(N[Cos[N[(x + x), $MachinePrecision]], $MachinePrecision] / t$95$0), $MachinePrecision] / t$95$0), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := s \cdot \left(x \cdot c\right)\\
\frac{\frac{\cos \left(x + x\right)}{t\_0}}{t\_0}
\end{array}
\end{array}
Derivation
  1. Initial program 66.6%

    \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
    3. lift-*.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left(x \cdot {s}^{2}\right)} \cdot x\right)} \]
    4. *-commutativeN/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]
    5. associate-*l*N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]
    6. associate-*r*N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]
    7. lift-pow.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{{c}^{2}} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)} \]
    8. lift-pow.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left({c}^{2} \cdot \color{blue}{{s}^{2}}\right) \cdot \left(x \cdot x\right)} \]
    9. pow-prod-downN/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(c \cdot s\right)}^{2}} \cdot \left(x \cdot x\right)} \]
    10. pow2N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(c \cdot s\right)}^{2} \cdot \color{blue}{{x}^{2}}} \]
    11. pow-prod-downN/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
    12. lower-pow.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
    13. lower-*.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}}^{2}} \]
    14. lower-*.f6498.1

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)}^{2}} \]
  4. Applied rewrites98.1%

    \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
  5. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
    2. lift-pow.f64N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
    3. unpow2N/A

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)}} \]
    4. associate-/r*N/A

      \[\leadsto \color{blue}{\frac{\frac{\cos \left(2 \cdot x\right)}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x}} \]
    5. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{\cos \left(2 \cdot x\right)}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x}} \]
    6. lower-/.f6498.2

      \[\leadsto \frac{\color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(c \cdot s\right) \cdot x}}}{\left(c \cdot s\right) \cdot x} \]
    7. lift-*.f64N/A

      \[\leadsto \frac{\frac{\cos \color{blue}{\left(2 \cdot x\right)}}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x} \]
    8. count-2N/A

      \[\leadsto \frac{\frac{\cos \color{blue}{\left(x + x\right)}}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x} \]
    9. lift-+.f6498.2

      \[\leadsto \frac{\frac{\cos \color{blue}{\left(x + x\right)}}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x} \]
    10. lift-*.f64N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{\left(c \cdot s\right) \cdot x}}}{\left(c \cdot s\right) \cdot x} \]
    11. lift-*.f64N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{\left(c \cdot s\right)} \cdot x}}{\left(c \cdot s\right) \cdot x} \]
    12. *-commutativeN/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{\left(s \cdot c\right)} \cdot x}}{\left(c \cdot s\right) \cdot x} \]
    13. associate-*l*N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{s \cdot \left(c \cdot x\right)}}}{\left(c \cdot s\right) \cdot x} \]
    14. *-commutativeN/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \color{blue}{\left(x \cdot c\right)}}}{\left(c \cdot s\right) \cdot x} \]
    15. lower-*.f64N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{s \cdot \left(x \cdot c\right)}}}{\left(c \cdot s\right) \cdot x} \]
    16. *-commutativeN/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \color{blue}{\left(c \cdot x\right)}}}{\left(c \cdot s\right) \cdot x} \]
    17. lower-*.f6496.8

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \color{blue}{\left(c \cdot x\right)}}}{\left(c \cdot s\right) \cdot x} \]
    18. lift-*.f64N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{\left(c \cdot s\right) \cdot x}} \]
    19. lift-*.f64N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{\left(c \cdot s\right)} \cdot x} \]
    20. *-commutativeN/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{\left(s \cdot c\right)} \cdot x} \]
    21. associate-*l*N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{s \cdot \left(c \cdot x\right)}} \]
    22. *-commutativeN/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \color{blue}{\left(x \cdot c\right)}} \]
    23. lower-*.f64N/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{s \cdot \left(x \cdot c\right)}} \]
    24. *-commutativeN/A

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \color{blue}{\left(c \cdot x\right)}} \]
    25. lower-*.f6498.1

      \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \color{blue}{\left(c \cdot x\right)}} \]
  6. Applied rewrites98.1%

    \[\leadsto \color{blue}{\frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \left(c \cdot x\right)}} \]
  7. Final simplification98.1%

    \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(x \cdot c\right)}}{s \cdot \left(x \cdot c\right)} \]
  8. Add Preprocessing

Alternative 2: 84.7% accurate, 2.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq 1.3 \cdot 10^{-40}:\\ \;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos \left(x + x\right)}{\left(x \cdot \left(s \cdot \left(x \cdot c\right)\right)\right) \cdot \left(s \cdot c\right)}\\ \end{array} \end{array} \]
(FPCore (x c s)
 :precision binary64
 (if (<= x 1.3e-40)
   (/ 1.0 (* c (* (* x s) (* c (* x s)))))
   (/ (cos (+ x x)) (* (* x (* s (* x c))) (* s c)))))
double code(double x, double c, double s) {
	double tmp;
	if (x <= 1.3e-40) {
		tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
	} else {
		tmp = cos((x + x)) / ((x * (s * (x * c))) * (s * c));
	}
	return tmp;
}
real(8) function code(x, c, s)
    real(8), intent (in) :: x
    real(8), intent (in) :: c
    real(8), intent (in) :: s
    real(8) :: tmp
    if (x <= 1.3d-40) then
        tmp = 1.0d0 / (c * ((x * s) * (c * (x * s))))
    else
        tmp = cos((x + x)) / ((x * (s * (x * c))) * (s * c))
    end if
    code = tmp
end function
public static double code(double x, double c, double s) {
	double tmp;
	if (x <= 1.3e-40) {
		tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
	} else {
		tmp = Math.cos((x + x)) / ((x * (s * (x * c))) * (s * c));
	}
	return tmp;
}
def code(x, c, s):
	tmp = 0
	if x <= 1.3e-40:
		tmp = 1.0 / (c * ((x * s) * (c * (x * s))))
	else:
		tmp = math.cos((x + x)) / ((x * (s * (x * c))) * (s * c))
	return tmp
function code(x, c, s)
	tmp = 0.0
	if (x <= 1.3e-40)
		tmp = Float64(1.0 / Float64(c * Float64(Float64(x * s) * Float64(c * Float64(x * s)))));
	else
		tmp = Float64(cos(Float64(x + x)) / Float64(Float64(x * Float64(s * Float64(x * c))) * Float64(s * c)));
	end
	return tmp
end
function tmp_2 = code(x, c, s)
	tmp = 0.0;
	if (x <= 1.3e-40)
		tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
	else
		tmp = cos((x + x)) / ((x * (s * (x * c))) * (s * c));
	end
	tmp_2 = tmp;
end
code[x_, c_, s_] := If[LessEqual[x, 1.3e-40], N[(1.0 / N[(c * N[(N[(x * s), $MachinePrecision] * N[(c * N[(x * s), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Cos[N[(x + x), $MachinePrecision]], $MachinePrecision] / N[(N[(x * N[(s * N[(x * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(s * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;x \leq 1.3 \cdot 10^{-40}:\\
\;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{\cos \left(x + x\right)}{\left(x \cdot \left(s \cdot \left(x \cdot c\right)\right)\right) \cdot \left(s \cdot c\right)}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < 1.3000000000000001e-40

    1. Initial program 65.1%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
    4. Step-by-step derivation
      1. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
      2. associate-*r*N/A

        \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot {x}^{2}}} \]
      3. unpow2N/A

        \[\leadsto \frac{1}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      4. associate-*r*N/A

        \[\leadsto \frac{1}{\color{blue}{\left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right) \cdot x}} \]
      5. *-commutativeN/A

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

        \[\leadsto \frac{1}{\color{blue}{x \cdot \left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right)}} \]
      7. *-commutativeN/A

        \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
      8. lower-*.f64N/A

        \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
      9. *-commutativeN/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left({s}^{2} \cdot {c}^{2}\right)}\right)} \]
      10. unpow2N/A

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

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
      12. lower-*.f64N/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
      13. unpow2N/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(s \cdot \color{blue}{\left(c \cdot c\right)}\right)\right)\right)} \]
      14. associate-*r*N/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(\left(s \cdot c\right) \cdot c\right)}\right)\right)} \]
      15. *-commutativeN/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
      16. lower-*.f64N/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
      17. *-commutativeN/A

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
      18. lower-*.f6475.8

        \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
    5. Applied rewrites75.8%

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(c \cdot s\right)\right)\right)\right)}} \]
    6. Step-by-step derivation
      1. Applied rewrites83.9%

        \[\leadsto \frac{1}{c \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)\right)}} \]
      2. Step-by-step derivation
        1. Applied rewrites84.0%

          \[\leadsto \frac{1}{c \cdot \left(\left(s \cdot x\right) \cdot \left(\left(x \cdot s\right) \cdot \color{blue}{c}\right)\right)} \]

        if 1.3000000000000001e-40 < x

        1. Initial program 70.9%

          \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
          2. lift-*.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
          3. lift-*.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left(x \cdot {s}^{2}\right)} \cdot x\right)} \]
          4. *-commutativeN/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]
          5. associate-*l*N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]
          6. associate-*r*N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]
          7. lift-pow.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{{c}^{2}} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)} \]
          8. lift-pow.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left({c}^{2} \cdot \color{blue}{{s}^{2}}\right) \cdot \left(x \cdot x\right)} \]
          9. pow-prod-downN/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(c \cdot s\right)}^{2}} \cdot \left(x \cdot x\right)} \]
          10. pow2N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(c \cdot s\right)}^{2} \cdot \color{blue}{{x}^{2}}} \]
          11. pow-prod-downN/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
          12. lower-pow.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
          13. lower-*.f64N/A

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}}^{2}} \]
          14. lower-*.f6498.1

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)}^{2}} \]
        4. Applied rewrites98.1%

          \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
        5. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \frac{\cos \color{blue}{\left(2 \cdot x\right)}}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}} \]
          2. count-2N/A

            \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}} \]
          3. lift-+.f6498.1

            \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}} \]
          4. lift-pow.f64N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
          5. unpow2N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)}} \]
          6. lift-*.f64N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)} \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
          7. associate-*l*N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{\left(c \cdot s\right) \cdot \left(x \cdot \left(\left(c \cdot s\right) \cdot x\right)\right)}} \]
          8. lower-*.f64N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{\left(c \cdot s\right) \cdot \left(x \cdot \left(\left(c \cdot s\right) \cdot x\right)\right)}} \]
          9. lower-*.f6498.2

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \color{blue}{\left(x \cdot \left(\left(c \cdot s\right) \cdot x\right)\right)}} \]
          10. lift-*.f64N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}\right)} \]
          11. lift-*.f64N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)\right)} \]
          12. *-commutativeN/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \left(\color{blue}{\left(s \cdot c\right)} \cdot x\right)\right)} \]
          13. associate-*l*N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}\right)} \]
          14. *-commutativeN/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(x \cdot c\right)}\right)\right)} \]
          15. lower-*.f64N/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(x \cdot c\right)\right)}\right)} \]
          16. *-commutativeN/A

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot x\right)}\right)\right)} \]
          17. lower-*.f6495.4

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot x\right)}\right)\right)} \]
        6. Applied rewrites95.4%

          \[\leadsto \color{blue}{\frac{\cos \left(x + x\right)}{\left(c \cdot s\right) \cdot \left(x \cdot \left(s \cdot \left(c \cdot x\right)\right)\right)}} \]
      3. Recombined 2 regimes into one program.
      4. Final simplification86.9%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 1.3 \cdot 10^{-40}:\\ \;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos \left(x + x\right)}{\left(x \cdot \left(s \cdot \left(x \cdot c\right)\right)\right) \cdot \left(s \cdot c\right)}\\ \end{array} \]
      5. Add Preprocessing

      Alternative 3: 82.6% accurate, 2.3× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq 4 \cdot 10^{-17}:\\ \;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos \left(x + x\right)}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(s \cdot c\right)\right)\right)\right)}\\ \end{array} \end{array} \]
      (FPCore (x c s)
       :precision binary64
       (if (<= x 4e-17)
         (/ 1.0 (* c (* (* x s) (* c (* x s)))))
         (/ (cos (+ x x)) (* x (* x (* s (* c (* s c))))))))
      double code(double x, double c, double s) {
      	double tmp;
      	if (x <= 4e-17) {
      		tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
      	} else {
      		tmp = cos((x + x)) / (x * (x * (s * (c * (s * c)))));
      	}
      	return tmp;
      }
      
      real(8) function code(x, c, s)
          real(8), intent (in) :: x
          real(8), intent (in) :: c
          real(8), intent (in) :: s
          real(8) :: tmp
          if (x <= 4d-17) then
              tmp = 1.0d0 / (c * ((x * s) * (c * (x * s))))
          else
              tmp = cos((x + x)) / (x * (x * (s * (c * (s * c)))))
          end if
          code = tmp
      end function
      
      public static double code(double x, double c, double s) {
      	double tmp;
      	if (x <= 4e-17) {
      		tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
      	} else {
      		tmp = Math.cos((x + x)) / (x * (x * (s * (c * (s * c)))));
      	}
      	return tmp;
      }
      
      def code(x, c, s):
      	tmp = 0
      	if x <= 4e-17:
      		tmp = 1.0 / (c * ((x * s) * (c * (x * s))))
      	else:
      		tmp = math.cos((x + x)) / (x * (x * (s * (c * (s * c)))))
      	return tmp
      
      function code(x, c, s)
      	tmp = 0.0
      	if (x <= 4e-17)
      		tmp = Float64(1.0 / Float64(c * Float64(Float64(x * s) * Float64(c * Float64(x * s)))));
      	else
      		tmp = Float64(cos(Float64(x + x)) / Float64(x * Float64(x * Float64(s * Float64(c * Float64(s * c))))));
      	end
      	return tmp
      end
      
      function tmp_2 = code(x, c, s)
      	tmp = 0.0;
      	if (x <= 4e-17)
      		tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
      	else
      		tmp = cos((x + x)) / (x * (x * (s * (c * (s * c)))));
      	end
      	tmp_2 = tmp;
      end
      
      code[x_, c_, s_] := If[LessEqual[x, 4e-17], N[(1.0 / N[(c * N[(N[(x * s), $MachinePrecision] * N[(c * N[(x * s), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Cos[N[(x + x), $MachinePrecision]], $MachinePrecision] / N[(x * N[(x * N[(s * N[(c * N[(s * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;x \leq 4 \cdot 10^{-17}:\\
      \;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\
      
      \mathbf{else}:\\
      \;\;\;\;\frac{\cos \left(x + x\right)}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(s \cdot c\right)\right)\right)\right)}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if x < 4.00000000000000029e-17

        1. Initial program 65.1%

          \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
        4. Step-by-step derivation
          1. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
          2. associate-*r*N/A

            \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot {x}^{2}}} \]
          3. unpow2N/A

            \[\leadsto \frac{1}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
          4. associate-*r*N/A

            \[\leadsto \frac{1}{\color{blue}{\left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right) \cdot x}} \]
          5. *-commutativeN/A

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

            \[\leadsto \frac{1}{\color{blue}{x \cdot \left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right)}} \]
          7. *-commutativeN/A

            \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
          8. lower-*.f64N/A

            \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
          9. *-commutativeN/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left({s}^{2} \cdot {c}^{2}\right)}\right)} \]
          10. unpow2N/A

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

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
          12. lower-*.f64N/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
          13. unpow2N/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(s \cdot \color{blue}{\left(c \cdot c\right)}\right)\right)\right)} \]
          14. associate-*r*N/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(\left(s \cdot c\right) \cdot c\right)}\right)\right)} \]
          15. *-commutativeN/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
          16. lower-*.f64N/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
          17. *-commutativeN/A

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
          18. lower-*.f6476.2

            \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
        5. Applied rewrites76.2%

          \[\leadsto \color{blue}{\frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(c \cdot s\right)\right)\right)\right)}} \]
        6. Step-by-step derivation
          1. Applied rewrites83.7%

            \[\leadsto \frac{1}{c \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)\right)}} \]
          2. Step-by-step derivation
            1. Applied rewrites83.8%

              \[\leadsto \frac{1}{c \cdot \left(\left(s \cdot x\right) \cdot \left(\left(x \cdot s\right) \cdot \color{blue}{c}\right)\right)} \]

            if 4.00000000000000029e-17 < x

            1. Initial program 71.1%

              \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
              2. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
              3. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left(x \cdot {s}^{2}\right)} \cdot x\right)} \]
              4. *-commutativeN/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]
              5. associate-*l*N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]
              6. associate-*r*N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]
              7. lift-pow.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{{c}^{2}} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)} \]
              8. lift-pow.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left({c}^{2} \cdot \color{blue}{{s}^{2}}\right) \cdot \left(x \cdot x\right)} \]
              9. pow-prod-downN/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(c \cdot s\right)}^{2}} \cdot \left(x \cdot x\right)} \]
              10. pow2N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(c \cdot s\right)}^{2} \cdot \color{blue}{{x}^{2}}} \]
              11. pow-prod-downN/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
              12. lower-pow.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
              13. lower-*.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}}^{2}} \]
              14. lower-*.f6498.1

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)}^{2}} \]
            4. Applied rewrites98.1%

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
            5. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
              2. lift-pow.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
              3. unpow2N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)}} \]
              4. associate-/r*N/A

                \[\leadsto \color{blue}{\frac{\frac{\cos \left(2 \cdot x\right)}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x}} \]
              5. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{\cos \left(2 \cdot x\right)}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x}} \]
              6. lower-/.f6498.2

                \[\leadsto \frac{\color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(c \cdot s\right) \cdot x}}}{\left(c \cdot s\right) \cdot x} \]
              7. lift-*.f64N/A

                \[\leadsto \frac{\frac{\cos \color{blue}{\left(2 \cdot x\right)}}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x} \]
              8. count-2N/A

                \[\leadsto \frac{\frac{\cos \color{blue}{\left(x + x\right)}}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x} \]
              9. lift-+.f6498.2

                \[\leadsto \frac{\frac{\cos \color{blue}{\left(x + x\right)}}{\left(c \cdot s\right) \cdot x}}{\left(c \cdot s\right) \cdot x} \]
              10. lift-*.f64N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{\left(c \cdot s\right) \cdot x}}}{\left(c \cdot s\right) \cdot x} \]
              11. lift-*.f64N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{\left(c \cdot s\right)} \cdot x}}{\left(c \cdot s\right) \cdot x} \]
              12. *-commutativeN/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{\left(s \cdot c\right)} \cdot x}}{\left(c \cdot s\right) \cdot x} \]
              13. associate-*l*N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{s \cdot \left(c \cdot x\right)}}}{\left(c \cdot s\right) \cdot x} \]
              14. *-commutativeN/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \color{blue}{\left(x \cdot c\right)}}}{\left(c \cdot s\right) \cdot x} \]
              15. lower-*.f64N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{\color{blue}{s \cdot \left(x \cdot c\right)}}}{\left(c \cdot s\right) \cdot x} \]
              16. *-commutativeN/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \color{blue}{\left(c \cdot x\right)}}}{\left(c \cdot s\right) \cdot x} \]
              17. lower-*.f6495.2

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \color{blue}{\left(c \cdot x\right)}}}{\left(c \cdot s\right) \cdot x} \]
              18. lift-*.f64N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{\left(c \cdot s\right) \cdot x}} \]
              19. lift-*.f64N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{\left(c \cdot s\right)} \cdot x} \]
              20. *-commutativeN/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{\left(s \cdot c\right)} \cdot x} \]
              21. associate-*l*N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{s \cdot \left(c \cdot x\right)}} \]
              22. *-commutativeN/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \color{blue}{\left(x \cdot c\right)}} \]
              23. lower-*.f64N/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{\color{blue}{s \cdot \left(x \cdot c\right)}} \]
              24. *-commutativeN/A

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \color{blue}{\left(c \cdot x\right)}} \]
              25. lower-*.f6496.5

                \[\leadsto \frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \color{blue}{\left(c \cdot x\right)}} \]
            6. Applied rewrites96.5%

              \[\leadsto \color{blue}{\frac{\frac{\cos \left(x + x\right)}{s \cdot \left(c \cdot x\right)}}{s \cdot \left(c \cdot x\right)}} \]
            7. Step-by-step derivation
              1. lift-/.f64N/A

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

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

                \[\leadsto \frac{\frac{\cos \color{blue}{\left(x + x\right)}}{s \cdot \left(c \cdot x\right)}}{s \cdot \left(c \cdot x\right)} \]
              4. count-2N/A

                \[\leadsto \frac{\frac{\cos \color{blue}{\left(2 \cdot x\right)}}{s \cdot \left(c \cdot x\right)}}{s \cdot \left(c \cdot x\right)} \]
              5. lift-*.f64N/A

                \[\leadsto \frac{\frac{\cos \color{blue}{\left(2 \cdot x\right)}}{s \cdot \left(c \cdot x\right)}}{s \cdot \left(c \cdot x\right)} \]
              6. associate-/r*N/A

                \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)}} \]
              7. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)}} \]
              8. lift-/.f6496.5

                \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)}} \]
              9. lift-*.f64N/A

                \[\leadsto \frac{\cos \color{blue}{\left(2 \cdot x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
              10. count-2N/A

                \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
              11. lift-+.f6496.5

                \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
              12. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)}} \]
              13. pow2N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{{\left(s \cdot \left(c \cdot x\right)\right)}^{2}}} \]
              14. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}}^{2}} \]
              15. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{{\left(s \cdot \color{blue}{\left(c \cdot x\right)}\right)}^{2}} \]
              16. associate-*r*N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right)}}^{2}} \]
              17. *-commutativeN/A

                \[\leadsto \frac{\cos \left(x + x\right)}{{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)}^{2}} \]
              18. lift-*.f64N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)}^{2}} \]
              19. unpow-prod-downN/A

                \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{{\left(c \cdot s\right)}^{2} \cdot {x}^{2}}} \]
              20. pow2N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right)} \cdot {x}^{2}} \]
              21. pow2N/A

                \[\leadsto \frac{\cos \left(x + x\right)}{\left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
            8. Applied rewrites90.7%

              \[\leadsto \color{blue}{\frac{\cos \left(x + x\right)}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(s \cdot c\right)\right)\right)\right)}} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification85.5%

            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 4 \cdot 10^{-17}:\\ \;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos \left(x + x\right)}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(s \cdot c\right)\right)\right)\right)}\\ \end{array} \]
          5. Add Preprocessing

          Alternative 4: 97.2% accurate, 2.4× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} t_0 := s \cdot \left(x \cdot c\right)\\ \frac{\cos \left(x + x\right)}{t\_0 \cdot t\_0} \end{array} \end{array} \]
          (FPCore (x c s)
           :precision binary64
           (let* ((t_0 (* s (* x c)))) (/ (cos (+ x x)) (* t_0 t_0))))
          double code(double x, double c, double s) {
          	double t_0 = s * (x * c);
          	return cos((x + x)) / (t_0 * t_0);
          }
          
          real(8) function code(x, c, s)
              real(8), intent (in) :: x
              real(8), intent (in) :: c
              real(8), intent (in) :: s
              real(8) :: t_0
              t_0 = s * (x * c)
              code = cos((x + x)) / (t_0 * t_0)
          end function
          
          public static double code(double x, double c, double s) {
          	double t_0 = s * (x * c);
          	return Math.cos((x + x)) / (t_0 * t_0);
          }
          
          def code(x, c, s):
          	t_0 = s * (x * c)
          	return math.cos((x + x)) / (t_0 * t_0)
          
          function code(x, c, s)
          	t_0 = Float64(s * Float64(x * c))
          	return Float64(cos(Float64(x + x)) / Float64(t_0 * t_0))
          end
          
          function tmp = code(x, c, s)
          	t_0 = s * (x * c);
          	tmp = cos((x + x)) / (t_0 * t_0);
          end
          
          code[x_, c_, s_] := Block[{t$95$0 = N[(s * N[(x * c), $MachinePrecision]), $MachinePrecision]}, N[(N[Cos[N[(x + x), $MachinePrecision]], $MachinePrecision] / N[(t$95$0 * t$95$0), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          t_0 := s \cdot \left(x \cdot c\right)\\
          \frac{\cos \left(x + x\right)}{t\_0 \cdot t\_0}
          \end{array}
          \end{array}
          
          Derivation
          1. Initial program 66.6%

            \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
            2. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(\left(x \cdot {s}^{2}\right) \cdot x\right)}} \]
            3. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left(x \cdot {s}^{2}\right)} \cdot x\right)} \]
            4. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]
            5. associate-*l*N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]
            6. associate-*r*N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]
            7. lift-pow.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{{c}^{2}} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)} \]
            8. lift-pow.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left({c}^{2} \cdot \color{blue}{{s}^{2}}\right) \cdot \left(x \cdot x\right)} \]
            9. pow-prod-downN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(c \cdot s\right)}^{2}} \cdot \left(x \cdot x\right)} \]
            10. pow2N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(c \cdot s\right)}^{2} \cdot \color{blue}{{x}^{2}}} \]
            11. pow-prod-downN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
            12. lower-pow.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
            13. lower-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}}^{2}} \]
            14. lower-*.f6498.1

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)}^{2}} \]
          4. Applied rewrites98.1%

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
          5. Step-by-step derivation
            1. lift-pow.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{{\left(\left(c \cdot s\right) \cdot x\right)}^{2}}} \]
            2. unpow2N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)}} \]
            3. lower-*.f6498.1

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)}} \]
            4. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)} \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            5. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{\left(c \cdot s\right)} \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            6. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{\left(s \cdot c\right)} \cdot x\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            7. associate-*l*N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)} \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            8. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \color{blue}{\left(x \cdot c\right)}\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            9. lower-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot \left(x \cdot c\right)\right)} \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            10. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \color{blue}{\left(c \cdot x\right)}\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            11. lower-*.f6496.7

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \color{blue}{\left(c \cdot x\right)}\right) \cdot \left(\left(c \cdot s\right) \cdot x\right)} \]
            12. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}} \]
            13. lift-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(\color{blue}{\left(c \cdot s\right)} \cdot x\right)} \]
            14. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot c\right)} \cdot x\right)} \]
            15. associate-*l*N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}} \]
            16. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \color{blue}{\left(x \cdot c\right)}\right)} \]
            17. lower-*.f64N/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(s \cdot \left(x \cdot c\right)\right)}} \]
            18. *-commutativeN/A

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \color{blue}{\left(c \cdot x\right)}\right)} \]
            19. lower-*.f6498.1

              \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \color{blue}{\left(c \cdot x\right)}\right)} \]
          6. Applied rewrites98.1%

            \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)}} \]
          7. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \frac{\cos \color{blue}{\left(2 \cdot x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
            2. count-2N/A

              \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
            3. lift-+.f6498.1

              \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
          8. Applied rewrites98.1%

            \[\leadsto \frac{\cos \color{blue}{\left(x + x\right)}}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]
          9. Final simplification98.1%

            \[\leadsto \frac{\cos \left(x + x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)} \]
          10. Add Preprocessing

          Alternative 5: 78.3% accurate, 9.0× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} t_0 := x \cdot \left(s \cdot c\right)\\ \frac{1}{t\_0 \cdot t\_0} \end{array} \end{array} \]
          (FPCore (x c s)
           :precision binary64
           (let* ((t_0 (* x (* s c)))) (/ 1.0 (* t_0 t_0))))
          double code(double x, double c, double s) {
          	double t_0 = x * (s * c);
          	return 1.0 / (t_0 * t_0);
          }
          
          real(8) function code(x, c, s)
              real(8), intent (in) :: x
              real(8), intent (in) :: c
              real(8), intent (in) :: s
              real(8) :: t_0
              t_0 = x * (s * c)
              code = 1.0d0 / (t_0 * t_0)
          end function
          
          public static double code(double x, double c, double s) {
          	double t_0 = x * (s * c);
          	return 1.0 / (t_0 * t_0);
          }
          
          def code(x, c, s):
          	t_0 = x * (s * c)
          	return 1.0 / (t_0 * t_0)
          
          function code(x, c, s)
          	t_0 = Float64(x * Float64(s * c))
          	return Float64(1.0 / Float64(t_0 * t_0))
          end
          
          function tmp = code(x, c, s)
          	t_0 = x * (s * c);
          	tmp = 1.0 / (t_0 * t_0);
          end
          
          code[x_, c_, s_] := Block[{t$95$0 = N[(x * N[(s * c), $MachinePrecision]), $MachinePrecision]}, N[(1.0 / N[(t$95$0 * t$95$0), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          t_0 := x \cdot \left(s \cdot c\right)\\
          \frac{1}{t\_0 \cdot t\_0}
          \end{array}
          \end{array}
          
          Derivation
          1. Initial program 66.6%

            \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
          2. Add Preprocessing
          3. Taylor expanded in x around 0

            \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
          4. Step-by-step derivation
            1. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
            2. associate-*r*N/A

              \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot {x}^{2}}} \]
            3. unpow2N/A

              \[\leadsto \frac{1}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
            4. associate-*r*N/A

              \[\leadsto \frac{1}{\color{blue}{\left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right) \cdot x}} \]
            5. *-commutativeN/A

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

              \[\leadsto \frac{1}{\color{blue}{x \cdot \left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right)}} \]
            7. *-commutativeN/A

              \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
            8. lower-*.f64N/A

              \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
            9. *-commutativeN/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left({s}^{2} \cdot {c}^{2}\right)}\right)} \]
            10. unpow2N/A

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

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
            12. lower-*.f64N/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
            13. unpow2N/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(s \cdot \color{blue}{\left(c \cdot c\right)}\right)\right)\right)} \]
            14. associate-*r*N/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(\left(s \cdot c\right) \cdot c\right)}\right)\right)} \]
            15. *-commutativeN/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
            16. lower-*.f64N/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
            17. *-commutativeN/A

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
            18. lower-*.f6474.7

              \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
          5. Applied rewrites74.7%

            \[\leadsto \color{blue}{\frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(c \cdot s\right)\right)\right)\right)}} \]
          6. Step-by-step derivation
            1. Applied rewrites80.4%

              \[\leadsto \frac{1}{c \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)\right)}} \]
            2. Step-by-step derivation
              1. Applied rewrites83.9%

                \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}} \]
              2. Add Preprocessing

              Alternative 6: 76.8% accurate, 9.0× speedup?

              \[\begin{array}{l} \\ \frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)} \end{array} \]
              (FPCore (x c s) :precision binary64 (/ 1.0 (* c (* (* x s) (* c (* x s))))))
              double code(double x, double c, double s) {
              	return 1.0 / (c * ((x * s) * (c * (x * s))));
              }
              
              real(8) function code(x, c, s)
                  real(8), intent (in) :: x
                  real(8), intent (in) :: c
                  real(8), intent (in) :: s
                  code = 1.0d0 / (c * ((x * s) * (c * (x * s))))
              end function
              
              public static double code(double x, double c, double s) {
              	return 1.0 / (c * ((x * s) * (c * (x * s))));
              }
              
              def code(x, c, s):
              	return 1.0 / (c * ((x * s) * (c * (x * s))))
              
              function code(x, c, s)
              	return Float64(1.0 / Float64(c * Float64(Float64(x * s) * Float64(c * Float64(x * s)))))
              end
              
              function tmp = code(x, c, s)
              	tmp = 1.0 / (c * ((x * s) * (c * (x * s))));
              end
              
              code[x_, c_, s_] := N[(1.0 / N[(c * N[(N[(x * s), $MachinePrecision] * N[(c * N[(x * s), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
              
              \begin{array}{l}
              
              \\
              \frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}
              \end{array}
              
              Derivation
              1. Initial program 66.6%

                \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
              2. Add Preprocessing
              3. Taylor expanded in x around 0

                \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
              4. Step-by-step derivation
                1. lower-/.f64N/A

                  \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
                2. associate-*r*N/A

                  \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot {x}^{2}}} \]
                3. unpow2N/A

                  \[\leadsto \frac{1}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
                4. associate-*r*N/A

                  \[\leadsto \frac{1}{\color{blue}{\left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right) \cdot x}} \]
                5. *-commutativeN/A

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

                  \[\leadsto \frac{1}{\color{blue}{x \cdot \left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right)}} \]
                7. *-commutativeN/A

                  \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
                8. lower-*.f64N/A

                  \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
                9. *-commutativeN/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left({s}^{2} \cdot {c}^{2}\right)}\right)} \]
                10. unpow2N/A

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

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
                12. lower-*.f64N/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
                13. unpow2N/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(s \cdot \color{blue}{\left(c \cdot c\right)}\right)\right)\right)} \]
                14. associate-*r*N/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(\left(s \cdot c\right) \cdot c\right)}\right)\right)} \]
                15. *-commutativeN/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
                16. lower-*.f64N/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
                17. *-commutativeN/A

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
                18. lower-*.f6474.7

                  \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
              5. Applied rewrites74.7%

                \[\leadsto \color{blue}{\frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(c \cdot s\right)\right)\right)\right)}} \]
              6. Step-by-step derivation
                1. Applied rewrites80.4%

                  \[\leadsto \frac{1}{c \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)\right)}} \]
                2. Step-by-step derivation
                  1. Applied rewrites80.6%

                    \[\leadsto \frac{1}{c \cdot \left(\left(s \cdot x\right) \cdot \left(\left(x \cdot s\right) \cdot \color{blue}{c}\right)\right)} \]
                  2. Final simplification80.6%

                    \[\leadsto \frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)} \]
                  3. Add Preprocessing

                  Alternative 7: 75.8% accurate, 9.0× speedup?

                  \[\begin{array}{l} \\ \frac{1}{c \cdot \left(\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(x \cdot s\right)\right)} \end{array} \]
                  (FPCore (x c s) :precision binary64 (/ 1.0 (* c (* (* s (* x c)) (* x s)))))
                  double code(double x, double c, double s) {
                  	return 1.0 / (c * ((s * (x * c)) * (x * s)));
                  }
                  
                  real(8) function code(x, c, s)
                      real(8), intent (in) :: x
                      real(8), intent (in) :: c
                      real(8), intent (in) :: s
                      code = 1.0d0 / (c * ((s * (x * c)) * (x * s)))
                  end function
                  
                  public static double code(double x, double c, double s) {
                  	return 1.0 / (c * ((s * (x * c)) * (x * s)));
                  }
                  
                  def code(x, c, s):
                  	return 1.0 / (c * ((s * (x * c)) * (x * s)))
                  
                  function code(x, c, s)
                  	return Float64(1.0 / Float64(c * Float64(Float64(s * Float64(x * c)) * Float64(x * s))))
                  end
                  
                  function tmp = code(x, c, s)
                  	tmp = 1.0 / (c * ((s * (x * c)) * (x * s)));
                  end
                  
                  code[x_, c_, s_] := N[(1.0 / N[(c * N[(N[(s * N[(x * c), $MachinePrecision]), $MachinePrecision] * N[(x * s), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
                  
                  \begin{array}{l}
                  
                  \\
                  \frac{1}{c \cdot \left(\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(x \cdot s\right)\right)}
                  \end{array}
                  
                  Derivation
                  1. Initial program 66.6%

                    \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
                  2. Add Preprocessing
                  3. Taylor expanded in x around 0

                    \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
                  4. Step-by-step derivation
                    1. lower-/.f64N/A

                      \[\leadsto \color{blue}{\frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
                    2. associate-*r*N/A

                      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot {x}^{2}}} \]
                    3. unpow2N/A

                      \[\leadsto \frac{1}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
                    4. associate-*r*N/A

                      \[\leadsto \frac{1}{\color{blue}{\left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right) \cdot x}} \]
                    5. *-commutativeN/A

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

                      \[\leadsto \frac{1}{\color{blue}{x \cdot \left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right)}} \]
                    7. *-commutativeN/A

                      \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
                    8. lower-*.f64N/A

                      \[\leadsto \frac{1}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
                    9. *-commutativeN/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left({s}^{2} \cdot {c}^{2}\right)}\right)} \]
                    10. unpow2N/A

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

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
                    12. lower-*.f64N/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \color{blue}{\left(s \cdot \left(s \cdot {c}^{2}\right)\right)}\right)} \]
                    13. unpow2N/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(s \cdot \color{blue}{\left(c \cdot c\right)}\right)\right)\right)} \]
                    14. associate-*r*N/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(\left(s \cdot c\right) \cdot c\right)}\right)\right)} \]
                    15. *-commutativeN/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
                    16. lower-*.f64N/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \color{blue}{\left(c \cdot \left(s \cdot c\right)\right)}\right)\right)} \]
                    17. *-commutativeN/A

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
                    18. lower-*.f6474.7

                      \[\leadsto \frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \color{blue}{\left(c \cdot s\right)}\right)\right)\right)} \]
                  5. Applied rewrites74.7%

                    \[\leadsto \color{blue}{\frac{1}{x \cdot \left(x \cdot \left(s \cdot \left(c \cdot \left(c \cdot s\right)\right)\right)\right)}} \]
                  6. Step-by-step derivation
                    1. Applied rewrites80.4%

                      \[\leadsto \frac{1}{c \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)\right)}} \]
                    2. Final simplification80.4%

                      \[\leadsto \frac{1}{c \cdot \left(\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(x \cdot s\right)\right)} \]
                    3. Add Preprocessing

                    Reproduce

                    ?
                    herbie shell --seed 2024237 
                    (FPCore (x c s)
                      :name "mixedcos"
                      :precision binary64
                      (/ (cos (* 2.0 x)) (* (pow c 2.0) (* (* x (pow s 2.0)) x))))