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

Percentage Accurate: 59.9% → 91.5%

Time: 8.9s

Alternatives: 8

Speedup: 1.0×

Specification

Math

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

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (-
 1.0
 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI (- (+ z0 z0) -0.5)))))))))

C

double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * ((z0 + z0) - -0.5)))))));
}

Java

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 * ((z0 + z0) - -0.5)))))));
}

Python

def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * ((z0 + z0) - -0.5)))))))

Julia

function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * Float64(Float64(z0 + z0) - -0.5))))))))
end

MATLAB

function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((pi * ((z0 + z0) - -0.5)))))));
end

Wolfram

code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(Pi * N[(N[(z0 + z0), $MachinePrecision] - -0.5), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

Initial Program: 59.9% accurate, 1.0× speedup

Math

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

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (-
 1.0
 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI (- (+ z0 z0) -0.5)))))))))

C

double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * ((z0 + z0) - -0.5)))))));
}

Java

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 * ((z0 + z0) - -0.5)))))));
}

Python

def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * ((z0 + z0) - -0.5)))))))

Julia

function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * Float64(Float64(z0 + z0) - -0.5))))))))
end

MATLAB

function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((pi * ((z0 + z0) - -0.5)))))));
end

Wolfram

code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(Pi * N[(N[(z0 + z0), $MachinePrecision] - -0.5), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

Alternative 1: 91.5% accurate, 0.3× speedup

Math

\[\begin{array}{l} t_0 := {\left(-\infty\right)}^{2}\\ t_1 := \pi - t\_0 \cdot \pi\\ t_2 := \left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi\\ t_3 := -4 \cdot \left(\pi \cdot \pi\right)\\ t_4 := t\_3 \cdot 2\\ t_5 := \left(z0 + z0\right) \cdot \pi\\ t_6 := \pi - \infty \cdot \pi\\ t_7 := \tan \left(\pi \cdot -0.5\right)\\ \mathbf{if}\;z0 \leq -48000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(t\_2 - t\_3 \cdot t\_6\right) + \infty \cdot \left(t\_2 - t\_4 \cdot t\_6\right)\right) \cdot z0 - \left(\left(\tan \left(1.5 \cdot \pi\right) \cdot 2\right) \cdot t\_6\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - t\_6 \cdot -2\right) \cdot z0 - t\_7\right) \cdot z1}{z2}\right)\right)\\ \mathbf{elif}\;z0 \leq 43:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_5 \cdot z1}{\left(-\sin t\_5\right) \cdot z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(t\_2 - t\_3 \cdot t\_1\right) + t\_0 \cdot \left(t\_2 - t\_4 \cdot t\_1\right)\right) \cdot z0 - \left(\left(\left(-\infty\right) \cdot 2\right) \cdot t\_1\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - t\_1 \cdot -2\right) \cdot z0 - t\_7\right) \cdot z1}{z2}\right)\right)\\ \end{array} \]

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (pow (- INFINITY) 2.0))
       (t_1 (- PI (* t_0 PI)))
       (t_2 (* (* (* PI PI) -1.3333333333333333) PI))
       (t_3 (* -4.0 (* PI PI)))
       (t_4 (* t_3 2.0))
       (t_5 (* (+ z0 z0) PI))
       (t_6 (- PI (* INFINITY PI)))
       (t_7 (tan (* PI -0.5))))
  (if (<= z0 -48000000.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (*
          (-
           (*
            (-
             (*
              (-
               (*
                (+
                 (- t_2 (* t_3 t_6))
                 (* INFINITY (- t_2 (* t_4 t_6))))
                z0)
               (* (* (* (tan (* 1.5 PI)) 2.0) t_6) (+ PI PI)))
              z0)
             (* t_6 -2.0))
            z0)
           t_7)
          z1)
         z2)))))
    (if (<= z0 43.0)
      (-
       1.0
       (cos
        (* -2.0 (atan (/ (* (cos t_5) z1) (* (- (sin t_5)) z2))))))
      (-
       1.0
       (cos
        (*
         -2.0
         (atan
          (/
           (*
            (-
             (*
              (-
               (*
                (-
                 (*
                  (+ (- t_2 (* t_3 t_1)) (* t_0 (- t_2 (* t_4 t_1))))
                  z0)
                 (* (* (* (- INFINITY) 2.0) t_1) (+ PI PI)))
                z0)
               (* t_1 -2.0))
              z0)
             t_7)
            z1)
           z2)))))))))

C

double code(double z1, double z2, double z0) {
	double t_0 = pow(-((double) INFINITY), 2.0);
	double t_1 = ((double) M_PI) - (t_0 * ((double) M_PI));
	double t_2 = ((((double) M_PI) * ((double) M_PI)) * -1.3333333333333333) * ((double) M_PI);
	double t_3 = -4.0 * (((double) M_PI) * ((double) M_PI));
	double t_4 = t_3 * 2.0;
	double t_5 = (z0 + z0) * ((double) M_PI);
	double t_6 = ((double) M_PI) - (((double) INFINITY) * ((double) M_PI));
	double t_7 = tan((((double) M_PI) * -0.5));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_2 - (t_3 * t_6)) + (((double) INFINITY) * (t_2 - (t_4 * t_6)))) * z0) - (((tan((1.5 * ((double) M_PI))) * 2.0) * t_6) * (((double) M_PI) + ((double) M_PI)))) * z0) - (t_6 * -2.0)) * z0) - t_7) * z1) / z2))));
	} else if (z0 <= 43.0) {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_5) * z1) / (-sin(t_5) * z2)))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_2 - (t_3 * t_1)) + (t_0 * (t_2 - (t_4 * t_1)))) * z0) - (((-((double) INFINITY) * 2.0) * t_1) * (((double) M_PI) + ((double) M_PI)))) * z0) - (t_1 * -2.0)) * z0) - t_7) * z1) / z2))));
	}
	return tmp;
}

Java

public static double code(double z1, double z2, double z0) {
	double t_0 = Math.pow(-Double.POSITIVE_INFINITY, 2.0);
	double t_1 = Math.PI - (t_0 * Math.PI);
	double t_2 = ((Math.PI * Math.PI) * -1.3333333333333333) * Math.PI;
	double t_3 = -4.0 * (Math.PI * Math.PI);
	double t_4 = t_3 * 2.0;
	double t_5 = (z0 + z0) * Math.PI;
	double t_6 = Math.PI - (Double.POSITIVE_INFINITY * Math.PI);
	double t_7 = Math.tan((Math.PI * -0.5));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((((((((((t_2 - (t_3 * t_6)) + (Double.POSITIVE_INFINITY * (t_2 - (t_4 * t_6)))) * z0) - (((Math.tan((1.5 * Math.PI)) * 2.0) * t_6) * (Math.PI + Math.PI))) * z0) - (t_6 * -2.0)) * z0) - t_7) * z1) / z2))));
	} else if (z0 <= 43.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_5) * z1) / (-Math.sin(t_5) * z2)))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((((((((((t_2 - (t_3 * t_1)) + (t_0 * (t_2 - (t_4 * t_1)))) * z0) - (((-Double.POSITIVE_INFINITY * 2.0) * t_1) * (Math.PI + Math.PI))) * z0) - (t_1 * -2.0)) * z0) - t_7) * z1) / z2))));
	}
	return tmp;
}

Python

def code(z1, z2, z0):
	t_0 = math.pow(-math.inf, 2.0)
	t_1 = math.pi - (t_0 * math.pi)
	t_2 = ((math.pi * math.pi) * -1.3333333333333333) * math.pi
	t_3 = -4.0 * (math.pi * math.pi)
	t_4 = t_3 * 2.0
	t_5 = (z0 + z0) * math.pi
	t_6 = math.pi - (math.inf * math.pi)
	t_7 = math.tan((math.pi * -0.5))
	tmp = 0
	if z0 <= -48000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((((((((((t_2 - (t_3 * t_6)) + (math.inf * (t_2 - (t_4 * t_6)))) * z0) - (((math.tan((1.5 * math.pi)) * 2.0) * t_6) * (math.pi + math.pi))) * z0) - (t_6 * -2.0)) * z0) - t_7) * z1) / z2))))
	elif z0 <= 43.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_5) * z1) / (-math.sin(t_5) * z2)))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((((((((((t_2 - (t_3 * t_1)) + (t_0 * (t_2 - (t_4 * t_1)))) * z0) - (((-math.inf * 2.0) * t_1) * (math.pi + math.pi))) * z0) - (t_1 * -2.0)) * z0) - t_7) * z1) / z2))))
	return tmp

Julia

function code(z1, z2, z0)
	t_0 = Float64(-Inf) ^ 2.0
	t_1 = Float64(pi - Float64(t_0 * pi))
	t_2 = Float64(Float64(Float64(pi * pi) * -1.3333333333333333) * pi)
	t_3 = Float64(-4.0 * Float64(pi * pi))
	t_4 = Float64(t_3 * 2.0)
	t_5 = Float64(Float64(z0 + z0) * pi)
	t_6 = Float64(pi - Float64(Inf * pi))
	t_7 = tan(Float64(pi * -0.5))
	tmp = 0.0
	if (z0 <= -48000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(t_2 - Float64(t_3 * t_6)) + Float64(Inf * Float64(t_2 - Float64(t_4 * t_6)))) * z0) - Float64(Float64(Float64(tan(Float64(1.5 * pi)) * 2.0) * t_6) * Float64(pi + pi))) * z0) - Float64(t_6 * -2.0)) * z0) - t_7) * z1) / z2)))));
	elseif (z0 <= 43.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_5) * z1) / Float64(Float64(-sin(t_5)) * z2))))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(t_2 - Float64(t_3 * t_1)) + Float64(t_0 * Float64(t_2 - Float64(t_4 * t_1)))) * z0) - Float64(Float64(Float64(Float64(-Inf) * 2.0) * t_1) * Float64(pi + pi))) * z0) - Float64(t_1 * -2.0)) * z0) - t_7) * z1) / z2)))));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z1, z2, z0)
	t_0 = -Inf ^ 2.0;
	t_1 = pi - (t_0 * pi);
	t_2 = ((pi * pi) * -1.3333333333333333) * pi;
	t_3 = -4.0 * (pi * pi);
	t_4 = t_3 * 2.0;
	t_5 = (z0 + z0) * pi;
	t_6 = pi - (Inf * pi);
	t_7 = tan((pi * -0.5));
	tmp = 0.0;
	if (z0 <= -48000000.0)
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_2 - (t_3 * t_6)) + (Inf * (t_2 - (t_4 * t_6)))) * z0) - (((tan((1.5 * pi)) * 2.0) * t_6) * (pi + pi))) * z0) - (t_6 * -2.0)) * z0) - t_7) * z1) / z2))));
	elseif (z0 <= 43.0)
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_5) * z1) / (-sin(t_5) * z2)))));
	else
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_2 - (t_3 * t_1)) + (t_0 * (t_2 - (t_4 * t_1)))) * z0) - (((-Inf * 2.0) * t_1) * (pi + pi))) * z0) - (t_1 * -2.0)) * z0) - t_7) * z1) / z2))));
	end
	tmp_2 = tmp;
end

Wolfram

code[z1_, z2_, z0_] := Block[{t$95$0 = N[Power[(-Infinity), 2.0], $MachinePrecision]}, Block[{t$95$1 = N[(Pi - N[(t$95$0 * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(N[(Pi * Pi), $MachinePrecision] * -1.3333333333333333), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$3 = N[(-4.0 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$4 = N[(t$95$3 * 2.0), $MachinePrecision]}, Block[{t$95$5 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$6 = N[(Pi - N[(Infinity * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$7 = N[Tan[N[(Pi * -0.5), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[z0, -48000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(N[(t$95$2 - N[(t$95$3 * t$95$6), $MachinePrecision]), $MachinePrecision] + N[(Infinity * N[(t$95$2 - N[(t$95$4 * t$95$6), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(N[(N[(N[Tan[N[(1.5 * Pi), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision] * t$95$6), $MachinePrecision] * N[(Pi + Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(t$95$6 * -2.0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - t$95$7), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], If[LessEqual[z0, 43.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$5], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$5], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(N[(t$95$2 - N[(t$95$3 * t$95$1), $MachinePrecision]), $MachinePrecision] + N[(t$95$0 * N[(t$95$2 - N[(t$95$4 * t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(N[(N[((-Infinity) * 2.0), $MachinePrecision] * t$95$1), $MachinePrecision] * N[(Pi + Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(t$95$1 * -2.0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - t$95$7), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]]]]]]

Derivation

1. Split input into 3 regimes

2. if z0 < -4.8e7

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   8. Applied rewrites 80.6%

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

   9. Evaluated real constant 84.6%

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

   10. Evaluated real constant 84.6%

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

   11. Evaluated real constant 84.6%

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

   12. Evaluated real constant 42.2%

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

   13. Evaluated real constant 42.2%

       \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(\left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi - \left(-4 \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(\pi - \infty \cdot \pi\right)\right) + \infty \cdot \left(\left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi - \left(\left(-4 \cdot \left(\pi \cdot \pi\right)\right) \cdot 2\right) \cdot \left(\pi - \infty \cdot \pi\right)\right)\right) \cdot z0 - \left(\left(\tan \left(1.5 \cdot \pi\right) \cdot 2\right) \cdot \left(\pi - \infty \cdot \pi\right)\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - \left(\pi - \infty \cdot \pi\right) \cdot -2\right) \cdot z0 - \tan \left(\pi \cdot -0.5\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(\left(z0 + z0\right) - -0.5\right)\right)\right)\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. lift-tan.f64 N/A

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

      4. tan-quot N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 69.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 43 < z0

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   8. Applied rewrites 80.6%

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

   9. Evaluated real constant 84.6%

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

   10. Evaluated real constant 84.6%

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

   11. Evaluated real constant 84.6%

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

   12. Evaluated real constant 42.3%

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

   13. Evaluated real constant 42.3%

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

   14. Evaluated real constant 42.3%

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

Alternative 2: 89.8% accurate, 0.4× speedup

Math

\[\begin{array}{l} t_0 := \tan \left(0.5 \cdot \pi\right)\\ t_1 := \pi \cdot \left(t\_0 \cdot t\_0\right)\\ t_2 := \left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi\\ t_3 := -4 \cdot \left(\pi \cdot \pi\right)\\ t_4 := \left(z0 + z0\right) \cdot \pi\\ t_5 := \pi - \infty \cdot \pi\\ t_6 := \tan \left(\pi \cdot -0.5\right)\\ \mathbf{if}\;z0 \leq -48000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(t\_2 - t\_3 \cdot t\_5\right) + \infty \cdot \left(t\_2 - \left(t\_3 \cdot 2\right) \cdot t\_5\right)\right) \cdot z0 - \left(\left(\tan \left(1.5 \cdot \pi\right) \cdot 2\right) \cdot t\_5\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - t\_5 \cdot -2\right) \cdot z0 - t\_6\right) \cdot z1}{z2}\right)\right)\\ \mathbf{elif}\;z0 \leq 0.0002:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_4 \cdot z1}{\left(-\sin t\_4\right) \cdot z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(2 \cdot \left(\left(\pi + \left(z0 \cdot \pi\right) \cdot \left(\left(2 \cdot \left(\pi + t\_1\right)\right) \cdot t\_0\right)\right) + t\_1\right)\right) \cdot z0 - t\_6\right) \cdot z1}{z2}\right)\right)\\ \end{array} \]

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (tan (* 0.5 PI)))
       (t_1 (* PI (* t_0 t_0)))
       (t_2 (* (* (* PI PI) -1.3333333333333333) PI))
       (t_3 (* -4.0 (* PI PI)))
       (t_4 (* (+ z0 z0) PI))
       (t_5 (- PI (* INFINITY PI)))
       (t_6 (tan (* PI -0.5))))
  (if (<= z0 -48000000.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (*
          (-
           (*
            (-
             (*
              (-
               (*
                (+
                 (- t_2 (* t_3 t_5))
                 (* INFINITY (- t_2 (* (* t_3 2.0) t_5))))
                z0)
               (* (* (* (tan (* 1.5 PI)) 2.0) t_5) (+ PI PI)))
              z0)
             (* t_5 -2.0))
            z0)
           t_6)
          z1)
         z2)))))
    (if (<= z0 0.0002)
      (-
       1.0
       (cos
        (* -2.0 (atan (/ (* (cos t_4) z1) (* (- (sin t_4)) z2))))))
      (-
       1.0
       (cos
        (*
         -2.0
         (atan
          (/
           (*
            (-
             (*
              (*
               2.0
               (+
                (+ PI (* (* z0 PI) (* (* 2.0 (+ PI t_1)) t_0)))
                t_1))
              z0)
             t_6)
            z1)
           z2)))))))))

C

double code(double z1, double z2, double z0) {
	double t_0 = tan((0.5 * ((double) M_PI)));
	double t_1 = ((double) M_PI) * (t_0 * t_0);
	double t_2 = ((((double) M_PI) * ((double) M_PI)) * -1.3333333333333333) * ((double) M_PI);
	double t_3 = -4.0 * (((double) M_PI) * ((double) M_PI));
	double t_4 = (z0 + z0) * ((double) M_PI);
	double t_5 = ((double) M_PI) - (((double) INFINITY) * ((double) M_PI));
	double t_6 = tan((((double) M_PI) * -0.5));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_2 - (t_3 * t_5)) + (((double) INFINITY) * (t_2 - ((t_3 * 2.0) * t_5)))) * z0) - (((tan((1.5 * ((double) M_PI))) * 2.0) * t_5) * (((double) M_PI) + ((double) M_PI)))) * z0) - (t_5 * -2.0)) * z0) - t_6) * z1) / z2))));
	} else if (z0 <= 0.0002) {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_4) * z1) / (-sin(t_4) * z2)))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan((((((2.0 * ((((double) M_PI) + ((z0 * ((double) M_PI)) * ((2.0 * (((double) M_PI) + t_1)) * t_0))) + t_1)) * z0) - t_6) * z1) / z2))));
	}
	return tmp;
}

Java

public static double code(double z1, double z2, double z0) {
	double t_0 = Math.tan((0.5 * Math.PI));
	double t_1 = Math.PI * (t_0 * t_0);
	double t_2 = ((Math.PI * Math.PI) * -1.3333333333333333) * Math.PI;
	double t_3 = -4.0 * (Math.PI * Math.PI);
	double t_4 = (z0 + z0) * Math.PI;
	double t_5 = Math.PI - (Double.POSITIVE_INFINITY * Math.PI);
	double t_6 = Math.tan((Math.PI * -0.5));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((((((((((t_2 - (t_3 * t_5)) + (Double.POSITIVE_INFINITY * (t_2 - ((t_3 * 2.0) * t_5)))) * z0) - (((Math.tan((1.5 * Math.PI)) * 2.0) * t_5) * (Math.PI + Math.PI))) * z0) - (t_5 * -2.0)) * z0) - t_6) * z1) / z2))));
	} else if (z0 <= 0.0002) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_4) * z1) / (-Math.sin(t_4) * z2)))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((((((2.0 * ((Math.PI + ((z0 * Math.PI) * ((2.0 * (Math.PI + t_1)) * t_0))) + t_1)) * z0) - t_6) * z1) / z2))));
	}
	return tmp;
}

Python

def code(z1, z2, z0):
	t_0 = math.tan((0.5 * math.pi))
	t_1 = math.pi * (t_0 * t_0)
	t_2 = ((math.pi * math.pi) * -1.3333333333333333) * math.pi
	t_3 = -4.0 * (math.pi * math.pi)
	t_4 = (z0 + z0) * math.pi
	t_5 = math.pi - (math.inf * math.pi)
	t_6 = math.tan((math.pi * -0.5))
	tmp = 0
	if z0 <= -48000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((((((((((t_2 - (t_3 * t_5)) + (math.inf * (t_2 - ((t_3 * 2.0) * t_5)))) * z0) - (((math.tan((1.5 * math.pi)) * 2.0) * t_5) * (math.pi + math.pi))) * z0) - (t_5 * -2.0)) * z0) - t_6) * z1) / z2))))
	elif z0 <= 0.0002:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_4) * z1) / (-math.sin(t_4) * z2)))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan((((((2.0 * ((math.pi + ((z0 * math.pi) * ((2.0 * (math.pi + t_1)) * t_0))) + t_1)) * z0) - t_6) * z1) / z2))))
	return tmp

Julia

function code(z1, z2, z0)
	t_0 = tan(Float64(0.5 * pi))
	t_1 = Float64(pi * Float64(t_0 * t_0))
	t_2 = Float64(Float64(Float64(pi * pi) * -1.3333333333333333) * pi)
	t_3 = Float64(-4.0 * Float64(pi * pi))
	t_4 = Float64(Float64(z0 + z0) * pi)
	t_5 = Float64(pi - Float64(Inf * pi))
	t_6 = tan(Float64(pi * -0.5))
	tmp = 0.0
	if (z0 <= -48000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(t_2 - Float64(t_3 * t_5)) + Float64(Inf * Float64(t_2 - Float64(Float64(t_3 * 2.0) * t_5)))) * z0) - Float64(Float64(Float64(tan(Float64(1.5 * pi)) * 2.0) * t_5) * Float64(pi + pi))) * z0) - Float64(t_5 * -2.0)) * z0) - t_6) * z1) / z2)))));
	elseif (z0 <= 0.0002)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_4) * z1) / Float64(Float64(-sin(t_4)) * z2))))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(2.0 * Float64(Float64(pi + Float64(Float64(z0 * pi) * Float64(Float64(2.0 * Float64(pi + t_1)) * t_0))) + t_1)) * z0) - t_6) * z1) / z2)))));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z1, z2, z0)
	t_0 = tan((0.5 * pi));
	t_1 = pi * (t_0 * t_0);
	t_2 = ((pi * pi) * -1.3333333333333333) * pi;
	t_3 = -4.0 * (pi * pi);
	t_4 = (z0 + z0) * pi;
	t_5 = pi - (Inf * pi);
	t_6 = tan((pi * -0.5));
	tmp = 0.0;
	if (z0 <= -48000000.0)
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_2 - (t_3 * t_5)) + (Inf * (t_2 - ((t_3 * 2.0) * t_5)))) * z0) - (((tan((1.5 * pi)) * 2.0) * t_5) * (pi + pi))) * z0) - (t_5 * -2.0)) * z0) - t_6) * z1) / z2))));
	elseif (z0 <= 0.0002)
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_4) * z1) / (-sin(t_4) * z2)))));
	else
		tmp = 1.0 - cos((-2.0 * atan((((((2.0 * ((pi + ((z0 * pi) * ((2.0 * (pi + t_1)) * t_0))) + t_1)) * z0) - t_6) * z1) / z2))));
	end
	tmp_2 = tmp;
end

Wolfram

code[z1_, z2_, z0_] := Block[{t$95$0 = N[Tan[N[(0.5 * Pi), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[(Pi * N[(t$95$0 * t$95$0), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(N[(Pi * Pi), $MachinePrecision] * -1.3333333333333333), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$3 = N[(-4.0 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$4 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$5 = N[(Pi - N[(Infinity * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$6 = N[Tan[N[(Pi * -0.5), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[z0, -48000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(N[(t$95$2 - N[(t$95$3 * t$95$5), $MachinePrecision]), $MachinePrecision] + N[(Infinity * N[(t$95$2 - N[(N[(t$95$3 * 2.0), $MachinePrecision] * t$95$5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(N[(N[(N[Tan[N[(1.5 * Pi), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision] * t$95$5), $MachinePrecision] * N[(Pi + Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(t$95$5 * -2.0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - t$95$6), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], If[LessEqual[z0, 0.0002], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$4], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$4], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(2.0 * N[(N[(Pi + N[(N[(z0 * Pi), $MachinePrecision] * N[(N[(2.0 * N[(Pi + t$95$1), $MachinePrecision]), $MachinePrecision] * t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - t$95$6), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]]]]]

Derivation

1. Split input into 3 regimes

2. if z0 < -4.8e7

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   8. Applied rewrites 80.6%

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

   9. Evaluated real constant 84.6%

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

   10. Evaluated real constant 84.6%

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

   11. Evaluated real constant 84.6%

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

   12. Evaluated real constant 42.2%

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

   13. Evaluated real constant 42.2%

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

   if -4.8e7 < z0 < 2.0000000000000001e-4

   1. Initial program 59.9%

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

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. lift-tan.f64 N/A

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

      4. tan-quot N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 69.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 2.0000000000000001e-4 < z0

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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 + 2 \cdot \frac{z0 \cdot \left(\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)\right)}{\cos \left(\frac{1}{2} \cdot \pi\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) \]

   4. Applied rewrites 75.4%

      \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \color{blue}{\left(z0 \cdot \left(\left(2 \cdot \pi + 2 \cdot \frac{z0 \cdot \left(\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)\right)}{\cos \left(0.5 \cdot \pi\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) \]

   6. Applied rewrites 78.6%

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

Alternative 3: 89.2% accurate, 0.2× speedup

Math

\[\begin{array}{l} t_0 := -4 \cdot \left(\pi \cdot \pi\right)\\ t_1 := \tan \left(1.5 \cdot \pi\right)\\ t_2 := {t\_1}^{2}\\ t_3 := \pi - t\_2 \cdot \pi\\ t_4 := \left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi\\ t_5 := \left(z0 + z0\right) \cdot \pi\\ \mathbf{if}\;\tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\right)\right) \leq 15:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(t\_4 - t\_0 \cdot t\_3\right) + t\_2 \cdot \left(t\_4 - \left(t\_0 \cdot 2\right) \cdot t\_3\right)\right) \cdot z0 - \left(\left(t\_1 \cdot 2\right) \cdot t\_3\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - t\_3 \cdot -2\right) \cdot z0 - \tan \left(\pi \cdot -0.5\right)\right) \cdot z1}{z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_5 \cdot z1}{\left(-\sin t\_5\right) \cdot z2}\right)\right)\\ \end{array} \]

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (* -4.0 (* PI PI)))
       (t_1 (tan (* 1.5 PI)))
       (t_2 (pow t_1 2.0))
       (t_3 (- PI (* t_2 PI)))
       (t_4 (* (* (* PI PI) -1.3333333333333333) PI))
       (t_5 (* (+ z0 z0) PI)))
  (if (<= (tan (* PI (- (+ z0 z0) -0.5))) 15.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (*
          (-
           (*
            (-
             (*
              (-
               (*
                (+
                 (- t_4 (* t_0 t_3))
                 (* t_2 (- t_4 (* (* t_0 2.0) t_3))))
                z0)
               (* (* (* t_1 2.0) t_3) (+ PI PI)))
              z0)
             (* t_3 -2.0))
            z0)
           (tan (* PI -0.5)))
          z1)
         z2)))))
    (-
     1.0
     (cos
      (* -2.0 (atan (/ (* (cos t_5) z1) (* (- (sin t_5)) z2)))))))))

C

double code(double z1, double z2, double z0) {
	double t_0 = -4.0 * (((double) M_PI) * ((double) M_PI));
	double t_1 = tan((1.5 * ((double) M_PI)));
	double t_2 = pow(t_1, 2.0);
	double t_3 = ((double) M_PI) - (t_2 * ((double) M_PI));
	double t_4 = ((((double) M_PI) * ((double) M_PI)) * -1.3333333333333333) * ((double) M_PI);
	double t_5 = (z0 + z0) * ((double) M_PI);
	double tmp;
	if (tan((((double) M_PI) * ((z0 + z0) - -0.5))) <= 15.0) {
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_4 - (t_0 * t_3)) + (t_2 * (t_4 - ((t_0 * 2.0) * t_3)))) * z0) - (((t_1 * 2.0) * t_3) * (((double) M_PI) + ((double) M_PI)))) * z0) - (t_3 * -2.0)) * z0) - tan((((double) M_PI) * -0.5))) * z1) / z2))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_5) * z1) / (-sin(t_5) * z2)))));
	}
	return tmp;
}

Java

public static double code(double z1, double z2, double z0) {
	double t_0 = -4.0 * (Math.PI * Math.PI);
	double t_1 = Math.tan((1.5 * Math.PI));
	double t_2 = Math.pow(t_1, 2.0);
	double t_3 = Math.PI - (t_2 * Math.PI);
	double t_4 = ((Math.PI * Math.PI) * -1.3333333333333333) * Math.PI;
	double t_5 = (z0 + z0) * Math.PI;
	double tmp;
	if (Math.tan((Math.PI * ((z0 + z0) - -0.5))) <= 15.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((((((((((t_4 - (t_0 * t_3)) + (t_2 * (t_4 - ((t_0 * 2.0) * t_3)))) * z0) - (((t_1 * 2.0) * t_3) * (Math.PI + Math.PI))) * z0) - (t_3 * -2.0)) * z0) - Math.tan((Math.PI * -0.5))) * z1) / z2))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_5) * z1) / (-Math.sin(t_5) * z2)))));
	}
	return tmp;
}

Python

def code(z1, z2, z0):
	t_0 = -4.0 * (math.pi * math.pi)
	t_1 = math.tan((1.5 * math.pi))
	t_2 = math.pow(t_1, 2.0)
	t_3 = math.pi - (t_2 * math.pi)
	t_4 = ((math.pi * math.pi) * -1.3333333333333333) * math.pi
	t_5 = (z0 + z0) * math.pi
	tmp = 0
	if math.tan((math.pi * ((z0 + z0) - -0.5))) <= 15.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((((((((((t_4 - (t_0 * t_3)) + (t_2 * (t_4 - ((t_0 * 2.0) * t_3)))) * z0) - (((t_1 * 2.0) * t_3) * (math.pi + math.pi))) * z0) - (t_3 * -2.0)) * z0) - math.tan((math.pi * -0.5))) * z1) / z2))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_5) * z1) / (-math.sin(t_5) * z2)))))
	return tmp

Julia

function code(z1, z2, z0)
	t_0 = Float64(-4.0 * Float64(pi * pi))
	t_1 = tan(Float64(1.5 * pi))
	t_2 = t_1 ^ 2.0
	t_3 = Float64(pi - Float64(t_2 * pi))
	t_4 = Float64(Float64(Float64(pi * pi) * -1.3333333333333333) * pi)
	t_5 = Float64(Float64(z0 + z0) * pi)
	tmp = 0.0
	if (tan(Float64(pi * Float64(Float64(z0 + z0) - -0.5))) <= 15.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(t_4 - Float64(t_0 * t_3)) + Float64(t_2 * Float64(t_4 - Float64(Float64(t_0 * 2.0) * t_3)))) * z0) - Float64(Float64(Float64(t_1 * 2.0) * t_3) * Float64(pi + pi))) * z0) - Float64(t_3 * -2.0)) * z0) - tan(Float64(pi * -0.5))) * z1) / z2)))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_5) * z1) / Float64(Float64(-sin(t_5)) * z2))))));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z1, z2, z0)
	t_0 = -4.0 * (pi * pi);
	t_1 = tan((1.5 * pi));
	t_2 = t_1 ^ 2.0;
	t_3 = pi - (t_2 * pi);
	t_4 = ((pi * pi) * -1.3333333333333333) * pi;
	t_5 = (z0 + z0) * pi;
	tmp = 0.0;
	if (tan((pi * ((z0 + z0) - -0.5))) <= 15.0)
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_4 - (t_0 * t_3)) + (t_2 * (t_4 - ((t_0 * 2.0) * t_3)))) * z0) - (((t_1 * 2.0) * t_3) * (pi + pi))) * z0) - (t_3 * -2.0)) * z0) - tan((pi * -0.5))) * z1) / z2))));
	else
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_5) * z1) / (-sin(t_5) * z2)))));
	end
	tmp_2 = tmp;
end

Wolfram

code[z1_, z2_, z0_] := Block[{t$95$0 = N[(-4.0 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[Tan[N[(1.5 * Pi), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$2 = N[Power[t$95$1, 2.0], $MachinePrecision]}, Block[{t$95$3 = N[(Pi - N[(t$95$2 * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$4 = N[(N[(N[(Pi * Pi), $MachinePrecision] * -1.3333333333333333), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$5 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, If[LessEqual[N[Tan[N[(Pi * N[(N[(z0 + z0), $MachinePrecision] - -0.5), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 15.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(N[(t$95$4 - N[(t$95$0 * t$95$3), $MachinePrecision]), $MachinePrecision] + N[(t$95$2 * N[(t$95$4 - N[(N[(t$95$0 * 2.0), $MachinePrecision] * t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(N[(N[(t$95$1 * 2.0), $MachinePrecision] * t$95$3), $MachinePrecision] * N[(Pi + Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(t$95$3 * -2.0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[Tan[N[(Pi * -0.5), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$5], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$5], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]]]

Derivation

1. Split input into 2 regimes

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

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   8. Applied rewrites 80.6%

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

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

   1. Initial program 59.9%

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

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. lift-tan.f64 N/A

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

      4. tan-quot N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 69.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 4: 86.7% accurate, 0.4× speedup

Math

\[\begin{array}{l} t_0 := \left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi\\ t_1 := -4 \cdot \left(\pi \cdot \pi\right)\\ t_2 := \left(z0 + z0\right) \cdot \pi\\ t_3 := \pi - \infty \cdot \pi\\ t_4 := \tan \left(\pi \cdot -0.5\right)\\ \mathbf{if}\;z0 \leq -48000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(t\_0 - t\_1 \cdot t\_3\right) + \infty \cdot \left(t\_0 - \left(t\_1 \cdot 2\right) \cdot t\_3\right)\right) \cdot z0 - \left(\left(\tan \left(1.5 \cdot \pi\right) \cdot 2\right) \cdot t\_3\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - t\_3 \cdot -2\right) \cdot z0 - t\_4\right) \cdot z1}{z2}\right)\right)\\ \mathbf{elif}\;z0 \leq 0.0002:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_2 \cdot z1}{\left(-\sin t\_2\right) \cdot z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(2 \cdot \left(\pi + \frac{\pi \cdot {\sin \left(0.5 \cdot \pi\right)}^{2}}{{\cos \left(0.5 \cdot \pi\right)}^{2}}\right)\right) \cdot z0 - t\_4\right) \cdot z1}{z2}\right)\right)\\ \end{array} \]

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (* (* (* PI PI) -1.3333333333333333) PI))
       (t_1 (* -4.0 (* PI PI)))
       (t_2 (* (+ z0 z0) PI))
       (t_3 (- PI (* INFINITY PI)))
       (t_4 (tan (* PI -0.5))))
  (if (<= z0 -48000000.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (*
          (-
           (*
            (-
             (*
              (-
               (*
                (+
                 (- t_0 (* t_1 t_3))
                 (* INFINITY (- t_0 (* (* t_1 2.0) t_3))))
                z0)
               (* (* (* (tan (* 1.5 PI)) 2.0) t_3) (+ PI PI)))
              z0)
             (* t_3 -2.0))
            z0)
           t_4)
          z1)
         z2)))))
    (if (<= z0 0.0002)
      (-
       1.0
       (cos
        (* -2.0 (atan (/ (* (cos t_2) z1) (* (- (sin t_2)) z2))))))
      (-
       1.0
       (cos
        (*
         -2.0
         (atan
          (/
           (*
            (-
             (*
              (*
               2.0
               (+
                PI
                (/
                 (* PI (pow (sin (* 0.5 PI)) 2.0))
                 (pow (cos (* 0.5 PI)) 2.0))))
              z0)
             t_4)
            z1)
           z2)))))))))

C

double code(double z1, double z2, double z0) {
	double t_0 = ((((double) M_PI) * ((double) M_PI)) * -1.3333333333333333) * ((double) M_PI);
	double t_1 = -4.0 * (((double) M_PI) * ((double) M_PI));
	double t_2 = (z0 + z0) * ((double) M_PI);
	double t_3 = ((double) M_PI) - (((double) INFINITY) * ((double) M_PI));
	double t_4 = tan((((double) M_PI) * -0.5));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_0 - (t_1 * t_3)) + (((double) INFINITY) * (t_0 - ((t_1 * 2.0) * t_3)))) * z0) - (((tan((1.5 * ((double) M_PI))) * 2.0) * t_3) * (((double) M_PI) + ((double) M_PI)))) * z0) - (t_3 * -2.0)) * z0) - t_4) * z1) / z2))));
	} else if (z0 <= 0.0002) {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_2) * z1) / (-sin(t_2) * z2)))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan((((((2.0 * (((double) M_PI) + ((((double) M_PI) * pow(sin((0.5 * ((double) M_PI))), 2.0)) / pow(cos((0.5 * ((double) M_PI))), 2.0)))) * z0) - t_4) * z1) / z2))));
	}
	return tmp;
}

Java

public static double code(double z1, double z2, double z0) {
	double t_0 = ((Math.PI * Math.PI) * -1.3333333333333333) * Math.PI;
	double t_1 = -4.0 * (Math.PI * Math.PI);
	double t_2 = (z0 + z0) * Math.PI;
	double t_3 = Math.PI - (Double.POSITIVE_INFINITY * Math.PI);
	double t_4 = Math.tan((Math.PI * -0.5));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((((((((((t_0 - (t_1 * t_3)) + (Double.POSITIVE_INFINITY * (t_0 - ((t_1 * 2.0) * t_3)))) * z0) - (((Math.tan((1.5 * Math.PI)) * 2.0) * t_3) * (Math.PI + Math.PI))) * z0) - (t_3 * -2.0)) * z0) - t_4) * z1) / z2))));
	} else if (z0 <= 0.0002) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_2) * z1) / (-Math.sin(t_2) * z2)))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan((((((2.0 * (Math.PI + ((Math.PI * Math.pow(Math.sin((0.5 * Math.PI)), 2.0)) / Math.pow(Math.cos((0.5 * Math.PI)), 2.0)))) * z0) - t_4) * z1) / z2))));
	}
	return tmp;
}

Python

def code(z1, z2, z0):
	t_0 = ((math.pi * math.pi) * -1.3333333333333333) * math.pi
	t_1 = -4.0 * (math.pi * math.pi)
	t_2 = (z0 + z0) * math.pi
	t_3 = math.pi - (math.inf * math.pi)
	t_4 = math.tan((math.pi * -0.5))
	tmp = 0
	if z0 <= -48000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((((((((((t_0 - (t_1 * t_3)) + (math.inf * (t_0 - ((t_1 * 2.0) * t_3)))) * z0) - (((math.tan((1.5 * math.pi)) * 2.0) * t_3) * (math.pi + math.pi))) * z0) - (t_3 * -2.0)) * z0) - t_4) * z1) / z2))))
	elif z0 <= 0.0002:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_2) * z1) / (-math.sin(t_2) * z2)))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan((((((2.0 * (math.pi + ((math.pi * math.pow(math.sin((0.5 * math.pi)), 2.0)) / math.pow(math.cos((0.5 * math.pi)), 2.0)))) * z0) - t_4) * z1) / z2))))
	return tmp

Julia

function code(z1, z2, z0)
	t_0 = Float64(Float64(Float64(pi * pi) * -1.3333333333333333) * pi)
	t_1 = Float64(-4.0 * Float64(pi * pi))
	t_2 = Float64(Float64(z0 + z0) * pi)
	t_3 = Float64(pi - Float64(Inf * pi))
	t_4 = tan(Float64(pi * -0.5))
	tmp = 0.0
	if (z0 <= -48000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(t_0 - Float64(t_1 * t_3)) + Float64(Inf * Float64(t_0 - Float64(Float64(t_1 * 2.0) * t_3)))) * z0) - Float64(Float64(Float64(tan(Float64(1.5 * pi)) * 2.0) * t_3) * Float64(pi + pi))) * z0) - Float64(t_3 * -2.0)) * z0) - t_4) * z1) / z2)))));
	elseif (z0 <= 0.0002)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_2) * z1) / Float64(Float64(-sin(t_2)) * z2))))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(2.0 * Float64(pi + Float64(Float64(pi * (sin(Float64(0.5 * pi)) ^ 2.0)) / (cos(Float64(0.5 * pi)) ^ 2.0)))) * z0) - t_4) * z1) / z2)))));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z1, z2, z0)
	t_0 = ((pi * pi) * -1.3333333333333333) * pi;
	t_1 = -4.0 * (pi * pi);
	t_2 = (z0 + z0) * pi;
	t_3 = pi - (Inf * pi);
	t_4 = tan((pi * -0.5));
	tmp = 0.0;
	if (z0 <= -48000000.0)
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_0 - (t_1 * t_3)) + (Inf * (t_0 - ((t_1 * 2.0) * t_3)))) * z0) - (((tan((1.5 * pi)) * 2.0) * t_3) * (pi + pi))) * z0) - (t_3 * -2.0)) * z0) - t_4) * z1) / z2))));
	elseif (z0 <= 0.0002)
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_2) * z1) / (-sin(t_2) * z2)))));
	else
		tmp = 1.0 - cos((-2.0 * atan((((((2.0 * (pi + ((pi * (sin((0.5 * pi)) ^ 2.0)) / (cos((0.5 * pi)) ^ 2.0)))) * z0) - t_4) * z1) / z2))));
	end
	tmp_2 = tmp;
end

Wolfram

code[z1_, z2_, z0_] := Block[{t$95$0 = N[(N[(N[(Pi * Pi), $MachinePrecision] * -1.3333333333333333), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$1 = N[(-4.0 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$3 = N[(Pi - N[(Infinity * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$4 = N[Tan[N[(Pi * -0.5), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[z0, -48000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(N[(t$95$0 - N[(t$95$1 * t$95$3), $MachinePrecision]), $MachinePrecision] + N[(Infinity * N[(t$95$0 - N[(N[(t$95$1 * 2.0), $MachinePrecision] * t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(N[(N[(N[Tan[N[(1.5 * Pi), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision] * t$95$3), $MachinePrecision] * N[(Pi + Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(t$95$3 * -2.0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - t$95$4), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], If[LessEqual[z0, 0.0002], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$2], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$2], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(2.0 * N[(Pi + N[(N[(Pi * N[Power[N[Sin[N[(0.5 * Pi), $MachinePrecision]], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] / N[Power[N[Cos[N[(0.5 * Pi), $MachinePrecision]], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - t$95$4), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]]]

Derivation

1. Split input into 3 regimes

2. if z0 < -4.8e7

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   8. Applied rewrites 80.6%

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

   9. Evaluated real constant 84.6%

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

   10. Evaluated real constant 84.6%

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

   11. Evaluated real constant 84.6%

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

   12. Evaluated real constant 42.2%

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

   13. Evaluated real constant 42.2%

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

   if -4.8e7 < z0 < 2.0000000000000001e-4

   1. Initial program 59.9%

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

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. lift-tan.f64 N/A

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

      4. tan-quot N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 69.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 2.0000000000000001e-4 < z0

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   7. Taylor expanded in z0 around 0

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

   9. Applied rewrites 72.4%

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

Alternative 5: 80.4% accurate, 0.6× speedup

Math

\[\begin{array}{l} t_0 := \left(\left(\pi \cdot \pi\right) \cdot -1.3333333333333333\right) \cdot \pi\\ t_1 := \left(z0 + z0\right) \cdot \pi\\ t_2 := -4 \cdot \left(\pi \cdot \pi\right)\\ t_3 := \pi - \infty \cdot \pi\\ \mathbf{if}\;z0 \leq -48000000:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\left(\left(\left(\left(\left(t\_0 - t\_2 \cdot t\_3\right) + \infty \cdot \left(t\_0 - \left(t\_2 \cdot 2\right) \cdot t\_3\right)\right) \cdot z0 - \left(\left(\tan \left(1.5 \cdot \pi\right) \cdot 2\right) \cdot t\_3\right) \cdot \left(\pi + \pi\right)\right) \cdot z0 - t\_3 \cdot -2\right) \cdot z0 - \tan \left(\pi \cdot -0.5\right)\right) \cdot z1}{z2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_1 \cdot z1}{\left(-\sin t\_1\right) \cdot z2}\right)\right)\\ \end{array} \]

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (* (* (* PI PI) -1.3333333333333333) PI))
       (t_1 (* (+ z0 z0) PI))
       (t_2 (* -4.0 (* PI PI)))
       (t_3 (- PI (* INFINITY PI))))
  (if (<= z0 -48000000.0)
    (-
     1.0
     (cos
      (*
       -2.0
       (atan
        (/
         (*
          (-
           (*
            (-
             (*
              (-
               (*
                (+
                 (- t_0 (* t_2 t_3))
                 (* INFINITY (- t_0 (* (* t_2 2.0) t_3))))
                z0)
               (* (* (* (tan (* 1.5 PI)) 2.0) t_3) (+ PI PI)))
              z0)
             (* t_3 -2.0))
            z0)
           (tan (* PI -0.5)))
          z1)
         z2)))))
    (-
     1.0
     (cos
      (* -2.0 (atan (/ (* (cos t_1) z1) (* (- (sin t_1)) z2)))))))))

C

double code(double z1, double z2, double z0) {
	double t_0 = ((((double) M_PI) * ((double) M_PI)) * -1.3333333333333333) * ((double) M_PI);
	double t_1 = (z0 + z0) * ((double) M_PI);
	double t_2 = -4.0 * (((double) M_PI) * ((double) M_PI));
	double t_3 = ((double) M_PI) - (((double) INFINITY) * ((double) M_PI));
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_0 - (t_2 * t_3)) + (((double) INFINITY) * (t_0 - ((t_2 * 2.0) * t_3)))) * z0) - (((tan((1.5 * ((double) M_PI))) * 2.0) * t_3) * (((double) M_PI) + ((double) M_PI)))) * z0) - (t_3 * -2.0)) * z0) - tan((((double) M_PI) * -0.5))) * z1) / z2))));
	} else {
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_1) * z1) / (-sin(t_1) * z2)))));
	}
	return tmp;
}

Java

public static double code(double z1, double z2, double z0) {
	double t_0 = ((Math.PI * Math.PI) * -1.3333333333333333) * Math.PI;
	double t_1 = (z0 + z0) * Math.PI;
	double t_2 = -4.0 * (Math.PI * Math.PI);
	double t_3 = Math.PI - (Double.POSITIVE_INFINITY * Math.PI);
	double tmp;
	if (z0 <= -48000000.0) {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((((((((((t_0 - (t_2 * t_3)) + (Double.POSITIVE_INFINITY * (t_0 - ((t_2 * 2.0) * t_3)))) * z0) - (((Math.tan((1.5 * Math.PI)) * 2.0) * t_3) * (Math.PI + Math.PI))) * z0) - (t_3 * -2.0)) * z0) - Math.tan((Math.PI * -0.5))) * z1) / z2))));
	} else {
		tmp = 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_1) * z1) / (-Math.sin(t_1) * z2)))));
	}
	return tmp;
}

Python

def code(z1, z2, z0):
	t_0 = ((math.pi * math.pi) * -1.3333333333333333) * math.pi
	t_1 = (z0 + z0) * math.pi
	t_2 = -4.0 * (math.pi * math.pi)
	t_3 = math.pi - (math.inf * math.pi)
	tmp = 0
	if z0 <= -48000000.0:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((((((((((t_0 - (t_2 * t_3)) + (math.inf * (t_0 - ((t_2 * 2.0) * t_3)))) * z0) - (((math.tan((1.5 * math.pi)) * 2.0) * t_3) * (math.pi + math.pi))) * z0) - (t_3 * -2.0)) * z0) - math.tan((math.pi * -0.5))) * z1) / z2))))
	else:
		tmp = 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_1) * z1) / (-math.sin(t_1) * z2)))))
	return tmp

Julia

function code(z1, z2, z0)
	t_0 = Float64(Float64(Float64(pi * pi) * -1.3333333333333333) * pi)
	t_1 = Float64(Float64(z0 + z0) * pi)
	t_2 = Float64(-4.0 * Float64(pi * pi))
	t_3 = Float64(pi - Float64(Inf * pi))
	tmp = 0.0
	if (z0 <= -48000000.0)
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(Float64(t_0 - Float64(t_2 * t_3)) + Float64(Inf * Float64(t_0 - Float64(Float64(t_2 * 2.0) * t_3)))) * z0) - Float64(Float64(Float64(tan(Float64(1.5 * pi)) * 2.0) * t_3) * Float64(pi + pi))) * z0) - Float64(t_3 * -2.0)) * z0) - tan(Float64(pi * -0.5))) * z1) / z2)))));
	else
		tmp = Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_1) * z1) / Float64(Float64(-sin(t_1)) * z2))))));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z1, z2, z0)
	t_0 = ((pi * pi) * -1.3333333333333333) * pi;
	t_1 = (z0 + z0) * pi;
	t_2 = -4.0 * (pi * pi);
	t_3 = pi - (Inf * pi);
	tmp = 0.0;
	if (z0 <= -48000000.0)
		tmp = 1.0 - cos((-2.0 * atan(((((((((((t_0 - (t_2 * t_3)) + (Inf * (t_0 - ((t_2 * 2.0) * t_3)))) * z0) - (((tan((1.5 * pi)) * 2.0) * t_3) * (pi + pi))) * z0) - (t_3 * -2.0)) * z0) - tan((pi * -0.5))) * z1) / z2))));
	else
		tmp = 1.0 - cos((-2.0 * atan(((cos(t_1) * z1) / (-sin(t_1) * z2)))));
	end
	tmp_2 = tmp;
end

Wolfram

code[z1_, z2_, z0_] := Block[{t$95$0 = N[(N[(N[(Pi * Pi), $MachinePrecision] * -1.3333333333333333), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$1 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$2 = N[(-4.0 * N[(Pi * Pi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(Pi - N[(Infinity * Pi), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z0, -48000000.0], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[(N[(N[(N[(N[(N[(N[(N[(t$95$0 - N[(t$95$2 * t$95$3), $MachinePrecision]), $MachinePrecision] + N[(Infinity * N[(t$95$0 - N[(N[(t$95$2 * 2.0), $MachinePrecision] * t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(N[(N[(N[Tan[N[(1.5 * Pi), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision] * t$95$3), $MachinePrecision] * N[(Pi + Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[(t$95$3 * -2.0), $MachinePrecision]), $MachinePrecision] * z0), $MachinePrecision] - N[Tan[N[(Pi * -0.5), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * z1), $MachinePrecision] / z2), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(N[Cos[t$95$1], $MachinePrecision] * z1), $MachinePrecision] / N[((-N[Sin[t$95$1], $MachinePrecision]) * z2), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]]]

Derivation

1. Split input into 2 regimes

2. if z0 < -4.8e7

   1. Initial program 59.9%

      \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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) \]

   4. Applied rewrites 76.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) \]

   6. Applied rewrites 80.6%

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

   8. Applied rewrites 80.6%

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

   9. Evaluated real constant 84.6%

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

   10. Evaluated real constant 84.6%

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

   11. Evaluated real constant 84.6%

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

   12. Evaluated real constant 42.2%

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

   13. Evaluated real constant 42.2%

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

   if -4.8e7 < z0

   1. Initial program 59.9%

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

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. lift-tan.f64 N/A

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

      4. tan-quot N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 69.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 6: 69.1% accurate, 0.8× speedup

Math

\[\begin{array}{l} t_0 := \left(z0 + z0\right) \cdot \pi\\ 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{\cos t\_0 \cdot z1}{\left(-\sin t\_0\right) \cdot z2}\right)\right) \end{array} \]

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (let* ((t_0 (* (+ z0 z0) PI)))
  (-
   1.0
   (cos (* -2.0 (atan (/ (* (cos t_0) z1) (* (- (sin t_0)) z2))))))))

C

double code(double z1, double z2, double z0) {
	double t_0 = (z0 + z0) * ((double) M_PI);
	return 1.0 - cos((-2.0 * atan(((cos(t_0) * z1) / (-sin(t_0) * z2)))));
}

Java

public static double code(double z1, double z2, double z0) {
	double t_0 = (z0 + z0) * Math.PI;
	return 1.0 - Math.cos((-2.0 * Math.atan(((Math.cos(t_0) * z1) / (-Math.sin(t_0) * z2)))));
}

Python

def code(z1, z2, z0):
	t_0 = (z0 + z0) * math.pi
	return 1.0 - math.cos((-2.0 * math.atan(((math.cos(t_0) * z1) / (-math.sin(t_0) * z2)))))

Julia

function code(z1, z2, z0)
	t_0 = Float64(Float64(z0 + z0) * pi)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(cos(t_0) * z1) / Float64(Float64(-sin(t_0)) * z2))))))
end

MATLAB

function tmp = code(z1, z2, z0)
	t_0 = (z0 + z0) * pi;
	tmp = 1.0 - cos((-2.0 * atan(((cos(t_0) * z1) / (-sin(t_0) * z2)))));
end

Wolfram

code[z1_, z2_, z0_] := Block[{t$95$0 = N[(N[(z0 + z0), $MachinePrecision] * Pi), $MachinePrecision]}, 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]]

Derivation

1. Initial program 59.9%

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

   1. lift-*.f64 N/A

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

   2. lift-/.f64 N/A

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

   3. lift-tan.f64 N/A

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

   4. tan-quot N/A

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

   5. frac-times N/A

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

   6. *-commutative N/A

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

   7. lower-/.f64 N/A

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

3. Applied rewrites 69.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. Add Preprocessing

Alternative 7: 61.2% accurate, 1.0× speedup

Math

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

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (- 1.0 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI 0.5))))))))

C

double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((((double) M_PI) * 0.5))))));
}

Java

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

Python

def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((math.pi * 0.5))))))

Julia

function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(pi * 0.5)))))))
end

MATLAB

function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((pi * 0.5))))));
end

Wolfram

code[z1_, z2_, z0_] := 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]

Derivation

1. Initial program 59.9%

   \[1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\pi \cdot \left(\left(z0 + z0\right) - -0.5\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

4. Applied rewrites 61.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) \]
5. Add Preprocessing

Alternative 8: 61.1% accurate, 1.0× speedup

Math

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

FPCore

(FPCore (z1 z2 z0)
  :precision binary64
  (- 1.0 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* 1.5 PI))))))))

C

double code(double z1, double z2, double z0) {
	return 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((1.5 * ((double) M_PI)))))));
}

Java

public static double code(double z1, double z2, double z0) {
	return 1.0 - Math.cos((-2.0 * Math.atan(((z1 / z2) * Math.tan((1.5 * Math.PI))))));
}

Python

def code(z1, z2, z0):
	return 1.0 - math.cos((-2.0 * math.atan(((z1 / z2) * math.tan((1.5 * math.pi))))))

Julia

function code(z1, z2, z0)
	return Float64(1.0 - cos(Float64(-2.0 * atan(Float64(Float64(z1 / z2) * tan(Float64(1.5 * pi)))))))
end

MATLAB

function tmp = code(z1, z2, z0)
	tmp = 1.0 - cos((-2.0 * atan(((z1 / z2) * tan((1.5 * pi))))));
end

Wolfram

code[z1_, z2_, z0_] := N[(1.0 - N[Cos[N[(-2.0 * N[ArcTan[N[(N[(z1 / z2), $MachinePrecision] * N[Tan[N[(1.5 * Pi), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 59.9%

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

   1. lift-tan.f64 N/A

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

   2. tan-+PI-rev N/A

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

   3. lower-tan.f64 N/A

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

   4. lift-*.f64 N/A

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

   5. *-commutative N/A

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

   6. lift-PI.f64 N/A

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

   7. distribute-lft1-in N/A

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

   8. lower-*.f64 N/A

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

   9. lift--.f64 N/A

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

   10. associate-+l- N/A

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

   11. lower--.f64 N/A

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

   12. metadata-eval 59.9%

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

3. Applied rewrites 59.9%

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

4. Taylor expanded in z0 around 0

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

6. Applied rewrites 61.1%

   \[\leadsto 1 - \cos \left(-2 \cdot \tan^{-1} \left(\frac{z1}{z2} \cdot \tan \left(\color{blue}{1.5} \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 (- (+ z0 z0) -1/2))))))))"
  :precision binary64
  (- 1.0 (cos (* -2.0 (atan (* (/ z1 z2) (tan (* PI (- (+ z0 z0) -0.5)))))))))