(- 1 (cos (* -2 (atan (* (/ z1 z2) (tan (* PI (+ 1/2 (+ z0 z0)))))))))

Percentage Accurate: 59.9% → 91.5%
Time: 8.2s
Alternatives: 7
Speedup: 0.8×

Specification

?
\[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
(FPCore (z1 z2 z0)
  :precision binary64
  (-
 1.0
 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI (+ 0.5 (+ z0 z0))))))))))
double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * (0.5 + (z0 + z0))))))));
}
public static double code(double z1, double z2, double z0) {
	return 1.0 - Math.cos((-2.0 * Math.atan(((z1 / z2) * Math.tan((Math.PI * (0.5 + (z0 + z0))))))));
}
def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * (0.5 + (z0 + z0))))))))
function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * Float64(0.5 + Float64(z0 + z0)))))))))
end
function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((pi * (0.5 + (z0 + z0))))))));
end
code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(Pi * N[(0.5 + N[(z0 + z0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right)

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 7 alternatives:

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

Initial Program: 59.9% accurate, 1.0× speedup?

\[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
(FPCore (z1 z2 z0)
  :precision binary64
  (-
 1.0
 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI (+ 0.5 (+ z0 z0))))))))))
double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * (0.5 + (z0 + z0))))))));
}
public static double code(double z1, double z2, double z0) {
	return 1.0 - Math.cos((-2.0 * Math.atan(((z1 / z2) * Math.tan((Math.PI * (0.5 + (z0 + z0))))))));
}
def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * (0.5 + (z0 + z0))))))))
function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * Float64(0.5 + Float64(z0 + z0)))))))))
end
function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((pi * (0.5 + (z0 + z0))))))));
end
code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(Pi * N[(0.5 + N[(z0 + z0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right)

Alternative 1: 91.5% accurate, 0.6× speedup?

\[\begin{array}{l} t_0 := \left(z0 + z0\right) \cdot \pi\\ t_1 := \cos \left(-\pi\right)\\ t_2 := 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\frac{\left(0.5 - t\_1 \cdot 0.5\right) \cdot \pi}{\left(t\_1 + 1\right) \cdot 0.5} + \pi\right) \cdot \left(z0 + z0\right) - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)\right)\\ \mathbf{if}\;z0 \leq -48000000:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;z0 \leq 43:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_0 \cdot z1}{\left(-\sin t\_0\right) \cdot z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]
(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (* (+ z0 z0) PI))
       (t_1 (cos (- PI)))
       (t_2
        (-
         1.0
         (cos
          (*
           -2.0
           (atan
            (/
             (*
              (-
               (*
                (+
                 (/ (* (- 0.5 (* t_1 0.5)) PI) (* (+ t_1 1.0) 0.5))
                 PI)
                (+ z0 z0))
               (tan (* -0.5 PI)))
              z1)
             z2)))))))
  (if (<= z0 -48000000.0)
    t_2
    (if (<= z0 43.0)
      (-
       1.0
       (cos
        (* -2.0 (atan (/ (* (cos t_0) z1) (* (- (sin t_0)) z2))))))
      t_2))))
double code(double z1, double z2, double z0) {
	double t_0 = (z0 + z0) * ((double) M_PI);
	double t_1 = cos(-((double) M_PI));
	double t_2 = 1.0 - cos((-2.0 * atan(((((((((0.5 - (t_1 * 0.5)) * ((double) M_PI)) / ((t_1 + 1.0) * 0.5)) + ((double) M_PI)) * (z0 + z0)) - tan((-0.5 * ((double) M_PI)))) * z1) / z2))));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = t_2;
	} else if (z0 <= 43.0) {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_0) * z1) / (-sin(t_0) * z2)))));
	} else {
		tmp = t_2;
	}
	return tmp;
}
public static double code(double z1, double z2, double z0) {
	double t_0 = (z0 + z0) * Math.PI;
	double t_1 = Math.cos(-Math.PI);
	double t_2 = 1.0 - Math.cos((-2.0 * Math.atan(((((((((0.5 - (t_1 * 0.5)) * Math.PI) / ((t_1 + 1.0) * 0.5)) + Math.PI) * (z0 + z0)) - Math.tan((-0.5 * Math.PI))) * z1) / z2))));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = t_2;
	} else if (z0 <= 43.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_0) * z1) / (-Math.sin(t_0) * z2)))));
	} else {
		tmp = t_2;
	}
	return tmp;
}
def code(z1, z2, z0):
	t_0 = (z0 + z0) * math.pi
	t_1 = math.cos(-math.pi)
	t_2 = 1.0 - math.cos((-2.0 * math.atan(((((((((0.5 - (t_1 * 0.5)) * math.pi) / ((t_1 + 1.0) * 0.5)) + math.pi) * (z0 + z0)) - math.tan((-0.5 * math.pi))) * z1) / z2))))
	tmp = 0
	if z0 <= -48000000.0:
		tmp = t_2
	elif z0 <= 43.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_0) * z1) / (-math.sin(t_0) * z2)))))
	else:
		tmp = t_2
	return tmp
function code(z1, z2, z0)
	t_0 = Float64(Float64(z0 + z0) * pi)
	t_1 = cos(Float64(-pi))
	t_2 = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(0.5 - Float64(t_1 * 0.5)) * pi) / Float64(Float64(t_1 + 1.0) * 0.5)) + pi) * Float64(z0 + z0)) - tan(Float64(-0.5 * pi))) * z1) / z2)))))
	tmp = 0.0
	if (z0 <= -48000000.0)
		tmp = t_2;
	elseif (z0 <= 43.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_0) * z1) / Float64(Float64(-sin(t_0)) * z2))))));
	else
		tmp = t_2;
	end
	return tmp
end
function tmp_2 = code(z1, z2, z0)
	t_0 = (z0 + z0) * pi;
	t_1 = cos(-pi);
	t_2 = 1.0 - cos((-2.0 * atan(((((((((0.5 - (t_1 * 0.5)) * pi) / ((t_1 + 1.0) * 0.5)) + pi) * (z0 + z0)) - tan((-0.5 * pi))) * z1) / z2))));
	tmp = 0.0;
	if (z0 <= -48000000.0)
		tmp = t_2;
	elseif (z0 <= 43.0)
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_0) * z1) / (-sin(t_0) * z2)))));
	else
		tmp = t_2;
	end
	tmp_2 = tmp;
end
code[z1_, z2_, z0_] := Block[{t$95$0 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$1 = N[Cos[(-Pi)], $MachinePrecision]}, Block[{t$95$2 = N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(0.5 - N[(t$95$1 * 0.5), $MachinePrecision]), $MachinePrecision] * Pi), $MachinePrecision] / N[(N[(t$95$1 + 1.0), $MachinePrecision] * 0.5), $MachinePrecision]), $MachinePrecision] + Pi), $MachinePrecision] * N[(z0 + z0), $MachinePrecision]), $MachinePrecision] - N[Tan[N[(-0.5 * Pi), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z0, -48000000.0], t$95$2, If[LessEqual[z0, 43.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$0], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$0], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], t$95$2]]]]]
\begin{array}{l}
t_0 := \left(z0 + z0\right) \cdot \pi\\
t_1 := \cos \left(-\pi\right)\\
t_2 := 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\frac{\left(0.5 - t\_1 \cdot 0.5\right) \cdot \pi}{\left(t\_1 + 1\right) \cdot 0.5} + \pi\right) \cdot \left(z0 + z0\right) - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)\right)\\
\mathbf{if}\;z0 \leq -48000000:\\
\;\;\;\;t\_2\\

\mathbf{elif}\;z0 \leq 43:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_0 \cdot z1}{\left(-\sin t\_0\right) \cdot z2}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;t\_2\\


\end{array}
Derivation
  1. Split input into 2 regimes
  2. if z0 < -4.8e7 or 43 < z0

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\left(z0 \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(\frac{1}{2} \cdot \pi\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}}\right) + \frac{\sin \left(\frac{1}{2} \cdot \pi\right)}{\cos \left(\frac{1}{2} \cdot \pi\right)}\right)}\right)\right) \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \left(z0 \cdot \left(2 \cdot \mathsf{PI}\left(\right) - -2 \cdot \frac{\mathsf{PI}\left(\right) \cdot {\sin \left(\frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)}^{2}}\right) + \color{blue}{\frac{\sin \left(\frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)}}\right)\right)\right) \]
    4. Applied rewrites71.7%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\left(z0 \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right) + \frac{\sin \left(0.5 \cdot \pi\right)}{\cos \left(0.5 \cdot \pi\right)}\right)}\right)\right) \]
    5. Applied rewrites72.4%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\left(\left(2 \cdot \left(\pi + \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right) \cdot \pi\right)\right) \cdot z0 - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)}\right) \]
    6. Applied rewrites84.6%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(2 \cdot \left(\pi + \frac{\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\pi \cdot 0.5\right)\right)\right) \cdot \pi}{0.5 + 0.5 \cdot \cos \left(2 \cdot \left(-0.5 \cdot \pi\right)\right)}\right)\right) \cdot z0 - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)\right) \]
    7. Applied rewrites84.6%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\frac{\left(0.5 - \cos \left(-\pi\right) \cdot 0.5\right) \cdot \pi}{\left(\cos \left(-\pi\right) + 1\right) \cdot 0.5} + \pi\right) \cdot \left(z0 + z0\right) - \tan \color{blue}{\left(-0.5 \cdot \pi\right)}\right) \cdot z1}{z2}\right)\right) \]

    if -4.8e7 < z0 < 43

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
      2. lift-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
      3. lift-tan.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
      4. tan-quotN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
      5. frac-timesN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
      6. *-commutativeN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
      7. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
    3. Applied rewrites69.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 2: 89.6% accurate, 0.2× speedup?

\[\begin{array}{l} t_0 := \tan \left(\pi \cdot 0.5\right)\\ t_1 := t\_0 \cdot t\_0\\ t_2 := \left(-1.3333333333333333 \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\\ t_3 := 2 \cdot \left(\pi + t\_1 \cdot \pi\right)\\ \mathbf{if}\;\tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right) \leq 40000000000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\pi + \pi\right) \cdot \left(t\_3 \cdot t\_0\right) + \left(t\_2 - \left(\left(\left(\left(\pi \cdot \pi\right) \cdot -2\right) \cdot t\_3 - t\_2 \cdot t\_1\right) + \left(-4 \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(t\_3 \cdot t\_1\right)\right)\right) \cdot z0\right) \cdot z0 + t\_3\right) \cdot z0 - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right)\\ \end{array} \]
(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (tan (* PI 0.5)))
       (t_1 (* t_0 t_0))
       (t_2 (* (* -1.3333333333333333 (* PI PI)) PI))
       (t_3 (* 2.0 (+ PI (* t_1 PI)))))
  (if (<= (tan (* PI (+ 0.5 (+ z0 z0)))) 40000000000000.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (*
          (-
           (*
            (+
             (*
              (+
               (* (+ PI PI) (* t_3 t_0))
               (*
                (-
                 t_2
                 (+
                  (- (* (* (* PI PI) -2.0) t_3) (* t_2 t_1))
                  (* (* -4.0 (* PI PI)) (* t_3 t_1))))
                z0))
              z0)
             t_3)
            z0)
           (tan (* -0.5 PI)))
          z1)
         z2)))))
    (- 1.0 (cos (* -2.0 (atan (* -0.5 (/ z1 (* z0 (* z2 PI)))))))))))
double code(double z1, double z2, double z0) {
	double t_0 = tan((((double) M_PI) * 0.5));
	double t_1 = t_0 * t_0;
	double t_2 = (-1.3333333333333333 * (((double) M_PI) * ((double) M_PI))) * ((double) M_PI);
	double t_3 = 2.0 * (((double) M_PI) + (t_1 * ((double) M_PI)));
	double tmp;
	if (tan((((double) M_PI) * (0.5 + (z0 + z0)))) <= 40000000000000.0) {
		tmp = 1.0 - cos((-2.0 * atan((((((((((((double) M_PI) + ((double) M_PI)) * (t_3 * t_0)) + ((t_2 - (((((((double) M_PI) * ((double) M_PI)) * -2.0) * t_3) - (t_2 * t_1)) + ((-4.0 * (((double) M_PI) * ((double) M_PI))) * (t_3 * t_1)))) * z0)) * z0) + t_3) * z0) - tan((-0.5 * ((double) M_PI)))) * z1) / z2))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan((-0.5 * (z1 / (z0 * (z2 * ((double) M_PI))))))));
	}
	return tmp;
}
public static double code(double z1, double z2, double z0) {
	double t_0 = Math.tan((Math.PI * 0.5));
	double t_1 = t_0 * t_0;
	double t_2 = (-1.3333333333333333 * (Math.PI * Math.PI)) * Math.PI;
	double t_3 = 2.0 * (Math.PI + (t_1 * Math.PI));
	double tmp;
	if (Math.tan((Math.PI * (0.5 + (z0 + z0)))) <= 40000000000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((((((((((Math.PI + Math.PI) * (t_3 * t_0)) + ((t_2 - (((((Math.PI * Math.PI) * -2.0) * t_3) - (t_2 * t_1)) + ((-4.0 * (Math.PI * Math.PI)) * (t_3 * t_1)))) * z0)) * z0) + t_3) * z0) - Math.tan((-0.5 * Math.PI))) * z1) / z2))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((-0.5 * (z1 / (z0 * (z2 * Math.PI)))))));
	}
	return tmp;
}
def code(z1, z2, z0):
	t_0 = math.tan((math.pi * 0.5))
	t_1 = t_0 * t_0
	t_2 = (-1.3333333333333333 * (math.pi * math.pi)) * math.pi
	t_3 = 2.0 * (math.pi + (t_1 * math.pi))
	tmp = 0
	if math.tan((math.pi * (0.5 + (z0 + z0)))) <= 40000000000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan((((((((((math.pi + math.pi) * (t_3 * t_0)) + ((t_2 - (((((math.pi * math.pi) * -2.0) * t_3) - (t_2 * t_1)) + ((-4.0 * (math.pi * math.pi)) * (t_3 * t_1)))) * z0)) * z0) + t_3) * z0) - math.tan((-0.5 * math.pi))) * z1) / z2))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan((-0.5 * (z1 / (z0 * (z2 * math.pi)))))))
	return tmp
function code(z1, z2, z0)
	t_0 = tan(Float64(pi * 0.5))
	t_1 = Float64(t_0 * t_0)
	t_2 = Float64(Float64(-1.3333333333333333 * Float64(pi * pi)) * pi)
	t_3 = Float64(2.0 * Float64(pi + Float64(t_1 * pi)))
	tmp = 0.0
	if (tan(Float64(pi * Float64(0.5 + Float64(z0 + z0)))) <= 40000000000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(pi + pi) * Float64(t_3 * t_0)) + Float64(Float64(t_2 - Float64(Float64(Float64(Float64(Float64(pi * pi) * -2.0) * t_3) - Float64(t_2 * t_1)) + Float64(Float64(-4.0 * Float64(pi * pi)) * Float64(t_3 * t_1)))) * z0)) * z0) + t_3) * z0) - tan(Float64(-0.5 * pi))) * z1) / z2)))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(-0.5 * Float64(z1 / Float64(z0 * Float64(z2 * pi))))))));
	end
	return tmp
end
function tmp_2 = code(z1, z2, z0)
	t_0 = tan((pi * 0.5));
	t_1 = t_0 * t_0;
	t_2 = (-1.3333333333333333 * (pi * pi)) * pi;
	t_3 = 2.0 * (pi + (t_1 * pi));
	tmp = 0.0;
	if (tan((pi * (0.5 + (z0 + z0)))) <= 40000000000000.0)
		tmp = 1.0 - cos((-2.0 * atan((((((((((pi + pi) * (t_3 * t_0)) + ((t_2 - (((((pi * pi) * -2.0) * t_3) - (t_2 * t_1)) + ((-4.0 * (pi * pi)) * (t_3 * t_1)))) * z0)) * z0) + t_3) * z0) - tan((-0.5 * pi))) * z1) / z2))));
	else
		tmp = 1.0 - cos((-2.0 * atan((-0.5 * (z1 / (z0 * (z2 * pi)))))));
	end
	tmp_2 = tmp;
end
code[z1_, z2_, z0_] := Block[{t$95$0 = N[Tan[N[(Pi * 0.5), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 * t$95$0), $MachinePrecision]}, Block[{t$95$2 = N[(N[(-1.3333333333333333 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$3 = N[(2.0 * N[(Pi + N[(t$95$1 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[Tan[N[(Pi * N[(0.5 + N[(z0 + z0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 40000000000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(Pi + Pi), $MachinePrecision] * N[(t$95$3 * t$95$0), $MachinePrecision]), $MachinePrecision] + N[(N[(t$95$2 - N[(N[(N[(N[(N[(Pi * Pi), $MachinePrecision] * -2.0), $MachinePrecision] * t$95$3), $MachinePrecision] - N[(t$95$2 * t$95$1), $MachinePrecision]), $MachinePrecision] + N[(N[(-4.0 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision] * N[(t$95$3 * t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] + t$95$3), $MachinePrecision] * z0), $MachinePrecision] - N[Tan[N[(-0.5 * Pi), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(-0.5 * N[(z1 / N[(z0 * N[(z2 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]
\begin{array}{l}
t_0 := \tan \left(\pi \cdot 0.5\right)\\
t_1 := t\_0 \cdot t\_0\\
t_2 := \left(-1.3333333333333333 \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\\
t_3 := 2 \cdot \left(\pi + t\_1 \cdot \pi\right)\\
\mathbf{if}\;\tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right) \leq 40000000000000:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\pi + \pi\right) \cdot \left(t\_3 \cdot t\_0\right) + \left(t\_2 - \left(\left(\left(\left(\pi \cdot \pi\right) \cdot -2\right) \cdot t\_3 - t\_2 \cdot t\_1\right) + \left(-4 \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(t\_3 \cdot t\_1\right)\right)\right) \cdot z0\right) \cdot z0 + t\_3\right) \cdot z0 - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right)\\


\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (tan.f64 (*.f64 (PI.f64) (+.f64 #s(literal 1/2 binary64) (+.f64 z0 z0)))) < 4e13

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\left(z0 \cdot \left(\left(2 \cdot \pi + z0 \cdot \left(z0 \cdot \left(\frac{-4}{3} \cdot {\pi}^{3} - \left(-4 \cdot \frac{{\pi}^{2} \cdot \left({\sin \left(\frac{1}{2} \cdot \pi\right)}^{2} \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(\frac{1}{2} \cdot \pi\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}}\right)\right)}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}} + \left(-2 \cdot \left({\pi}^{2} \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(\frac{1}{2} \cdot \pi\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}}\right)\right) + \frac{4}{3} \cdot \frac{{\pi}^{3} \cdot {\sin \left(\frac{1}{2} \cdot \pi\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}}\right)\right)\right) - -2 \cdot \frac{\pi \cdot \left(\sin \left(\frac{1}{2} \cdot \pi\right) \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(\frac{1}{2} \cdot \pi\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}}\right)\right)}{\cos \left(\frac{1}{2} \cdot \pi\right)}\right)\right) - -2 \cdot \frac{\pi \cdot {\sin \left(\frac{1}{2} \cdot \pi\right)}^{2}}{{\cos \left(\frac{1}{2} \cdot \pi\right)}^{2}}\right) + \frac{\sin \left(\frac{1}{2} \cdot \pi\right)}{\cos \left(\frac{1}{2} \cdot \pi\right)}\right)}\right)\right) \]
    3. Applied rewrites76.4%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\left(z0 \cdot \left(\left(2 \cdot \pi + z0 \cdot \left(z0 \cdot \left(-1.3333333333333333 \cdot {\pi}^{3} - \left(-4 \cdot \frac{{\pi}^{2} \cdot \left({\sin \left(0.5 \cdot \pi\right)}^{2} \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right)\right)}{{\cos \left(0.5 \cdot \pi\right)}^{2}} + \left(-2 \cdot \left({\pi}^{2} \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right)\right) + 1.3333333333333333 \cdot \frac{{\pi}^{3} \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right)\right)\right) - -2 \cdot \frac{\pi \cdot \left(\sin \left(0.5 \cdot \pi\right) \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right)\right)}{\cos \left(0.5 \cdot \pi\right)}\right)\right) - -2 \cdot \frac{\pi \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right) + \frac{\sin \left(0.5 \cdot \pi\right)}{\cos \left(0.5 \cdot \pi\right)}\right)}\right)\right) \]
    4. Applied rewrites80.6%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\left(\left(\left(\left(\pi + \pi\right) \cdot \left(\left(2 \cdot \left(\pi + \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right) \cdot \pi\right)\right) \cdot \tan \left(\pi \cdot 0.5\right)\right) + \left(\left(-1.3333333333333333 \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi - \left(\left(\left(\left(\pi \cdot \pi\right) \cdot -2\right) \cdot \left(2 \cdot \left(\pi + \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right) \cdot \pi\right)\right) - \left(\left(-1.3333333333333333 \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right) \cdot \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right)\right) + \left(-4 \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(\left(2 \cdot \left(\pi + \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right) \cdot \pi\right)\right) \cdot \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right)\right)\right)\right) \cdot z0\right) \cdot z0 + 2 \cdot \left(\pi + \left(\tan \left(\pi \cdot 0.5\right) \cdot \tan \left(\pi \cdot 0.5\right)\right) \cdot \pi\right)\right) \cdot z0 - \tan \left(-0.5 \cdot \pi\right)\right) \cdot z1}{z2}\right)}\right) \]

    if 4e13 < (tan.f64 (*.f64 (PI.f64) (+.f64 #s(literal 1/2 binary64) (+.f64 z0 z0))))

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
      2. lift-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
      3. lift-tan.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
      4. tan-quotN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
      5. frac-timesN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
      6. *-commutativeN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
      7. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
    3. Applied rewrites69.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
    4. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)}\right) \]
    5. Step-by-step derivation
      1. lower-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \color{blue}{\frac{z1}{z0 \cdot \left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
      2. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{\color{blue}{z0 \cdot \left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
      3. lower-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \color{blue}{\left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
      4. lower-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}\right)\right) \]
      5. lower-PI.f6459.1%

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right) \]
    6. Applied rewrites59.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)}\right) \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 3: 86.2% accurate, 0.6× speedup?

\[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\pi}^{2}\right)\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
(FPCore (z1 z2 z0)
  :precision binary64
  (-
 1.0
 (cos
  (*
   -2.0
   (atan
    (/
     (* (+ 1.0 (* -2.0 (* (pow z0 2.0) (pow PI 2.0)))) z1)
     (* (- (sin (* (+ z0 z0) PI))) z2)))))))
double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan((((1.0 + (-2.0 * (pow(z0, 2.0) * pow(((double) M_PI), 2.0)))) * z1) / (-sin(((z0 + z0) * ((double) M_PI))) * z2)))));
}
public static double code(double z1, double z2, double z0) {
	return 1.0 - Math.cos((-2.0 * Math.atan((((1.0 + (-2.0 * (Math.pow(z0, 2.0) * Math.pow(Math.PI, 2.0)))) * z1) / (-Math.sin(((z0 + z0) * Math.PI)) * z2)))));
}
def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan((((1.0 + (-2.0 * (math.pow(z0, 2.0) * math.pow(math.pi, 2.0)))) * z1) / (-math.sin(((z0 + z0) * math.pi)) * z2)))))
function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(1.0 + Float64(-2.0 * Float64((z0 ^ 2.0) * (pi ^ 2.0)))) * z1) / Float64(Float64(-sin(Float64(Float64(z0 + z0) * pi))) * z2))))))
end
function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan((((1.0 + (-2.0 * ((z0 ^ 2.0) * (pi ^ 2.0)))) * z1) / (-sin(((z0 + z0) * pi)) * z2)))));
end
code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(1.0 + N[(-2.0 * N[(N[Power[z0, 2.0], $MachinePrecision] * N[Power[Pi, 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\pi}^{2}\right)\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right)
Derivation
  1. Initial program 59.9%

    \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
  2. Step-by-step derivation
    1. lift-*.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
    2. lift-/.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
    3. lift-tan.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
    4. tan-quotN/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
    5. frac-timesN/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
    6. *-commutativeN/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
    7. lower-/.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
  3. Applied rewrites69.1%

    \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
  4. Taylor expanded in z0 around 0

    \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\color{blue}{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\pi}^{2}\right)\right)} \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
  5. Step-by-step derivation
    1. lower-+.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + \color{blue}{-2 \cdot \left({z0}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
    2. lower-*.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \color{blue}{\left({z0}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
    3. lower-*.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \left({z0}^{2} \cdot \color{blue}{{\mathsf{PI}\left(\right)}^{2}}\right)\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
    4. lower-pow.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\color{blue}{\mathsf{PI}\left(\right)}}^{2}\right)\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
    5. lower-pow.f64N/A

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{2}}\right)\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
    6. lower-PI.f6486.2%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\pi}^{2}\right)\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
  6. Applied rewrites86.2%

    \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\color{blue}{\left(1 + -2 \cdot \left({z0}^{2} \cdot {\pi}^{2}\right)\right)} \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)\right) \]
  7. Add Preprocessing

Alternative 4: 81.0% accurate, 0.8× speedup?

\[\begin{array}{l} t_0 := \frac{\left|z1\right|}{\left|z2\right|}\\ t_1 := \frac{\left|z1\right| \cdot \pi}{\left|z2\right|}\\ \mathbf{if}\;t\_0 \leq 140000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot t\_1 - -0.3333333333333333 \cdot t\_1\right)\right) + -0.5 \cdot \frac{\left|z1\right|}{\left|z2\right| \cdot \pi}}{z0}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(t\_0 \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right)\\ \end{array} \]
(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (/ (fabs z1) (fabs z2)))
       (t_1 (/ (* (fabs z1) PI) (fabs z2))))
  (if (<= t_0 140000000.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (+
          (*
           -1.0
           (*
            (pow z0 2.0)
            (- (* -1.0 t_1) (* -0.3333333333333333 t_1))))
          (* -0.5 (/ (fabs z1) (* (fabs z2) PI))))
         z0)))))
    (-
     1.0
     (cos (* -2.0 (atan (* t_0 (tan (* PI (+ 0.5 (+ z0 z0))))))))))))
double code(double z1, double z2, double z0) {
	double t_0 = fabs(z1) / fabs(z2);
	double t_1 = (fabs(z1) * ((double) M_PI)) / fabs(z2);
	double tmp;
	if (t_0 <= 140000000.0) {
		tmp = 1.0 - cos((-2.0 * atan((((-1.0 * (pow(z0, 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (fabs(z1) / (fabs(z2) * ((double) M_PI))))) / z0))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan((t_0 * tan((((double) M_PI) * (0.5 + (z0 + z0))))))));
	}
	return tmp;
}
public static double code(double z1, double z2, double z0) {
	double t_0 = Math.abs(z1) / Math.abs(z2);
	double t_1 = (Math.abs(z1) * Math.PI) / Math.abs(z2);
	double tmp;
	if (t_0 <= 140000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((((-1.0 * (Math.pow(z0, 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (Math.abs(z1) / (Math.abs(z2) * Math.PI)))) / z0))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((t_0 * Math.tan((Math.PI * (0.5 + (z0 + z0))))))));
	}
	return tmp;
}
def code(z1, z2, z0):
	t_0 = math.fabs(z1) / math.fabs(z2)
	t_1 = (math.fabs(z1) * math.pi) / math.fabs(z2)
	tmp = 0
	if t_0 <= 140000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan((((-1.0 * (math.pow(z0, 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (math.fabs(z1) / (math.fabs(z2) * math.pi)))) / z0))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan((t_0 * math.tan((math.pi * (0.5 + (z0 + z0))))))))
	return tmp
function code(z1, z2, z0)
	t_0 = Float64(abs(z1) / abs(z2))
	t_1 = Float64(Float64(abs(z1) * pi) / abs(z2))
	tmp = 0.0
	if (t_0 <= 140000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(-1.0 * Float64((z0 ^ 2.0) * Float64(Float64(-1.0 * t_1) - Float64(-0.3333333333333333 * t_1)))) + Float64(-0.5 * Float64(abs(z1) / Float64(abs(z2) * pi)))) / z0)))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(t_0 * tan(Float64(pi * Float64(0.5 + Float64(z0 + z0)))))))));
	end
	return tmp
end
function tmp_2 = code(z1, z2, z0)
	t_0 = abs(z1) / abs(z2);
	t_1 = (abs(z1) * pi) / abs(z2);
	tmp = 0.0;
	if (t_0 <= 140000000.0)
		tmp = 1.0 - cos((-2.0 * atan((((-1.0 * ((z0 ^ 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (abs(z1) / (abs(z2) * pi)))) / z0))));
	else
		tmp = 1.0 - cos((-2.0 * atan((t_0 * tan((pi * (0.5 + (z0 + z0))))))));
	end
	tmp_2 = tmp;
end
code[z1_, z2_, z0_] := Block[{t$95$0 = N[(N[Abs[z1], $MachinePrecision] / N[Abs[z2], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(N[Abs[z1], $MachinePrecision] * Pi), $MachinePrecision] / N[Abs[z2], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$0, 140000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(-1.0 * N[(N[Power[z0, 2.0], $MachinePrecision] * N[(N[(-1.0 * t$95$1), $MachinePrecision] - N[(-0.3333333333333333 * t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(-0.5 * N[(N[Abs[z1], $MachinePrecision] / N[(N[Abs[z2], $MachinePrecision] * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / z0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(t$95$0 * N[Tan[N[(Pi * N[(0.5 + N[(z0 + z0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]
\begin{array}{l}
t_0 := \frac{\left|z1\right|}{\left|z2\right|}\\
t_1 := \frac{\left|z1\right| \cdot \pi}{\left|z2\right|}\\
\mathbf{if}\;t\_0 \leq 140000000:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot t\_1 - -0.3333333333333333 \cdot t\_1\right)\right) + -0.5 \cdot \frac{\left|z1\right|}{\left|z2\right| \cdot \pi}}{z0}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(t\_0 \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right)\\


\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 z1 z2) < 1.4e8

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
      2. lift-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
      3. lift-tan.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
      4. tan-quotN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
      5. frac-timesN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
      6. *-commutativeN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
      7. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
    3. Applied rewrites69.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
    4. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot \frac{z1 \cdot \pi}{z2} - \frac{-1}{3} \cdot \frac{z1 \cdot \pi}{z2}\right)\right) + \frac{-1}{2} \cdot \frac{z1}{z2 \cdot \pi}}{z0}\right)}\right) \]
    5. Step-by-step derivation
      1. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot \frac{z1 \cdot \mathsf{PI}\left(\right)}{z2} - \frac{-1}{3} \cdot \frac{z1 \cdot \mathsf{PI}\left(\right)}{z2}\right)\right) + \frac{-1}{2} \cdot \frac{z1}{z2 \cdot \mathsf{PI}\left(\right)}}{\color{blue}{z0}}\right)\right) \]
    6. Applied rewrites68.0%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot \frac{z1 \cdot \pi}{z2} - -0.3333333333333333 \cdot \frac{z1 \cdot \pi}{z2}\right)\right) + -0.5 \cdot \frac{z1}{z2 \cdot \pi}}{z0}\right)}\right) \]

    if 1.4e8 < (/.f64 z1 z2)

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 5: 81.0% accurate, 0.4× speedup?

\[\begin{array}{l} t_0 := \left(z0 + z0\right) \cdot \pi\\ t_1 := \frac{z1 \cdot \pi}{z2}\\ \mathbf{if}\;\cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \leq -0.999999998:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_0 \cdot z1}{\left(-\sin t\_0\right) \cdot z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot t\_1 - -0.3333333333333333 \cdot t\_1\right)\right) + -0.5 \cdot \frac{z1}{z2 \cdot \pi}}{z0}\right)\right)\\ \end{array} \]
(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (* (+ z0 z0) PI)) (t_1 (/ (* z1 PI) z2)))
  (if (<=
       (cos
        (* -2.0 (atan (* (/ z1 z2) (tan (* PI (+ 0.5 (+ z0 z0))))))))
       -0.999999998)
    (-
     1.0
     (cos (* -2.0 (atan (/ (* (cos t_0) z1) (* (- (sin t_0)) z2))))))
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (+
          (*
           -1.0
           (*
            (pow z0 2.0)
            (- (* -1.0 t_1) (* -0.3333333333333333 t_1))))
          (* -0.5 (/ z1 (* z2 PI))))
         z0))))))))
double code(double z1, double z2, double z0) {
	double t_0 = (z0 + z0) * ((double) M_PI);
	double t_1 = (z1 * ((double) M_PI)) / z2;
	double tmp;
	if (cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * (0.5 + (z0 + z0)))))))) <= -0.999999998) {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_0) * z1) / (-sin(t_0) * z2)))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan((((-1.0 * (pow(z0, 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (z1 / (z2 * ((double) M_PI))))) / z0))));
	}
	return tmp;
}
public static double code(double z1, double z2, double z0) {
	double t_0 = (z0 + z0) * Math.PI;
	double t_1 = (z1 * Math.PI) / z2;
	double tmp;
	if (Math.cos((-2.0 * Math.atan(((z1 / z2) * Math.tan((Math.PI * (0.5 + (z0 + z0)))))))) <= -0.999999998) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_0) * z1) / (-Math.sin(t_0) * z2)))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((((-1.0 * (Math.pow(z0, 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (z1 / (z2 * Math.PI)))) / z0))));
	}
	return tmp;
}
def code(z1, z2, z0):
	t_0 = (z0 + z0) * math.pi
	t_1 = (z1 * math.pi) / z2
	tmp = 0
	if math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * (0.5 + (z0 + z0)))))))) <= -0.999999998:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_0) * z1) / (-math.sin(t_0) * z2)))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan((((-1.0 * (math.pow(z0, 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (z1 / (z2 * math.pi)))) / z0))))
	return tmp
function code(z1, z2, z0)
	t_0 = Float64(Float64(z0 + z0) * pi)
	t_1 = Float64(Float64(z1 * pi) / z2)
	tmp = 0.0
	if (cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * Float64(0.5 + Float64(z0 + z0)))))))) <= -0.999999998)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_0) * z1) / Float64(Float64(-sin(t_0)) * z2))))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(-1.0 * Float64((z0 ^ 2.0) * Float64(Float64(-1.0 * t_1) - Float64(-0.3333333333333333 * t_1)))) + Float64(-0.5 * Float64(z1 / Float64(z2 * pi)))) / z0)))));
	end
	return tmp
end
function tmp_2 = code(z1, z2, z0)
	t_0 = (z0 + z0) * pi;
	t_1 = (z1 * pi) / z2;
	tmp = 0.0;
	if (cos((-2.0 * atan(((z1 / z2) * tan((pi * (0.5 + (z0 + z0)))))))) <= -0.999999998)
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_0) * z1) / (-sin(t_0) * z2)))));
	else
		tmp = 1.0 - cos((-2.0 * atan((((-1.0 * ((z0 ^ 2.0) * ((-1.0 * t_1) - (-0.3333333333333333 * t_1)))) + (-0.5 * (z1 / (z2 * pi)))) / z0))));
	end
	tmp_2 = tmp;
end
code[z1_, z2_, z0_] := Block[{t$95$0 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$1 = N[(N[(z1 * Pi), $MachinePrecision] / z2), $MachinePrecision]}, If[LessEqual[N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(Pi * N[(0.5 + N[(z0 + z0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision], -0.999999998], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$0], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$0], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(-1.0 * N[(N[Power[z0, 2.0], $MachinePrecision] * N[(N[(-1.0 * t$95$1), $MachinePrecision] - N[(-0.3333333333333333 * t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(-0.5 * N[(z1 / N[(z2 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / z0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]
\begin{array}{l}
t_0 := \left(z0 + z0\right) \cdot \pi\\
t_1 := \frac{z1 \cdot \pi}{z2}\\
\mathbf{if}\;\cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \leq -0.999999998:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_0 \cdot z1}{\left(-\sin t\_0\right) \cdot z2}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot t\_1 - -0.3333333333333333 \cdot t\_1\right)\right) + -0.5 \cdot \frac{z1}{z2 \cdot \pi}}{z0}\right)\right)\\


\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (*.f64 #s(literal -2 binary64) (atan.f64 (*.f64 (/.f64 z1 z2) (tan.f64 (*.f64 (PI.f64) (+.f64 #s(literal 1/2 binary64) (+.f64 z0 z0)))))))) < -0.99999999799999995

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
      2. lift-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
      3. lift-tan.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
      4. tan-quotN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
      5. frac-timesN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
      6. *-commutativeN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
      7. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
    3. Applied rewrites69.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]

    if -0.99999999799999995 < (cos.f64 (*.f64 #s(literal -2 binary64) (atan.f64 (*.f64 (/.f64 z1 z2) (tan.f64 (*.f64 (PI.f64) (+.f64 #s(literal 1/2 binary64) (+.f64 z0 z0))))))))

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
      2. lift-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
      3. lift-tan.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
      4. tan-quotN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
      5. frac-timesN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
      6. *-commutativeN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
      7. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
    3. Applied rewrites69.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
    4. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot \frac{z1 \cdot \pi}{z2} - \frac{-1}{3} \cdot \frac{z1 \cdot \pi}{z2}\right)\right) + \frac{-1}{2} \cdot \frac{z1}{z2 \cdot \pi}}{z0}\right)}\right) \]
    5. Step-by-step derivation
      1. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot \frac{z1 \cdot \mathsf{PI}\left(\right)}{z2} - \frac{-1}{3} \cdot \frac{z1 \cdot \mathsf{PI}\left(\right)}{z2}\right)\right) + \frac{-1}{2} \cdot \frac{z1}{z2 \cdot \mathsf{PI}\left(\right)}}{\color{blue}{z0}}\right)\right) \]
    6. Applied rewrites68.0%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1 \cdot \left({z0}^{2} \cdot \left(-1 \cdot \frac{z1 \cdot \pi}{z2} - -0.3333333333333333 \cdot \frac{z1 \cdot \pi}{z2}\right)\right) + -0.5 \cdot \frac{z1}{z2 \cdot \pi}}{z0}\right)}\right) \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 6: 70.2% accurate, 0.8× speedup?

\[\begin{array}{l} \mathbf{if}\;\tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right) \leq 40000000000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot 0.5\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right)\\ \end{array} \]
(FPCore (z1 z2 z0)
  :precision binary64
  (if (<= (tan (* PI (+ 0.5 (+ z0 z0)))) 40000000000000.0)
  (- 1.0 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI 0.5)))))))
  (- 1.0 (cos (* -2.0 (atan (* -0.5 (/ z1 (* z0 (* z2 PI))))))))))
double code(double z1, double z2, double z0) {
	double tmp;
	if (tan((((double) M_PI) * (0.5 + (z0 + z0)))) <= 40000000000000.0) {
		tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * 0.5))))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan((-0.5 * (z1 / (z0 * (z2 * ((double) M_PI))))))));
	}
	return tmp;
}
public static double code(double z1, double z2, double z0) {
	double tmp;
	if (Math.tan((Math.PI * (0.5 + (z0 + z0)))) <= 40000000000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((z1 / z2) * Math.tan((Math.PI * 0.5))))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((-0.5 * (z1 / (z0 * (z2 * Math.PI)))))));
	}
	return tmp;
}
def code(z1, z2, z0):
	tmp = 0
	if math.tan((math.pi * (0.5 + (z0 + z0)))) <= 40000000000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * 0.5))))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan((-0.5 * (z1 / (z0 * (z2 * math.pi)))))))
	return tmp
function code(z1, z2, z0)
	tmp = 0.0
	if (tan(Float64(pi * Float64(0.5 + Float64(z0 + z0)))) <= 40000000000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * 0.5)))))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(-0.5 * Float64(z1 / Float64(z0 * Float64(z2 * pi))))))));
	end
	return tmp
end
function tmp_2 = code(z1, z2, z0)
	tmp = 0.0;
	if (tan((pi * (0.5 + (z0 + z0)))) <= 40000000000000.0)
		tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((pi * 0.5))))));
	else
		tmp = 1.0 - cos((-2.0 * atan((-0.5 * (z1 / (z0 * (z2 * pi)))))));
	end
	tmp_2 = tmp;
end
code[z1_, z2_, z0_] := If[LessEqual[N[Tan[N[(Pi * N[(0.5 + N[(z0 + z0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 40000000000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(Pi * 0.5), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(-0.5 * N[(z1 / N[(z0 * N[(z2 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\mathbf{if}\;\tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right) \leq 40000000000000:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot 0.5\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right)\\


\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (tan.f64 (*.f64 (PI.f64) (+.f64 #s(literal 1/2 binary64) (+.f64 z0 z0)))) < 4e13

    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \color{blue}{\frac{1}{2}}\right)\right)\right) \]
    3. Step-by-step derivation
      1. Applied rewrites61.2%

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \color{blue}{0.5}\right)\right)\right) \]

      if 4e13 < (tan.f64 (*.f64 (PI.f64) (+.f64 #s(literal 1/2 binary64) (+.f64 z0 z0))))

      1. Initial program 59.9%

        \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
      2. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
        2. lift-/.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
        3. lift-tan.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
        4. tan-quotN/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
        5. frac-timesN/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
        6. *-commutativeN/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
        7. lower-/.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
      3. Applied rewrites69.1%

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
      4. Taylor expanded in z0 around 0

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)}\right) \]
      5. Step-by-step derivation
        1. lower-*.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \color{blue}{\frac{z1}{z0 \cdot \left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
        2. lower-/.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{\color{blue}{z0 \cdot \left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
        3. lower-*.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \color{blue}{\left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
        4. lower-*.f64N/A

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}\right)\right) \]
        5. lower-PI.f6459.1%

          \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right) \]
      6. Applied rewrites59.1%

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)}\right) \]
    4. Recombined 2 regimes into one program.
    5. Add Preprocessing

    Alternative 7: 59.1% accurate, 1.4× speedup?

    \[1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right) \]
    (FPCore (z1 z2 z0)
      :precision binary64
      (- 1.0 (cos (* -2.0 (atan (* -0.5 (/ z1 (* z0 (* z2 PI)))))))))
    double code(double z1, double z2, double z0) {
    	return 1.0 - cos((-2.0 * atan((-0.5 * (z1 / (z0 * (z2 * ((double) M_PI))))))));
    }
    
    public static double code(double z1, double z2, double z0) {
    	return 1.0 - Math.cos((-2.0 * Math.atan((-0.5 * (z1 / (z0 * (z2 * Math.PI)))))));
    }
    
    def code(z1, z2, z0):
    	return 1.0 - math.cos((-2.0 * math.atan((-0.5 * (z1 / (z0 * (z2 * math.pi)))))))
    
    function code(z1, z2, z0)
    	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(-0.5 * Float64(z1 / Float64(z0 * Float64(z2 * pi))))))))
    end
    
    function tmp = code(z1, z2, z0)
    	tmp = 1.0 - cos((-2.0 * atan((-0.5 * (z1 / (z0 * (z2 * pi)))))));
    end
    
    code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(-0.5 * N[(z1 / N[(z0 * N[(z2 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
    
    1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right)
    
    Derivation
    1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(0.5 + \left(z0 + z0\right)\right)\right)\right)\right) \]
    2. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)}\right) \]
      2. lift-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\color{blue}{\frac{z1}{z2}} \cdot \tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)\right)\right) \]
      3. lift-tan.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\tan \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)\right) \]
      4. tan-quotN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}}\right)\right) \]
      5. frac-timesN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{z2 \cdot \cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}\right)}\right) \]
      6. *-commutativeN/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}}\right)\right) \]
      7. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{z1 \cdot \sin \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right)}{\cos \left(\pi \cdot \left(\frac{1}{2} + \left(z0 + z0\right)\right)\right) \cdot z2}\right)}\right) \]
    3. Applied rewrites69.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{\cos \left(\left(z0 + z0\right) \cdot \pi\right) \cdot z1}{\left(-\sin \left(\left(z0 + z0\right) \cdot \pi\right)\right) \cdot z2}\right)}\right) \]
    4. Taylor expanded in z0 around 0

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)}\right) \]
    5. Step-by-step derivation
      1. lower-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \color{blue}{\frac{z1}{z0 \cdot \left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
      2. lower-/.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{\color{blue}{z0 \cdot \left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
      3. lower-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \color{blue}{\left(z2 \cdot \mathsf{PI}\left(\right)\right)}}\right)\right) \]
      4. lower-*.f64N/A

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{-1}{2} \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}\right)\right) \]
      5. lower-PI.f6459.1%

        \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)\right) \]
    6. Applied rewrites59.1%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \color{blue}{\left(-0.5 \cdot \frac{z1}{z0 \cdot \left(z2 \cdot \pi\right)}\right)}\right) \]
    7. Add Preprocessing

    Reproduce

    ?
    herbie shell --seed 2025250 
    (FPCore (z1 z2 z0)
      :name "(- 1 (cos (* -2 (atan (* (/ z1 z2) (tan (* PI (+ 1/2 (+ z0 z0)))))))))"
      :precision binary64
      (- 1.0 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI (+ 0.5 (+ z0 z0))))))))))