UniformSampleCone 2

Percentage Accurate: 99.0% → 99.0%
Time: 8.9s
Alternatives: 20
Speedup: 1.0×

Specification

?
\[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\ t_2 := \left(uy \cdot 2\right) \cdot \pi\\ \left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux))
        (t_1 (sqrt (- 1.0 (* t_0 t_0))))
        (t_2 (* (* uy 2.0) PI)))
   (+ (+ (* (* (cos t_2) t_1) xi) (* (* (sin t_2) t_1) yi)) (* t_0 zi))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((1.0f - ux) * maxCos) * ux;
	float t_1 = sqrtf((1.0f - (t_0 * t_0)));
	float t_2 = (uy * 2.0f) * ((float) M_PI);
	return (((cosf(t_2) * t_1) * xi) + ((sinf(t_2) * t_1) * yi)) + (t_0 * zi);
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
	t_1 = sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))
	t_2 = Float32(Float32(uy * Float32(2.0)) * Float32(pi))
	return Float32(Float32(Float32(Float32(cos(t_2) * t_1) * xi) + Float32(Float32(sin(t_2) * t_1) * yi)) + Float32(t_0 * zi))
end
function tmp = code(xi, yi, zi, ux, uy, maxCos)
	t_0 = ((single(1.0) - ux) * maxCos) * ux;
	t_1 = sqrt((single(1.0) - (t_0 * t_0)));
	t_2 = (uy * single(2.0)) * single(pi);
	tmp = (((cos(t_2) * t_1) * xi) + ((sin(t_2) * t_1) * yi)) + (t_0 * zi);
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\
t_2 := \left(uy \cdot 2\right) \cdot \pi\\
\left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi
\end{array}
\end{array}

Sampling outcomes in binary32 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 20 alternatives:

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

Initial Program: 99.0% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\ t_2 := \left(uy \cdot 2\right) \cdot \pi\\ \left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux))
        (t_1 (sqrt (- 1.0 (* t_0 t_0))))
        (t_2 (* (* uy 2.0) PI)))
   (+ (+ (* (* (cos t_2) t_1) xi) (* (* (sin t_2) t_1) yi)) (* t_0 zi))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((1.0f - ux) * maxCos) * ux;
	float t_1 = sqrtf((1.0f - (t_0 * t_0)));
	float t_2 = (uy * 2.0f) * ((float) M_PI);
	return (((cosf(t_2) * t_1) * xi) + ((sinf(t_2) * t_1) * yi)) + (t_0 * zi);
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
	t_1 = sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))
	t_2 = Float32(Float32(uy * Float32(2.0)) * Float32(pi))
	return Float32(Float32(Float32(Float32(cos(t_2) * t_1) * xi) + Float32(Float32(sin(t_2) * t_1) * yi)) + Float32(t_0 * zi))
end
function tmp = code(xi, yi, zi, ux, uy, maxCos)
	t_0 = ((single(1.0) - ux) * maxCos) * ux;
	t_1 = sqrt((single(1.0) - (t_0 * t_0)));
	t_2 = (uy * single(2.0)) * single(pi);
	tmp = (((cos(t_2) * t_1) * xi) + ((sin(t_2) * t_1) * yi)) + (t_0 * zi);
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\
t_2 := \left(uy \cdot 2\right) \cdot \pi\\
\left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi
\end{array}
\end{array}

Alternative 1: 99.0% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\ t_2 := \left(uy \cdot 2\right) \cdot \pi\\ \left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux))
        (t_1 (sqrt (- 1.0 (* t_0 t_0))))
        (t_2 (* (* uy 2.0) PI)))
   (+
    (+ (* (* (cos t_2) t_1) xi) (* (* (sin t_2) t_1) yi))
    (* (* (fma (- maxCos) ux maxCos) ux) zi))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((1.0f - ux) * maxCos) * ux;
	float t_1 = sqrtf((1.0f - (t_0 * t_0)));
	float t_2 = (uy * 2.0f) * ((float) M_PI);
	return (((cosf(t_2) * t_1) * xi) + ((sinf(t_2) * t_1) * yi)) + ((fmaf(-maxCos, ux, maxCos) * ux) * zi);
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
	t_1 = sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))
	t_2 = Float32(Float32(uy * Float32(2.0)) * Float32(pi))
	return Float32(Float32(Float32(Float32(cos(t_2) * t_1) * xi) + Float32(Float32(sin(t_2) * t_1) * yi)) + Float32(Float32(fma(Float32(-maxCos), ux, maxCos) * ux) * zi))
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\
t_2 := \left(uy \cdot 2\right) \cdot \pi\\
\left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi
\end{array}
\end{array}
Derivation
  1. Initial program 98.7%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Add Preprocessing
  3. Taylor expanded in ux around 0

    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\left(maxCos + -1 \cdot \left(maxCos \cdot ux\right)\right)} \cdot ux\right) \cdot zi \]
  4. Step-by-step derivation
    1. +-commutativeN/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(-1 \cdot \left(maxCos \cdot ux\right) + \color{blue}{maxCos}\right) \cdot ux\right) \cdot zi \]
    2. associate-*r*N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(-1 \cdot maxCos\right) \cdot ux + maxCos\right) \cdot ux\right) \cdot zi \]
    3. lower-fma.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-1 \cdot maxCos, \color{blue}{ux}, maxCos\right) \cdot ux\right) \cdot zi \]
    4. mul-1-negN/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(\mathsf{neg}\left(maxCos\right), ux, maxCos\right) \cdot ux\right) \cdot zi \]
    5. lower-neg.f3298.7

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \]
  5. Applied rewrites98.7%

    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\mathsf{fma}\left(-maxCos, ux, maxCos\right)} \cdot ux\right) \cdot zi \]
  6. Add Preprocessing

Alternative 2: 98.9% accurate, 1.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - t\_0 \cdot t\_0}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + t\_0 \cdot zi \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux)))
   (+
    (+
     (* (* (cos (* (* uy 2.0) PI)) (sqrt (- 1.0 (* t_0 t_0)))) xi)
     (* (sin (* PI (* 2.0 uy))) yi))
    (* t_0 zi))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((1.0f - ux) * maxCos) * ux;
	return (((cosf(((uy * 2.0f) * ((float) M_PI))) * sqrtf((1.0f - (t_0 * t_0)))) * xi) + (sinf((((float) M_PI) * (2.0f * uy))) * yi)) + (t_0 * zi);
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
	return Float32(Float32(Float32(Float32(cos(Float32(Float32(uy * Float32(2.0)) * Float32(pi))) * sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))) * xi) + Float32(sin(Float32(Float32(pi) * Float32(Float32(2.0) * uy))) * yi)) + Float32(t_0 * zi))
end
function tmp = code(xi, yi, zi, ux, uy, maxCos)
	t_0 = ((single(1.0) - ux) * maxCos) * ux;
	tmp = (((cos(((uy * single(2.0)) * single(pi))) * sqrt((single(1.0) - (t_0 * t_0)))) * xi) + (sin((single(pi) * (single(2.0) * uy))) * yi)) + (t_0 * zi);
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - t\_0 \cdot t\_0}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + t\_0 \cdot zi
\end{array}
\end{array}
Derivation
  1. Initial program 98.7%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Add Preprocessing
  3. Taylor expanded in ux around 0

    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  4. Step-by-step derivation
    1. associate-*r*N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(2 \cdot uy\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    2. *-commutativeN/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    3. lift-*.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    4. lift-*.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    5. lift-PI.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    6. lift-sin.f3298.7

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    7. lift-PI.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    8. lift-*.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    9. *-commutativeN/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    10. lower-*.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    11. lift-PI.f3298.7

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    12. lift-*.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    13. *-commutativeN/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    14. lower-*.f3298.7

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  5. Applied rewrites98.7%

    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  6. Add Preprocessing

Alternative 3: 98.7% accurate, 1.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \pi \cdot \left(2 \cdot uy\right)\\ \mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot zi, \mathsf{fma}\left(\cos t\_0, xi, \sin t\_0 \cdot yi\right)\right) \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* PI (* 2.0 uy))))
   (fma (* maxCos ux) (* (- 1.0 ux) zi) (fma (cos t_0) xi (* (sin t_0) yi)))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((float) M_PI) * (2.0f * uy);
	return fmaf((maxCos * ux), ((1.0f - ux) * zi), fmaf(cosf(t_0), xi, (sinf(t_0) * yi)));
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(pi) * Float32(Float32(2.0) * uy))
	return fma(Float32(maxCos * ux), Float32(Float32(Float32(1.0) - ux) * zi), fma(cos(t_0), xi, Float32(sin(t_0) * yi)))
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \pi \cdot \left(2 \cdot uy\right)\\
\mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot zi, \mathsf{fma}\left(\cos t\_0, xi, \sin t\_0 \cdot yi\right)\right)
\end{array}
\end{array}
Derivation
  1. Initial program 98.7%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Add Preprocessing
  3. Taylor expanded in maxCos around 0

    \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
  4. Step-by-step derivation
    1. associate-*r*N/A

      \[\leadsto \left(maxCos \cdot ux\right) \cdot \left(zi \cdot \left(1 - ux\right)\right) + \left(\color{blue}{xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
    2. lower-fma.f32N/A

      \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \color{blue}{zi \cdot \left(1 - ux\right)}, xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
    3. lower-*.f32N/A

      \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \color{blue}{zi} \cdot \left(1 - ux\right), xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
    4. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot \color{blue}{zi}, xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
    5. lower-*.f32N/A

      \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot \color{blue}{zi}, xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
    6. lift--.f32N/A

      \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot zi, xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
    7. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot zi, \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot xi + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
  5. Applied rewrites98.6%

    \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos \cdot ux, \left(1 - ux\right) \cdot zi, \mathsf{fma}\left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right), xi, \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right)\right)} \]
  6. Add Preprocessing

Alternative 4: 95.8% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := 2 \cdot \left(uy \cdot \pi\right)\\ \mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right)\right) \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* 2.0 (* uy PI))))
   (fma maxCos (* ux zi) (fma xi (cos t_0) (* yi (sin t_0))))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = 2.0f * (uy * ((float) M_PI));
	return fmaf(maxCos, (ux * zi), fmaf(xi, cosf(t_0), (yi * sinf(t_0))));
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(2.0) * Float32(uy * Float32(pi)))
	return fma(maxCos, Float32(ux * zi), fma(xi, cos(t_0), Float32(yi * sin(t_0))))
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := 2 \cdot \left(uy \cdot \pi\right)\\
\mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right)\right)
\end{array}
\end{array}
Derivation
  1. Initial program 98.7%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-cos.f32N/A

      \[\leadsto \left(\left(\color{blue}{\cos \left(\left(uy \cdot 2\right) \cdot \pi\right)} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    2. lift-PI.f32N/A

      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    3. lift-*.f32N/A

      \[\leadsto \left(\left(\cos \color{blue}{\left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    4. lift-*.f32N/A

      \[\leadsto \left(\left(\cos \left(\color{blue}{\left(uy \cdot 2\right)} \cdot \mathsf{PI}\left(\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    5. *-commutativeN/A

      \[\leadsto \left(\left(\cos \left(\color{blue}{\left(2 \cdot uy\right)} \cdot \mathsf{PI}\left(\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    6. associate-*r*N/A

      \[\leadsto \left(\left(\cos \color{blue}{\left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    7. cos-2N/A

      \[\leadsto \left(\left(\color{blue}{\left(\cos \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    8. lower--.f32N/A

      \[\leadsto \left(\left(\color{blue}{\left(\cos \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    9. lower-*.f32N/A

      \[\leadsto \left(\left(\left(\color{blue}{\cos \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right)} - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    10. lower-cos.f32N/A

      \[\leadsto \left(\left(\left(\color{blue}{\cos \left(uy \cdot \mathsf{PI}\left(\right)\right)} \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    11. *-commutativeN/A

      \[\leadsto \left(\left(\left(\cos \color{blue}{\left(\mathsf{PI}\left(\right) \cdot uy\right)} \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    12. lower-*.f32N/A

      \[\leadsto \left(\left(\left(\cos \color{blue}{\left(\mathsf{PI}\left(\right) \cdot uy\right)} \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    13. lift-PI.f32N/A

      \[\leadsto \left(\left(\left(\cos \left(\color{blue}{\pi} \cdot uy\right) \cdot \cos \left(uy \cdot \mathsf{PI}\left(\right)\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    14. lower-cos.f32N/A

      \[\leadsto \left(\left(\left(\cos \left(\pi \cdot uy\right) \cdot \color{blue}{\cos \left(uy \cdot \mathsf{PI}\left(\right)\right)} - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    15. *-commutativeN/A

      \[\leadsto \left(\left(\left(\cos \left(\pi \cdot uy\right) \cdot \cos \color{blue}{\left(\mathsf{PI}\left(\right) \cdot uy\right)} - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    16. lower-*.f32N/A

      \[\leadsto \left(\left(\left(\cos \left(\pi \cdot uy\right) \cdot \cos \color{blue}{\left(\mathsf{PI}\left(\right) \cdot uy\right)} - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    17. lift-PI.f32N/A

      \[\leadsto \left(\left(\left(\cos \left(\pi \cdot uy\right) \cdot \cos \left(\color{blue}{\pi} \cdot uy\right) - \sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    18. lower-*.f32N/A

      \[\leadsto \left(\left(\left(\cos \left(\pi \cdot uy\right) \cdot \cos \left(\pi \cdot uy\right) - \color{blue}{\sin \left(uy \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(uy \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  4. Applied rewrites98.7%

    \[\leadsto \left(\left(\color{blue}{\left(\cos \left(\pi \cdot uy\right) \cdot \cos \left(\pi \cdot uy\right) - \sin \left(\pi \cdot uy\right) \cdot \sin \left(\pi \cdot uy\right)\right)} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  5. Taylor expanded in ux around 0

    \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot zi\right) + \left(xi \cdot \left({\cos \left(uy \cdot \mathsf{PI}\left(\right)\right)}^{2} - {\sin \left(uy \cdot \mathsf{PI}\left(\right)\right)}^{2}\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
  6. Step-by-step derivation
    1. Applied rewrites95.6%

      \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right)} \]
    2. Add Preprocessing

    Alternative 5: 95.8% accurate, 1.5× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_0 := \pi \cdot \left(2 \cdot uy\right)\\ \mathsf{fma}\left(maxCos \cdot ux, zi, \mathsf{fma}\left(\cos t\_0, xi, \sin t\_0 \cdot yi\right)\right) \end{array} \end{array} \]
    (FPCore (xi yi zi ux uy maxCos)
     :precision binary32
     (let* ((t_0 (* PI (* 2.0 uy))))
       (fma (* maxCos ux) zi (fma (cos t_0) xi (* (sin t_0) yi)))))
    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
    	float t_0 = ((float) M_PI) * (2.0f * uy);
    	return fmaf((maxCos * ux), zi, fmaf(cosf(t_0), xi, (sinf(t_0) * yi)));
    }
    
    function code(xi, yi, zi, ux, uy, maxCos)
    	t_0 = Float32(Float32(pi) * Float32(Float32(2.0) * uy))
    	return fma(Float32(maxCos * ux), zi, fma(cos(t_0), xi, Float32(sin(t_0) * yi)))
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_0 := \pi \cdot \left(2 \cdot uy\right)\\
    \mathsf{fma}\left(maxCos \cdot ux, zi, \mathsf{fma}\left(\cos t\_0, xi, \sin t\_0 \cdot yi\right)\right)
    \end{array}
    \end{array}
    
    Derivation
    1. Initial program 98.7%

      \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    2. Add Preprocessing
    3. Taylor expanded in ux around 0

      \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot zi\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
    4. Step-by-step derivation
      1. associate-*r*N/A

        \[\leadsto \left(maxCos \cdot ux\right) \cdot zi + \left(\color{blue}{xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
      2. lower-fma.f32N/A

        \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, \color{blue}{zi}, xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
      3. lower-*.f32N/A

        \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, zi, xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
      4. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, zi, \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot xi + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
      5. lower-fma.f32N/A

        \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, zi, \mathsf{fma}\left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right), xi, yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]
    5. Applied rewrites95.6%

      \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos \cdot ux, zi, \mathsf{fma}\left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right), xi, \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right)\right)} \]
    6. Add Preprocessing

    Alternative 6: 96.7% accurate, 1.5× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_0 := \pi \cdot \left(2 \cdot uy\right)\\ \mathbf{if}\;uy \leq 0.014999999664723873:\\ \;\;\;\;\left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \pi}{xi}, uy \cdot \mathsf{fma}\left(-2, \pi \cdot \pi, -1.3333333333333333 \cdot \frac{uy \cdot \left(yi \cdot {\pi}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos t\_0, xi, \sin t\_0 \cdot yi\right)\\ \end{array} \end{array} \]
    (FPCore (xi yi zi ux uy maxCos)
     :precision binary32
     (let* ((t_0 (* PI (* 2.0 uy))))
       (if (<= uy 0.014999999664723873)
         (+
          (*
           (*
            1.0
            (+
             1.0
             (*
              uy
              (fma
               2.0
               (/ (* yi PI) xi)
               (*
                uy
                (fma
                 -2.0
                 (* PI PI)
                 (* -1.3333333333333333 (/ (* uy (* yi (pow PI 3.0))) xi))))))))
           xi)
          (* (* (* (- 1.0 ux) maxCos) ux) zi))
         (fma (cos t_0) xi (* (sin t_0) yi)))))
    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
    	float t_0 = ((float) M_PI) * (2.0f * uy);
    	float tmp;
    	if (uy <= 0.014999999664723873f) {
    		tmp = ((1.0f * (1.0f + (uy * fmaf(2.0f, ((yi * ((float) M_PI)) / xi), (uy * fmaf(-2.0f, (((float) M_PI) * ((float) M_PI)), (-1.3333333333333333f * ((uy * (yi * powf(((float) M_PI), 3.0f))) / xi)))))))) * xi) + ((((1.0f - ux) * maxCos) * ux) * zi);
    	} else {
    		tmp = fmaf(cosf(t_0), xi, (sinf(t_0) * yi));
    	}
    	return tmp;
    }
    
    function code(xi, yi, zi, ux, uy, maxCos)
    	t_0 = Float32(Float32(pi) * Float32(Float32(2.0) * uy))
    	tmp = Float32(0.0)
    	if (uy <= Float32(0.014999999664723873))
    		tmp = Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(uy * fma(Float32(2.0), Float32(Float32(yi * Float32(pi)) / xi), Float32(uy * fma(Float32(-2.0), Float32(Float32(pi) * Float32(pi)), Float32(Float32(-1.3333333333333333) * Float32(Float32(uy * Float32(yi * (Float32(pi) ^ Float32(3.0)))) / xi)))))))) * xi) + Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi));
    	else
    		tmp = fma(cos(t_0), xi, Float32(sin(t_0) * yi));
    	end
    	return tmp
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_0 := \pi \cdot \left(2 \cdot uy\right)\\
    \mathbf{if}\;uy \leq 0.014999999664723873:\\
    \;\;\;\;\left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \pi}{xi}, uy \cdot \mathsf{fma}\left(-2, \pi \cdot \pi, -1.3333333333333333 \cdot \frac{uy \cdot \left(yi \cdot {\pi}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(\cos t\_0, xi, \sin t\_0 \cdot yi\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if uy < 0.0149999997

      1. Initial program 99.0%

        \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      2. Add Preprocessing
      3. Taylor expanded in xi around inf

        \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      4. Applied rewrites98.9%

        \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      5. Taylor expanded in ux around 0

        \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      6. Step-by-step derivation
        1. Applied rewrites98.7%

          \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        2. Taylor expanded in uy around 0

          \[\leadsto \left(1 \cdot \left(1 + uy \cdot \left(2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi} + uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        3. Step-by-step derivation
          1. lower-+.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \left(2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi} + uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. lower-*.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \left(2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi} + uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          3. lower-fma.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}, uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          4. lower-/.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}, uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          5. lower-*.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}, uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          6. lift-PI.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \pi}{xi}, uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          7. lower-*.f32N/A

            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \pi}{xi}, uy \cdot \left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{-4}{3} \cdot \frac{uy \cdot \left(yi \cdot {\mathsf{PI}\left(\right)}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        4. Applied rewrites97.8%

          \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(2, \frac{yi \cdot \pi}{xi}, uy \cdot \mathsf{fma}\left(-2, \pi \cdot \pi, -1.3333333333333333 \cdot \frac{uy \cdot \left(yi \cdot {\pi}^{3}\right)}{xi}\right)\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]

        if 0.0149999997 < uy

        1. Initial program 97.4%

          \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        2. Add Preprocessing
        3. Taylor expanded in ux around 0

          \[\leadsto \color{blue}{xi \cdot \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot xi + \color{blue}{yi} \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \]
          2. lower-fma.f32N/A

            \[\leadsto \mathsf{fma}\left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right), \color{blue}{xi}, yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
        5. Applied rewrites90.0%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right), xi, \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right)} \]
      7. Recombined 2 regimes into one program.
      8. Add Preprocessing

      Alternative 7: 92.1% accurate, 1.7× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_1 := t\_0 \cdot zi\\ t_2 := \sqrt{1 - t\_0 \cdot t\_0}\\ \mathbf{if}\;yi \leq 7.399999700872703 \cdot 10^{-26}:\\ \;\;\;\;\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot t\_2\right) \cdot xi + \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot yi\right) + t\_1\\ \mathbf{else}:\\ \;\;\;\;\left(\left(1 \cdot t\_2\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + t\_1\\ \end{array} \end{array} \]
      (FPCore (xi yi zi ux uy maxCos)
       :precision binary32
       (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux))
              (t_1 (* t_0 zi))
              (t_2 (sqrt (- 1.0 (* t_0 t_0)))))
         (if (<= yi 7.399999700872703e-26)
           (+
            (+ (* (* (cos (* (* uy 2.0) PI)) t_2) xi) (* (* 2.0 (* uy PI)) yi))
            t_1)
           (+ (+ (* (* 1.0 t_2) xi) (* (sin (* PI (* 2.0 uy))) yi)) t_1))))
      float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
      	float t_0 = ((1.0f - ux) * maxCos) * ux;
      	float t_1 = t_0 * zi;
      	float t_2 = sqrtf((1.0f - (t_0 * t_0)));
      	float tmp;
      	if (yi <= 7.399999700872703e-26f) {
      		tmp = (((cosf(((uy * 2.0f) * ((float) M_PI))) * t_2) * xi) + ((2.0f * (uy * ((float) M_PI))) * yi)) + t_1;
      	} else {
      		tmp = (((1.0f * t_2) * xi) + (sinf((((float) M_PI) * (2.0f * uy))) * yi)) + t_1;
      	}
      	return tmp;
      }
      
      function code(xi, yi, zi, ux, uy, maxCos)
      	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
      	t_1 = Float32(t_0 * zi)
      	t_2 = sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))
      	tmp = Float32(0.0)
      	if (yi <= Float32(7.399999700872703e-26))
      		tmp = Float32(Float32(Float32(Float32(cos(Float32(Float32(uy * Float32(2.0)) * Float32(pi))) * t_2) * xi) + Float32(Float32(Float32(2.0) * Float32(uy * Float32(pi))) * yi)) + t_1);
      	else
      		tmp = Float32(Float32(Float32(Float32(Float32(1.0) * t_2) * xi) + Float32(sin(Float32(Float32(pi) * Float32(Float32(2.0) * uy))) * yi)) + t_1);
      	end
      	return tmp
      end
      
      function tmp_2 = code(xi, yi, zi, ux, uy, maxCos)
      	t_0 = ((single(1.0) - ux) * maxCos) * ux;
      	t_1 = t_0 * zi;
      	t_2 = sqrt((single(1.0) - (t_0 * t_0)));
      	tmp = single(0.0);
      	if (yi <= single(7.399999700872703e-26))
      		tmp = (((cos(((uy * single(2.0)) * single(pi))) * t_2) * xi) + ((single(2.0) * (uy * single(pi))) * yi)) + t_1;
      	else
      		tmp = (((single(1.0) * t_2) * xi) + (sin((single(pi) * (single(2.0) * uy))) * yi)) + t_1;
      	end
      	tmp_2 = tmp;
      end
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
      t_1 := t\_0 \cdot zi\\
      t_2 := \sqrt{1 - t\_0 \cdot t\_0}\\
      \mathbf{if}\;yi \leq 7.399999700872703 \cdot 10^{-26}:\\
      \;\;\;\;\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot t\_2\right) \cdot xi + \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot yi\right) + t\_1\\
      
      \mathbf{else}:\\
      \;\;\;\;\left(\left(1 \cdot t\_2\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + t\_1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if yi < 7.3999997e-26

        1. Initial program 98.8%

          \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        2. Add Preprocessing
        3. Taylor expanded in ux around 0

          \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        4. Step-by-step derivation
          1. associate-*r*N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(2 \cdot uy\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. *-commutativeN/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          3. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          4. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          5. lift-PI.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          6. lift-sin.f3298.8

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          7. lift-PI.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          8. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          9. *-commutativeN/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          10. lower-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          11. lift-PI.f3298.8

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          12. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          13. *-commutativeN/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          14. lower-*.f3298.8

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        5. Applied rewrites98.8%

          \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        6. Taylor expanded in uy around 0

          \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(2 \cdot \color{blue}{\left(uy \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        7. Step-by-step derivation
          1. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. lift-PI.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          3. lift-*.f3292.8

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(2 \cdot \left(uy \cdot \color{blue}{\pi}\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        8. Applied rewrites92.8%

          \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(2 \cdot \color{blue}{\left(uy \cdot \pi\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]

        if 7.3999997e-26 < yi

        1. Initial program 98.6%

          \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        2. Add Preprocessing
        3. Taylor expanded in ux around 0

          \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        4. Step-by-step derivation
          1. associate-*r*N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(2 \cdot uy\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. *-commutativeN/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          3. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          4. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          5. lift-PI.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          6. lift-sin.f3298.6

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          7. lift-PI.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          8. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          9. *-commutativeN/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          10. lower-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          11. lift-PI.f3298.6

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          12. lift-*.f32N/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          13. *-commutativeN/A

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          14. lower-*.f3298.6

            \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        5. Applied rewrites98.6%

          \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        6. Taylor expanded in uy around 0

          \[\leadsto \left(\left(\color{blue}{1} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        7. Step-by-step derivation
          1. Applied rewrites94.2%

            \[\leadsto \left(\left(\color{blue}{1} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        8. Recombined 2 regimes into one program.
        9. Final simplification93.3%

          \[\leadsto \begin{array}{l} \mathbf{if}\;yi \leq 7.399999700872703 \cdot 10^{-26}:\\ \;\;\;\;\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \mathbf{else}:\\ \;\;\;\;\left(\left(1 \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \end{array} \]
        10. Add Preprocessing

        Alternative 8: 91.9% accurate, 1.8× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_0 := \pi \cdot \left(2 \cdot uy\right)\\ t_1 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_2 := t\_1 \cdot zi\\ \mathbf{if}\;yi \leq 7.399999700872703 \cdot 10^{-26}:\\ \;\;\;\;\left(1 \cdot \left(\cos t\_0 + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + t\_2\\ \mathbf{else}:\\ \;\;\;\;\left(\left(1 \cdot \sqrt{1 - t\_1 \cdot t\_1}\right) \cdot xi + \sin t\_0 \cdot yi\right) + t\_2\\ \end{array} \end{array} \]
        (FPCore (xi yi zi ux uy maxCos)
         :precision binary32
         (let* ((t_0 (* PI (* 2.0 uy)))
                (t_1 (* (* (- 1.0 ux) maxCos) ux))
                (t_2 (* t_1 zi)))
           (if (<= yi 7.399999700872703e-26)
             (+ (* (* 1.0 (+ (cos t_0) (* yi (/ (* 2.0 (* uy PI)) xi)))) xi) t_2)
             (+ (+ (* (* 1.0 (sqrt (- 1.0 (* t_1 t_1)))) xi) (* (sin t_0) yi)) t_2))))
        float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
        	float t_0 = ((float) M_PI) * (2.0f * uy);
        	float t_1 = ((1.0f - ux) * maxCos) * ux;
        	float t_2 = t_1 * zi;
        	float tmp;
        	if (yi <= 7.399999700872703e-26f) {
        		tmp = ((1.0f * (cosf(t_0) + (yi * ((2.0f * (uy * ((float) M_PI))) / xi)))) * xi) + t_2;
        	} else {
        		tmp = (((1.0f * sqrtf((1.0f - (t_1 * t_1)))) * xi) + (sinf(t_0) * yi)) + t_2;
        	}
        	return tmp;
        }
        
        function code(xi, yi, zi, ux, uy, maxCos)
        	t_0 = Float32(Float32(pi) * Float32(Float32(2.0) * uy))
        	t_1 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
        	t_2 = Float32(t_1 * zi)
        	tmp = Float32(0.0)
        	if (yi <= Float32(7.399999700872703e-26))
        		tmp = Float32(Float32(Float32(Float32(1.0) * Float32(cos(t_0) + Float32(yi * Float32(Float32(Float32(2.0) * Float32(uy * Float32(pi))) / xi)))) * xi) + t_2);
        	else
        		tmp = Float32(Float32(Float32(Float32(Float32(1.0) * sqrt(Float32(Float32(1.0) - Float32(t_1 * t_1)))) * xi) + Float32(sin(t_0) * yi)) + t_2);
        	end
        	return tmp
        end
        
        function tmp_2 = code(xi, yi, zi, ux, uy, maxCos)
        	t_0 = single(pi) * (single(2.0) * uy);
        	t_1 = ((single(1.0) - ux) * maxCos) * ux;
        	t_2 = t_1 * zi;
        	tmp = single(0.0);
        	if (yi <= single(7.399999700872703e-26))
        		tmp = ((single(1.0) * (cos(t_0) + (yi * ((single(2.0) * (uy * single(pi))) / xi)))) * xi) + t_2;
        	else
        		tmp = (((single(1.0) * sqrt((single(1.0) - (t_1 * t_1)))) * xi) + (sin(t_0) * yi)) + t_2;
        	end
        	tmp_2 = tmp;
        end
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_0 := \pi \cdot \left(2 \cdot uy\right)\\
        t_1 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
        t_2 := t\_1 \cdot zi\\
        \mathbf{if}\;yi \leq 7.399999700872703 \cdot 10^{-26}:\\
        \;\;\;\;\left(1 \cdot \left(\cos t\_0 + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + t\_2\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(\left(1 \cdot \sqrt{1 - t\_1 \cdot t\_1}\right) \cdot xi + \sin t\_0 \cdot yi\right) + t\_2\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if yi < 7.3999997e-26

          1. Initial program 98.8%

            \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. Add Preprocessing
          3. Taylor expanded in xi around inf

            \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          4. Applied rewrites98.7%

            \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          5. Taylor expanded in ux around 0

            \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          6. Step-by-step derivation
            1. Applied rewrites98.5%

              \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            2. Taylor expanded in uy around 0

              \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            3. Step-by-step derivation
              1. lift-*.f32N/A

                \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              2. lift-PI.f32N/A

                \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              3. lift-*.f3292.6

                \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            4. Applied rewrites92.6%

              \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]

            if 7.3999997e-26 < yi

            1. Initial program 98.6%

              \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            2. Add Preprocessing
            3. Taylor expanded in ux around 0

              \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            4. Step-by-step derivation
              1. associate-*r*N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(2 \cdot uy\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              2. *-commutativeN/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              3. lift-*.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              4. lift-*.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              5. lift-PI.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              6. lift-sin.f3298.6

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              7. lift-PI.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              8. lift-*.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\left(uy \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              9. *-commutativeN/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              10. lower-*.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\mathsf{PI}\left(\right) \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              11. lift-PI.f3298.6

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              12. lift-*.f32N/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(uy \cdot 2\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              13. *-commutativeN/A

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              14. lower-*.f3298.6

                \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            5. Applied rewrites98.6%

              \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \color{blue}{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)} \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            6. Taylor expanded in uy around 0

              \[\leadsto \left(\left(\color{blue}{1} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            7. Step-by-step derivation
              1. Applied rewrites94.2%

                \[\leadsto \left(\left(\color{blue}{1} \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            8. Recombined 2 regimes into one program.
            9. Final simplification93.1%

              \[\leadsto \begin{array}{l} \mathbf{if}\;yi \leq 7.399999700872703 \cdot 10^{-26}:\\ \;\;\;\;\left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \mathbf{else}:\\ \;\;\;\;\left(\left(1 \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \sin \left(\pi \cdot \left(2 \cdot uy\right)\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \end{array} \]
            10. Add Preprocessing

            Alternative 9: 92.2% accurate, 2.0× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} t_0 := \pi \cdot \left(2 \cdot uy\right)\\ t_1 := \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \mathbf{if}\;yi \leq 3.99999987306209 \cdot 10^{-20}:\\ \;\;\;\;\left(1 \cdot \left(\cos t\_0 + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + t\_1\\ \mathbf{else}:\\ \;\;\;\;\left(1 \cdot \left(1 + yi \cdot \frac{\sin t\_0}{xi}\right)\right) \cdot xi + t\_1\\ \end{array} \end{array} \]
            (FPCore (xi yi zi ux uy maxCos)
             :precision binary32
             (let* ((t_0 (* PI (* 2.0 uy))) (t_1 (* (* (* (- 1.0 ux) maxCos) ux) zi)))
               (if (<= yi 3.99999987306209e-20)
                 (+ (* (* 1.0 (+ (cos t_0) (* yi (/ (* 2.0 (* uy PI)) xi)))) xi) t_1)
                 (+ (* (* 1.0 (+ 1.0 (* yi (/ (sin t_0) xi)))) xi) t_1))))
            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
            	float t_0 = ((float) M_PI) * (2.0f * uy);
            	float t_1 = (((1.0f - ux) * maxCos) * ux) * zi;
            	float tmp;
            	if (yi <= 3.99999987306209e-20f) {
            		tmp = ((1.0f * (cosf(t_0) + (yi * ((2.0f * (uy * ((float) M_PI))) / xi)))) * xi) + t_1;
            	} else {
            		tmp = ((1.0f * (1.0f + (yi * (sinf(t_0) / xi)))) * xi) + t_1;
            	}
            	return tmp;
            }
            
            function code(xi, yi, zi, ux, uy, maxCos)
            	t_0 = Float32(Float32(pi) * Float32(Float32(2.0) * uy))
            	t_1 = Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi)
            	tmp = Float32(0.0)
            	if (yi <= Float32(3.99999987306209e-20))
            		tmp = Float32(Float32(Float32(Float32(1.0) * Float32(cos(t_0) + Float32(yi * Float32(Float32(Float32(2.0) * Float32(uy * Float32(pi))) / xi)))) * xi) + t_1);
            	else
            		tmp = Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(yi * Float32(sin(t_0) / xi)))) * xi) + t_1);
            	end
            	return tmp
            end
            
            function tmp_2 = code(xi, yi, zi, ux, uy, maxCos)
            	t_0 = single(pi) * (single(2.0) * uy);
            	t_1 = (((single(1.0) - ux) * maxCos) * ux) * zi;
            	tmp = single(0.0);
            	if (yi <= single(3.99999987306209e-20))
            		tmp = ((single(1.0) * (cos(t_0) + (yi * ((single(2.0) * (uy * single(pi))) / xi)))) * xi) + t_1;
            	else
            		tmp = ((single(1.0) * (single(1.0) + (yi * (sin(t_0) / xi)))) * xi) + t_1;
            	end
            	tmp_2 = tmp;
            end
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            t_0 := \pi \cdot \left(2 \cdot uy\right)\\
            t_1 := \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\
            \mathbf{if}\;yi \leq 3.99999987306209 \cdot 10^{-20}:\\
            \;\;\;\;\left(1 \cdot \left(\cos t\_0 + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + t\_1\\
            
            \mathbf{else}:\\
            \;\;\;\;\left(1 \cdot \left(1 + yi \cdot \frac{\sin t\_0}{xi}\right)\right) \cdot xi + t\_1\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if yi < 3.99999987e-20

              1. Initial program 98.7%

                \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              2. Add Preprocessing
              3. Taylor expanded in xi around inf

                \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              4. Applied rewrites98.6%

                \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              5. Taylor expanded in ux around 0

                \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              6. Step-by-step derivation
                1. Applied rewrites98.4%

                  \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                2. Taylor expanded in uy around 0

                  \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                3. Step-by-step derivation
                  1. lift-*.f32N/A

                    \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  2. lift-PI.f32N/A

                    \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  3. lift-*.f3292.2

                    \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                4. Applied rewrites92.2%

                  \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{2 \cdot \left(uy \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]

                if 3.99999987e-20 < yi

                1. Initial program 98.6%

                  \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                2. Add Preprocessing
                3. Taylor expanded in xi around inf

                  \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                4. Applied rewrites98.7%

                  \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                5. Taylor expanded in ux around 0

                  \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                6. Step-by-step derivation
                  1. Applied rewrites98.7%

                    \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  2. Taylor expanded in uy around 0

                    \[\leadsto \left(1 \cdot \left(1 + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  3. Step-by-step derivation
                    1. Applied rewrites95.6%

                      \[\leadsto \left(1 \cdot \left(1 + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  4. Recombined 2 regimes into one program.
                  5. Add Preprocessing

                  Alternative 10: 88.7% accurate, 2.2× speedup?

                  \[\begin{array}{l} \\ \left(1 \cdot \left(1 + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \end{array} \]
                  (FPCore (xi yi zi ux uy maxCos)
                   :precision binary32
                   (+
                    (* (* 1.0 (+ 1.0 (* yi (/ (sin (* PI (* 2.0 uy))) xi)))) xi)
                    (* (* (* (- 1.0 ux) maxCos) ux) zi)))
                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                  	return ((1.0f * (1.0f + (yi * (sinf((((float) M_PI) * (2.0f * uy))) / xi)))) * xi) + ((((1.0f - ux) * maxCos) * ux) * zi);
                  }
                  
                  function code(xi, yi, zi, ux, uy, maxCos)
                  	return Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(yi * Float32(sin(Float32(Float32(pi) * Float32(Float32(2.0) * uy))) / xi)))) * xi) + Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi))
                  end
                  
                  function tmp = code(xi, yi, zi, ux, uy, maxCos)
                  	tmp = ((single(1.0) * (single(1.0) + (yi * (sin((single(pi) * (single(2.0) * uy))) / xi)))) * xi) + ((((single(1.0) - ux) * maxCos) * ux) * zi);
                  end
                  
                  \begin{array}{l}
                  
                  \\
                  \left(1 \cdot \left(1 + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
                  \end{array}
                  
                  Derivation
                  1. Initial program 98.7%

                    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  2. Add Preprocessing
                  3. Taylor expanded in xi around inf

                    \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  4. Applied rewrites98.6%

                    \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  5. Taylor expanded in ux around 0

                    \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  6. Step-by-step derivation
                    1. Applied rewrites98.5%

                      \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                    2. Taylor expanded in uy around 0

                      \[\leadsto \left(1 \cdot \left(1 + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                    3. Step-by-step derivation
                      1. Applied rewrites89.0%

                        \[\leadsto \left(1 \cdot \left(1 + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      2. Add Preprocessing

                      Alternative 11: 85.8% accurate, 4.6× speedup?

                      \[\begin{array}{l} \\ \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \pi}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \end{array} \]
                      (FPCore (xi yi zi ux uy maxCos)
                       :precision binary32
                       (+
                        (*
                         (* 1.0 (+ 1.0 (* uy (fma -2.0 (* uy (* PI PI)) (* 2.0 (/ (* yi PI) xi))))))
                         xi)
                        (* (* (* (- 1.0 ux) maxCos) ux) zi)))
                      float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                      	return ((1.0f * (1.0f + (uy * fmaf(-2.0f, (uy * (((float) M_PI) * ((float) M_PI))), (2.0f * ((yi * ((float) M_PI)) / xi)))))) * xi) + ((((1.0f - ux) * maxCos) * ux) * zi);
                      }
                      
                      function code(xi, yi, zi, ux, uy, maxCos)
                      	return Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(uy * fma(Float32(-2.0), Float32(uy * Float32(Float32(pi) * Float32(pi))), Float32(Float32(2.0) * Float32(Float32(yi * Float32(pi)) / xi)))))) * xi) + Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi))
                      end
                      
                      \begin{array}{l}
                      
                      \\
                      \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \pi}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
                      \end{array}
                      
                      Derivation
                      1. Initial program 98.7%

                        \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      2. Add Preprocessing
                      3. Taylor expanded in xi around inf

                        \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      4. Applied rewrites98.6%

                        \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      5. Taylor expanded in ux around 0

                        \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      6. Step-by-step derivation
                        1. Applied rewrites98.5%

                          \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        2. Taylor expanded in uy around 0

                          \[\leadsto \left(1 \cdot \left(1 + uy \cdot \left(-2 \cdot \left(uy \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        3. Step-by-step derivation
                          1. lower-+.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \left(-2 \cdot \left(uy \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          2. lower-*.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \left(-2 \cdot \left(uy \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          3. lower-fma.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot {\mathsf{PI}\left(\right)}^{2}, 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          4. lower-*.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot {\mathsf{PI}\left(\right)}^{2}, 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          5. unpow2N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          6. lower-*.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          7. lift-PI.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \mathsf{PI}\left(\right)\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          8. lift-PI.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          9. lower-*.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          10. lower-/.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          11. lower-*.f32N/A

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \mathsf{PI}\left(\right)}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          12. lift-PI.f3284.7

                            \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \pi}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        4. Applied rewrites84.7%

                          \[\leadsto \left(1 \cdot \left(1 + uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(\pi \cdot \pi\right), 2 \cdot \frac{yi \cdot \pi}{xi}\right)\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        5. Add Preprocessing

                        Alternative 12: 82.3% accurate, 5.8× speedup?

                        \[\begin{array}{l} \\ \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot \left(ux \cdot \left(1 - ux\right)\right)\right) \cdot zi \end{array} \]
                        (FPCore (xi yi zi ux uy maxCos)
                         :precision binary32
                         (+
                          (* (* 1.0 (+ 1.0 (* 2.0 (/ (* uy (* yi PI)) xi)))) xi)
                          (* (* maxCos (* ux (- 1.0 ux))) zi)))
                        float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                        	return ((1.0f * (1.0f + (2.0f * ((uy * (yi * ((float) M_PI))) / xi)))) * xi) + ((maxCos * (ux * (1.0f - ux))) * zi);
                        }
                        
                        function code(xi, yi, zi, ux, uy, maxCos)
                        	return Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(Float32(2.0) * Float32(Float32(uy * Float32(yi * Float32(pi))) / xi)))) * xi) + Float32(Float32(maxCos * Float32(ux * Float32(Float32(1.0) - ux))) * zi))
                        end
                        
                        function tmp = code(xi, yi, zi, ux, uy, maxCos)
                        	tmp = ((single(1.0) * (single(1.0) + (single(2.0) * ((uy * (yi * single(pi))) / xi)))) * xi) + ((maxCos * (ux * (single(1.0) - ux))) * zi);
                        end
                        
                        \begin{array}{l}
                        
                        \\
                        \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot \left(ux \cdot \left(1 - ux\right)\right)\right) \cdot zi
                        \end{array}
                        
                        Derivation
                        1. Initial program 98.7%

                          \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        2. Add Preprocessing
                        3. Taylor expanded in xi around inf

                          \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        4. Applied rewrites98.6%

                          \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        5. Taylor expanded in ux around 0

                          \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        6. Step-by-step derivation
                          1. Applied rewrites98.5%

                            \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          2. Taylor expanded in uy around 0

                            \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          3. Step-by-step derivation
                            1. lower-+.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            2. lower-*.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            3. lower-/.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            4. lower-*.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            5. lower-*.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            6. lift-PI.f3282.0

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          4. Applied rewrites82.0%

                            \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          5. Taylor expanded in maxCos around 0

                            \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \color{blue}{\left(maxCos \cdot \left(ux \cdot \left(1 - ux\right)\right)\right)} \cdot zi \]
                          6. Step-by-step derivation
                            1. lower-*.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot \color{blue}{\left(ux \cdot \left(1 - ux\right)\right)}\right) \cdot zi \]
                            2. lower-*.f32N/A

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot \left(ux \cdot \color{blue}{\left(1 - ux\right)}\right)\right) \cdot zi \]
                            3. lift--.f3282.0

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot \left(ux \cdot \left(1 - \color{blue}{ux}\right)\right)\right) \cdot zi \]
                          7. Applied rewrites82.0%

                            \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \color{blue}{\left(maxCos \cdot \left(ux \cdot \left(1 - ux\right)\right)\right)} \cdot zi \]
                          8. Add Preprocessing

                          Alternative 13: 82.4% accurate, 5.8× speedup?

                          \[\begin{array}{l} \\ \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \end{array} \]
                          (FPCore (xi yi zi ux uy maxCos)
                           :precision binary32
                           (+
                            (* (* 1.0 (/ (+ xi (* 2.0 (* uy (* yi PI)))) xi)) xi)
                            (* (* (* (- 1.0 ux) maxCos) ux) zi)))
                          float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                          	return ((1.0f * ((xi + (2.0f * (uy * (yi * ((float) M_PI))))) / xi)) * xi) + ((((1.0f - ux) * maxCos) * ux) * zi);
                          }
                          
                          function code(xi, yi, zi, ux, uy, maxCos)
                          	return Float32(Float32(Float32(Float32(1.0) * Float32(Float32(xi + Float32(Float32(2.0) * Float32(uy * Float32(yi * Float32(pi))))) / xi)) * xi) + Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi))
                          end
                          
                          function tmp = code(xi, yi, zi, ux, uy, maxCos)
                          	tmp = ((single(1.0) * ((xi + (single(2.0) * (uy * (yi * single(pi))))) / xi)) * xi) + ((((single(1.0) - ux) * maxCos) * ux) * zi);
                          end
                          
                          \begin{array}{l}
                          
                          \\
                          \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
                          \end{array}
                          
                          Derivation
                          1. Initial program 98.7%

                            \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          2. Add Preprocessing
                          3. Taylor expanded in xi around inf

                            \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          4. Applied rewrites98.6%

                            \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          5. Taylor expanded in ux around 0

                            \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          6. Step-by-step derivation
                            1. Applied rewrites98.5%

                              \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            2. Taylor expanded in uy around 0

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            3. Step-by-step derivation
                              1. lower-+.f32N/A

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              2. lower-*.f32N/A

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              3. lower-/.f32N/A

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              4. lower-*.f32N/A

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              5. lower-*.f32N/A

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              6. lift-PI.f3282.0

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            4. Applied rewrites82.0%

                              \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            5. Taylor expanded in xi around 0

                              \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            6. Step-by-step derivation
                              1. lower-/.f32N/A

                                \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              2. lower-+.f32N/A

                                \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              3. lower-*.f32N/A

                                \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              4. lift-*.f32N/A

                                \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              5. lift-PI.f32N/A

                                \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              6. lift-*.f3282.0

                                \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            7. Applied rewrites82.0%

                              \[\leadsto \left(1 \cdot \frac{xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)}{xi}\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            8. Add Preprocessing

                            Alternative 14: 79.7% accurate, 6.7× speedup?

                            \[\begin{array}{l} \\ \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot ux\right) \cdot zi \end{array} \]
                            (FPCore (xi yi zi ux uy maxCos)
                             :precision binary32
                             (+
                              (* (* 1.0 (+ 1.0 (* 2.0 (/ (* uy (* yi PI)) xi)))) xi)
                              (* (* maxCos ux) zi)))
                            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                            	return ((1.0f * (1.0f + (2.0f * ((uy * (yi * ((float) M_PI))) / xi)))) * xi) + ((maxCos * ux) * zi);
                            }
                            
                            function code(xi, yi, zi, ux, uy, maxCos)
                            	return Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(Float32(2.0) * Float32(Float32(uy * Float32(yi * Float32(pi))) / xi)))) * xi) + Float32(Float32(maxCos * ux) * zi))
                            end
                            
                            function tmp = code(xi, yi, zi, ux, uy, maxCos)
                            	tmp = ((single(1.0) * (single(1.0) + (single(2.0) * ((uy * (yi * single(pi))) / xi)))) * xi) + ((maxCos * ux) * zi);
                            end
                            
                            \begin{array}{l}
                            
                            \\
                            \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(maxCos \cdot ux\right) \cdot zi
                            \end{array}
                            
                            Derivation
                            1. Initial program 98.7%

                              \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            2. Add Preprocessing
                            3. Taylor expanded in xi around inf

                              \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            4. Applied rewrites98.6%

                              \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            5. Taylor expanded in ux around 0

                              \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            6. Step-by-step derivation
                              1. Applied rewrites98.5%

                                \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              2. Taylor expanded in uy around 0

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              3. Step-by-step derivation
                                1. lower-+.f32N/A

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                2. lower-*.f32N/A

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                3. lower-/.f32N/A

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                4. lower-*.f32N/A

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                5. lower-*.f32N/A

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                6. lift-PI.f3282.0

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              4. Applied rewrites82.0%

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              5. Taylor expanded in ux around 0

                                \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\color{blue}{maxCos} \cdot ux\right) \cdot zi \]
                              6. Step-by-step derivation
                                1. Applied rewrites79.2%

                                  \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\color{blue}{maxCos} \cdot ux\right) \cdot zi \]
                                2. Add Preprocessing

                                Alternative 15: 79.7% accurate, 6.7× speedup?

                                \[\begin{array}{l} \\ \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + maxCos \cdot \left(ux \cdot zi\right) \end{array} \]
                                (FPCore (xi yi zi ux uy maxCos)
                                 :precision binary32
                                 (+
                                  (* (* 1.0 (+ 1.0 (* 2.0 (/ (* uy (* yi PI)) xi)))) xi)
                                  (* maxCos (* ux zi))))
                                float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                	return ((1.0f * (1.0f + (2.0f * ((uy * (yi * ((float) M_PI))) / xi)))) * xi) + (maxCos * (ux * zi));
                                }
                                
                                function code(xi, yi, zi, ux, uy, maxCos)
                                	return Float32(Float32(Float32(Float32(1.0) * Float32(Float32(1.0) + Float32(Float32(2.0) * Float32(Float32(uy * Float32(yi * Float32(pi))) / xi)))) * xi) + Float32(maxCos * Float32(ux * zi)))
                                end
                                
                                function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                	tmp = ((single(1.0) * (single(1.0) + (single(2.0) * ((uy * (yi * single(pi))) / xi)))) * xi) + (maxCos * (ux * zi));
                                end
                                
                                \begin{array}{l}
                                
                                \\
                                \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + maxCos \cdot \left(ux \cdot zi\right)
                                \end{array}
                                
                                Derivation
                                1. Initial program 98.7%

                                  \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                2. Add Preprocessing
                                3. Taylor expanded in xi around inf

                                  \[\leadsto \color{blue}{xi \cdot \left(\cos \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} + \frac{yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)}{xi} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                4. Applied rewrites98.6%

                                  \[\leadsto \color{blue}{\left(\sqrt{1 - {\left(\left(1 - ux\right) \cdot ux\right)}^{2} \cdot \left(maxCos \cdot maxCos\right)} \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                5. Taylor expanded in ux around 0

                                  \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                6. Step-by-step derivation
                                  1. Applied rewrites98.5%

                                    \[\leadsto \left(1 \cdot \left(\cos \left(\pi \cdot \left(2 \cdot uy\right)\right) + yi \cdot \frac{\sin \left(\pi \cdot \left(2 \cdot uy\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  2. Taylor expanded in uy around 0

                                    \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  3. Step-by-step derivation
                                    1. lower-+.f32N/A

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    2. lower-*.f32N/A

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    3. lower-/.f32N/A

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    4. lower-*.f32N/A

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    5. lower-*.f32N/A

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    6. lift-PI.f3282.0

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  4. Applied rewrites82.0%

                                    \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  5. Taylor expanded in ux around 0

                                    \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \color{blue}{maxCos \cdot \left(ux \cdot zi\right)} \]
                                  6. Step-by-step derivation
                                    1. lower-*.f32N/A

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + maxCos \cdot \color{blue}{\left(ux \cdot zi\right)} \]
                                    2. lower-*.f3279.2

                                      \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + maxCos \cdot \left(ux \cdot \color{blue}{zi}\right) \]
                                  7. Applied rewrites79.2%

                                    \[\leadsto \left(1 \cdot \left(1 + 2 \cdot \frac{uy \cdot \left(yi \cdot \pi\right)}{xi}\right)\right) \cdot xi + \color{blue}{maxCos \cdot \left(ux \cdot zi\right)} \]
                                  8. Add Preprocessing

                                  Alternative 16: 51.8% accurate, 7.7× speedup?

                                  \[\begin{array}{l} \\ xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, -0.5 \cdot \left(\left(maxCos \cdot maxCos\right) \cdot xi\right)\right)\right) \end{array} \]
                                  (FPCore (xi yi zi ux uy maxCos)
                                   :precision binary32
                                   (+
                                    xi
                                    (*
                                     ux
                                     (fma
                                      maxCos
                                      zi
                                      (* ux (fma -1.0 (* maxCos zi) (* -0.5 (* (* maxCos maxCos) xi))))))))
                                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                  	return xi + (ux * fmaf(maxCos, zi, (ux * fmaf(-1.0f, (maxCos * zi), (-0.5f * ((maxCos * maxCos) * xi))))));
                                  }
                                  
                                  function code(xi, yi, zi, ux, uy, maxCos)
                                  	return Float32(xi + Float32(ux * fma(maxCos, zi, Float32(ux * fma(Float32(-1.0), Float32(maxCos * zi), Float32(Float32(-0.5) * Float32(Float32(maxCos * maxCos) * xi)))))))
                                  end
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, -0.5 \cdot \left(\left(maxCos \cdot maxCos\right) \cdot xi\right)\right)\right)
                                  \end{array}
                                  
                                  Derivation
                                  1. Initial program 98.7%

                                    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in ux around 0

                                    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\left(maxCos + -1 \cdot \left(maxCos \cdot ux\right)\right)} \cdot ux\right) \cdot zi \]
                                  4. Step-by-step derivation
                                    1. +-commutativeN/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(-1 \cdot \left(maxCos \cdot ux\right) + \color{blue}{maxCos}\right) \cdot ux\right) \cdot zi \]
                                    2. associate-*r*N/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(-1 \cdot maxCos\right) \cdot ux + maxCos\right) \cdot ux\right) \cdot zi \]
                                    3. lower-fma.f32N/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-1 \cdot maxCos, \color{blue}{ux}, maxCos\right) \cdot ux\right) \cdot zi \]
                                    4. mul-1-negN/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(\mathsf{neg}\left(maxCos\right), ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                    5. lower-neg.f3298.7

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                  5. Applied rewrites98.7%

                                    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\mathsf{fma}\left(-maxCos, ux, maxCos\right)} \cdot ux\right) \cdot zi \]
                                  6. Taylor expanded in uy around 0

                                    \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}} \]
                                  7. Step-by-step derivation
                                    1. lower-fma.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, \color{blue}{ux \cdot \left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    2. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \color{blue}{\left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    3. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \color{blue}{\left(1 - ux\right)}\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    4. lift--.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - \color{blue}{ux}\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    5. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    6. lower-sqrt.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    7. lower--.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                  8. Applied rewrites50.1%

                                    \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - \left(maxCos \cdot maxCos\right) \cdot {\left(ux \cdot \left(1 - ux\right)\right)}^{2}}\right)} \]
                                  9. Taylor expanded in ux around 0

                                    \[\leadsto xi + \color{blue}{ux \cdot \left(maxCos \cdot zi + ux \cdot \left(-1 \cdot \left(maxCos \cdot zi\right) + \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right)} \]
                                  10. Step-by-step derivation
                                    1. lower-+.f32N/A

                                      \[\leadsto xi + ux \cdot \color{blue}{\left(maxCos \cdot zi + ux \cdot \left(-1 \cdot \left(maxCos \cdot zi\right) + \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right)} \]
                                    2. lower-*.f32N/A

                                      \[\leadsto xi + ux \cdot \left(maxCos \cdot zi + \color{blue}{ux \cdot \left(-1 \cdot \left(maxCos \cdot zi\right) + \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)}\right) \]
                                    3. lower-fma.f32N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \left(-1 \cdot \left(maxCos \cdot zi\right) + \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right) \]
                                    4. lower-*.f32N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \left(-1 \cdot \left(maxCos \cdot zi\right) + \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right) \]
                                    5. lower-fma.f32N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right) \]
                                    6. lower-*.f32N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right) \]
                                    7. lower-*.f32N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right) \]
                                    8. lower-*.f32N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, \frac{-1}{2} \cdot \left({maxCos}^{2} \cdot xi\right)\right)\right) \]
                                    9. pow2N/A

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, \frac{-1}{2} \cdot \left(\left(maxCos \cdot maxCos\right) \cdot xi\right)\right)\right) \]
                                    10. lift-*.f3250.0

                                      \[\leadsto xi + ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, -0.5 \cdot \left(\left(maxCos \cdot maxCos\right) \cdot xi\right)\right)\right) \]
                                  11. Applied rewrites50.0%

                                    \[\leadsto xi + \color{blue}{ux \cdot \mathsf{fma}\left(maxCos, zi, ux \cdot \mathsf{fma}\left(-1, maxCos \cdot zi, -0.5 \cdot \left(\left(maxCos \cdot maxCos\right) \cdot xi\right)\right)\right)} \]
                                  12. Add Preprocessing

                                  Alternative 17: 51.7% accurate, 16.0× speedup?

                                  \[\begin{array}{l} \\ xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) \end{array} \]
                                  (FPCore (xi yi zi ux uy maxCos)
                                   :precision binary32
                                   (+ xi (* maxCos (* ux (* zi (- 1.0 ux))))))
                                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                  	return xi + (maxCos * (ux * (zi * (1.0f - ux))));
                                  }
                                  
                                  module fmin_fmax_functions
                                      implicit none
                                      private
                                      public fmax
                                      public fmin
                                  
                                      interface fmax
                                          module procedure fmax88
                                          module procedure fmax44
                                          module procedure fmax84
                                          module procedure fmax48
                                      end interface
                                      interface fmin
                                          module procedure fmin88
                                          module procedure fmin44
                                          module procedure fmin84
                                          module procedure fmin48
                                      end interface
                                  contains
                                      real(8) function fmax88(x, y) result (res)
                                          real(8), intent (in) :: x
                                          real(8), intent (in) :: y
                                          res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                      end function
                                      real(4) function fmax44(x, y) result (res)
                                          real(4), intent (in) :: x
                                          real(4), intent (in) :: y
                                          res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                      end function
                                      real(8) function fmax84(x, y) result(res)
                                          real(8), intent (in) :: x
                                          real(4), intent (in) :: y
                                          res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                                      end function
                                      real(8) function fmax48(x, y) result(res)
                                          real(4), intent (in) :: x
                                          real(8), intent (in) :: y
                                          res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                                      end function
                                      real(8) function fmin88(x, y) result (res)
                                          real(8), intent (in) :: x
                                          real(8), intent (in) :: y
                                          res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                      end function
                                      real(4) function fmin44(x, y) result (res)
                                          real(4), intent (in) :: x
                                          real(4), intent (in) :: y
                                          res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                      end function
                                      real(8) function fmin84(x, y) result(res)
                                          real(8), intent (in) :: x
                                          real(4), intent (in) :: y
                                          res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                                      end function
                                      real(8) function fmin48(x, y) result(res)
                                          real(4), intent (in) :: x
                                          real(8), intent (in) :: y
                                          res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                                      end function
                                  end module
                                  
                                  real(4) function code(xi, yi, zi, ux, uy, maxcos)
                                  use fmin_fmax_functions
                                      real(4), intent (in) :: xi
                                      real(4), intent (in) :: yi
                                      real(4), intent (in) :: zi
                                      real(4), intent (in) :: ux
                                      real(4), intent (in) :: uy
                                      real(4), intent (in) :: maxcos
                                      code = xi + (maxcos * (ux * (zi * (1.0e0 - ux))))
                                  end function
                                  
                                  function code(xi, yi, zi, ux, uy, maxCos)
                                  	return Float32(xi + Float32(maxCos * Float32(ux * Float32(zi * Float32(Float32(1.0) - ux)))))
                                  end
                                  
                                  function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                  	tmp = xi + (maxCos * (ux * (zi * (single(1.0) - ux))));
                                  end
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)
                                  \end{array}
                                  
                                  Derivation
                                  1. Initial program 98.7%

                                    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in ux around 0

                                    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\left(maxCos + -1 \cdot \left(maxCos \cdot ux\right)\right)} \cdot ux\right) \cdot zi \]
                                  4. Step-by-step derivation
                                    1. +-commutativeN/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(-1 \cdot \left(maxCos \cdot ux\right) + \color{blue}{maxCos}\right) \cdot ux\right) \cdot zi \]
                                    2. associate-*r*N/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(-1 \cdot maxCos\right) \cdot ux + maxCos\right) \cdot ux\right) \cdot zi \]
                                    3. lower-fma.f32N/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-1 \cdot maxCos, \color{blue}{ux}, maxCos\right) \cdot ux\right) \cdot zi \]
                                    4. mul-1-negN/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(\mathsf{neg}\left(maxCos\right), ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                    5. lower-neg.f3298.7

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                  5. Applied rewrites98.7%

                                    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\mathsf{fma}\left(-maxCos, ux, maxCos\right)} \cdot ux\right) \cdot zi \]
                                  6. Taylor expanded in uy around 0

                                    \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}} \]
                                  7. Step-by-step derivation
                                    1. lower-fma.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, \color{blue}{ux \cdot \left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    2. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \color{blue}{\left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    3. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \color{blue}{\left(1 - ux\right)}\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    4. lift--.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - \color{blue}{ux}\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    5. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    6. lower-sqrt.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    7. lower--.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                  8. Applied rewrites50.1%

                                    \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - \left(maxCos \cdot maxCos\right) \cdot {\left(ux \cdot \left(1 - ux\right)\right)}^{2}}\right)} \]
                                  9. Taylor expanded in maxCos around 0

                                    \[\leadsto xi + \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                  10. Step-by-step derivation
                                    1. lower-+.f32N/A

                                      \[\leadsto xi + maxCos \cdot \color{blue}{\left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                    2. lower-*.f32N/A

                                      \[\leadsto xi + maxCos \cdot \left(ux \cdot \color{blue}{\left(zi \cdot \left(1 - ux\right)\right)}\right) \]
                                    3. lift-*.f32N/A

                                      \[\leadsto xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - \color{blue}{ux}\right)\right)\right) \]
                                    4. lift--.f32N/A

                                      \[\leadsto xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) \]
                                    5. lift-*.f3250.0

                                      \[\leadsto xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \color{blue}{\left(1 - ux\right)}\right)\right) \]
                                  11. Applied rewrites50.0%

                                    \[\leadsto xi + \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                  12. Add Preprocessing

                                  Alternative 18: 51.7% accurate, 17.7× speedup?

                                  \[\begin{array}{l} \\ \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi\right) \end{array} \]
                                  (FPCore (xi yi zi ux uy maxCos)
                                   :precision binary32
                                   (fma maxCos (* ux (* zi (- 1.0 ux))) xi))
                                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                  	return fmaf(maxCos, (ux * (zi * (1.0f - ux))), xi);
                                  }
                                  
                                  function code(xi, yi, zi, ux, uy, maxCos)
                                  	return fma(maxCos, Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))), xi)
                                  end
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi\right)
                                  \end{array}
                                  
                                  Derivation
                                  1. Initial program 98.7%

                                    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in ux around 0

                                    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\left(maxCos + -1 \cdot \left(maxCos \cdot ux\right)\right)} \cdot ux\right) \cdot zi \]
                                  4. Step-by-step derivation
                                    1. +-commutativeN/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(-1 \cdot \left(maxCos \cdot ux\right) + \color{blue}{maxCos}\right) \cdot ux\right) \cdot zi \]
                                    2. associate-*r*N/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(-1 \cdot maxCos\right) \cdot ux + maxCos\right) \cdot ux\right) \cdot zi \]
                                    3. lower-fma.f32N/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-1 \cdot maxCos, \color{blue}{ux}, maxCos\right) \cdot ux\right) \cdot zi \]
                                    4. mul-1-negN/A

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(\mathsf{neg}\left(maxCos\right), ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                    5. lower-neg.f3298.7

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                  5. Applied rewrites98.7%

                                    \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\mathsf{fma}\left(-maxCos, ux, maxCos\right)} \cdot ux\right) \cdot zi \]
                                  6. Taylor expanded in uy around 0

                                    \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}} \]
                                  7. Step-by-step derivation
                                    1. lower-fma.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, \color{blue}{ux \cdot \left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    2. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \color{blue}{\left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    3. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \color{blue}{\left(1 - ux\right)}\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    4. lift--.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - \color{blue}{ux}\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    5. lower-*.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    6. lower-sqrt.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    7. lower--.f32N/A

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                  8. Applied rewrites50.1%

                                    \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - \left(maxCos \cdot maxCos\right) \cdot {\left(ux \cdot \left(1 - ux\right)\right)}^{2}}\right)} \]
                                  9. Taylor expanded in ux around 0

                                    \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi\right) \]
                                  10. Step-by-step derivation
                                    1. Applied rewrites49.9%

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi\right) \]
                                    2. Add Preprocessing

                                    Alternative 19: 49.7% accurate, 25.2× speedup?

                                    \[\begin{array}{l} \\ xi + maxCos \cdot \left(ux \cdot zi\right) \end{array} \]
                                    (FPCore (xi yi zi ux uy maxCos)
                                     :precision binary32
                                     (+ xi (* maxCos (* ux zi))))
                                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                    	return xi + (maxCos * (ux * zi));
                                    }
                                    
                                    module fmin_fmax_functions
                                        implicit none
                                        private
                                        public fmax
                                        public fmin
                                    
                                        interface fmax
                                            module procedure fmax88
                                            module procedure fmax44
                                            module procedure fmax84
                                            module procedure fmax48
                                        end interface
                                        interface fmin
                                            module procedure fmin88
                                            module procedure fmin44
                                            module procedure fmin84
                                            module procedure fmin48
                                        end interface
                                    contains
                                        real(8) function fmax88(x, y) result (res)
                                            real(8), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                        end function
                                        real(4) function fmax44(x, y) result (res)
                                            real(4), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                        end function
                                        real(8) function fmax84(x, y) result(res)
                                            real(8), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                                        end function
                                        real(8) function fmax48(x, y) result(res)
                                            real(4), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                                        end function
                                        real(8) function fmin88(x, y) result (res)
                                            real(8), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                        end function
                                        real(4) function fmin44(x, y) result (res)
                                            real(4), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                        end function
                                        real(8) function fmin84(x, y) result(res)
                                            real(8), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                                        end function
                                        real(8) function fmin48(x, y) result(res)
                                            real(4), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                                        end function
                                    end module
                                    
                                    real(4) function code(xi, yi, zi, ux, uy, maxcos)
                                    use fmin_fmax_functions
                                        real(4), intent (in) :: xi
                                        real(4), intent (in) :: yi
                                        real(4), intent (in) :: zi
                                        real(4), intent (in) :: ux
                                        real(4), intent (in) :: uy
                                        real(4), intent (in) :: maxcos
                                        code = xi + (maxcos * (ux * zi))
                                    end function
                                    
                                    function code(xi, yi, zi, ux, uy, maxCos)
                                    	return Float32(xi + Float32(maxCos * Float32(ux * zi)))
                                    end
                                    
                                    function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                    	tmp = xi + (maxCos * (ux * zi));
                                    end
                                    
                                    \begin{array}{l}
                                    
                                    \\
                                    xi + maxCos \cdot \left(ux \cdot zi\right)
                                    \end{array}
                                    
                                    Derivation
                                    1. Initial program 98.7%

                                      \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    2. Add Preprocessing
                                    3. Taylor expanded in ux around 0

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\left(maxCos + -1 \cdot \left(maxCos \cdot ux\right)\right)} \cdot ux\right) \cdot zi \]
                                    4. Step-by-step derivation
                                      1. +-commutativeN/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(-1 \cdot \left(maxCos \cdot ux\right) + \color{blue}{maxCos}\right) \cdot ux\right) \cdot zi \]
                                      2. associate-*r*N/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(-1 \cdot maxCos\right) \cdot ux + maxCos\right) \cdot ux\right) \cdot zi \]
                                      3. lower-fma.f32N/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-1 \cdot maxCos, \color{blue}{ux}, maxCos\right) \cdot ux\right) \cdot zi \]
                                      4. mul-1-negN/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(\mathsf{neg}\left(maxCos\right), ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                      5. lower-neg.f3298.7

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                    5. Applied rewrites98.7%

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\mathsf{fma}\left(-maxCos, ux, maxCos\right)} \cdot ux\right) \cdot zi \]
                                    6. Taylor expanded in uy around 0

                                      \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}} \]
                                    7. Step-by-step derivation
                                      1. lower-fma.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, \color{blue}{ux \cdot \left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      2. lower-*.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \color{blue}{\left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      3. lower-*.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \color{blue}{\left(1 - ux\right)}\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      4. lift--.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - \color{blue}{ux}\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      5. lower-*.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      6. lower-sqrt.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      7. lower--.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    8. Applied rewrites50.1%

                                      \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - \left(maxCos \cdot maxCos\right) \cdot {\left(ux \cdot \left(1 - ux\right)\right)}^{2}}\right)} \]
                                    9. Taylor expanded in ux around 0

                                      \[\leadsto xi + \color{blue}{maxCos \cdot \left(ux \cdot zi\right)} \]
                                    10. Step-by-step derivation
                                      1. lower-+.f32N/A

                                        \[\leadsto xi + maxCos \cdot \color{blue}{\left(ux \cdot zi\right)} \]
                                      2. lower-*.f32N/A

                                        \[\leadsto xi + maxCos \cdot \left(ux \cdot \color{blue}{zi}\right) \]
                                      3. lower-*.f3247.8

                                        \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                    11. Applied rewrites47.8%

                                      \[\leadsto xi + \color{blue}{maxCos \cdot \left(ux \cdot zi\right)} \]
                                    12. Add Preprocessing

                                    Alternative 20: 45.6% accurate, 353.0× speedup?

                                    \[\begin{array}{l} \\ xi \end{array} \]
                                    (FPCore (xi yi zi ux uy maxCos) :precision binary32 xi)
                                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                    	return xi;
                                    }
                                    
                                    module fmin_fmax_functions
                                        implicit none
                                        private
                                        public fmax
                                        public fmin
                                    
                                        interface fmax
                                            module procedure fmax88
                                            module procedure fmax44
                                            module procedure fmax84
                                            module procedure fmax48
                                        end interface
                                        interface fmin
                                            module procedure fmin88
                                            module procedure fmin44
                                            module procedure fmin84
                                            module procedure fmin48
                                        end interface
                                    contains
                                        real(8) function fmax88(x, y) result (res)
                                            real(8), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                        end function
                                        real(4) function fmax44(x, y) result (res)
                                            real(4), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                                        end function
                                        real(8) function fmax84(x, y) result(res)
                                            real(8), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                                        end function
                                        real(8) function fmax48(x, y) result(res)
                                            real(4), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                                        end function
                                        real(8) function fmin88(x, y) result (res)
                                            real(8), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                        end function
                                        real(4) function fmin44(x, y) result (res)
                                            real(4), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                                        end function
                                        real(8) function fmin84(x, y) result(res)
                                            real(8), intent (in) :: x
                                            real(4), intent (in) :: y
                                            res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                                        end function
                                        real(8) function fmin48(x, y) result(res)
                                            real(4), intent (in) :: x
                                            real(8), intent (in) :: y
                                            res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                                        end function
                                    end module
                                    
                                    real(4) function code(xi, yi, zi, ux, uy, maxcos)
                                    use fmin_fmax_functions
                                        real(4), intent (in) :: xi
                                        real(4), intent (in) :: yi
                                        real(4), intent (in) :: zi
                                        real(4), intent (in) :: ux
                                        real(4), intent (in) :: uy
                                        real(4), intent (in) :: maxcos
                                        code = xi
                                    end function
                                    
                                    function code(xi, yi, zi, ux, uy, maxCos)
                                    	return xi
                                    end
                                    
                                    function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                    	tmp = xi;
                                    end
                                    
                                    \begin{array}{l}
                                    
                                    \\
                                    xi
                                    \end{array}
                                    
                                    Derivation
                                    1. Initial program 98.7%

                                      \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    2. Add Preprocessing
                                    3. Taylor expanded in ux around 0

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\left(maxCos + -1 \cdot \left(maxCos \cdot ux\right)\right)} \cdot ux\right) \cdot zi \]
                                    4. Step-by-step derivation
                                      1. +-commutativeN/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(-1 \cdot \left(maxCos \cdot ux\right) + \color{blue}{maxCos}\right) \cdot ux\right) \cdot zi \]
                                      2. associate-*r*N/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(-1 \cdot maxCos\right) \cdot ux + maxCos\right) \cdot ux\right) \cdot zi \]
                                      3. lower-fma.f32N/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-1 \cdot maxCos, \color{blue}{ux}, maxCos\right) \cdot ux\right) \cdot zi \]
                                      4. mul-1-negN/A

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(\mathsf{neg}\left(maxCos\right), ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                      5. lower-neg.f3298.7

                                        \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\mathsf{fma}\left(-maxCos, ux, maxCos\right) \cdot ux\right) \cdot zi \]
                                    5. Applied rewrites98.7%

                                      \[\leadsto \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\color{blue}{\mathsf{fma}\left(-maxCos, ux, maxCos\right)} \cdot ux\right) \cdot zi \]
                                    6. Taylor expanded in uy around 0

                                      \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}} \]
                                    7. Step-by-step derivation
                                      1. lower-fma.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, \color{blue}{ux \cdot \left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      2. lower-*.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \color{blue}{\left(zi \cdot \left(1 - ux\right)\right)}, xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      3. lower-*.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \color{blue}{\left(1 - ux\right)}\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      4. lift--.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - \color{blue}{ux}\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      5. lower-*.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      6. lower-sqrt.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      7. lower--.f32N/A

                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                    8. Applied rewrites50.1%

                                      \[\leadsto \color{blue}{\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - \left(maxCos \cdot maxCos\right) \cdot {\left(ux \cdot \left(1 - ux\right)\right)}^{2}}\right)} \]
                                    9. Taylor expanded in ux around 0

                                      \[\leadsto xi \]
                                    10. Step-by-step derivation
                                      1. Applied rewrites42.9%

                                        \[\leadsto xi \]
                                      2. Add Preprocessing

                                      Reproduce

                                      ?
                                      herbie shell --seed 2025085 
                                      (FPCore (xi yi zi ux uy maxCos)
                                        :name "UniformSampleCone 2"
                                        :precision binary32
                                        :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0)) (and (<= -10000.0 yi) (<= yi 10000.0))) (and (<= -10000.0 zi) (<= zi 10000.0))) (and (<= 2.328306437e-10 ux) (<= ux 1.0))) (and (<= 2.328306437e-10 uy) (<= uy 1.0))) (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                        (+ (+ (* (* (cos (* (* uy 2.0) PI)) (sqrt (- 1.0 (* (* (* (- 1.0 ux) maxCos) ux) (* (* (- 1.0 ux) maxCos) ux))))) xi) (* (* (sin (* (* uy 2.0) PI)) (sqrt (- 1.0 (* (* (* (- 1.0 ux) maxCos) ux) (* (* (- 1.0 ux) maxCos) ux))))) yi)) (* (* (* (- 1.0 ux) maxCos) ux) zi)))