Codec.Picture.Jpg.FastDct:referenceDct from JuicyPixels-3.2.6.1

Percentage Accurate: 27.7% → 32.0%
Time: 16.4s
Alternatives: 10
Speedup: 24.5×

Specification

?
\[\begin{array}{l} \\ \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \end{array} \]
(FPCore (x y z t a b)
 :precision binary64
 (*
  (* x (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0)))
  (cos (/ (* (* (+ (* a 2.0) 1.0) b) t) 16.0))))
double code(double x, double y, double z, double t, double a, double b) {
	return (x * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * cos((((((a * 2.0) + 1.0) * b) * t) / 16.0));
}
real(8) function code(x, y, z, t, a, b)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = (x * cos((((((y * 2.0d0) + 1.0d0) * z) * t) / 16.0d0))) * cos((((((a * 2.0d0) + 1.0d0) * b) * t) / 16.0d0))
end function
public static double code(double x, double y, double z, double t, double a, double b) {
	return (x * Math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * Math.cos((((((a * 2.0) + 1.0) * b) * t) / 16.0));
}
def code(x, y, z, t, a, b):
	return (x * math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * math.cos((((((a * 2.0) + 1.0) * b) * t) / 16.0))
function code(x, y, z, t, a, b)
	return Float64(Float64(x * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * cos(Float64(Float64(Float64(Float64(Float64(a * 2.0) + 1.0) * b) * t) / 16.0)))
end
function tmp = code(x, y, z, t, a, b)
	tmp = (x * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * cos((((((a * 2.0) + 1.0) * b) * t) / 16.0));
end
code[x_, y_, z_, t_, a_, b_] := N[(N[(x * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Cos[N[(N[(N[(N[(N[(a * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * b), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\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 10 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: 27.7% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \end{array} \]
(FPCore (x y z t a b)
 :precision binary64
 (*
  (* x (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0)))
  (cos (/ (* (* (+ (* a 2.0) 1.0) b) t) 16.0))))
double code(double x, double y, double z, double t, double a, double b) {
	return (x * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * cos((((((a * 2.0) + 1.0) * b) * t) / 16.0));
}
real(8) function code(x, y, z, t, a, b)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = (x * cos((((((y * 2.0d0) + 1.0d0) * z) * t) / 16.0d0))) * cos((((((a * 2.0d0) + 1.0d0) * b) * t) / 16.0d0))
end function
public static double code(double x, double y, double z, double t, double a, double b) {
	return (x * Math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * Math.cos((((((a * 2.0) + 1.0) * b) * t) / 16.0));
}
def code(x, y, z, t, a, b):
	return (x * math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * math.cos((((((a * 2.0) + 1.0) * b) * t) / 16.0))
function code(x, y, z, t, a, b)
	return Float64(Float64(x * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * cos(Float64(Float64(Float64(Float64(Float64(a * 2.0) + 1.0) * b) * t) / 16.0)))
end
function tmp = code(x, y, z, t, a, b)
	tmp = (x * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * cos((((((a * 2.0) + 1.0) * b) * t) / 16.0));
end
code[x_, y_, z_, t_, a_, b_] := N[(N[(x * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Cos[N[(N[(N[(N[(N[(a * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * b), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right)
\end{array}

Alternative 1: 32.0% accurate, 0.3× speedup?

\[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \left(\left(2 \cdot a\right) \cdot b\right) \cdot \left(t \cdot 0.0625\right)\\ t_2 := x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\\ t_3 := t \cdot \left(b \cdot 0.0625\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t\_2 \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+89}:\\ \;\;\;\;t\_2 \cdot \left(\cos t\_1 \cdot \cos t\_3 - \sin t\_1 \cdot \sin t\_3\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m y z t a b)
 :precision binary64
 (let* ((t_1 (* (* (* 2.0 a) b) (* t 0.0625)))
        (t_2 (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))))
        (t_3 (* t (* b 0.0625))))
   (*
    x_s
    (if (<= (* t_2 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))) 1e+89)
      (* t_2 (- (* (cos t_1) (cos t_3)) (* (sin t_1) (sin t_3))))
      (* (* x_m 1.0) 1.0)))))
x\_m = fabs(x);
x\_s = copysign(1.0, x);
double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
	double t_1 = ((2.0 * a) * b) * (t * 0.0625);
	double t_2 = x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0));
	double t_3 = t * (b * 0.0625);
	double tmp;
	if ((t_2 * cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))) <= 1e+89) {
		tmp = t_2 * ((cos(t_1) * cos(t_3)) - (sin(t_1) * sin(t_3)));
	} else {
		tmp = (x_m * 1.0) * 1.0;
	}
	return x_s * tmp;
}
x\_m = abs(x)
x\_s = copysign(1.0d0, x)
real(8) function code(x_s, x_m, y, z, t, a, b)
    real(8), intent (in) :: x_s
    real(8), intent (in) :: x_m
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: t_3
    real(8) :: tmp
    t_1 = ((2.0d0 * a) * b) * (t * 0.0625d0)
    t_2 = x_m * cos((((((y * 2.0d0) + 1.0d0) * z) * t) / 16.0d0))
    t_3 = t * (b * 0.0625d0)
    if ((t_2 * cos(((t * ((1.0d0 + (2.0d0 * a)) * b)) / 16.0d0))) <= 1d+89) then
        tmp = t_2 * ((cos(t_1) * cos(t_3)) - (sin(t_1) * sin(t_3)))
    else
        tmp = (x_m * 1.0d0) * 1.0d0
    end if
    code = x_s * tmp
end function
x\_m = Math.abs(x);
x\_s = Math.copySign(1.0, x);
public static double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
	double t_1 = ((2.0 * a) * b) * (t * 0.0625);
	double t_2 = x_m * Math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0));
	double t_3 = t * (b * 0.0625);
	double tmp;
	if ((t_2 * Math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))) <= 1e+89) {
		tmp = t_2 * ((Math.cos(t_1) * Math.cos(t_3)) - (Math.sin(t_1) * Math.sin(t_3)));
	} else {
		tmp = (x_m * 1.0) * 1.0;
	}
	return x_s * tmp;
}
x\_m = math.fabs(x)
x\_s = math.copysign(1.0, x)
def code(x_s, x_m, y, z, t, a, b):
	t_1 = ((2.0 * a) * b) * (t * 0.0625)
	t_2 = x_m * math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))
	t_3 = t * (b * 0.0625)
	tmp = 0
	if (t_2 * math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))) <= 1e+89:
		tmp = t_2 * ((math.cos(t_1) * math.cos(t_3)) - (math.sin(t_1) * math.sin(t_3)))
	else:
		tmp = (x_m * 1.0) * 1.0
	return x_s * tmp
x\_m = abs(x)
x\_s = copysign(1.0, x)
function code(x_s, x_m, y, z, t, a, b)
	t_1 = Float64(Float64(Float64(2.0 * a) * b) * Float64(t * 0.0625))
	t_2 = Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0)))
	t_3 = Float64(t * Float64(b * 0.0625))
	tmp = 0.0
	if (Float64(t_2 * cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))) <= 1e+89)
		tmp = Float64(t_2 * Float64(Float64(cos(t_1) * cos(t_3)) - Float64(sin(t_1) * sin(t_3))));
	else
		tmp = Float64(Float64(x_m * 1.0) * 1.0);
	end
	return Float64(x_s * tmp)
end
x\_m = abs(x);
x\_s = sign(x) * abs(1.0);
function tmp_2 = code(x_s, x_m, y, z, t, a, b)
	t_1 = ((2.0 * a) * b) * (t * 0.0625);
	t_2 = x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0));
	t_3 = t * (b * 0.0625);
	tmp = 0.0;
	if ((t_2 * cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))) <= 1e+89)
		tmp = t_2 * ((cos(t_1) * cos(t_3)) - (sin(t_1) * sin(t_3)));
	else
		tmp = (x_m * 1.0) * 1.0;
	end
	tmp_2 = x_s * tmp;
end
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(N[(2.0 * a), $MachinePrecision] * b), $MachinePrecision] * N[(t * 0.0625), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(t * N[(b * 0.0625), $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(t$95$2 * N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], 1e+89], N[(t$95$2 * N[(N[(N[Cos[t$95$1], $MachinePrecision] * N[Cos[t$95$3], $MachinePrecision]), $MachinePrecision] - N[(N[Sin[t$95$1], $MachinePrecision] * N[Sin[t$95$3], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]]]
\begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
\begin{array}{l}
t_1 := \left(\left(2 \cdot a\right) \cdot b\right) \cdot \left(t \cdot 0.0625\right)\\
t_2 := x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\\
t_3 := t \cdot \left(b \cdot 0.0625\right)\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;t\_2 \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+89}:\\
\;\;\;\;t\_2 \cdot \left(\cos t\_1 \cdot \cos t\_3 - \sin t\_1 \cdot \sin t\_3\right)\\

\mathbf{else}:\\
\;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\


\end{array}
\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 9.99999999999999995e88

    1. Initial program 41.5%

      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-cos.f64N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \color{blue}{\cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right)} \]
      2. lift-/.f64N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right)} \]
      3. lift-*.f64N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\color{blue}{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}}{16}\right) \]
      4. associate-/l*N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot \frac{t}{16}\right)} \]
      5. *-commutativeN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\frac{t}{16} \cdot \left(\left(a \cdot 2 + 1\right) \cdot b\right)\right)} \]
      6. lift-*.f64N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t}{16} \cdot \color{blue}{\left(\left(a \cdot 2 + 1\right) \cdot b\right)}\right) \]
      7. *-commutativeN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t}{16} \cdot \color{blue}{\left(b \cdot \left(a \cdot 2 + 1\right)\right)}\right) \]
      8. lift-+.f64N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t}{16} \cdot \left(b \cdot \color{blue}{\left(a \cdot 2 + 1\right)}\right)\right) \]
      9. distribute-lft-inN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t}{16} \cdot \color{blue}{\left(b \cdot \left(a \cdot 2\right) + b \cdot 1\right)}\right) \]
      10. *-rgt-identityN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t}{16} \cdot \left(b \cdot \left(a \cdot 2\right) + \color{blue}{b}\right)\right) \]
      11. distribute-rgt-inN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\left(b \cdot \left(a \cdot 2\right)\right) \cdot \frac{t}{16} + b \cdot \frac{t}{16}\right)} \]
      12. *-commutativeN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\color{blue}{\left(\left(a \cdot 2\right) \cdot b\right)} \cdot \frac{t}{16} + b \cdot \frac{t}{16}\right) \]
      13. cos-sumN/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \color{blue}{\left(\cos \left(\left(\left(a \cdot 2\right) \cdot b\right) \cdot \frac{t}{16}\right) \cdot \cos \left(b \cdot \frac{t}{16}\right) - \sin \left(\left(\left(a \cdot 2\right) \cdot b\right) \cdot \frac{t}{16}\right) \cdot \sin \left(b \cdot \frac{t}{16}\right)\right)} \]
      14. lower--.f64N/A

        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \color{blue}{\left(\cos \left(\left(\left(a \cdot 2\right) \cdot b\right) \cdot \frac{t}{16}\right) \cdot \cos \left(b \cdot \frac{t}{16}\right) - \sin \left(\left(\left(a \cdot 2\right) \cdot b\right) \cdot \frac{t}{16}\right) \cdot \sin \left(b \cdot \frac{t}{16}\right)\right)} \]
    4. Applied rewrites41.7%

      \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \color{blue}{\left(\cos \left(\left(\left(2 \cdot a\right) \cdot b\right) \cdot \left(t \cdot 0.0625\right)\right) \cdot \cos \left(t \cdot \left(b \cdot 0.0625\right)\right) - \sin \left(\left(\left(2 \cdot a\right) \cdot b\right) \cdot \left(t \cdot 0.0625\right)\right) \cdot \sin \left(t \cdot \left(b \cdot 0.0625\right)\right)\right)} \]

    if 9.99999999999999995e88 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

    1. Initial program 10.2%

      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
    2. Add Preprocessing
    3. Taylor expanded in z around 0

      \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
    4. Step-by-step derivation
      1. Applied rewrites14.0%

        \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
      2. Taylor expanded in b around 0

        \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
      3. Step-by-step derivation
        1. Applied rewrites18.8%

          \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
      4. Recombined 2 regimes into one program.
      5. Final simplification28.9%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+89}:\\ \;\;\;\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \left(\cos \left(\left(\left(2 \cdot a\right) \cdot b\right) \cdot \left(t \cdot 0.0625\right)\right) \cdot \cos \left(t \cdot \left(b \cdot 0.0625\right)\right) - \sin \left(\left(\left(2 \cdot a\right) \cdot b\right) \cdot \left(t \cdot 0.0625\right)\right) \cdot \sin \left(t \cdot \left(b \cdot 0.0625\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
      6. Add Preprocessing

      Alternative 2: 32.2% accurate, 0.5× speedup?

      \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\ \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(\frac{t \cdot \left(z \cdot \left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\mathsf{fma}\left(y, 2, -1\right)}\right)\right)\right)}{16}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
      x\_m = (fabs.f64 x)
      x\_s = (copysign.f64 #s(literal 1 binary64) x)
      (FPCore (x_s x_m y z t a b)
       :precision binary64
       (let* ((t_1 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))))
         (*
          x_s
          (if (<=
               (* (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) t_1)
               1e+306)
            (*
             t_1
             (*
              x_m
              (cos
               (/
                (*
                 t
                 (*
                  z
                  (* (fma y 2.0 1.0) (* (fma y 2.0 -1.0) (/ 1.0 (fma y 2.0 -1.0))))))
                16.0))))
            (* (* x_m 1.0) 1.0)))))
      x\_m = fabs(x);
      x\_s = copysign(1.0, x);
      double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
      	double t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
      	double tmp;
      	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
      		tmp = t_1 * (x_m * cos(((t * (z * (fma(y, 2.0, 1.0) * (fma(y, 2.0, -1.0) * (1.0 / fma(y, 2.0, -1.0)))))) / 16.0)));
      	} else {
      		tmp = (x_m * 1.0) * 1.0;
      	}
      	return x_s * tmp;
      }
      
      x\_m = abs(x)
      x\_s = copysign(1.0, x)
      function code(x_s, x_m, y, z, t, a, b)
      	t_1 = cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))
      	tmp = 0.0
      	if (Float64(Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
      		tmp = Float64(t_1 * Float64(x_m * cos(Float64(Float64(t * Float64(z * Float64(fma(y, 2.0, 1.0) * Float64(fma(y, 2.0, -1.0) * Float64(1.0 / fma(y, 2.0, -1.0)))))) / 16.0))));
      	else
      		tmp = Float64(Float64(x_m * 1.0) * 1.0);
      	end
      	return Float64(x_s * tmp)
      end
      
      x\_m = N[Abs[x], $MachinePrecision]
      x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * t$95$1), $MachinePrecision], 1e+306], N[(t$95$1 * N[(x$95$m * N[Cos[N[(N[(t * N[(z * N[(N[(y * 2.0 + 1.0), $MachinePrecision] * N[(N[(y * 2.0 + -1.0), $MachinePrecision] * N[(1.0 / N[(y * 2.0 + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
      
      \begin{array}{l}
      x\_m = \left|x\right|
      \\
      x\_s = \mathsf{copysign}\left(1, x\right)
      
      \\
      \begin{array}{l}
      t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\
      x\_s \cdot \begin{array}{l}
      \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\
      \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(\frac{t \cdot \left(z \cdot \left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\mathsf{fma}\left(y, 2, -1\right)}\right)\right)\right)}{16}\right)\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
      
      
      \end{array}
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 1.00000000000000002e306

        1. Initial program 43.8%

          \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-+.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\color{blue}{\left(y \cdot 2 + 1\right)} \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          2. flip-+N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\color{blue}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) - 1 \cdot 1}{y \cdot 2 - 1}} \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          3. div-invN/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\color{blue}{\left(\left(\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) - 1 \cdot 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)} \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          4. metadata-evalN/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\left(\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) - \color{blue}{1}\right) \cdot \frac{1}{y \cdot 2 - 1}\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          5. difference-of-sqr-1N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\color{blue}{\left(\left(y \cdot 2 + 1\right) \cdot \left(y \cdot 2 - 1\right)\right)} \cdot \frac{1}{y \cdot 2 - 1}\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          6. lift-+.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\left(\color{blue}{\left(y \cdot 2 + 1\right)} \cdot \left(y \cdot 2 - 1\right)\right) \cdot \frac{1}{y \cdot 2 - 1}\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          7. associate-*l*N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\color{blue}{\left(\left(y \cdot 2 + 1\right) \cdot \left(\left(y \cdot 2 - 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right)} \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          8. lower-*.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\color{blue}{\left(\left(y \cdot 2 + 1\right) \cdot \left(\left(y \cdot 2 - 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right)} \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          9. lift-+.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\color{blue}{\left(y \cdot 2 + 1\right)} \cdot \left(\left(y \cdot 2 - 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          10. lift-*.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\left(\color{blue}{y \cdot 2} + 1\right) \cdot \left(\left(y \cdot 2 - 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          11. lower-fma.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\color{blue}{\mathsf{fma}\left(y, 2, 1\right)} \cdot \left(\left(y \cdot 2 - 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          12. lower-*.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \color{blue}{\left(\left(y \cdot 2 - 1\right) \cdot \frac{1}{y \cdot 2 - 1}\right)}\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          13. sub-negN/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\color{blue}{\left(y \cdot 2 + \left(\mathsf{neg}\left(1\right)\right)\right)} \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          14. lift-*.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\left(\color{blue}{y \cdot 2} + \left(\mathsf{neg}\left(1\right)\right)\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          15. metadata-evalN/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\left(y \cdot 2 + \color{blue}{-1}\right) \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          16. lower-fma.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\color{blue}{\mathsf{fma}\left(y, 2, -1\right)} \cdot \frac{1}{y \cdot 2 - 1}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          17. lower-/.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \color{blue}{\frac{1}{y \cdot 2 - 1}}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          18. sub-negN/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\color{blue}{y \cdot 2 + \left(\mathsf{neg}\left(1\right)\right)}}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          19. lift-*.f64N/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\color{blue}{y \cdot 2} + \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          20. metadata-evalN/A

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{y \cdot 2 + \color{blue}{-1}}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          21. lower-fma.f6443.9

            \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\color{blue}{\mathsf{fma}\left(y, 2, -1\right)}}\right)\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
        4. Applied rewrites43.9%

          \[\leadsto \left(x \cdot \cos \left(\frac{\left(\color{blue}{\left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\mathsf{fma}\left(y, 2, -1\right)}\right)\right)} \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]

        if 1.00000000000000002e306 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

        1. Initial program 0.8%

          \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
        2. Add Preprocessing
        3. Taylor expanded in z around 0

          \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
        4. Step-by-step derivation
          1. Applied rewrites5.9%

            \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
          2. Taylor expanded in b around 0

            \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
          3. Step-by-step derivation
            1. Applied rewrites11.6%

              \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
          4. Recombined 2 regimes into one program.
          5. Final simplification29.0%

            \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+306}:\\ \;\;\;\;\cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \cdot \left(x \cdot \cos \left(\frac{t \cdot \left(z \cdot \left(\mathsf{fma}\left(y, 2, 1\right) \cdot \left(\mathsf{fma}\left(y, 2, -1\right) \cdot \frac{1}{\mathsf{fma}\left(y, 2, -1\right)}\right)\right)\right)}{16}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
          6. Add Preprocessing

          Alternative 3: 32.1% accurate, 0.5× speedup?

          \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\ \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(\frac{z \cdot t}{16 \cdot \frac{1}{\mathsf{fma}\left(y, 2, 1\right)}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
          x\_m = (fabs.f64 x)
          x\_s = (copysign.f64 #s(literal 1 binary64) x)
          (FPCore (x_s x_m y z t a b)
           :precision binary64
           (let* ((t_1 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))))
             (*
              x_s
              (if (<=
                   (* (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) t_1)
                   1e+306)
                (* t_1 (* x_m (cos (/ (* z t) (* 16.0 (/ 1.0 (fma y 2.0 1.0)))))))
                (* (* x_m 1.0) 1.0)))))
          x\_m = fabs(x);
          x\_s = copysign(1.0, x);
          double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
          	double t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
          	double tmp;
          	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
          		tmp = t_1 * (x_m * cos(((z * t) / (16.0 * (1.0 / fma(y, 2.0, 1.0))))));
          	} else {
          		tmp = (x_m * 1.0) * 1.0;
          	}
          	return x_s * tmp;
          }
          
          x\_m = abs(x)
          x\_s = copysign(1.0, x)
          function code(x_s, x_m, y, z, t, a, b)
          	t_1 = cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))
          	tmp = 0.0
          	if (Float64(Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
          		tmp = Float64(t_1 * Float64(x_m * cos(Float64(Float64(z * t) / Float64(16.0 * Float64(1.0 / fma(y, 2.0, 1.0)))))));
          	else
          		tmp = Float64(Float64(x_m * 1.0) * 1.0);
          	end
          	return Float64(x_s * tmp)
          end
          
          x\_m = N[Abs[x], $MachinePrecision]
          x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
          code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * t$95$1), $MachinePrecision], 1e+306], N[(t$95$1 * N[(x$95$m * N[Cos[N[(N[(z * t), $MachinePrecision] / N[(16.0 * N[(1.0 / N[(y * 2.0 + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
          
          \begin{array}{l}
          x\_m = \left|x\right|
          \\
          x\_s = \mathsf{copysign}\left(1, x\right)
          
          \\
          \begin{array}{l}
          t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\
          x\_s \cdot \begin{array}{l}
          \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\
          \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(\frac{z \cdot t}{16 \cdot \frac{1}{\mathsf{fma}\left(y, 2, 1\right)}}\right)\right)\\
          
          \mathbf{else}:\\
          \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
          
          
          \end{array}
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 1.00000000000000002e306

            1. Initial program 43.8%

              \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              2. lift-*.f64N/A

                \[\leadsto \left(x \cdot \cos \left(\frac{\color{blue}{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              3. lift-*.f64N/A

                \[\leadsto \left(x \cdot \cos \left(\frac{\color{blue}{\left(\left(y \cdot 2 + 1\right) \cdot z\right)} \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              4. associate-*l*N/A

                \[\leadsto \left(x \cdot \cos \left(\frac{\color{blue}{\left(y \cdot 2 + 1\right) \cdot \left(z \cdot t\right)}}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              5. associate-/l*N/A

                \[\leadsto \left(x \cdot \cos \color{blue}{\left(\left(y \cdot 2 + 1\right) \cdot \frac{z \cdot t}{16}\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              6. lift-+.f64N/A

                \[\leadsto \left(x \cdot \cos \left(\color{blue}{\left(y \cdot 2 + 1\right)} \cdot \frac{z \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              7. flip3-+N/A

                \[\leadsto \left(x \cdot \cos \left(\color{blue}{\frac{{\left(y \cdot 2\right)}^{3} + {1}^{3}}{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}} \cdot \frac{z \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              8. clear-numN/A

                \[\leadsto \left(x \cdot \cos \left(\color{blue}{\frac{1}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}{{\left(y \cdot 2\right)}^{3} + {1}^{3}}}} \cdot \frac{z \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              9. frac-timesN/A

                \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1 \cdot \left(z \cdot t\right)}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}{{\left(y \cdot 2\right)}^{3} + {1}^{3}} \cdot 16}\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              10. lower-/.f64N/A

                \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1 \cdot \left(z \cdot t\right)}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}{{\left(y \cdot 2\right)}^{3} + {1}^{3}} \cdot 16}\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              11. lower-*.f64N/A

                \[\leadsto \left(x \cdot \cos \left(\frac{\color{blue}{1 \cdot \left(z \cdot t\right)}}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}{{\left(y \cdot 2\right)}^{3} + {1}^{3}} \cdot 16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              12. lower-*.f64N/A

                \[\leadsto \left(x \cdot \cos \left(\frac{1 \cdot \color{blue}{\left(z \cdot t\right)}}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}{{\left(y \cdot 2\right)}^{3} + {1}^{3}} \cdot 16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              13. lower-*.f64N/A

                \[\leadsto \left(x \cdot \cos \left(\frac{1 \cdot \left(z \cdot t\right)}{\color{blue}{\frac{\left(y \cdot 2\right) \cdot \left(y \cdot 2\right) + \left(1 \cdot 1 - \left(y \cdot 2\right) \cdot 1\right)}{{\left(y \cdot 2\right)}^{3} + {1}^{3}} \cdot 16}}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
            4. Applied rewrites43.9%

              \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1 \cdot \left(z \cdot t\right)}{\frac{1}{\mathsf{fma}\left(y, 2, 1\right)} \cdot 16}\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]

            if 1.00000000000000002e306 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

            1. Initial program 0.8%

              \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
            2. Add Preprocessing
            3. Taylor expanded in z around 0

              \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
            4. Step-by-step derivation
              1. Applied rewrites5.9%

                \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
              2. Taylor expanded in b around 0

                \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
              3. Step-by-step derivation
                1. Applied rewrites11.6%

                  \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
              4. Recombined 2 regimes into one program.
              5. Final simplification29.0%

                \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+306}:\\ \;\;\;\;\cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \cdot \left(x \cdot \cos \left(\frac{z \cdot t}{16 \cdot \frac{1}{\mathsf{fma}\left(y, 2, 1\right)}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
              6. Add Preprocessing

              Alternative 4: 32.2% accurate, 0.5× speedup?

              \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t\_1 \leq 10^{+306}:\\ \;\;\;\;t\_1\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
              x\_m = (fabs.f64 x)
              x\_s = (copysign.f64 #s(literal 1 binary64) x)
              (FPCore (x_s x_m y z t a b)
               :precision binary64
               (let* ((t_1
                       (*
                        (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0)))
                        (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0)))))
                 (* x_s (if (<= t_1 1e+306) t_1 (* (* x_m 1.0) 1.0)))))
              x\_m = fabs(x);
              x\_s = copysign(1.0, x);
              double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
              	double t_1 = (x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
              	double tmp;
              	if (t_1 <= 1e+306) {
              		tmp = t_1;
              	} else {
              		tmp = (x_m * 1.0) * 1.0;
              	}
              	return x_s * tmp;
              }
              
              x\_m = abs(x)
              x\_s = copysign(1.0d0, x)
              real(8) function code(x_s, x_m, y, z, t, a, b)
                  real(8), intent (in) :: x_s
                  real(8), intent (in) :: x_m
                  real(8), intent (in) :: y
                  real(8), intent (in) :: z
                  real(8), intent (in) :: t
                  real(8), intent (in) :: a
                  real(8), intent (in) :: b
                  real(8) :: t_1
                  real(8) :: tmp
                  t_1 = (x_m * cos((((((y * 2.0d0) + 1.0d0) * z) * t) / 16.0d0))) * cos(((t * ((1.0d0 + (2.0d0 * a)) * b)) / 16.0d0))
                  if (t_1 <= 1d+306) then
                      tmp = t_1
                  else
                      tmp = (x_m * 1.0d0) * 1.0d0
                  end if
                  code = x_s * tmp
              end function
              
              x\_m = Math.abs(x);
              x\_s = Math.copySign(1.0, x);
              public static double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
              	double t_1 = (x_m * Math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * Math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
              	double tmp;
              	if (t_1 <= 1e+306) {
              		tmp = t_1;
              	} else {
              		tmp = (x_m * 1.0) * 1.0;
              	}
              	return x_s * tmp;
              }
              
              x\_m = math.fabs(x)
              x\_s = math.copysign(1.0, x)
              def code(x_s, x_m, y, z, t, a, b):
              	t_1 = (x_m * math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))
              	tmp = 0
              	if t_1 <= 1e+306:
              		tmp = t_1
              	else:
              		tmp = (x_m * 1.0) * 1.0
              	return x_s * tmp
              
              x\_m = abs(x)
              x\_s = copysign(1.0, x)
              function code(x_s, x_m, y, z, t, a, b)
              	t_1 = Float64(Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0)))
              	tmp = 0.0
              	if (t_1 <= 1e+306)
              		tmp = t_1;
              	else
              		tmp = Float64(Float64(x_m * 1.0) * 1.0);
              	end
              	return Float64(x_s * tmp)
              end
              
              x\_m = abs(x);
              x\_s = sign(x) * abs(1.0);
              function tmp_2 = code(x_s, x_m, y, z, t, a, b)
              	t_1 = (x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
              	tmp = 0.0;
              	if (t_1 <= 1e+306)
              		tmp = t_1;
              	else
              		tmp = (x_m * 1.0) * 1.0;
              	end
              	tmp_2 = x_s * tmp;
              end
              
              x\_m = N[Abs[x], $MachinePrecision]
              x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
              code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[t$95$1, 1e+306], t$95$1, N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
              
              \begin{array}{l}
              x\_m = \left|x\right|
              \\
              x\_s = \mathsf{copysign}\left(1, x\right)
              
              \\
              \begin{array}{l}
              t_1 := \left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\
              x\_s \cdot \begin{array}{l}
              \mathbf{if}\;t\_1 \leq 10^{+306}:\\
              \;\;\;\;t\_1\\
              
              \mathbf{else}:\\
              \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
              
              
              \end{array}
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 1.00000000000000002e306

                1. Initial program 43.8%

                  \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                2. Add Preprocessing

                if 1.00000000000000002e306 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

                1. Initial program 0.8%

                  \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                2. Add Preprocessing
                3. Taylor expanded in z around 0

                  \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                4. Step-by-step derivation
                  1. Applied rewrites5.9%

                    \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                  2. Taylor expanded in b around 0

                    \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                  3. Step-by-step derivation
                    1. Applied rewrites11.6%

                      \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                  4. Recombined 2 regimes into one program.
                  5. Final simplification29.0%

                    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+306}:\\ \;\;\;\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
                  6. Add Preprocessing

                  Alternative 5: 32.0% accurate, 0.5× speedup?

                  \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t\_1 \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+89}:\\ \;\;\;\;t\_1 \cdot \cos \left(\left(t \cdot b\right) \cdot \mathsf{fma}\left(0.125, a, 0.0625\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
                  x\_m = (fabs.f64 x)
                  x\_s = (copysign.f64 #s(literal 1 binary64) x)
                  (FPCore (x_s x_m y z t a b)
                   :precision binary64
                   (let* ((t_1 (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0)))))
                     (*
                      x_s
                      (if (<= (* t_1 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))) 1e+89)
                        (* t_1 (cos (* (* t b) (fma 0.125 a 0.0625))))
                        (* (* x_m 1.0) 1.0)))))
                  x\_m = fabs(x);
                  x\_s = copysign(1.0, x);
                  double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                  	double t_1 = x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0));
                  	double tmp;
                  	if ((t_1 * cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))) <= 1e+89) {
                  		tmp = t_1 * cos(((t * b) * fma(0.125, a, 0.0625)));
                  	} else {
                  		tmp = (x_m * 1.0) * 1.0;
                  	}
                  	return x_s * tmp;
                  }
                  
                  x\_m = abs(x)
                  x\_s = copysign(1.0, x)
                  function code(x_s, x_m, y, z, t, a, b)
                  	t_1 = Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0)))
                  	tmp = 0.0
                  	if (Float64(t_1 * cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))) <= 1e+89)
                  		tmp = Float64(t_1 * cos(Float64(Float64(t * b) * fma(0.125, a, 0.0625))));
                  	else
                  		tmp = Float64(Float64(x_m * 1.0) * 1.0);
                  	end
                  	return Float64(x_s * tmp)
                  end
                  
                  x\_m = N[Abs[x], $MachinePrecision]
                  x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                  code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(t$95$1 * N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], 1e+89], N[(t$95$1 * N[Cos[N[(N[(t * b), $MachinePrecision] * N[(0.125 * a + 0.0625), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
                  
                  \begin{array}{l}
                  x\_m = \left|x\right|
                  \\
                  x\_s = \mathsf{copysign}\left(1, x\right)
                  
                  \\
                  \begin{array}{l}
                  t_1 := x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\\
                  x\_s \cdot \begin{array}{l}
                  \mathbf{if}\;t\_1 \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+89}:\\
                  \;\;\;\;t\_1 \cdot \cos \left(\left(t \cdot b\right) \cdot \mathsf{fma}\left(0.125, a, 0.0625\right)\right)\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
                  
                  
                  \end{array}
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 2 regimes
                  2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 9.99999999999999995e88

                    1. Initial program 41.5%

                      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                    2. Add Preprocessing
                    3. Taylor expanded in a around 0

                      \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\frac{1}{16} \cdot \left(b \cdot t\right) + \frac{1}{8} \cdot \left(a \cdot \left(b \cdot t\right)\right)\right)} \]
                    4. Step-by-step derivation
                      1. associate-*r*N/A

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(b \cdot t\right) + \color{blue}{\left(\frac{1}{8} \cdot a\right) \cdot \left(b \cdot t\right)}\right) \]
                      2. distribute-rgt-outN/A

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\left(b \cdot t\right) \cdot \left(\frac{1}{16} + \frac{1}{8} \cdot a\right)\right)} \]
                      3. lower-*.f64N/A

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\left(b \cdot t\right) \cdot \left(\frac{1}{16} + \frac{1}{8} \cdot a\right)\right)} \]
                      4. *-commutativeN/A

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\color{blue}{\left(t \cdot b\right)} \cdot \left(\frac{1}{16} + \frac{1}{8} \cdot a\right)\right) \]
                      5. lower-*.f64N/A

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\color{blue}{\left(t \cdot b\right)} \cdot \left(\frac{1}{16} + \frac{1}{8} \cdot a\right)\right) \]
                      6. +-commutativeN/A

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \color{blue}{\left(\frac{1}{8} \cdot a + \frac{1}{16}\right)}\right) \]
                      7. lower-fma.f6441.5

                        \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \color{blue}{\mathsf{fma}\left(0.125, a, 0.0625\right)}\right) \]
                    5. Applied rewrites41.5%

                      \[\leadsto \left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \color{blue}{\left(\left(t \cdot b\right) \cdot \mathsf{fma}\left(0.125, a, 0.0625\right)\right)} \]

                    if 9.99999999999999995e88 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

                    1. Initial program 10.2%

                      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                    2. Add Preprocessing
                    3. Taylor expanded in z around 0

                      \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                    4. Step-by-step derivation
                      1. Applied rewrites14.0%

                        \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                      2. Taylor expanded in b around 0

                        \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                      3. Step-by-step derivation
                        1. Applied rewrites18.8%

                          \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                      4. Recombined 2 regimes into one program.
                      5. Final simplification28.8%

                        \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+89}:\\ \;\;\;\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \mathsf{fma}\left(0.125, a, 0.0625\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
                      6. Add Preprocessing

                      Alternative 6: 32.1% accurate, 0.5× speedup?

                      \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\ \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(\left(z \cdot t\right) \cdot \mathsf{fma}\left(0.125, y, 0.0625\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
                      x\_m = (fabs.f64 x)
                      x\_s = (copysign.f64 #s(literal 1 binary64) x)
                      (FPCore (x_s x_m y z t a b)
                       :precision binary64
                       (let* ((t_1 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))))
                         (*
                          x_s
                          (if (<=
                               (* (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) t_1)
                               1e+306)
                            (* t_1 (* x_m (cos (* (* z t) (fma 0.125 y 0.0625)))))
                            (* (* x_m 1.0) 1.0)))))
                      x\_m = fabs(x);
                      x\_s = copysign(1.0, x);
                      double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                      	double t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                      	double tmp;
                      	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
                      		tmp = t_1 * (x_m * cos(((z * t) * fma(0.125, y, 0.0625))));
                      	} else {
                      		tmp = (x_m * 1.0) * 1.0;
                      	}
                      	return x_s * tmp;
                      }
                      
                      x\_m = abs(x)
                      x\_s = copysign(1.0, x)
                      function code(x_s, x_m, y, z, t, a, b)
                      	t_1 = cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))
                      	tmp = 0.0
                      	if (Float64(Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
                      		tmp = Float64(t_1 * Float64(x_m * cos(Float64(Float64(z * t) * fma(0.125, y, 0.0625)))));
                      	else
                      		tmp = Float64(Float64(x_m * 1.0) * 1.0);
                      	end
                      	return Float64(x_s * tmp)
                      end
                      
                      x\_m = N[Abs[x], $MachinePrecision]
                      x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                      code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * t$95$1), $MachinePrecision], 1e+306], N[(t$95$1 * N[(x$95$m * N[Cos[N[(N[(z * t), $MachinePrecision] * N[(0.125 * y + 0.0625), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
                      
                      \begin{array}{l}
                      x\_m = \left|x\right|
                      \\
                      x\_s = \mathsf{copysign}\left(1, x\right)
                      
                      \\
                      \begin{array}{l}
                      t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\
                      x\_s \cdot \begin{array}{l}
                      \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\
                      \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(\left(z \cdot t\right) \cdot \mathsf{fma}\left(0.125, y, 0.0625\right)\right)\right)\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
                      
                      
                      \end{array}
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 1.00000000000000002e306

                        1. Initial program 43.8%

                          \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                        2. Add Preprocessing
                        3. Taylor expanded in y around 0

                          \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1}{16} \cdot \left(t \cdot z\right) + \frac{1}{8} \cdot \left(t \cdot \left(y \cdot z\right)\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                        4. Step-by-step derivation
                          1. +-commutativeN/A

                            \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1}{8} \cdot \left(t \cdot \left(y \cdot z\right)\right) + \frac{1}{16} \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          2. *-commutativeN/A

                            \[\leadsto \left(x \cdot \cos \left(\frac{1}{8} \cdot \left(t \cdot \color{blue}{\left(z \cdot y\right)}\right) + \frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          3. associate-*r*N/A

                            \[\leadsto \left(x \cdot \cos \left(\frac{1}{8} \cdot \color{blue}{\left(\left(t \cdot z\right) \cdot y\right)} + \frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          4. associate-*l*N/A

                            \[\leadsto \left(x \cdot \cos \left(\color{blue}{\left(\frac{1}{8} \cdot \left(t \cdot z\right)\right) \cdot y} + \frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          5. *-commutativeN/A

                            \[\leadsto \left(x \cdot \cos \left(\color{blue}{\left(\left(t \cdot z\right) \cdot \frac{1}{8}\right)} \cdot y + \frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          6. associate-*l*N/A

                            \[\leadsto \left(x \cdot \cos \left(\color{blue}{\left(t \cdot z\right) \cdot \left(\frac{1}{8} \cdot y\right)} + \frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          7. *-commutativeN/A

                            \[\leadsto \left(x \cdot \cos \left(\left(t \cdot z\right) \cdot \left(\frac{1}{8} \cdot y\right) + \color{blue}{\left(t \cdot z\right) \cdot \frac{1}{16}}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          8. distribute-lft-outN/A

                            \[\leadsto \left(x \cdot \cos \color{blue}{\left(\left(t \cdot z\right) \cdot \left(\frac{1}{8} \cdot y + \frac{1}{16}\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          9. lower-*.f64N/A

                            \[\leadsto \left(x \cdot \cos \color{blue}{\left(\left(t \cdot z\right) \cdot \left(\frac{1}{8} \cdot y + \frac{1}{16}\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          10. lower-*.f64N/A

                            \[\leadsto \left(x \cdot \cos \left(\color{blue}{\left(t \cdot z\right)} \cdot \left(\frac{1}{8} \cdot y + \frac{1}{16}\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          11. lower-fma.f6443.4

                            \[\leadsto \left(x \cdot \cos \left(\left(t \cdot z\right) \cdot \color{blue}{\mathsf{fma}\left(0.125, y, 0.0625\right)}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                        5. Applied rewrites43.4%

                          \[\leadsto \left(x \cdot \cos \color{blue}{\left(\left(t \cdot z\right) \cdot \mathsf{fma}\left(0.125, y, 0.0625\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]

                        if 1.00000000000000002e306 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

                        1. Initial program 0.8%

                          \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                        2. Add Preprocessing
                        3. Taylor expanded in z around 0

                          \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                        4. Step-by-step derivation
                          1. Applied rewrites5.9%

                            \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                          2. Taylor expanded in b around 0

                            \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                          3. Step-by-step derivation
                            1. Applied rewrites11.6%

                              \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                          4. Recombined 2 regimes into one program.
                          5. Final simplification28.8%

                            \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+306}:\\ \;\;\;\;\cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \cdot \left(x \cdot \cos \left(\left(z \cdot t\right) \cdot \mathsf{fma}\left(0.125, y, 0.0625\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
                          6. Add Preprocessing

                          Alternative 7: 31.8% accurate, 0.5× speedup?

                          \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\ \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(0.125 \cdot \left(t \cdot \left(y \cdot z\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
                          x\_m = (fabs.f64 x)
                          x\_s = (copysign.f64 #s(literal 1 binary64) x)
                          (FPCore (x_s x_m y z t a b)
                           :precision binary64
                           (let* ((t_1 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))))
                             (*
                              x_s
                              (if (<=
                                   (* (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) t_1)
                                   1e+306)
                                (* t_1 (* x_m (cos (* 0.125 (* t (* y z))))))
                                (* (* x_m 1.0) 1.0)))))
                          x\_m = fabs(x);
                          x\_s = copysign(1.0, x);
                          double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                          	double t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                          	double tmp;
                          	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
                          		tmp = t_1 * (x_m * cos((0.125 * (t * (y * z)))));
                          	} else {
                          		tmp = (x_m * 1.0) * 1.0;
                          	}
                          	return x_s * tmp;
                          }
                          
                          x\_m = abs(x)
                          x\_s = copysign(1.0d0, x)
                          real(8) function code(x_s, x_m, y, z, t, a, b)
                              real(8), intent (in) :: x_s
                              real(8), intent (in) :: x_m
                              real(8), intent (in) :: y
                              real(8), intent (in) :: z
                              real(8), intent (in) :: t
                              real(8), intent (in) :: a
                              real(8), intent (in) :: b
                              real(8) :: t_1
                              real(8) :: tmp
                              t_1 = cos(((t * ((1.0d0 + (2.0d0 * a)) * b)) / 16.0d0))
                              if (((x_m * cos((((((y * 2.0d0) + 1.0d0) * z) * t) / 16.0d0))) * t_1) <= 1d+306) then
                                  tmp = t_1 * (x_m * cos((0.125d0 * (t * (y * z)))))
                              else
                                  tmp = (x_m * 1.0d0) * 1.0d0
                              end if
                              code = x_s * tmp
                          end function
                          
                          x\_m = Math.abs(x);
                          x\_s = Math.copySign(1.0, x);
                          public static double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                          	double t_1 = Math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                          	double tmp;
                          	if (((x_m * Math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
                          		tmp = t_1 * (x_m * Math.cos((0.125 * (t * (y * z)))));
                          	} else {
                          		tmp = (x_m * 1.0) * 1.0;
                          	}
                          	return x_s * tmp;
                          }
                          
                          x\_m = math.fabs(x)
                          x\_s = math.copysign(1.0, x)
                          def code(x_s, x_m, y, z, t, a, b):
                          	t_1 = math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))
                          	tmp = 0
                          	if ((x_m * math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306:
                          		tmp = t_1 * (x_m * math.cos((0.125 * (t * (y * z)))))
                          	else:
                          		tmp = (x_m * 1.0) * 1.0
                          	return x_s * tmp
                          
                          x\_m = abs(x)
                          x\_s = copysign(1.0, x)
                          function code(x_s, x_m, y, z, t, a, b)
                          	t_1 = cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))
                          	tmp = 0.0
                          	if (Float64(Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
                          		tmp = Float64(t_1 * Float64(x_m * cos(Float64(0.125 * Float64(t * Float64(y * z))))));
                          	else
                          		tmp = Float64(Float64(x_m * 1.0) * 1.0);
                          	end
                          	return Float64(x_s * tmp)
                          end
                          
                          x\_m = abs(x);
                          x\_s = sign(x) * abs(1.0);
                          function tmp_2 = code(x_s, x_m, y, z, t, a, b)
                          	t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                          	tmp = 0.0;
                          	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
                          		tmp = t_1 * (x_m * cos((0.125 * (t * (y * z)))));
                          	else
                          		tmp = (x_m * 1.0) * 1.0;
                          	end
                          	tmp_2 = x_s * tmp;
                          end
                          
                          x\_m = N[Abs[x], $MachinePrecision]
                          x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                          code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * t$95$1), $MachinePrecision], 1e+306], N[(t$95$1 * N[(x$95$m * N[Cos[N[(0.125 * N[(t * N[(y * z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
                          
                          \begin{array}{l}
                          x\_m = \left|x\right|
                          \\
                          x\_s = \mathsf{copysign}\left(1, x\right)
                          
                          \\
                          \begin{array}{l}
                          t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\
                          x\_s \cdot \begin{array}{l}
                          \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\
                          \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(0.125 \cdot \left(t \cdot \left(y \cdot z\right)\right)\right)\right)\\
                          
                          \mathbf{else}:\\
                          \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
                          
                          
                          \end{array}
                          \end{array}
                          \end{array}
                          
                          Derivation
                          1. Split input into 2 regimes
                          2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 1.00000000000000002e306

                            1. Initial program 43.8%

                              \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                            2. Add Preprocessing
                            3. Taylor expanded in y around inf

                              \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1}{8} \cdot \left(t \cdot \left(y \cdot z\right)\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                            4. Step-by-step derivation
                              1. lower-*.f64N/A

                                \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1}{8} \cdot \left(t \cdot \left(y \cdot z\right)\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                              2. lower-*.f64N/A

                                \[\leadsto \left(x \cdot \cos \left(\frac{1}{8} \cdot \color{blue}{\left(t \cdot \left(y \cdot z\right)\right)}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                              3. *-commutativeN/A

                                \[\leadsto \left(x \cdot \cos \left(\frac{1}{8} \cdot \left(t \cdot \color{blue}{\left(z \cdot y\right)}\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                              4. lower-*.f6442.7

                                \[\leadsto \left(x \cdot \cos \left(0.125 \cdot \left(t \cdot \color{blue}{\left(z \cdot y\right)}\right)\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                            5. Applied rewrites42.7%

                              \[\leadsto \left(x \cdot \cos \color{blue}{\left(0.125 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]

                            if 1.00000000000000002e306 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

                            1. Initial program 0.8%

                              \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                            2. Add Preprocessing
                            3. Taylor expanded in z around 0

                              \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                            4. Step-by-step derivation
                              1. Applied rewrites5.9%

                                \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                              2. Taylor expanded in b around 0

                                \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                              3. Step-by-step derivation
                                1. Applied rewrites11.6%

                                  \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                              4. Recombined 2 regimes into one program.
                              5. Final simplification28.4%

                                \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+306}:\\ \;\;\;\;\cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \cdot \left(x \cdot \cos \left(0.125 \cdot \left(t \cdot \left(y \cdot z\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
                              6. Add Preprocessing

                              Alternative 8: 31.8% accurate, 0.5× speedup?

                              \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ \begin{array}{l} t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\ x\_s \cdot \begin{array}{l} \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\ \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(0.0625 \cdot \left(z \cdot t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \end{array} \]
                              x\_m = (fabs.f64 x)
                              x\_s = (copysign.f64 #s(literal 1 binary64) x)
                              (FPCore (x_s x_m y z t a b)
                               :precision binary64
                               (let* ((t_1 (cos (/ (* t (* (+ 1.0 (* 2.0 a)) b)) 16.0))))
                                 (*
                                  x_s
                                  (if (<=
                                       (* (* x_m (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) t_1)
                                       1e+306)
                                    (* t_1 (* x_m (cos (* 0.0625 (* z t)))))
                                    (* (* x_m 1.0) 1.0)))))
                              x\_m = fabs(x);
                              x\_s = copysign(1.0, x);
                              double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                              	double t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                              	double tmp;
                              	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
                              		tmp = t_1 * (x_m * cos((0.0625 * (z * t))));
                              	} else {
                              		tmp = (x_m * 1.0) * 1.0;
                              	}
                              	return x_s * tmp;
                              }
                              
                              x\_m = abs(x)
                              x\_s = copysign(1.0d0, x)
                              real(8) function code(x_s, x_m, y, z, t, a, b)
                                  real(8), intent (in) :: x_s
                                  real(8), intent (in) :: x_m
                                  real(8), intent (in) :: y
                                  real(8), intent (in) :: z
                                  real(8), intent (in) :: t
                                  real(8), intent (in) :: a
                                  real(8), intent (in) :: b
                                  real(8) :: t_1
                                  real(8) :: tmp
                                  t_1 = cos(((t * ((1.0d0 + (2.0d0 * a)) * b)) / 16.0d0))
                                  if (((x_m * cos((((((y * 2.0d0) + 1.0d0) * z) * t) / 16.0d0))) * t_1) <= 1d+306) then
                                      tmp = t_1 * (x_m * cos((0.0625d0 * (z * t))))
                                  else
                                      tmp = (x_m * 1.0d0) * 1.0d0
                                  end if
                                  code = x_s * tmp
                              end function
                              
                              x\_m = Math.abs(x);
                              x\_s = Math.copySign(1.0, x);
                              public static double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                              	double t_1 = Math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                              	double tmp;
                              	if (((x_m * Math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306) {
                              		tmp = t_1 * (x_m * Math.cos((0.0625 * (z * t))));
                              	} else {
                              		tmp = (x_m * 1.0) * 1.0;
                              	}
                              	return x_s * tmp;
                              }
                              
                              x\_m = math.fabs(x)
                              x\_s = math.copysign(1.0, x)
                              def code(x_s, x_m, y, z, t, a, b):
                              	t_1 = math.cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0))
                              	tmp = 0
                              	if ((x_m * math.cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306:
                              		tmp = t_1 * (x_m * math.cos((0.0625 * (z * t))))
                              	else:
                              		tmp = (x_m * 1.0) * 1.0
                              	return x_s * tmp
                              
                              x\_m = abs(x)
                              x\_s = copysign(1.0, x)
                              function code(x_s, x_m, y, z, t, a, b)
                              	t_1 = cos(Float64(Float64(t * Float64(Float64(1.0 + Float64(2.0 * a)) * b)) / 16.0))
                              	tmp = 0.0
                              	if (Float64(Float64(x_m * cos(Float64(Float64(Float64(Float64(Float64(y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
                              		tmp = Float64(t_1 * Float64(x_m * cos(Float64(0.0625 * Float64(z * t)))));
                              	else
                              		tmp = Float64(Float64(x_m * 1.0) * 1.0);
                              	end
                              	return Float64(x_s * tmp)
                              end
                              
                              x\_m = abs(x);
                              x\_s = sign(x) * abs(1.0);
                              function tmp_2 = code(x_s, x_m, y, z, t, a, b)
                              	t_1 = cos(((t * ((1.0 + (2.0 * a)) * b)) / 16.0));
                              	tmp = 0.0;
                              	if (((x_m * cos((((((y * 2.0) + 1.0) * z) * t) / 16.0))) * t_1) <= 1e+306)
                              		tmp = t_1 * (x_m * cos((0.0625 * (z * t))));
                              	else
                              		tmp = (x_m * 1.0) * 1.0;
                              	end
                              	tmp_2 = x_s * tmp;
                              end
                              
                              x\_m = N[Abs[x], $MachinePrecision]
                              x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                              code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[Cos[N[(N[(t * N[(N[(1.0 + N[(2.0 * a), $MachinePrecision]), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]}, N[(x$95$s * If[LessEqual[N[(N[(x$95$m * N[Cos[N[(N[(N[(N[(N[(y * 2.0), $MachinePrecision] + 1.0), $MachinePrecision] * z), $MachinePrecision] * t), $MachinePrecision] / 16.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * t$95$1), $MachinePrecision], 1e+306], N[(t$95$1 * N[(x$95$m * N[Cos[N[(0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]]
                              
                              \begin{array}{l}
                              x\_m = \left|x\right|
                              \\
                              x\_s = \mathsf{copysign}\left(1, x\right)
                              
                              \\
                              \begin{array}{l}
                              t_1 := \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right)\\
                              x\_s \cdot \begin{array}{l}
                              \mathbf{if}\;\left(x\_m \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot t\_1 \leq 10^{+306}:\\
                              \;\;\;\;t\_1 \cdot \left(x\_m \cdot \cos \left(0.0625 \cdot \left(z \cdot t\right)\right)\right)\\
                              
                              \mathbf{else}:\\
                              \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
                              
                              
                              \end{array}
                              \end{array}
                              \end{array}
                              
                              Derivation
                              1. Split input into 2 regimes
                              2. if (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64)))) < 1.00000000000000002e306

                                1. Initial program 43.8%

                                  \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                2. Add Preprocessing
                                3. Taylor expanded in y around 0

                                  \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                4. Step-by-step derivation
                                  1. lower-*.f64N/A

                                    \[\leadsto \left(x \cdot \cos \color{blue}{\left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                  2. lower-*.f6442.6

                                    \[\leadsto \left(x \cdot \cos \left(0.0625 \cdot \color{blue}{\left(t \cdot z\right)}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                5. Applied rewrites42.6%

                                  \[\leadsto \left(x \cdot \cos \color{blue}{\left(0.0625 \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]

                                if 1.00000000000000002e306 < (*.f64 (*.f64 x (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 y #s(literal 2 binary64)) #s(literal 1 binary64)) z) t) #s(literal 16 binary64)))) (cos.f64 (/.f64 (*.f64 (*.f64 (+.f64 (*.f64 a #s(literal 2 binary64)) #s(literal 1 binary64)) b) t) #s(literal 16 binary64))))

                                1. Initial program 0.8%

                                  \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                2. Add Preprocessing
                                3. Taylor expanded in z around 0

                                  \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                4. Step-by-step derivation
                                  1. Applied rewrites5.9%

                                    \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                  2. Taylor expanded in b around 0

                                    \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                                  3. Step-by-step derivation
                                    1. Applied rewrites11.6%

                                      \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                                  4. Recombined 2 regimes into one program.
                                  5. Final simplification28.3%

                                    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \leq 10^{+306}:\\ \;\;\;\;\cos \left(\frac{t \cdot \left(\left(1 + 2 \cdot a\right) \cdot b\right)}{16}\right) \cdot \left(x \cdot \cos \left(0.0625 \cdot \left(z \cdot t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
                                  6. Add Preprocessing

                                  Alternative 9: 30.0% accurate, 1.1× speedup?

                                  \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;t \leq 4 \cdot 10^{-94}:\\ \;\;\;\;x\_m \cdot \left(\cos \left(0.0625 \cdot \left(b \cdot \mathsf{fma}\left(t, 2 \cdot a, t\right)\right)\right) \cdot \cos \left(0.0625 \cdot \left(z \cdot t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\ \end{array} \end{array} \]
                                  x\_m = (fabs.f64 x)
                                  x\_s = (copysign.f64 #s(literal 1 binary64) x)
                                  (FPCore (x_s x_m y z t a b)
                                   :precision binary64
                                   (*
                                    x_s
                                    (if (<= t 4e-94)
                                      (*
                                       x_m
                                       (* (cos (* 0.0625 (* b (fma t (* 2.0 a) t)))) (cos (* 0.0625 (* z t)))))
                                      (* (* x_m 1.0) 1.0))))
                                  x\_m = fabs(x);
                                  x\_s = copysign(1.0, x);
                                  double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                                  	double tmp;
                                  	if (t <= 4e-94) {
                                  		tmp = x_m * (cos((0.0625 * (b * fma(t, (2.0 * a), t)))) * cos((0.0625 * (z * t))));
                                  	} else {
                                  		tmp = (x_m * 1.0) * 1.0;
                                  	}
                                  	return x_s * tmp;
                                  }
                                  
                                  x\_m = abs(x)
                                  x\_s = copysign(1.0, x)
                                  function code(x_s, x_m, y, z, t, a, b)
                                  	tmp = 0.0
                                  	if (t <= 4e-94)
                                  		tmp = Float64(x_m * Float64(cos(Float64(0.0625 * Float64(b * fma(t, Float64(2.0 * a), t)))) * cos(Float64(0.0625 * Float64(z * t)))));
                                  	else
                                  		tmp = Float64(Float64(x_m * 1.0) * 1.0);
                                  	end
                                  	return Float64(x_s * tmp)
                                  end
                                  
                                  x\_m = N[Abs[x], $MachinePrecision]
                                  x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                                  code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := N[(x$95$s * If[LessEqual[t, 4e-94], N[(x$95$m * N[(N[Cos[N[(0.0625 * N[(b * N[(t * N[(2.0 * a), $MachinePrecision] + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]]), $MachinePrecision]
                                  
                                  \begin{array}{l}
                                  x\_m = \left|x\right|
                                  \\
                                  x\_s = \mathsf{copysign}\left(1, x\right)
                                  
                                  \\
                                  x\_s \cdot \begin{array}{l}
                                  \mathbf{if}\;t \leq 4 \cdot 10^{-94}:\\
                                  \;\;\;\;x\_m \cdot \left(\cos \left(0.0625 \cdot \left(b \cdot \mathsf{fma}\left(t, 2 \cdot a, t\right)\right)\right) \cdot \cos \left(0.0625 \cdot \left(z \cdot t\right)\right)\right)\\
                                  
                                  \mathbf{else}:\\
                                  \;\;\;\;\left(x\_m \cdot 1\right) \cdot 1\\
                                  
                                  
                                  \end{array}
                                  \end{array}
                                  
                                  Derivation
                                  1. Split input into 2 regimes
                                  2. if t < 3.9999999999999998e-94

                                    1. Initial program 28.3%

                                      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                    2. Add Preprocessing
                                    3. Taylor expanded in z around 0

                                      \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                    4. Step-by-step derivation
                                      1. Applied rewrites29.6%

                                        \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                      2. Taylor expanded in y around 0

                                        \[\leadsto \color{blue}{x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \left(1 + 2 \cdot a\right)\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right)} \]
                                      3. Step-by-step derivation
                                        1. lower-*.f64N/A

                                          \[\leadsto \color{blue}{x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \left(1 + 2 \cdot a\right)\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right)} \]
                                        2. lower-*.f64N/A

                                          \[\leadsto x \cdot \color{blue}{\left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \left(1 + 2 \cdot a\right)\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right)} \]
                                        3. lower-cos.f64N/A

                                          \[\leadsto x \cdot \left(\color{blue}{\cos \left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \left(1 + 2 \cdot a\right)\right)\right)\right)} \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        4. lower-*.f64N/A

                                          \[\leadsto x \cdot \left(\cos \color{blue}{\left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \left(1 + 2 \cdot a\right)\right)\right)\right)} \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        5. lower-*.f64N/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \color{blue}{\left(b \cdot \left(t \cdot \left(1 + 2 \cdot a\right)\right)\right)}\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        6. +-commutativeN/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \color{blue}{\left(2 \cdot a + 1\right)}\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        7. distribute-lft-inN/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \color{blue}{\left(t \cdot \left(2 \cdot a\right) + t \cdot 1\right)}\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        8. *-rgt-identityN/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \left(t \cdot \left(2 \cdot a\right) + \color{blue}{t}\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        9. lower-fma.f64N/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \color{blue}{\mathsf{fma}\left(t, 2 \cdot a, t\right)}\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        10. *-commutativeN/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \mathsf{fma}\left(t, \color{blue}{a \cdot 2}, t\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        11. lower-*.f64N/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \mathsf{fma}\left(t, \color{blue}{a \cdot 2}, t\right)\right)\right) \cdot \cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)\right) \]
                                        12. lower-cos.f64N/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \mathsf{fma}\left(t, a \cdot 2, t\right)\right)\right) \cdot \color{blue}{\cos \left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)}\right) \]
                                        13. lower-*.f64N/A

                                          \[\leadsto x \cdot \left(\cos \left(\frac{1}{16} \cdot \left(b \cdot \mathsf{fma}\left(t, a \cdot 2, t\right)\right)\right) \cdot \cos \color{blue}{\left(\frac{1}{16} \cdot \left(t \cdot z\right)\right)}\right) \]
                                        14. lower-*.f6429.9

                                          \[\leadsto x \cdot \left(\cos \left(0.0625 \cdot \left(b \cdot \mathsf{fma}\left(t, a \cdot 2, t\right)\right)\right) \cdot \cos \left(0.0625 \cdot \color{blue}{\left(t \cdot z\right)}\right)\right) \]
                                      4. Applied rewrites29.9%

                                        \[\leadsto \color{blue}{x \cdot \left(\cos \left(0.0625 \cdot \left(b \cdot \mathsf{fma}\left(t, a \cdot 2, t\right)\right)\right) \cdot \cos \left(0.0625 \cdot \left(t \cdot z\right)\right)\right)} \]

                                      if 3.9999999999999998e-94 < t

                                      1. Initial program 15.8%

                                        \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                      2. Add Preprocessing
                                      3. Taylor expanded in z around 0

                                        \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                      4. Step-by-step derivation
                                        1. Applied rewrites16.1%

                                          \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                        2. Taylor expanded in b around 0

                                          \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites20.2%

                                            \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                                        4. Recombined 2 regimes into one program.
                                        5. Final simplification26.6%

                                          \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 4 \cdot 10^{-94}:\\ \;\;\;\;x \cdot \left(\cos \left(0.0625 \cdot \left(b \cdot \mathsf{fma}\left(t, 2 \cdot a, t\right)\right)\right) \cdot \cos \left(0.0625 \cdot \left(z \cdot t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 1\right) \cdot 1\\ \end{array} \]
                                        6. Add Preprocessing

                                        Alternative 10: 30.9% accurate, 24.5× speedup?

                                        \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \left(\left(x\_m \cdot 1\right) \cdot 1\right) \end{array} \]
                                        x\_m = (fabs.f64 x)
                                        x\_s = (copysign.f64 #s(literal 1 binary64) x)
                                        (FPCore (x_s x_m y z t a b) :precision binary64 (* x_s (* (* x_m 1.0) 1.0)))
                                        x\_m = fabs(x);
                                        x\_s = copysign(1.0, x);
                                        double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                                        	return x_s * ((x_m * 1.0) * 1.0);
                                        }
                                        
                                        x\_m = abs(x)
                                        x\_s = copysign(1.0d0, x)
                                        real(8) function code(x_s, x_m, y, z, t, a, b)
                                            real(8), intent (in) :: x_s
                                            real(8), intent (in) :: x_m
                                            real(8), intent (in) :: y
                                            real(8), intent (in) :: z
                                            real(8), intent (in) :: t
                                            real(8), intent (in) :: a
                                            real(8), intent (in) :: b
                                            code = x_s * ((x_m * 1.0d0) * 1.0d0)
                                        end function
                                        
                                        x\_m = Math.abs(x);
                                        x\_s = Math.copySign(1.0, x);
                                        public static double code(double x_s, double x_m, double y, double z, double t, double a, double b) {
                                        	return x_s * ((x_m * 1.0) * 1.0);
                                        }
                                        
                                        x\_m = math.fabs(x)
                                        x\_s = math.copysign(1.0, x)
                                        def code(x_s, x_m, y, z, t, a, b):
                                        	return x_s * ((x_m * 1.0) * 1.0)
                                        
                                        x\_m = abs(x)
                                        x\_s = copysign(1.0, x)
                                        function code(x_s, x_m, y, z, t, a, b)
                                        	return Float64(x_s * Float64(Float64(x_m * 1.0) * 1.0))
                                        end
                                        
                                        x\_m = abs(x);
                                        x\_s = sign(x) * abs(1.0);
                                        function tmp = code(x_s, x_m, y, z, t, a, b)
                                        	tmp = x_s * ((x_m * 1.0) * 1.0);
                                        end
                                        
                                        x\_m = N[Abs[x], $MachinePrecision]
                                        x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
                                        code[x$95$s_, x$95$m_, y_, z_, t_, a_, b_] := N[(x$95$s * N[(N[(x$95$m * 1.0), $MachinePrecision] * 1.0), $MachinePrecision]), $MachinePrecision]
                                        
                                        \begin{array}{l}
                                        x\_m = \left|x\right|
                                        \\
                                        x\_s = \mathsf{copysign}\left(1, x\right)
                                        
                                        \\
                                        x\_s \cdot \left(\left(x\_m \cdot 1\right) \cdot 1\right)
                                        \end{array}
                                        
                                        Derivation
                                        1. Initial program 24.0%

                                          \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                        2. Add Preprocessing
                                        3. Taylor expanded in z around 0

                                          \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                        4. Step-by-step derivation
                                          1. Applied rewrites24.9%

                                            \[\leadsto \left(x \cdot \color{blue}{1}\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right) \]
                                          2. Taylor expanded in b around 0

                                            \[\leadsto \left(x \cdot 1\right) \cdot \color{blue}{1} \]
                                          3. Step-by-step derivation
                                            1. Applied rewrites26.2%

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

                                            Developer Target 1: 30.5% accurate, 1.1× speedup?

                                            \[\begin{array}{l} \\ x \cdot \cos \left(\frac{b}{16} \cdot \frac{t}{\left(1 - a \cdot 2\right) + {\left(a \cdot 2\right)}^{2}}\right) \end{array} \]
                                            (FPCore (x y z t a b)
                                             :precision binary64
                                             (* x (cos (* (/ b 16.0) (/ t (+ (- 1.0 (* a 2.0)) (pow (* a 2.0) 2.0)))))))
                                            double code(double x, double y, double z, double t, double a, double b) {
                                            	return x * cos(((b / 16.0) * (t / ((1.0 - (a * 2.0)) + pow((a * 2.0), 2.0)))));
                                            }
                                            
                                            real(8) function code(x, y, z, t, a, b)
                                                real(8), intent (in) :: x
                                                real(8), intent (in) :: y
                                                real(8), intent (in) :: z
                                                real(8), intent (in) :: t
                                                real(8), intent (in) :: a
                                                real(8), intent (in) :: b
                                                code = x * cos(((b / 16.0d0) * (t / ((1.0d0 - (a * 2.0d0)) + ((a * 2.0d0) ** 2.0d0)))))
                                            end function
                                            
                                            public static double code(double x, double y, double z, double t, double a, double b) {
                                            	return x * Math.cos(((b / 16.0) * (t / ((1.0 - (a * 2.0)) + Math.pow((a * 2.0), 2.0)))));
                                            }
                                            
                                            def code(x, y, z, t, a, b):
                                            	return x * math.cos(((b / 16.0) * (t / ((1.0 - (a * 2.0)) + math.pow((a * 2.0), 2.0)))))
                                            
                                            function code(x, y, z, t, a, b)
                                            	return Float64(x * cos(Float64(Float64(b / 16.0) * Float64(t / Float64(Float64(1.0 - Float64(a * 2.0)) + (Float64(a * 2.0) ^ 2.0))))))
                                            end
                                            
                                            function tmp = code(x, y, z, t, a, b)
                                            	tmp = x * cos(((b / 16.0) * (t / ((1.0 - (a * 2.0)) + ((a * 2.0) ^ 2.0)))));
                                            end
                                            
                                            code[x_, y_, z_, t_, a_, b_] := N[(x * N[Cos[N[(N[(b / 16.0), $MachinePrecision] * N[(t / N[(N[(1.0 - N[(a * 2.0), $MachinePrecision]), $MachinePrecision] + N[Power[N[(a * 2.0), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
                                            
                                            \begin{array}{l}
                                            
                                            \\
                                            x \cdot \cos \left(\frac{b}{16} \cdot \frac{t}{\left(1 - a \cdot 2\right) + {\left(a \cdot 2\right)}^{2}}\right)
                                            \end{array}
                                            

                                            Reproduce

                                            ?
                                            herbie shell --seed 2024220 
                                            (FPCore (x y z t a b)
                                              :name "Codec.Picture.Jpg.FastDct:referenceDct from JuicyPixels-3.2.6.1"
                                              :precision binary64
                                            
                                              :alt
                                              (! :herbie-platform default (* x (cos (* (/ b 16) (/ t (+ (- 1 (* a 2)) (pow (* a 2) 2)))))))
                                            
                                              (* (* x (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) (cos (/ (* (* (+ (* a 2.0) 1.0) b) t) 16.0))))