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

Percentage Accurate: 63.5% → 88.8%

Time: 23.6s

Alternatives: 8

Speedup: 1.0×

Specification

Math

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

FPCore

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

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Initial Program: 63.5% accurate, 1.0× speedup

Math

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

FPCore

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

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Alternative 1: 88.8% accurate, 0.3× speedup

Math

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

FPCore

(FPCore (z2 z0 z1)
  :precision binary64
  (let* ((t_0 (tan (* 0.5 PI)))
       (t_1 (pow t_0 2.0))
       (t_2 (* (- (+ z2 z2) -0.5) PI))
       (t_3 (* PI (+ z2 z2)))
       (t_4
        (-
         -1.0
         (cos
          (*
           (atan
            (/
             (*
              (+
               (*
                (-
                 (+
                  (*
                   (*
                    (/
                     (*
                      (* PI (sin (* 0.5 PI)))
                      (* (* (+ t_1 1.0) PI) 2.0))
                     (sin (+ (- (* 0.5 PI)) (* 0.5 PI))))
                    2.0)
                   z2)
                  (+ PI PI))
                 (* -2.0 (* t_1 PI)))
                z2)
               t_0)
              z0)
             z1))
           2.0)))))
  (if (<= t_2 -2e+27)
    t_4
    (if (<= t_2 2.0)
      (-
       -1.0
       (cos (* (atan (/ (* (cos t_3) z0) (* (- (sin t_3)) z1))) 2.0)))
      t_4))))

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Split input into 2 regimes

2. if (*.f64 (-.f64 (+.f64 z2 z2) #s(literal -1/2 binary64)) (PI.f64)) < -2e27 or 2 < (*.f64 (-.f64 (+.f64 z2 z2) #s(literal -1/2 binary64)) (PI.f64))

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 79.9%

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

   5. Taylor expanded in z2 around 0

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

   7. Applied rewrites 78.7%

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

   9. Applied rewrites 82.2%

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

       1. lift-cos.f64 N/A

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

       2. cos-neg-rev N/A

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

       3. sin-+PI/2-rev N/A

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

       4. lower-sin.f64 N/A

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

       5. lower-+.f64 N/A

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

       6. lift-*.f64 N/A

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

       7. *-commutative N/A

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

       8. metadata-eval N/A

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

       9. mult-flip N/A

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

       10. lift-PI.f64 N/A

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

       11. lower-neg.f64 N/A

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

       12. lift-PI.f64 N/A

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

       13. mult-flip N/A

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

       14. metadata-eval N/A

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

       15. *-commutative N/A

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

       16. lift-*.f64 N/A

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

       17. lift-PI.f64 N/A

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

       18. mult-flip N/A

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

       19. metadata-eval N/A

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

       20. *-commutative N/A

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

       21. lift-*.f64 74.1%

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

   11. Applied rewrites 74.1%

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

   if -2e27 < (*.f64 (-.f64 (+.f64 z2 z2) #s(literal -1/2 binary64)) (PI.f64)) < 2

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

Alternative 2: 87.1% accurate, 0.2× speedup

Math

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

FPCore

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

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Split input into 2 regimes

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

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 79.9%

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

   6. Applied rewrites 84.3%

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

   8. Applied rewrites 84.3%

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

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

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

Alternative 3: 85.0% accurate, 0.3× speedup

Math

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

FPCore

(FPCore (z2 z0 z1)
  :precision binary64
  (let* ((t_0 (tan (* 0.5 PI)))
       (t_1 (pow t_0 2.0))
       (t_2 (* PI (+ z2 z2))))
  (if (<= (tan (* (- (+ z2 z2) -0.5) PI)) 40000000000000.0)
    (-
     -1.0
     (cos
      (*
       (atan
        (/
         (*
          (+
           (*
            (-
             (+
              (*
               (*
                (/
                 (*
                  (* PI (sin (* 0.5 PI)))
                  (* (* (+ t_1 1.0) PI) 2.0))
                 (cos (* 0.5 PI)))
                2.0)
               z2)
              (+ PI PI))
             (* -2.0 (* t_1 PI)))
            z2)
           t_0)
          z0)
         z1))
       2.0)))
    (-
     -1.0
     (cos (* (atan (/ (* (cos t_2) z0) (* (- (sin t_2)) z1))) 2.0))))))

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Split input into 2 regimes

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

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 79.9%

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

   5. Taylor expanded in z2 around 0

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

   7. Applied rewrites 78.7%

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

   9. Applied rewrites 82.2%

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

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

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

Alternative 4: 85.0% accurate, 0.3× speedup

Math

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

FPCore

(FPCore (z2 z0 z1)
  :precision binary64
  (let* ((t_0 (tan (* 0.5 PI)))
       (t_1 (pow t_0 2.0))
       (t_2 (* PI (+ z2 z2))))
  (if (<= (tan (* (- (+ z2 z2) -0.5) PI)) 40000000000000.0)
    (-
     -1.0
     (cos
      (*
       (atan
        (/
         (*
          (+
           (*
            (-
             (+
              (+
               (*
                (*
                 (*
                  (* (sin (* 0.5 PI)) PI)
                  (/ (* (- t_1 -1.0) (+ PI PI)) (sin (* 1.0 PI))))
                 2.0)
                z2)
               PI)
              PI)
             (* -2.0 (* t_1 PI)))
            z2)
           t_0)
          z0)
         z1))
       2.0)))
    (-
     -1.0
     (cos (* (atan (/ (* (cos t_2) z0) (* (- (sin t_2)) z1))) 2.0))))))

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Split input into 2 regimes

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

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 79.9%

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

   5. Taylor expanded in z2 around 0

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

   7. Applied rewrites 78.7%

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

   9. Applied rewrites 82.2%

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

   11. Applied rewrites 82.2%

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

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

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

Alternative 5: 83.9% accurate, 0.5× speedup

Math

\[\begin{array}{l} t_0 := 0.5 \cdot \cos \pi\\ t_1 := -1 - \cos \left(\tan^{-1} \left(\left(z2 \cdot \left(2 \cdot \pi - -2 \cdot \frac{\pi \cdot \left(0.5 - t\_0\right)}{0.5 + t\_0}\right) + \frac{\sin \left(0.5 \cdot \pi\right)}{\cos \left(0.5 \cdot \pi\right)}\right) \cdot \frac{z0}{z1}\right) \cdot 2\right)\\ t_2 := \pi \cdot \left(z2 + z2\right)\\ \mathbf{if}\;z2 \leq -4.15 \cdot 10^{+21}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;z2 \leq 650000000000:\\ \;\;\;\;-1 - \cos \left(\tan^{-1} \left(\frac{\cos t\_2 \cdot z0}{\left(-\sin t\_2\right) \cdot z1}\right) \cdot 2\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \]

FPCore

(FPCore (z2 z0 z1)
  :precision binary64
  (let* ((t_0 (* 0.5 (cos PI)))
       (t_1
        (-
         -1.0
         (cos
          (*
           (atan
            (*
             (+
              (*
               z2
               (-
                (* 2.0 PI)
                (* -2.0 (/ (* PI (- 0.5 t_0)) (+ 0.5 t_0)))))
              (/ (sin (* 0.5 PI)) (cos (* 0.5 PI))))
             (/ z0 z1)))
           2.0))))
       (t_2 (* PI (+ z2 z2))))
  (if (<= z2 -4.15e+21)
    t_1
    (if (<= z2 650000000000.0)
      (-
       -1.0
       (cos (* (atan (/ (* (cos t_2) z0) (* (- (sin t_2)) z1))) 2.0)))
      t_1))))

C

double code(double z2, double z0, double z1) {
	double t_0 = 0.5 * cos(((double) M_PI));
	double t_1 = -1.0 - cos((atan((((z2 * ((2.0 * ((double) M_PI)) - (-2.0 * ((((double) M_PI) * (0.5 - t_0)) / (0.5 + t_0))))) + (sin((0.5 * ((double) M_PI))) / cos((0.5 * ((double) M_PI))))) * (z0 / z1))) * 2.0));
	double t_2 = ((double) M_PI) * (z2 + z2);
	double tmp;
	if (z2 <= -4.15e+21) {
		tmp = t_1;
	} else if (z2 <= 650000000000.0) {
		tmp = -1.0 - cos((atan(((cos(t_2) * z0) / (-sin(t_2) * z1))) * 2.0));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Java

public static double code(double z2, double z0, double z1) {
	double t_0 = 0.5 * Math.cos(Math.PI);
	double t_1 = -1.0 - Math.cos((Math.atan((((z2 * ((2.0 * Math.PI) - (-2.0 * ((Math.PI * (0.5 - t_0)) / (0.5 + t_0))))) + (Math.sin((0.5 * Math.PI)) / Math.cos((0.5 * Math.PI)))) * (z0 / z1))) * 2.0));
	double t_2 = Math.PI * (z2 + z2);
	double tmp;
	if (z2 <= -4.15e+21) {
		tmp = t_1;
	} else if (z2 <= 650000000000.0) {
		tmp = -1.0 - Math.cos((Math.atan(((Math.cos(t_2) * z0) / (-Math.sin(t_2) * z1))) * 2.0));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(z2, z0, z1):
	t_0 = 0.5 * math.cos(math.pi)
	t_1 = -1.0 - math.cos((math.atan((((z2 * ((2.0 * math.pi) - (-2.0 * ((math.pi * (0.5 - t_0)) / (0.5 + t_0))))) + (math.sin((0.5 * math.pi)) / math.cos((0.5 * math.pi)))) * (z0 / z1))) * 2.0))
	t_2 = math.pi * (z2 + z2)
	tmp = 0
	if z2 <= -4.15e+21:
		tmp = t_1
	elif z2 <= 650000000000.0:
		tmp = -1.0 - math.cos((math.atan(((math.cos(t_2) * z0) / (-math.sin(t_2) * z1))) * 2.0))
	else:
		tmp = t_1
	return tmp

Julia

function code(z2, z0, z1)
	t_0 = Float64(0.5 * cos(pi))
	t_1 = Float64(-1.0 - cos(Float64(atan(Float64(Float64(Float64(z2 * Float64(Float64(2.0 * pi) - Float64(-2.0 * Float64(Float64(pi * Float64(0.5 - t_0)) / Float64(0.5 + t_0))))) + Float64(sin(Float64(0.5 * pi)) / cos(Float64(0.5 * pi)))) * Float64(z0 / z1))) * 2.0)))
	t_2 = Float64(pi * Float64(z2 + z2))
	tmp = 0.0
	if (z2 <= -4.15e+21)
		tmp = t_1;
	elseif (z2 <= 650000000000.0)
		tmp = Float64(-1.0 - cos(Float64(atan(Float64(Float64(cos(t_2) * z0) / Float64(Float64(-sin(t_2)) * z1))) * 2.0)));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp_2 = code(z2, z0, z1)
	t_0 = 0.5 * cos(pi);
	t_1 = -1.0 - cos((atan((((z2 * ((2.0 * pi) - (-2.0 * ((pi * (0.5 - t_0)) / (0.5 + t_0))))) + (sin((0.5 * pi)) / cos((0.5 * pi)))) * (z0 / z1))) * 2.0));
	t_2 = pi * (z2 + z2);
	tmp = 0.0;
	if (z2 <= -4.15e+21)
		tmp = t_1;
	elseif (z2 <= 650000000000.0)
		tmp = -1.0 - cos((atan(((cos(t_2) * z0) / (-sin(t_2) * z1))) * 2.0));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[z2_, z0_, z1_] := Block[{t$95$0 = N[(0.5 * N[Cos[Pi], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(-1.0 - N[Cos[N[(N[ArcTan[N[(N[(N[(z2 * N[(N[(2.0 * Pi), $MachinePrecision] - N[(-2.0 * N[(N[(Pi * N[(0.5 - t$95$0), $MachinePrecision]), $MachinePrecision] / N[(0.5 + t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sin[N[(0.5 * Pi), $MachinePrecision]], $MachinePrecision] / N[Cos[N[(0.5 * Pi), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(z0 / z1), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(Pi * N[(z2 + z2), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z2, -4.15e+21], t$95$1, If[LessEqual[z2, 650000000000.0], N[(-1.0 - N[Cos[N[(N[ArcTan[N[(N[(N[Cos[t$95$2], $MachinePrecision] * z0), $MachinePrecision] / N[((-N[Sin[t$95$2], $MachinePrecision]) * z1), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], t$95$1]]]]]

Derivation

1. Split input into 2 regimes

2. if z2 < -4.15e21 or 6.5e11 < z2

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 79.9%

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

   5. Taylor expanded in z2 around 0

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

   7. Applied rewrites 78.7%

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

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. lift-pow.f64 N/A

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

      4. lift-cos.f64 N/A

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

      5. lift-*.f64 N/A

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

      6. lift-PI.f64 N/A

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

      7. associate-*r/ N/A

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

      8. lower-/.f64 N/A

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

   9. Applied rewrites 68.2%

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

       1. lift-*.f64 N/A

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

       2. lift-/.f64 N/A

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

       3. lift-pow.f64 N/A

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

       4. lift-cos.f64 N/A

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

       5. lift-*.f64 N/A

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

       6. lift-PI.f64 N/A

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

       7. associate-*r/ N/A

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

       8. lower-/.f64 N/A

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

   11. Applied rewrites 34.3%

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

   12. Taylor expanded in z2 around 0

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

   14. Applied rewrites 68.2%

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

   if -4.15e21 < z2 < 6.5e11

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

Alternative 6: 77.8% accurate, 0.5× speedup

Math

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

FPCore

(FPCore (z2 z0 z1)
  :precision binary64
  (let* ((t_0 (* PI (+ z2 z2))) (t_1 (tan (* 0.5 PI))))
  (if (<= (tan (* (- (+ z2 z2) -0.5) PI)) 10.0)
    (-
     -1.0
     (cos
      (*
       (atan
        (/
         (*
          (+ (* (- (* 2.0 PI) (* -2.0 (* (pow t_1 2.0) PI))) z2) t_1)
          z0)
         z1))
       2.0)))
    (-
     -1.0
     (cos (* (atan (/ (* (cos t_0) z0) (* (- (sin t_0)) z1))) 2.0))))))

C

double code(double z2, double z0, double z1) {
	double t_0 = ((double) M_PI) * (z2 + z2);
	double t_1 = tan((0.5 * ((double) M_PI)));
	double tmp;
	if (tan((((z2 + z2) - -0.5) * ((double) M_PI))) <= 10.0) {
		tmp = -1.0 - cos((atan(((((((2.0 * ((double) M_PI)) - (-2.0 * (pow(t_1, 2.0) * ((double) M_PI)))) * z2) + t_1) * z0) / z1)) * 2.0));
	} else {
		tmp = -1.0 - cos((atan(((cos(t_0) * z0) / (-sin(t_0) * z1))) * 2.0));
	}
	return tmp;
}

Java

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

Python

def code(z2, z0, z1):
	t_0 = math.pi * (z2 + z2)
	t_1 = math.tan((0.5 * math.pi))
	tmp = 0
	if math.tan((((z2 + z2) - -0.5) * math.pi)) <= 10.0:
		tmp = -1.0 - math.cos((math.atan(((((((2.0 * math.pi) - (-2.0 * (math.pow(t_1, 2.0) * math.pi))) * z2) + t_1) * z0) / z1)) * 2.0))
	else:
		tmp = -1.0 - math.cos((math.atan(((math.cos(t_0) * z0) / (-math.sin(t_0) * z1))) * 2.0))
	return tmp

Julia

function code(z2, z0, z1)
	t_0 = Float64(pi * Float64(z2 + z2))
	t_1 = tan(Float64(0.5 * pi))
	tmp = 0.0
	if (tan(Float64(Float64(Float64(z2 + z2) - -0.5) * pi)) <= 10.0)
		tmp = Float64(-1.0 - cos(Float64(atan(Float64(Float64(Float64(Float64(Float64(Float64(2.0 * pi) - Float64(-2.0 * Float64((t_1 ^ 2.0) * pi))) * z2) + t_1) * z0) / z1)) * 2.0)));
	else
		tmp = Float64(-1.0 - cos(Float64(atan(Float64(Float64(cos(t_0) * z0) / Float64(Float64(-sin(t_0)) * z1))) * 2.0)));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z2, z0, z1)
	t_0 = pi * (z2 + z2);
	t_1 = tan((0.5 * pi));
	tmp = 0.0;
	if (tan((((z2 + z2) - -0.5) * pi)) <= 10.0)
		tmp = -1.0 - cos((atan(((((((2.0 * pi) - (-2.0 * ((t_1 ^ 2.0) * pi))) * z2) + t_1) * z0) / z1)) * 2.0));
	else
		tmp = -1.0 - cos((atan(((cos(t_0) * z0) / (-sin(t_0) * z1))) * 2.0));
	end
	tmp_2 = tmp;
end

Wolfram

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

Derivation

1. Split input into 2 regimes

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

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 79.9%

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

   5. Taylor expanded in z2 around 0

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

   7. Applied rewrites 78.7%

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

   9. Applied rewrites 82.2%

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

   10. Taylor expanded in z2 around 0

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

   12. Applied rewrites 75.4%

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

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

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

Alternative 7: 67.4% accurate, 0.7× speedup

Math

\[\begin{array}{l} t_0 := \pi \cdot \left(z2 + z2\right)\\ t_1 := \frac{\left|z0\right|}{\left|z1\right|}\\ \mathbf{if}\;t\_1 \leq 10^{-12}:\\ \;\;\;\;-1 - \cos \left(\tan^{-1} \left(\frac{\cos t\_0 \cdot \left|z0\right|}{\left(-\sin t\_0\right) \cdot \left|z1\right|}\right) \cdot 2\right)\\ \mathbf{else}:\\ \;\;\;\;-1 - \cos \left(\tan^{-1} \left(\tan \left(0.5 \cdot \pi\right) \cdot t\_1\right) \cdot 2\right)\\ \end{array} \]

FPCore

(FPCore (z2 z0 z1)
  :precision binary64
  (let* ((t_0 (* PI (+ z2 z2))) (t_1 (/ (fabs z0) (fabs z1))))
  (if (<= t_1 1e-12)
    (-
     -1.0
     (cos
      (*
       (atan (/ (* (cos t_0) (fabs z0)) (* (- (sin t_0)) (fabs z1))))
       2.0)))
    (- -1.0 (cos (* (atan (* (tan (* 0.5 PI)) t_1)) 2.0))))))

C

double code(double z2, double z0, double z1) {
	double t_0 = ((double) M_PI) * (z2 + z2);
	double t_1 = fabs(z0) / fabs(z1);
	double tmp;
	if (t_1 <= 1e-12) {
		tmp = -1.0 - cos((atan(((cos(t_0) * fabs(z0)) / (-sin(t_0) * fabs(z1)))) * 2.0));
	} else {
		tmp = -1.0 - cos((atan((tan((0.5 * ((double) M_PI))) * t_1)) * 2.0));
	}
	return tmp;
}

Java

public static double code(double z2, double z0, double z1) {
	double t_0 = Math.PI * (z2 + z2);
	double t_1 = Math.abs(z0) / Math.abs(z1);
	double tmp;
	if (t_1 <= 1e-12) {
		tmp = -1.0 - Math.cos((Math.atan(((Math.cos(t_0) * Math.abs(z0)) / (-Math.sin(t_0) * Math.abs(z1)))) * 2.0));
	} else {
		tmp = -1.0 - Math.cos((Math.atan((Math.tan((0.5 * Math.PI)) * t_1)) * 2.0));
	}
	return tmp;
}

Python

def code(z2, z0, z1):
	t_0 = math.pi * (z2 + z2)
	t_1 = math.fabs(z0) / math.fabs(z1)
	tmp = 0
	if t_1 <= 1e-12:
		tmp = -1.0 - math.cos((math.atan(((math.cos(t_0) * math.fabs(z0)) / (-math.sin(t_0) * math.fabs(z1)))) * 2.0))
	else:
		tmp = -1.0 - math.cos((math.atan((math.tan((0.5 * math.pi)) * t_1)) * 2.0))
	return tmp

Julia

function code(z2, z0, z1)
	t_0 = Float64(pi * Float64(z2 + z2))
	t_1 = Float64(abs(z0) / abs(z1))
	tmp = 0.0
	if (t_1 <= 1e-12)
		tmp = Float64(-1.0 - cos(Float64(atan(Float64(Float64(cos(t_0) * abs(z0)) / Float64(Float64(-sin(t_0)) * abs(z1)))) * 2.0)));
	else
		tmp = Float64(-1.0 - cos(Float64(atan(Float64(tan(Float64(0.5 * pi)) * t_1)) * 2.0)));
	end
	return tmp
end

MATLAB

function tmp_2 = code(z2, z0, z1)
	t_0 = pi * (z2 + z2);
	t_1 = abs(z0) / abs(z1);
	tmp = 0.0;
	if (t_1 <= 1e-12)
		tmp = -1.0 - cos((atan(((cos(t_0) * abs(z0)) / (-sin(t_0) * abs(z1)))) * 2.0));
	else
		tmp = -1.0 - cos((atan((tan((0.5 * pi)) * t_1)) * 2.0));
	end
	tmp_2 = tmp;
end

Wolfram

code[z2_, z0_, z1_] := Block[{t$95$0 = N[(Pi * N[(z2 + z2), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[Abs[z0], $MachinePrecision] / N[Abs[z1], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, 1e-12], N[(-1.0 - N[Cos[N[(N[ArcTan[N[(N[(N[Cos[t$95$0], $MachinePrecision] * N[Abs[z0], $MachinePrecision]), $MachinePrecision] / N[((-N[Sin[t$95$0], $MachinePrecision]) * N[Abs[z1], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(-1.0 - N[Cos[N[(N[ArcTan[N[(N[Tan[N[(0.5 * Pi), $MachinePrecision]], $MachinePrecision] * t$95$1), $MachinePrecision]], $MachinePrecision] * 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if (/.f64 z0 z1) < 9.9999999999999998e-13

   1. Initial program 63.5%

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

      1. lift-*.f64 N/A

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

      2. lift-tan.f64 N/A

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

      3. tan-quot N/A

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

      4. lift-/.f64 N/A

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

      5. frac-times N/A

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

      6. *-commutative N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 66.4%

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

   if 9.9999999999999998e-13 < (/.f64 z0 z1)

   1. Initial program 63.5%

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

   2. Taylor expanded in z2 around 0

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

   4. Applied rewrites 64.7%

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

Alternative 8: 64.7% accurate, 1.0× speedup

Math

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

FPCore

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

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Initial program 63.5%

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

2. Taylor expanded in z2 around 0

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

4. Applied rewrites 64.7%

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

Reproduce

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