mixedcos

Average Error: 28.5 → 2.4

Time: 17.2s

Precision: binary64

Cost: 7888

\[ \begin{array}{c}[c, s] = \mathsf{sort}([c, s])\\ \end{array} \]

Math

\[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]

↓

\[\begin{array}{l} t_0 := s \cdot \left(x \cdot c\right)\\ t_1 := \frac{\cos \left(2 \cdot x\right)}{t_0 \cdot t_0}\\ \mathbf{if}\;x \leq -8.2 \cdot 10^{-9}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;x \leq -1.02 \cdot 10^{-302}:\\ \;\;\;\;{\left(c \cdot \left(x \cdot s\right)\right)}^{-2}\\ \mathbf{elif}\;x \leq 1.55 \cdot 10^{-165}:\\ \;\;\;\;{t_0}^{-2}\\ \mathbf{elif}\;x \leq 8.8 \cdot 10^{+201}:\\ \;\;\;\;\frac{\frac{\cos \left(x + x\right)}{c \cdot s}}{x \cdot \left(x \cdot \left(c \cdot s\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

FPCore

(FPCore (x c s)
 :precision binary64
 (/ (cos (* 2.0 x)) (* (pow c 2.0) (* (* x (pow s 2.0)) x))))

↓

(FPCore (x c s)
 :precision binary64
 (let* ((t_0 (* s (* x c))) (t_1 (/ (cos (* 2.0 x)) (* t_0 t_0))))
   (if (<= x -8.2e-9)
     t_1
     (if (<= x -1.02e-302)
       (pow (* c (* x s)) -2.0)
       (if (<= x 1.55e-165)
         (pow t_0 -2.0)
         (if (<= x 8.8e+201)
           (/ (/ (cos (+ x x)) (* c s)) (* x (* x (* c s))))
           t_1))))))

C

double code(double x, double c, double s) {
	return cos((2.0 * x)) / (pow(c, 2.0) * ((x * pow(s, 2.0)) * x));
}

↓

double code(double x, double c, double s) {
	double t_0 = s * (x * c);
	double t_1 = cos((2.0 * x)) / (t_0 * t_0);
	double tmp;
	if (x <= -8.2e-9) {
		tmp = t_1;
	} else if (x <= -1.02e-302) {
		tmp = pow((c * (x * s)), -2.0);
	} else if (x <= 1.55e-165) {
		tmp = pow(t_0, -2.0);
	} else if (x <= 8.8e+201) {
		tmp = (cos((x + x)) / (c * s)) / (x * (x * (c * s)));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

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

↓

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
    real(8) :: t_1
    real(8) :: tmp
    t_0 = s * (x * c)
    t_1 = cos((2.0d0 * x)) / (t_0 * t_0)
    if (x <= (-8.2d-9)) then
        tmp = t_1
    else if (x <= (-1.02d-302)) then
        tmp = (c * (x * s)) ** (-2.0d0)
    else if (x <= 1.55d-165) then
        tmp = t_0 ** (-2.0d0)
    else if (x <= 8.8d+201) then
        tmp = (cos((x + x)) / (c * s)) / (x * (x * (c * s)))
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

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));
}

↓

public static double code(double x, double c, double s) {
	double t_0 = s * (x * c);
	double t_1 = Math.cos((2.0 * x)) / (t_0 * t_0);
	double tmp;
	if (x <= -8.2e-9) {
		tmp = t_1;
	} else if (x <= -1.02e-302) {
		tmp = Math.pow((c * (x * s)), -2.0);
	} else if (x <= 1.55e-165) {
		tmp = Math.pow(t_0, -2.0);
	} else if (x <= 8.8e+201) {
		tmp = (Math.cos((x + x)) / (c * s)) / (x * (x * (c * s)));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(x, c, s):
	return math.cos((2.0 * x)) / (math.pow(c, 2.0) * ((x * math.pow(s, 2.0)) * x))

↓

def code(x, c, s):
	t_0 = s * (x * c)
	t_1 = math.cos((2.0 * x)) / (t_0 * t_0)
	tmp = 0
	if x <= -8.2e-9:
		tmp = t_1
	elif x <= -1.02e-302:
		tmp = math.pow((c * (x * s)), -2.0)
	elif x <= 1.55e-165:
		tmp = math.pow(t_0, -2.0)
	elif x <= 8.8e+201:
		tmp = (math.cos((x + x)) / (c * s)) / (x * (x * (c * s)))
	else:
		tmp = t_1
	return tmp

Julia

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 code(x, c, s)
	t_0 = Float64(s * Float64(x * c))
	t_1 = Float64(cos(Float64(2.0 * x)) / Float64(t_0 * t_0))
	tmp = 0.0
	if (x <= -8.2e-9)
		tmp = t_1;
	elseif (x <= -1.02e-302)
		tmp = Float64(c * Float64(x * s)) ^ -2.0;
	elseif (x <= 1.55e-165)
		tmp = t_0 ^ -2.0;
	elseif (x <= 8.8e+201)
		tmp = Float64(Float64(cos(Float64(x + x)) / Float64(c * s)) / Float64(x * Float64(x * Float64(c * s))));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp = code(x, c, s)
	tmp = cos((2.0 * x)) / ((c ^ 2.0) * ((x * (s ^ 2.0)) * x));
end

↓

function tmp_2 = code(x, c, s)
	t_0 = s * (x * c);
	t_1 = cos((2.0 * x)) / (t_0 * t_0);
	tmp = 0.0;
	if (x <= -8.2e-9)
		tmp = t_1;
	elseif (x <= -1.02e-302)
		tmp = (c * (x * s)) ^ -2.0;
	elseif (x <= 1.55e-165)
		tmp = t_0 ^ -2.0;
	elseif (x <= 8.8e+201)
		tmp = (cos((x + x)) / (c * s)) / (x * (x * (c * s)));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

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]

↓

code[x_, c_, s_] := Block[{t$95$0 = N[(s * N[(x * c), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[Cos[N[(2.0 * x), $MachinePrecision]], $MachinePrecision] / N[(t$95$0 * t$95$0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[x, -8.2e-9], t$95$1, If[LessEqual[x, -1.02e-302], N[Power[N[(c * N[(x * s), $MachinePrecision]), $MachinePrecision], -2.0], $MachinePrecision], If[LessEqual[x, 1.55e-165], N[Power[t$95$0, -2.0], $MachinePrecision], If[LessEqual[x, 8.8e+201], N[(N[(N[Cos[N[(x + x), $MachinePrecision]], $MachinePrecision] / N[(c * s), $MachinePrecision]), $MachinePrecision] / N[(x * N[(x * N[(c * s), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]]]]

Derivation

1. Split input into 4 regimes

2. if x < -8.2000000000000006e-9 or 8.8e201 < x

   1. Initial program 24.5

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]

   2. Simplified 3.0

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

      [Start] 24.5	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
      *-commutative [=>] 24.5	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]
      associate-*l* [=>] 25.8	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]
      associate-*r* [=>] 26.1	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]
      *-commutative [=>] 26.1	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]
      unpow2 [=>] 26.1	\[ \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot {s}^{2}\right)} \]
      unpow2 [=>] 26.1	\[ \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]
      unswap-sqr [=>] 15.2	\[ \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right)}} \]
      unswap-sqr [=>] 3.0	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot \left(c \cdot s\right)\right) \cdot \left(x \cdot \left(c \cdot s\right)\right)}} \]

   3. Taylor expanded in x around 0 4.9

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

   4. Taylor expanded in x around 0 2.6

      \[\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)} \]

   if -8.2000000000000006e-9 < x < -1.02e-302

   1. Initial program 35.8

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]

   2. Simplified 19.3

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

      [Start] 35.8	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
      associate-*r* [=>] 33.9	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot \left(x \cdot {s}^{2}\right)\right) \cdot x}} \]
      *-commutative [=>] 33.9	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{x \cdot \left({c}^{2} \cdot \left(x \cdot {s}^{2}\right)\right)}} \]
      *-commutative [=>] 33.9	\[ \frac{\cos \left(2 \cdot x\right)}{x \cdot \left({c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot x\right)}\right)} \]
      associate-*r* [=>] 35.3	\[ \frac{\cos \left(2 \cdot x\right)}{x \cdot \color{blue}{\left(\left({c}^{2} \cdot {s}^{2}\right) \cdot x\right)}} \]
      *-commutative [=>] 35.3	\[ \frac{\cos \left(2 \cdot x\right)}{x \cdot \color{blue}{\left(x \cdot \left({c}^{2} \cdot {s}^{2}\right)\right)}} \]
      unpow2 [=>] 35.3	\[ \frac{\cos \left(2 \cdot x\right)}{x \cdot \left(x \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot {s}^{2}\right)\right)} \]
      unpow2 [=>] 35.3	\[ \frac{\cos \left(2 \cdot x\right)}{x \cdot \left(x \cdot \left(\left(c \cdot c\right) \cdot \color{blue}{\left(s \cdot s\right)}\right)\right)} \]
      unswap-sqr [=>] 19.3	\[ \frac{\cos \left(2 \cdot x\right)}{x \cdot \left(x \cdot \color{blue}{\left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right)}\right)} \]

   3. Taylor expanded in x around 0 42.7

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

   4. Simplified 3.8

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

      [Start] 42.7	\[ \frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]
      associate-*r* [=>] 42.2	\[ \frac{1}{\color{blue}{\left({s}^{2} \cdot {c}^{2}\right) \cdot {x}^{2}}} \]
      associate-/r* [=>] 42.2	\[ \color{blue}{\frac{\frac{1}{{s}^{2} \cdot {c}^{2}}}{{x}^{2}}} \]
      *-commutative [<=] 42.2	\[ \frac{\frac{1}{\color{blue}{{c}^{2} \cdot {s}^{2}}}}{{x}^{2}} \]
      unpow2 [=>] 42.2	\[ \frac{\frac{1}{\color{blue}{\left(c \cdot c\right)} \cdot {s}^{2}}}{{x}^{2}} \]
      unpow2 [=>] 42.2	\[ \frac{\frac{1}{\left(c \cdot c\right) \cdot \color{blue}{\left(s \cdot s\right)}}}{{x}^{2}} \]
      swap-sqr [<=] 30.3	\[ \frac{\frac{1}{\color{blue}{\left(c \cdot s\right) \cdot \left(c \cdot s\right)}}}{{x}^{2}} \]
      unpow2 [<=] 30.3	\[ \frac{\frac{1}{\color{blue}{{\left(c \cdot s\right)}^{2}}}}{{x}^{2}} \]
      associate-/l/ [=>] 30.3	\[ \color{blue}{\frac{1}{{x}^{2} \cdot {\left(c \cdot s\right)}^{2}}} \]
      unpow2 [=>] 30.3	\[ \frac{1}{\color{blue}{\left(x \cdot x\right)} \cdot {\left(c \cdot s\right)}^{2}} \]
      unpow2 [=>] 30.3	\[ \frac{1}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right)}} \]
      swap-sqr [<=] 3.5	\[ \frac{1}{\color{blue}{\left(x \cdot \left(c \cdot s\right)\right) \cdot \left(x \cdot \left(c \cdot s\right)\right)}} \]
      unpow2 [<=] 3.5	\[ \frac{1}{\color{blue}{{\left(x \cdot \left(c \cdot s\right)\right)}^{2}}} \]
      *-commutative [=>] 3.5	\[ \frac{1}{{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)}}^{2}} \]
      associate-*l* [=>] 3.8	\[ \frac{1}{{\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}}^{2}} \]

   5. Taylor expanded in c around 0 42.9

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

   6. Simplified 3.6

      \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-2}} \]
      Proof

      [Start] 42.9	\[ \frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)} \]
      unpow2 [=>] 42.9	\[ \frac{1}{\color{blue}{\left(c \cdot c\right)} \cdot \left({s}^{2} \cdot {x}^{2}\right)} \]
      unpow2 [=>] 42.9	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\color{blue}{\left(s \cdot s\right)} \cdot {x}^{2}\right)} \]
      unpow2 [=>] 42.9	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(s \cdot s\right) \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]
      swap-sqr [<=] 26.3	\[ \frac{1}{\left(c \cdot c\right) \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot \left(s \cdot x\right)\right)}} \]
      swap-sqr [<=] 3.8	\[ \frac{1}{\color{blue}{\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(c \cdot \left(s \cdot x\right)\right)}} \]
      associate-/r* [=>] 3.6	\[ \color{blue}{\frac{\frac{1}{c \cdot \left(s \cdot x\right)}}{c \cdot \left(s \cdot x\right)}} \]
      *-lft-identity [<=] 3.6	\[ \frac{\color{blue}{1 \cdot \frac{1}{c \cdot \left(s \cdot x\right)}}}{c \cdot \left(s \cdot x\right)} \]
      associate-*l/ [<=] 3.7	\[ \color{blue}{\frac{1}{c \cdot \left(s \cdot x\right)} \cdot \frac{1}{c \cdot \left(s \cdot x\right)}} \]
      unpow-1 [<=] 3.7	\[ \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \cdot \frac{1}{c \cdot \left(s \cdot x\right)} \]
      unpow-1 [<=] 3.7	\[ {\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]
      pow-sqr [=>] 3.6	\[ \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]
      metadata-eval [=>] 3.6	\[ {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

   if -1.02e-302 < x < 1.54999999999999998e-165

   1. Initial program 46.0

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]

   2. Simplified 40.6

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

      [Start] 46.0	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
      associate-*r* [=>] 40.6	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot \left(x \cdot {s}^{2}\right)\right) \cdot x}} \]
      unpow2 [=>] 40.6	\[ \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(x \cdot {s}^{2}\right)\right) \cdot x} \]
      unpow2 [=>] 40.6	\[ \frac{\cos \left(2 \cdot x\right)}{\left(\left(c \cdot c\right) \cdot \left(x \cdot \color{blue}{\left(s \cdot s\right)}\right)\right) \cdot x} \]

   3. Taylor expanded in x around 0 64.0

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

   4. Simplified 31.8

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

      [Start] 64.0	\[ \frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]
      associate-*r* [=>] 64.0	\[ \frac{1}{\color{blue}{\left({s}^{2} \cdot {c}^{2}\right) \cdot {x}^{2}}} \]
      *-commutative [<=] 64.0	\[ \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right)} \cdot {x}^{2}} \]
      associate-*r* [<=] 64.0	\[ \frac{1}{\color{blue}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)}} \]
      unpow2 [=>] 64.0	\[ \frac{1}{\color{blue}{\left(c \cdot c\right)} \cdot \left({s}^{2} \cdot {x}^{2}\right)} \]
      sqr-pow [=>] 64.0	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\color{blue}{\left({s}^{\left(\frac{2}{2}\right)} \cdot {s}^{\left(\frac{2}{2}\right)}\right)} \cdot {x}^{2}\right)} \]
      unpow2 [=>] 64.0	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left({s}^{\left(\frac{2}{2}\right)} \cdot {s}^{\left(\frac{2}{2}\right)}\right) \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]
      unswap-sqr [=>] 29.1	\[ \frac{1}{\left(c \cdot c\right) \cdot \color{blue}{\left(\left({s}^{\left(\frac{2}{2}\right)} \cdot x\right) \cdot \left({s}^{\left(\frac{2}{2}\right)} \cdot x\right)\right)}} \]
      metadata-eval [=>] 29.1	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left({s}^{\color{blue}{1}} \cdot x\right) \cdot \left({s}^{\left(\frac{2}{2}\right)} \cdot x\right)\right)} \]
      unpow1 [=>] 29.1	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(\color{blue}{s} \cdot x\right) \cdot \left({s}^{\left(\frac{2}{2}\right)} \cdot x\right)\right)} \]
      rem-square-sqrt [<=] 29.9	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(s \cdot \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)}\right) \cdot \left({s}^{\left(\frac{2}{2}\right)} \cdot x\right)\right)} \]
      metadata-eval [=>] 29.9	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(s \cdot \left(\sqrt{x} \cdot \sqrt{x}\right)\right) \cdot \left({s}^{\color{blue}{1}} \cdot x\right)\right)} \]
      unpow1 [=>] 29.9	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(s \cdot \left(\sqrt{x} \cdot \sqrt{x}\right)\right) \cdot \left(\color{blue}{s} \cdot x\right)\right)} \]
      rem-square-sqrt [<=] 30.0	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(s \cdot \left(\sqrt{x} \cdot \sqrt{x}\right)\right) \cdot \left(s \cdot \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)}\right)\right)} \]
      associate-*l* [<=] 30.0	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\color{blue}{\left(\left(s \cdot \sqrt{x}\right) \cdot \sqrt{x}\right)} \cdot \left(s \cdot \left(\sqrt{x} \cdot \sqrt{x}\right)\right)\right)} \]
      associate-*l* [<=] 30.0	\[ \frac{1}{\left(c \cdot c\right) \cdot \left(\left(\left(s \cdot \sqrt{x}\right) \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\left(s \cdot \sqrt{x}\right) \cdot \sqrt{x}\right)}\right)} \]

   5. Taylor expanded in c around 0 64.0

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

   6. Simplified 5.1

      \[\leadsto \color{blue}{{\left(s \cdot \left(c \cdot x\right)\right)}^{-2}} \]
      Proof

      [Start] 64.0	\[ \frac{1}{{c}^{2} \cdot \left({s}^{2} \cdot {x}^{2}\right)} \]
      associate-/r* [=>] 64.0	\[ \color{blue}{\frac{\frac{1}{{c}^{2}}}{{s}^{2} \cdot {x}^{2}}} \]
      unpow2 [=>] 64.0	\[ \frac{\frac{1}{\color{blue}{c \cdot c}}}{{s}^{2} \cdot {x}^{2}} \]
      associate-/r* [=>] 64.0	\[ \frac{\color{blue}{\frac{\frac{1}{c}}{c}}}{{s}^{2} \cdot {x}^{2}} \]
      *-lft-identity [<=] 64.0	\[ \frac{\frac{\color{blue}{1 \cdot \frac{1}{c}}}{c}}{{s}^{2} \cdot {x}^{2}} \]
      associate-*l/ [<=] 64.0	\[ \frac{\color{blue}{\frac{1}{c} \cdot \frac{1}{c}}}{{s}^{2} \cdot {x}^{2}} \]
      *-commutative [=>] 64.0	\[ \frac{\frac{1}{c} \cdot \frac{1}{c}}{\color{blue}{{x}^{2} \cdot {s}^{2}}} \]
      unpow2 [=>] 64.0	\[ \frac{\frac{1}{c} \cdot \frac{1}{c}}{{x}^{2} \cdot \color{blue}{\left(s \cdot s\right)}} \]
      unpow2 [=>] 64.0	\[ \frac{\frac{1}{c} \cdot \frac{1}{c}}{\color{blue}{\left(x \cdot x\right)} \cdot \left(s \cdot s\right)} \]
      swap-sqr [<=] 29.1	\[ \frac{\frac{1}{c} \cdot \frac{1}{c}}{\color{blue}{\left(x \cdot s\right) \cdot \left(x \cdot s\right)}} \]
      times-frac [=>] 4.5	\[ \color{blue}{\frac{\frac{1}{c}}{x \cdot s} \cdot \frac{\frac{1}{c}}{x \cdot s}} \]
      associate-/r* [<=] 4.4	\[ \color{blue}{\frac{1}{c \cdot \left(x \cdot s\right)}} \cdot \frac{\frac{1}{c}}{x \cdot s} \]
      unpow-1 [<=] 4.4	\[ \color{blue}{{\left(c \cdot \left(x \cdot s\right)\right)}^{-1}} \cdot \frac{\frac{1}{c}}{x \cdot s} \]
      associate-/r* [<=] 4.6	\[ {\left(c \cdot \left(x \cdot s\right)\right)}^{-1} \cdot \color{blue}{\frac{1}{c \cdot \left(x \cdot s\right)}} \]
      unpow-1 [<=] 4.6	\[ {\left(c \cdot \left(x \cdot s\right)\right)}^{-1} \cdot \color{blue}{{\left(c \cdot \left(x \cdot s\right)\right)}^{-1}} \]
      pow-sqr [=>] 4.4	\[ \color{blue}{{\left(c \cdot \left(x \cdot s\right)\right)}^{\left(2 \cdot -1\right)}} \]
      associate-*r* [=>] 5.1	\[ {\color{blue}{\left(\left(c \cdot x\right) \cdot s\right)}}^{\left(2 \cdot -1\right)} \]
      *-commutative [=>] 5.1	\[ {\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}}^{\left(2 \cdot -1\right)} \]
      metadata-eval [=>] 5.1	\[ {\left(s \cdot \left(c \cdot x\right)\right)}^{\color{blue}{-2}} \]

   if 1.54999999999999998e-165 < x < 8.8e201

   1. Initial program 25.7

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]

   2. Simplified 0.9

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

      [Start] 25.7	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
      *-commutative [=>] 25.7	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]
      associate-*l* [=>] 26.5	\[ \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]
      associate-*r* [=>] 26.4	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]
      *-commutative [=>] 26.4	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]
      unpow2 [=>] 26.4	\[ \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot {s}^{2}\right)} \]
      unpow2 [=>] 26.4	\[ \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]
      unswap-sqr [=>] 10.4	\[ \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right)}} \]
      unswap-sqr [=>] 0.9	\[ \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot \left(c \cdot s\right)\right) \cdot \left(x \cdot \left(c \cdot s\right)\right)}} \]

   3. Taylor expanded in x around 0 2.9

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

   4. Applied egg-rr 2.5

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

   5. Applied egg-rr 1.0

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

4. Final simplification 2.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -8.2 \cdot 10^{-9}:\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)}\\ \mathbf{elif}\;x \leq -1.02 \cdot 10^{-302}:\\ \;\;\;\;{\left(c \cdot \left(x \cdot s\right)\right)}^{-2}\\ \mathbf{elif}\;x \leq 1.55 \cdot 10^{-165}:\\ \;\;\;\;{\left(s \cdot \left(x \cdot c\right)\right)}^{-2}\\ \mathbf{elif}\;x \leq 8.8 \cdot 10^{+201}:\\ \;\;\;\;\frac{\frac{\cos \left(x + x\right)}{c \cdot s}}{x \cdot \left(x \cdot \left(c \cdot s\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)}\\ \end{array} \]

Alternatives

Alternative 1
Error	0.9
Cost	53380

\[\begin{array}{l} t_0 := \cos \left(x + x\right)\\ t_1 := c \cdot \left(x \cdot s\right)\\ \mathbf{if}\;\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(x \cdot \left(x \cdot {s}^{2}\right)\right)} \leq \infty:\\ \;\;\;\;\frac{\sqrt[3]{{t_0}^{2}}}{t_1} \cdot \frac{\sqrt[3]{t_0}}{t_1}\\ \mathbf{else}:\\ \;\;\;\;t_0 \cdot \frac{\frac{\frac{1}{x}}{c \cdot s}}{x \cdot \left(c \cdot s\right)}\\ \end{array} \]

Alternative 2
Error	2.3
Cost	13572

\[\begin{array}{l} t_0 := \cos \left(x + x\right)\\ \mathbf{if}\;s \leq 5 \cdot 10^{+211}:\\ \;\;\;\;t_0 \cdot {\left(s \cdot \left(x \cdot c\right)\right)}^{-2}\\ \mathbf{else}:\\ \;\;\;\;t_0 \cdot \frac{\frac{\frac{1}{x}}{c \cdot s}}{x \cdot \left(c \cdot s\right)}\\ \end{array} \]

Alternative 3
Error	12.3
Cost	7888

\[\begin{array}{l} t_0 := \frac{\cos \left(2 \cdot x\right)}{x \cdot \left(c \cdot \left(c \cdot \left(x \cdot \left(s \cdot s\right)\right)\right)\right)}\\ t_1 := s \cdot \left(x \cdot c\right)\\ t_2 := \frac{1}{c \cdot \left(x \cdot s\right)}\\ \mathbf{if}\;s \leq -1.4 \cdot 10^{+26}:\\ \;\;\;\;\frac{1}{t_1} \cdot t_2\\ \mathbf{elif}\;s \leq -1.6 \cdot 10^{-158}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;s \leq 3.1 \cdot 10^{-114}:\\ \;\;\;\;{t_1}^{-2}\\ \mathbf{elif}\;s \leq 3.2 \cdot 10^{+101}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;t_2 \cdot t_2\\ \end{array} \]

Alternative 4
Error	2.5
Cost	7884

\[\begin{array}{l} t_0 := s \cdot \left(x \cdot c\right)\\ t_1 := x \cdot \left(c \cdot s\right)\\ \mathbf{if}\;x \leq -3.5 \cdot 10^{-9}:\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{t_0 \cdot t_0}\\ \mathbf{elif}\;x \leq -8.6 \cdot 10^{-304}:\\ \;\;\;\;{\left(c \cdot \left(x \cdot s\right)\right)}^{-2}\\ \mathbf{elif}\;x \leq 3.05 \cdot 10^{-161}:\\ \;\;\;\;{t_0}^{-2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos \left(x + x\right)}{t_1} \cdot \frac{1}{t_1}\\ \end{array} \]

Alternative 5
Error	6.6
Cost	7625

\[\begin{array}{l} \mathbf{if}\;x \leq -2 \cdot 10^{-13} \lor \neg \left(x \leq 1.2 \cdot 10^{-10}\right):\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{x \cdot \left(c \cdot \left(s \cdot \left(s \cdot \left(x \cdot c\right)\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;{\left(c \cdot \left(x \cdot s\right)\right)}^{-2}\\ \end{array} \]

Alternative 6
Error	6.7
Cost	7624

\[\begin{array}{l} t_0 := c \cdot \left(x \cdot s\right)\\ t_1 := \cos \left(2 \cdot x\right)\\ \mathbf{if}\;x \leq -2 \cdot 10^{-13}:\\ \;\;\;\;\frac{t_1}{x \cdot \left(c \cdot \left(s \cdot \left(s \cdot \left(x \cdot c\right)\right)\right)\right)}\\ \mathbf{elif}\;x \leq 3.35 \cdot 10^{-28}:\\ \;\;\;\;{t_0}^{-2}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_1}{x \cdot \left(s \cdot \left(c \cdot t_0\right)\right)}\\ \end{array} \]

Alternative 7
Error	2.3
Cost	7620

\[\begin{array}{l} t_0 := x \cdot \left(c \cdot s\right)\\ t_1 := \cos \left(x + x\right)\\ \mathbf{if}\;s \leq 2.05 \cdot 10^{+211}:\\ \;\;\;\;\frac{\frac{t_1}{s}}{x \cdot c} \cdot \frac{1}{s \cdot \left(x \cdot c\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_1}{t_0} \cdot \frac{1}{t_0}\\ \end{array} \]

Alternative 8
Error	2.3
Cost	7620

\[\begin{array}{l} t_0 := \cos \left(x + x\right)\\ \mathbf{if}\;s \leq 3.9 \cdot 10^{+213}:\\ \;\;\;\;\frac{\frac{t_0}{s}}{x \cdot c} \cdot \frac{1}{s \cdot \left(x \cdot c\right)}\\ \mathbf{else}:\\ \;\;\;\;t_0 \cdot \frac{\frac{\frac{1}{x}}{c \cdot s}}{x \cdot \left(c \cdot s\right)}\\ \end{array} \]

Alternative 9
Error	2.8
Cost	7492

\[\begin{array}{l} t_0 := s \cdot \left(x \cdot c\right)\\ \mathbf{if}\;s \leq 8 \cdot 10^{+261}:\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{t_0 \cdot t_0}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{c \cdot \left(\left(x \cdot s\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)\right)}\\ \end{array} \]

Alternative 10
Error	2.9
Cost	7492

\[\begin{array}{l} t_0 := \cos \left(2 \cdot x\right)\\ t_1 := s \cdot \left(x \cdot c\right)\\ \mathbf{if}\;s \leq 2 \cdot 10^{+211}:\\ \;\;\;\;\frac{t_0}{t_1 \cdot t_1}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{\left(c \cdot \left(x \cdot s\right)\right) \cdot \left(x \cdot \left(c \cdot s\right)\right)}\\ \end{array} \]

Alternative 11
Error	2.5
Cost	7492

\[\begin{array}{l} t_0 := x \cdot \left(c \cdot s\right)\\ t_1 := \cos \left(2 \cdot x\right)\\ t_2 := s \cdot \left(x \cdot c\right)\\ \mathbf{if}\;s \leq 8 \cdot 10^{+210}:\\ \;\;\;\;\frac{t_1}{t_2 \cdot t_2}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_1}{t_0 \cdot t_0}\\ \end{array} \]

Alternative 12
Error	16.4
Cost	6784

\[{\left(c \cdot \left(x \cdot s\right)\right)}^{-2} \]

Alternative 13
Error	23.1
Cost	1097

\[\begin{array}{l} \mathbf{if}\;x \leq -2.05 \cdot 10^{-78} \lor \neg \left(x \leq -8.2 \cdot 10^{-137}\right):\\ \;\;\;\;\frac{1}{\left(c \cdot s\right) \cdot \left(c \cdot \left(x \cdot \left(x \cdot s\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\left(c \cdot s\right) \cdot \left(s \cdot \left(c \cdot \left(x \cdot x\right)\right)\right)}\\ \end{array} \]

Alternative 14
Error	16.2
Cost	1096

\[\begin{array}{l} t_0 := c \cdot \left(x \cdot s\right)\\ t_1 := \frac{1}{t_0}\\ \mathbf{if}\;s \leq 5.4 \cdot 10^{-177}:\\ \;\;\;\;t_1 \cdot t_1\\ \mathbf{elif}\;s \leq 2.1 \cdot 10^{+44}:\\ \;\;\;\;\frac{\frac{1}{x \cdot c}}{s \cdot \left(x \cdot \left(c \cdot s\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{t_0 \cdot t_0}\\ \end{array} \]

Alternative 15
Error	28.2
Cost	832

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

Alternative 16
Error	23.1
Cost	832

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

Alternative 17
Error	19.6
Cost	832

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

Alternative 18
Error	16.4
Cost	832

\[\begin{array}{l} t_0 := c \cdot \left(x \cdot s\right)\\ \frac{1}{t_0 \cdot t_0} \end{array} \]

Reproduce

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