UniformSampleCone 2

Percentage Accurate: 98.9% → 98.9%
Time: 13.5s
Alternatives: 18
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 \mathsf{PI}\left(\right)\\ \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))))
\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 \mathsf{PI}\left(\right)\\
\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 18 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: 98.9% 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 \mathsf{PI}\left(\right)\\ \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))))
\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 \mathsf{PI}\left(\right)\\
\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: 98.9% 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 \mathsf{PI}\left(\right)\\ \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))))
\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 \mathsf{PI}\left(\right)\\
\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}
Derivation
  1. Initial program 99.0%

    \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Add Preprocessing
  3. Add Preprocessing

Alternative 2: 98.7% accurate, 1.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot uy\\ \mathsf{fma}\left(\cos \left(-2 \cdot t\_0\right), xi, \mathsf{fma}\left(\sin \left(t\_0 \cdot 2\right), yi, \left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos\right)\right) \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (PI) uy)))
   (fma
    (cos (* -2.0 t_0))
    xi
    (fma (sin (* t_0 2.0)) yi (* (* (* (- 1.0 ux) zi) ux) maxCos)))))
\begin{array}{l}

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

    \[\left(\left(\cos \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 \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 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. +-commutativeN/A

      \[\leadsto \color{blue}{\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) + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
    2. associate-+l+N/A

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

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

      \[\leadsto \color{blue}{\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) + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right)} \]
    5. cos-neg-revN/A

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

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

      \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right) \]
    8. metadata-evalN/A

      \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right) \]
    9. lower-*.f32N/A

      \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right) \]
    10. *-commutativeN/A

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

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

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

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

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

Alternative 3: 95.7% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot uy\\ \mathsf{fma}\left(\cos \left(-2 \cdot t\_0\right), xi, \mathsf{fma}\left(\sin \left(t\_0 \cdot 2\right), yi, \left(zi \cdot ux\right) \cdot maxCos\right)\right) \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (PI) uy)))
   (fma
    (cos (* -2.0 t_0))
    xi
    (fma (sin (* t_0 2.0)) yi (* (* zi ux) maxCos)))))
\begin{array}{l}

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

    \[\left(\left(\cos \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 \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 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. +-commutativeN/A

      \[\leadsto \color{blue}{\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) + maxCos \cdot \left(ux \cdot zi\right)} \]
    2. associate-+l+N/A

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

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

      \[\leadsto \color{blue}{\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) + maxCos \cdot \left(ux \cdot zi\right)\right)} \]
    5. cos-neg-revN/A

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

      \[\leadsto \mathsf{fma}\left(\color{blue}{\cos \left(\mathsf{neg}\left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right)}, xi, yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) + maxCos \cdot \left(ux \cdot zi\right)\right) \]
    7. distribute-lft-neg-inN/A

      \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + maxCos \cdot \left(ux \cdot zi\right)\right) \]
    8. metadata-evalN/A

      \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + maxCos \cdot \left(ux \cdot zi\right)\right) \]
    9. lower-*.f32N/A

      \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + maxCos \cdot \left(ux \cdot zi\right)\right) \]
    10. *-commutativeN/A

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

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

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

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

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

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

Alternative 4: 96.9% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot uy\\ t_1 := \sin \left(t\_0 \cdot 2\right) \cdot yi\\ \mathbf{if}\;uy \leq 0.00559999980032444:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2 \cdot \left(uy \cdot uy\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right), xi, t\_1\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos \left(t\_0 \cdot -2\right), xi, t\_1\right)\\ \end{array} \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
 :precision binary32
 (let* ((t_0 (* (PI) uy)) (t_1 (* (sin (* t_0 2.0)) yi)))
   (if (<= uy 0.00559999980032444)
     (+
      (fma (fma (* -2.0 (* uy uy)) (* (PI) (PI)) 1.0) xi t_1)
      (* (* (* (- 1.0 ux) maxCos) ux) zi))
     (fma (cos (* t_0 -2.0)) xi t_1))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \mathsf{PI}\left(\right) \cdot uy\\
t_1 := \sin \left(t\_0 \cdot 2\right) \cdot yi\\
\mathbf{if}\;uy \leq 0.00559999980032444:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2 \cdot \left(uy \cdot uy\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right), xi, t\_1\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\cos \left(t\_0 \cdot -2\right), xi, t\_1\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if uy < 0.0055999998

    1. Initial program 99.3%

      \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      2. lower-fma.f32N/A

        \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      3. cos-neg-revN/A

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

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

        \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      6. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      7. lower-*.f32N/A

        \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      8. *-commutativeN/A

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

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

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

        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
      12. lower-*.f32N/A

        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
      13. lower-sin.f32N/A

        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
      14. *-commutativeN/A

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

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

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

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

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

      \[\leadsto \color{blue}{\mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\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 \mathsf{fma}\left(1 + -2 \cdot \left({uy}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\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 rewrites99.1%

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2 \cdot \left(uy \cdot uy\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]

      if 0.0055999998 < uy

      1. Initial program 98.1%

        \[\left(\left(\cos \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 \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 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--.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{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. metadata-evalN/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{1 \cdot 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 \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{1 \cdot 1 - \color{blue}{\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. difference-of-squaresN/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(1 + \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(1 - \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. lower-*.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(1 + \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(1 - \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. lower-+.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(1 + \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)} \cdot \left(1 - \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. lift-*.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \color{blue}{\left(\left(1 - ux\right) \cdot maxCos\right)} \cdot ux\right) \cdot \left(1 - \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. *-commutativeN/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \color{blue}{\left(maxCos \cdot \left(1 - ux\right)\right)} \cdot ux\right) \cdot \left(1 - \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(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \color{blue}{\left(maxCos \cdot \left(1 - ux\right)\right)} \cdot ux\right) \cdot \left(1 - \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--.f3298.1

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot \color{blue}{\left(1 - \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. lift-*.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot \left(1 - \color{blue}{\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. *-commutativeN/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot \left(1 - \color{blue}{\left(maxCos \cdot \left(1 - ux\right)\right)} \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        13. lower-*.f3298.1

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(1 + \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot \left(1 - \color{blue}{\left(maxCos \cdot \left(1 - ux\right)\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.1%

        \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(1 + \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\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 inf

        \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left({ux}^{2} \cdot \left(-1 \cdot maxCos + \left(\frac{1}{{ux}^{2}} + \frac{maxCos}{ux}\right)\right)\right)} \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      6. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(\left(-1 \cdot maxCos + \left(\frac{1}{{ux}^{2}} + \frac{maxCos}{ux}\right)\right) \cdot {ux}^{2}\right)} \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        2. lower-*.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(\left(-1 \cdot maxCos + \left(\frac{1}{{ux}^{2}} + \frac{maxCos}{ux}\right)\right) \cdot {ux}^{2}\right)} \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        3. associate-+r+N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\color{blue}{\left(\left(-1 \cdot maxCos + \frac{1}{{ux}^{2}}\right) + \frac{maxCos}{ux}\right)} \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        4. lower-+.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\color{blue}{\left(\left(-1 \cdot maxCos + \frac{1}{{ux}^{2}}\right) + \frac{maxCos}{ux}\right)} \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        5. lower-fma.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\color{blue}{\mathsf{fma}\left(-1, maxCos, \frac{1}{{ux}^{2}}\right)} + \frac{maxCos}{ux}\right) \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        6. lower-/.f32N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(-1, maxCos, \color{blue}{\frac{1}{{ux}^{2}}}\right) + \frac{maxCos}{ux}\right) \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        7. unpow2N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(-1, maxCos, \frac{1}{\color{blue}{ux \cdot ux}}\right) + \frac{maxCos}{ux}\right) \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\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(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(-1, maxCos, \frac{1}{\color{blue}{ux \cdot ux}}\right) + \frac{maxCos}{ux}\right) \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\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(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(-1, maxCos, \frac{1}{ux \cdot ux}\right) + \color{blue}{\frac{maxCos}{ux}}\right) \cdot {ux}^{2}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        10. unpow2N/A

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(-1, maxCos, \frac{1}{ux \cdot ux}\right) + \frac{maxCos}{ux}\right) \cdot \color{blue}{\left(ux \cdot ux\right)}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        11. lower-*.f3298.0

          \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(-1, maxCos, \frac{1}{ux \cdot ux}\right) + \frac{maxCos}{ux}\right) \cdot \color{blue}{\left(ux \cdot ux\right)}\right) \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      7. Applied rewrites98.0%

        \[\leadsto \left(\left(\cos \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 \mathsf{PI}\left(\right)\right) \cdot \sqrt{\color{blue}{\left(\left(\mathsf{fma}\left(-1, maxCos, \frac{1}{ux \cdot ux}\right) + \frac{maxCos}{ux}\right) \cdot \left(ux \cdot ux\right)\right)} \cdot \left(1 - \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      8. 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)} \]
      9. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \color{blue}{\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) \]
        2. lower-fma.f32N/A

          \[\leadsto \color{blue}{\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)} \]
        3. metadata-evalN/A

          \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{\left(\mathsf{neg}\left(-2\right)\right)} \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) \]
        4. distribute-lft-neg-inN/A

          \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\mathsf{neg}\left(-2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right)}, xi, yi \cdot \sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]
        5. cos-neg-revN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\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) \]
        6. lower-cos.f32N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\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) \]
        7. *-commutativeN/A

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

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

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

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

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

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

          \[\leadsto \mathsf{fma}\left(\cos \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot -2\right), xi, \color{blue}{\sin \left(2 \cdot \left(uy \cdot \mathsf{PI}\left(\right)\right)\right) \cdot yi}\right) \]
      10. Applied rewrites93.6%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\cos \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot -2\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\right) \cdot yi\right)} \]
    8. Recombined 2 regimes into one program.
    9. Final simplification97.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;uy \leq 0.00559999980032444:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2 \cdot \left(uy \cdot uy\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot -2\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\right) \cdot yi\right)\\ \end{array} \]
    10. Add Preprocessing

    Alternative 5: 92.9% accurate, 2.2× speedup?

    \[\begin{array}{l} \\ \mathsf{fma}\left(\mathsf{fma}\left(-2 \cdot \left(uy \cdot uy\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\right) \cdot yi\right) + \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
     (+
      (fma
       (fma (* -2.0 (* uy uy)) (* (PI) (PI)) 1.0)
       xi
       (* (sin (* (* (PI) uy) 2.0)) yi))
      (* (* (* (- 1.0 ux) maxCos) ux) zi)))
    \begin{array}{l}
    
    \\
    \mathsf{fma}\left(\mathsf{fma}\left(-2 \cdot \left(uy \cdot uy\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
    \end{array}
    
    Derivation
    1. Initial program 99.0%

      \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      2. lower-fma.f32N/A

        \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      3. cos-neg-revN/A

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

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

        \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      6. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      7. lower-*.f32N/A

        \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      8. *-commutativeN/A

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

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

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

        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
      12. lower-*.f32N/A

        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
      13. lower-sin.f32N/A

        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
      14. *-commutativeN/A

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

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

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

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

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

      \[\leadsto \color{blue}{\mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\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 \mathsf{fma}\left(1 + -2 \cdot \left({uy}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\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 rewrites92.5%

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

      Alternative 6: 89.6% accurate, 2.3× speedup?

      \[\begin{array}{l} \\ \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, \left(\left(\mathsf{PI}\left(\right) \cdot yi\right) \cdot uy\right) \cdot 2\right) + \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
       (+
        (fma (cos (* -2.0 (* (PI) uy))) xi (* (* (* (PI) yi) uy) 2.0))
        (* (* (* (- 1.0 ux) maxCos) ux) zi)))
      \begin{array}{l}
      
      \\
      \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, \left(\left(\mathsf{PI}\left(\right) \cdot yi\right) \cdot uy\right) \cdot 2\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
      \end{array}
      
      Derivation
      1. Initial program 99.0%

        \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      4. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        2. lower-fma.f32N/A

          \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        3. cos-neg-revN/A

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

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

          \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        6. metadata-evalN/A

          \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        7. lower-*.f32N/A

          \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        8. *-commutativeN/A

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

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

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

          \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
        12. lower-*.f32N/A

          \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
        13. lower-sin.f32N/A

          \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
        14. *-commutativeN/A

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

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

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

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

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\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 \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, 2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      7. Step-by-step derivation
        1. Applied rewrites89.1%

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

        Alternative 7: 88.0% accurate, 3.5× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\ \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\left(t\_0 \cdot \mathsf{PI}\left(\right)\right) \cdot uy, -1.3333333333333333, \frac{t\_0 \cdot xi}{yi} \cdot -2\right), uy, \mathsf{PI}\left(\right) \cdot 2\right), uy, \frac{xi}{yi}\right) \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \end{array} \end{array} \]
        (FPCore (xi yi zi ux uy maxCos)
         :precision binary32
         (let* ((t_0 (* (PI) (PI))))
           (+
            (*
             (fma
              (fma
               (fma (* (* t_0 (PI)) uy) -1.3333333333333333 (* (/ (* t_0 xi) yi) -2.0))
               uy
               (* (PI) 2.0))
              uy
              (/ xi yi))
             yi)
            (* (* (* (- 1.0 ux) maxCos) ux) zi))))
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_0 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\
        \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\left(t\_0 \cdot \mathsf{PI}\left(\right)\right) \cdot uy, -1.3333333333333333, \frac{t\_0 \cdot xi}{yi} \cdot -2\right), uy, \mathsf{PI}\left(\right) \cdot 2\right), uy, \frac{xi}{yi}\right) \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
        \end{array}
        \end{array}
        
        Derivation
        1. Initial program 99.0%

          \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. lower-fma.f32N/A

            \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          3. cos-neg-revN/A

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

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

            \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          6. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          7. lower-*.f32N/A

            \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          8. *-commutativeN/A

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

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

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

            \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
          12. lower-*.f32N/A

            \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
          13. lower-sin.f32N/A

            \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
          14. *-commutativeN/A

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

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

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

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

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

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

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

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

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

              \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left({\mathsf{PI}\left(\right)}^{3} \cdot uy, -1.3333333333333333, \frac{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot xi}{yi} \cdot -2\right), uy, \mathsf{PI}\left(\right) \cdot 2\right), uy, \frac{xi}{yi}\right) \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
            2. Step-by-step derivation
              1. Applied rewrites88.2%

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

              Alternative 8: 88.0% accurate, 3.5× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\ \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{PI}\left(\right), t\_0 \cdot \left(-1.3333333333333333 \cdot uy\right), \frac{t\_0 \cdot xi}{yi} \cdot -2\right), uy, \mathsf{PI}\left(\right) \cdot 2\right), uy, \frac{xi}{yi}\right) \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \end{array} \end{array} \]
              (FPCore (xi yi zi ux uy maxCos)
               :precision binary32
               (let* ((t_0 (* (PI) (PI))))
                 (+
                  (*
                   (fma
                    (fma
                     (fma (PI) (* t_0 (* -1.3333333333333333 uy)) (* (/ (* t_0 xi) yi) -2.0))
                     uy
                     (* (PI) 2.0))
                    uy
                    (/ xi yi))
                   yi)
                  (* (* (* (- 1.0 ux) maxCos) ux) zi))))
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              t_0 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\
              \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{PI}\left(\right), t\_0 \cdot \left(-1.3333333333333333 \cdot uy\right), \frac{t\_0 \cdot xi}{yi} \cdot -2\right), uy, \mathsf{PI}\left(\right) \cdot 2\right), uy, \frac{xi}{yi}\right) \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
              \end{array}
              \end{array}
              
              Derivation
              1. Initial program 99.0%

                \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
              4. Step-by-step derivation
                1. *-commutativeN/A

                  \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                2. lower-fma.f32N/A

                  \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                3. cos-neg-revN/A

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

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

                  \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                6. metadata-evalN/A

                  \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                7. lower-*.f32N/A

                  \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                8. *-commutativeN/A

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

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

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

                  \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                12. lower-*.f32N/A

                  \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                13. lower-sin.f32N/A

                  \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                14. *-commutativeN/A

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

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

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

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

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

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

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

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

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

                    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left({\mathsf{PI}\left(\right)}^{3} \cdot uy, -1.3333333333333333, \frac{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot xi}{yi} \cdot -2\right), uy, \mathsf{PI}\left(\right) \cdot 2\right), uy, \frac{xi}{yi}\right) \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  2. Step-by-step derivation
                    1. Applied rewrites88.2%

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

                    Alternative 9: 85.3% accurate, 6.5× speedup?

                    \[\begin{array}{l} \\ \mathsf{fma}\left(zi \cdot maxCos, \left(1 - ux\right) \cdot ux, \mathsf{fma}\left(-2 \cdot uy, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot xi\right) \cdot uy - yi \cdot \mathsf{PI}\left(\right), xi\right)\right) \end{array} \]
                    (FPCore (xi yi zi ux uy maxCos)
                     :precision binary32
                     (fma
                      (* zi maxCos)
                      (* (- 1.0 ux) ux)
                      (fma (* -2.0 uy) (- (* (* (* (PI) (PI)) xi) uy) (* yi (PI))) xi)))
                    \begin{array}{l}
                    
                    \\
                    \mathsf{fma}\left(zi \cdot maxCos, \left(1 - ux\right) \cdot ux, \mathsf{fma}\left(-2 \cdot uy, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot xi\right) \cdot uy - yi \cdot \mathsf{PI}\left(\right), xi\right)\right)
                    \end{array}
                    
                    Derivation
                    1. Initial program 99.0%

                      \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                    4. Step-by-step derivation
                      1. *-commutativeN/A

                        \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      2. lower-fma.f32N/A

                        \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      3. cos-neg-revN/A

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

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

                        \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      6. metadata-evalN/A

                        \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      7. lower-*.f32N/A

                        \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                      8. *-commutativeN/A

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

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

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

                        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                      12. lower-*.f32N/A

                        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                      13. lower-sin.f32N/A

                        \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                      14. *-commutativeN/A

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

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

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

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

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

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

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

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

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

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

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

                            \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi + \mathsf{fma}\left(-2 \cdot \left(\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot xi\right) \cdot uy - \mathsf{PI}\left(\right) \cdot yi\right), uy, xi\right)} \]
                        3. Applied rewrites84.8%

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

                        Alternative 10: 81.1% accurate, 8.8× speedup?

                        \[\begin{array}{l} \\ \mathsf{fma}\left(-2 \cdot \left(\left(-yi\right) \cdot \mathsf{PI}\left(\right)\right), uy, xi\right) + \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
                         (+ (fma (* -2.0 (* (- yi) (PI))) uy xi) (* (* (* (- 1.0 ux) maxCos) ux) zi)))
                        \begin{array}{l}
                        
                        \\
                        \mathsf{fma}\left(-2 \cdot \left(\left(-yi\right) \cdot \mathsf{PI}\left(\right)\right), uy, xi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
                        \end{array}
                        
                        Derivation
                        1. Initial program 99.0%

                          \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                        4. Step-by-step derivation
                          1. *-commutativeN/A

                            \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          2. lower-fma.f32N/A

                            \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          3. cos-neg-revN/A

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

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

                            \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          6. metadata-evalN/A

                            \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          7. lower-*.f32N/A

                            \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          8. *-commutativeN/A

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

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

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

                            \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                          12. lower-*.f32N/A

                            \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                          13. lower-sin.f32N/A

                            \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                          14. *-commutativeN/A

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

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

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

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

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

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

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

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

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

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

                              \[\leadsto \mathsf{fma}\left(-2 \cdot \left(-1 \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right), uy, xi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                            3. Step-by-step derivation
                              1. Applied rewrites80.9%

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

                              Alternative 11: 81.1% accurate, 9.3× speedup?

                              \[\begin{array}{l} \\ \mathsf{fma}\left(\left(\mathsf{PI}\left(\right) \cdot yi\right) \cdot uy, 2, xi\right) + \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
                               (+ (fma (* (* (PI) yi) uy) 2.0 xi) (* (* (* (- 1.0 ux) maxCos) ux) zi)))
                              \begin{array}{l}
                              
                              \\
                              \mathsf{fma}\left(\left(\mathsf{PI}\left(\right) \cdot yi\right) \cdot uy, 2, xi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
                              \end{array}
                              
                              Derivation
                              1. Initial program 99.0%

                                \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              4. Step-by-step derivation
                                1. *-commutativeN/A

                                  \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                2. lower-fma.f32N/A

                                  \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                3. cos-neg-revN/A

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

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

                                  \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                6. metadata-evalN/A

                                  \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                7. lower-*.f32N/A

                                  \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                8. *-commutativeN/A

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

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

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

                                  \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                                12. lower-*.f32N/A

                                  \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                                13. lower-sin.f32N/A

                                  \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                                14. *-commutativeN/A

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

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

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

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

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

                                \[\leadsto \color{blue}{\mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), xi, \sin \left(\left(\mathsf{PI}\left(\right) \cdot uy\right) \cdot 2\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(xi + \color{blue}{2 \cdot \left(uy \cdot \left(yi \cdot \mathsf{PI}\left(\right)\right)\right)}\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                              7. Step-by-step derivation
                                1. Applied rewrites80.9%

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

                                Alternative 12: 51.2% accurate, 9.3× speedup?

                                \[\begin{array}{l} \\ \frac{xi}{yi} \cdot yi + \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
                                 (+ (* (/ xi yi) yi) (* (* (* (- 1.0 ux) maxCos) ux) zi)))
                                float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                	return ((xi / yi) * yi) + ((((1.0f - ux) * 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 / yi) * yi) + ((((1.0e0 - ux) * maxcos) * ux) * zi)
                                end function
                                
                                function code(xi, yi, zi, ux, uy, maxCos)
                                	return Float32(Float32(Float32(xi / yi) * yi) + Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi))
                                end
                                
                                function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                	tmp = ((xi / yi) * yi) + ((((single(1.0) - ux) * maxCos) * ux) * zi);
                                end
                                
                                \begin{array}{l}
                                
                                \\
                                \frac{xi}{yi} \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
                                \end{array}
                                
                                Derivation
                                1. Initial program 99.0%

                                  \[\left(\left(\cos \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 \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 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}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                4. Step-by-step derivation
                                  1. *-commutativeN/A

                                    \[\leadsto \left(\color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  2. lower-fma.f32N/A

                                    \[\leadsto \color{blue}{\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)} + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  3. cos-neg-revN/A

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

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

                                    \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\left(\left(\mathsf{neg}\left(2\right)\right) \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  6. metadata-evalN/A

                                    \[\leadsto \mathsf{fma}\left(\cos \left(\color{blue}{-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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  7. lower-*.f32N/A

                                    \[\leadsto \mathsf{fma}\left(\cos \color{blue}{\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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  8. *-commutativeN/A

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

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

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

                                    \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                                  12. lower-*.f32N/A

                                    \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                                  13. lower-sin.f32N/A

                                    \[\leadsto \mathsf{fma}\left(\cos \left(-2 \cdot \left(\mathsf{PI}\left(\right) \cdot uy\right)\right), 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 \]
                                  14. *-commutativeN/A

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

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

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

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

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

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

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

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

                                    \[\leadsto \frac{xi}{yi} \cdot yi + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                  3. Step-by-step derivation
                                    1. Applied rewrites49.9%

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

                                    Alternative 13: 13.4% accurate, 10.7× speedup?

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

                                      \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                    2. Add Preprocessing
                                    3. Taylor expanded in zi around inf

                                      \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                    4. Step-by-step derivation
                                      1. *-commutativeN/A

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

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

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

                                        \[\leadsto \color{blue}{\left(\left(zi \cdot \left(1 - ux\right)\right) \cdot ux\right)} \cdot maxCos \]
                                      5. *-commutativeN/A

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

                                        \[\leadsto \left(\color{blue}{\left(\left(1 - ux\right) \cdot zi\right)} \cdot ux\right) \cdot maxCos \]
                                      7. lower--.f3213.9

                                        \[\leadsto \left(\left(\color{blue}{\left(1 - ux\right)} \cdot zi\right) \cdot ux\right) \cdot maxCos \]
                                    5. Applied rewrites13.9%

                                      \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos} \]
                                    6. Taylor expanded in ux around inf

                                      \[\leadsto \left(\left(ux \cdot \left(-1 \cdot zi + \frac{zi}{ux}\right)\right) \cdot ux\right) \cdot maxCos \]
                                    7. Step-by-step derivation
                                      1. Applied rewrites14.0%

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

                                      Alternative 14: 13.4% accurate, 18.6× speedup?

                                      \[\begin{array}{l} \\ \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot zi \end{array} \]
                                      (FPCore (xi yi zi ux uy maxCos)
                                       :precision binary32
                                       (* (* (* maxCos (- 1.0 ux)) ux) zi))
                                      float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                      	return ((maxCos * (1.0f - ux)) * 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 = ((maxcos * (1.0e0 - ux)) * ux) * zi
                                      end function
                                      
                                      function code(xi, yi, zi, ux, uy, maxCos)
                                      	return Float32(Float32(Float32(maxCos * Float32(Float32(1.0) - ux)) * ux) * zi)
                                      end
                                      
                                      function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                      	tmp = ((maxCos * (single(1.0) - ux)) * ux) * zi;
                                      end
                                      
                                      \begin{array}{l}
                                      
                                      \\
                                      \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot zi
                                      \end{array}
                                      
                                      Derivation
                                      1. Initial program 99.0%

                                        \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                      2. Add Preprocessing
                                      3. Taylor expanded in zi around inf

                                        \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                      4. Step-by-step derivation
                                        1. *-commutativeN/A

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

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

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

                                          \[\leadsto \color{blue}{\left(\left(zi \cdot \left(1 - ux\right)\right) \cdot ux\right)} \cdot maxCos \]
                                        5. *-commutativeN/A

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

                                          \[\leadsto \left(\color{blue}{\left(\left(1 - ux\right) \cdot zi\right)} \cdot ux\right) \cdot maxCos \]
                                        7. lower--.f3213.9

                                          \[\leadsto \left(\left(\color{blue}{\left(1 - ux\right)} \cdot zi\right) \cdot ux\right) \cdot maxCos \]
                                      5. Applied rewrites13.9%

                                        \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos} \]
                                      6. Step-by-step derivation
                                        1. Applied rewrites14.0%

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

                                        Alternative 15: 13.4% accurate, 18.6× speedup?

                                        \[\begin{array}{l} \\ \left(zi \cdot \left(maxCos \cdot \left(1 - ux\right)\right)\right) \cdot ux \end{array} \]
                                        (FPCore (xi yi zi ux uy maxCos)
                                         :precision binary32
                                         (* (* zi (* maxCos (- 1.0 ux))) ux))
                                        float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                        	return (zi * (maxCos * (1.0f - ux))) * 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 = (zi * (maxcos * (1.0e0 - ux))) * ux
                                        end function
                                        
                                        function code(xi, yi, zi, ux, uy, maxCos)
                                        	return Float32(Float32(zi * Float32(maxCos * Float32(Float32(1.0) - ux))) * ux)
                                        end
                                        
                                        function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                        	tmp = (zi * (maxCos * (single(1.0) - ux))) * ux;
                                        end
                                        
                                        \begin{array}{l}
                                        
                                        \\
                                        \left(zi \cdot \left(maxCos \cdot \left(1 - ux\right)\right)\right) \cdot ux
                                        \end{array}
                                        
                                        Derivation
                                        1. Initial program 99.0%

                                          \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                        2. Add Preprocessing
                                        3. Taylor expanded in zi around inf

                                          \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                        4. Step-by-step derivation
                                          1. *-commutativeN/A

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

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

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

                                            \[\leadsto \color{blue}{\left(\left(zi \cdot \left(1 - ux\right)\right) \cdot ux\right)} \cdot maxCos \]
                                          5. *-commutativeN/A

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

                                            \[\leadsto \left(\color{blue}{\left(\left(1 - ux\right) \cdot zi\right)} \cdot ux\right) \cdot maxCos \]
                                          7. lower--.f3213.9

                                            \[\leadsto \left(\left(\color{blue}{\left(1 - ux\right)} \cdot zi\right) \cdot ux\right) \cdot maxCos \]
                                        5. Applied rewrites13.9%

                                          \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos} \]
                                        6. Step-by-step derivation
                                          1. Applied rewrites14.0%

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

                                          Alternative 16: 12.0% accurate, 32.1× speedup?

                                          \[\begin{array}{l} \\ \left(zi \cdot ux\right) \cdot maxCos \end{array} \]
                                          (FPCore (xi yi zi ux uy maxCos) :precision binary32 (* (* zi ux) maxCos))
                                          float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                          	return (zi * ux) * maxCos;
                                          }
                                          
                                          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 = (zi * ux) * maxcos
                                          end function
                                          
                                          function code(xi, yi, zi, ux, uy, maxCos)
                                          	return Float32(Float32(zi * ux) * maxCos)
                                          end
                                          
                                          function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                          	tmp = (zi * ux) * maxCos;
                                          end
                                          
                                          \begin{array}{l}
                                          
                                          \\
                                          \left(zi \cdot ux\right) \cdot maxCos
                                          \end{array}
                                          
                                          Derivation
                                          1. Initial program 99.0%

                                            \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                          2. Add Preprocessing
                                          3. Taylor expanded in zi around inf

                                            \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                          4. Step-by-step derivation
                                            1. *-commutativeN/A

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

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

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

                                              \[\leadsto \color{blue}{\left(\left(zi \cdot \left(1 - ux\right)\right) \cdot ux\right)} \cdot maxCos \]
                                            5. *-commutativeN/A

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

                                              \[\leadsto \left(\color{blue}{\left(\left(1 - ux\right) \cdot zi\right)} \cdot ux\right) \cdot maxCos \]
                                            7. lower--.f3213.9

                                              \[\leadsto \left(\left(\color{blue}{\left(1 - ux\right)} \cdot zi\right) \cdot ux\right) \cdot maxCos \]
                                          5. Applied rewrites13.9%

                                            \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos} \]
                                          6. Taylor expanded in ux around 0

                                            \[\leadsto \left(ux \cdot zi\right) \cdot maxCos \]
                                          7. Step-by-step derivation
                                            1. Applied rewrites12.7%

                                              \[\leadsto \left(zi \cdot ux\right) \cdot maxCos \]
                                            2. Add Preprocessing

                                            Alternative 17: 12.0% accurate, 32.1× speedup?

                                            \[\begin{array}{l} \\ \left(zi \cdot maxCos\right) \cdot ux \end{array} \]
                                            (FPCore (xi yi zi ux uy maxCos) :precision binary32 (* (* zi maxCos) ux))
                                            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                            	return (zi * maxCos) * 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 = (zi * maxcos) * ux
                                            end function
                                            
                                            function code(xi, yi, zi, ux, uy, maxCos)
                                            	return Float32(Float32(zi * maxCos) * ux)
                                            end
                                            
                                            function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                            	tmp = (zi * maxCos) * ux;
                                            end
                                            
                                            \begin{array}{l}
                                            
                                            \\
                                            \left(zi \cdot maxCos\right) \cdot ux
                                            \end{array}
                                            
                                            Derivation
                                            1. Initial program 99.0%

                                              \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                            2. Add Preprocessing
                                            3. Taylor expanded in zi around inf

                                              \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                            4. Step-by-step derivation
                                              1. *-commutativeN/A

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

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

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

                                                \[\leadsto \color{blue}{\left(\left(zi \cdot \left(1 - ux\right)\right) \cdot ux\right)} \cdot maxCos \]
                                              5. *-commutativeN/A

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

                                                \[\leadsto \left(\color{blue}{\left(\left(1 - ux\right) \cdot zi\right)} \cdot ux\right) \cdot maxCos \]
                                              7. lower--.f3213.9

                                                \[\leadsto \left(\left(\color{blue}{\left(1 - ux\right)} \cdot zi\right) \cdot ux\right) \cdot maxCos \]
                                            5. Applied rewrites13.9%

                                              \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos} \]
                                            6. Taylor expanded in ux around 0

                                              \[\leadsto \left(ux \cdot zi\right) \cdot maxCos \]
                                            7. Step-by-step derivation
                                              1. Applied rewrites12.7%

                                                \[\leadsto \left(zi \cdot ux\right) \cdot maxCos \]
                                              2. Taylor expanded in ux around 0

                                                \[\leadsto maxCos \cdot \color{blue}{\left(ux \cdot zi\right)} \]
                                              3. Step-by-step derivation
                                                1. Applied rewrites12.7%

                                                  \[\leadsto \left(ux \cdot maxCos\right) \cdot \color{blue}{zi} \]
                                                2. Step-by-step derivation
                                                  1. Applied rewrites12.7%

                                                    \[\leadsto \left(zi \cdot maxCos\right) \cdot ux \]
                                                  2. Add Preprocessing

                                                  Alternative 18: 12.0% accurate, 32.1× speedup?

                                                  \[\begin{array}{l} \\ \left(ux \cdot maxCos\right) \cdot zi \end{array} \]
                                                  (FPCore (xi yi zi ux uy maxCos) :precision binary32 (* (* ux maxCos) zi))
                                                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                  	return (ux * maxCos) * 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 = (ux * maxcos) * zi
                                                  end function
                                                  
                                                  function code(xi, yi, zi, ux, uy, maxCos)
                                                  	return Float32(Float32(ux * maxCos) * zi)
                                                  end
                                                  
                                                  function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                                  	tmp = (ux * maxCos) * zi;
                                                  end
                                                  
                                                  \begin{array}{l}
                                                  
                                                  \\
                                                  \left(ux \cdot maxCos\right) \cdot zi
                                                  \end{array}
                                                  
                                                  Derivation
                                                  1. Initial program 99.0%

                                                    \[\left(\left(\cos \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 \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 yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                                  2. Add Preprocessing
                                                  3. Taylor expanded in zi around inf

                                                    \[\leadsto \color{blue}{maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)} \]
                                                  4. Step-by-step derivation
                                                    1. *-commutativeN/A

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

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

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

                                                      \[\leadsto \color{blue}{\left(\left(zi \cdot \left(1 - ux\right)\right) \cdot ux\right)} \cdot maxCos \]
                                                    5. *-commutativeN/A

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

                                                      \[\leadsto \left(\color{blue}{\left(\left(1 - ux\right) \cdot zi\right)} \cdot ux\right) \cdot maxCos \]
                                                    7. lower--.f3213.9

                                                      \[\leadsto \left(\left(\color{blue}{\left(1 - ux\right)} \cdot zi\right) \cdot ux\right) \cdot maxCos \]
                                                  5. Applied rewrites13.9%

                                                    \[\leadsto \color{blue}{\left(\left(\left(1 - ux\right) \cdot zi\right) \cdot ux\right) \cdot maxCos} \]
                                                  6. Taylor expanded in ux around 0

                                                    \[\leadsto \left(ux \cdot zi\right) \cdot maxCos \]
                                                  7. Step-by-step derivation
                                                    1. Applied rewrites12.7%

                                                      \[\leadsto \left(zi \cdot ux\right) \cdot maxCos \]
                                                    2. Taylor expanded in ux around 0

                                                      \[\leadsto maxCos \cdot \color{blue}{\left(ux \cdot zi\right)} \]
                                                    3. Step-by-step derivation
                                                      1. Applied rewrites12.7%

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

                                                      Reproduce

                                                      ?
                                                      herbie shell --seed 2025010 
                                                      (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)))