GTR1 distribution

Percentage Accurate: 98.5% → 98.5%
Time: 7.6s
Alternatives: 9
Speedup: 1.0×

Specification

?
\[\left(0 \leq cosTheta \land cosTheta \leq 1\right) \land \left(0.0001 \leq \alpha \land \alpha \leq 1\right)\]
\[\begin{array}{l} \\ \begin{array}{l} t_0 := \alpha \cdot \alpha - 1\\ \frac{t\_0}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(t\_0 \cdot cosTheta\right) \cdot cosTheta\right)} \end{array} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (let* ((t_0 (- (* alpha alpha) 1.0)))
   (/
    t_0
    (* (* (PI) (log (* alpha alpha))) (+ 1.0 (* (* t_0 cosTheta) cosTheta))))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \alpha \cdot \alpha - 1\\
\frac{t\_0}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(t\_0 \cdot cosTheta\right) \cdot cosTheta\right)}
\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 9 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.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \alpha \cdot \alpha - 1\\ \frac{t\_0}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(t\_0 \cdot cosTheta\right) \cdot cosTheta\right)} \end{array} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (let* ((t_0 (- (* alpha alpha) 1.0)))
   (/
    t_0
    (* (* (PI) (log (* alpha alpha))) (+ 1.0 (* (* t_0 cosTheta) cosTheta))))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \alpha \cdot \alpha - 1\\
\frac{t\_0}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(t\_0 \cdot cosTheta\right) \cdot cosTheta\right)}
\end{array}
\end{array}

Alternative 1: 98.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(\mathsf{fma}\left(cosTheta \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(2 \cdot \log \alpha\right)} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (/
  (fma alpha alpha -1.0)
  (*
   (* (fma (* cosTheta (fma alpha alpha -1.0)) cosTheta 1.0) (PI))
   (* 2.0 (log alpha)))))
\begin{array}{l}

\\
\frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(\mathsf{fma}\left(cosTheta \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(2 \cdot \log \alpha\right)}
\end{array}
Derivation
  1. Initial program 98.5%

    \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-+.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)}} \]
    2. +-commutativeN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta + 1\right)}} \]
    3. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(\color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta} + 1\right)} \]
    4. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(\color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right)} \cdot cosTheta + 1\right)} \]
    5. associate-*l*N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(\color{blue}{\left(\alpha \cdot \alpha - 1\right) \cdot \left(cosTheta \cdot cosTheta\right)} + 1\right)} \]
    6. lower-fma.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\mathsf{fma}\left(\alpha \cdot \alpha - 1, cosTheta \cdot cosTheta, 1\right)}} \]
    7. lift--.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\alpha \cdot \alpha - 1}, cosTheta \cdot cosTheta, 1\right)} \]
    8. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\alpha \cdot \alpha} - 1, cosTheta \cdot cosTheta, 1\right)} \]
    9. difference-of-sqr-1N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\left(\alpha + 1\right) \cdot \left(\alpha - 1\right)}, cosTheta \cdot cosTheta, 1\right)} \]
    10. difference-of-sqr--1-revN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\alpha \cdot \alpha + -1}, cosTheta \cdot cosTheta, 1\right)} \]
    11. lower-fma.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1\right)}, cosTheta \cdot cosTheta, 1\right)} \]
    12. lower-*.f3298.5

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), \color{blue}{cosTheta \cdot cosTheta}, 1\right)} \]
  4. Applied rewrites98.5%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)}} \]
  5. Taylor expanded in alpha around 0

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(2 \cdot \log \alpha\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  6. Step-by-step derivation
    1. *-commutativeN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha \cdot 2\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    2. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha \cdot 2\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    3. lower-log.f3298.4

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \left(\color{blue}{\log \alpha} \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  7. Applied rewrites98.4%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha \cdot 2\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  8. Step-by-step derivation
    1. lift--.f32N/A

      \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha - 1}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    2. lift-*.f32N/A

      \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha} - 1}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    3. difference-of-sqr-1N/A

      \[\leadsto \frac{\color{blue}{\left(\alpha + 1\right) \cdot \left(\alpha - 1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    4. difference-of-sqr--1N/A

      \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha + -1}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    5. lift-fma.f3298.6

      \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    6. lift-*.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)}} \]
    7. *-commutativeN/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)}} \]
    8. lift-fma.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(\mathsf{fma}\left(\alpha, \alpha, -1\right) \cdot \left(cosTheta \cdot cosTheta\right) + 1\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    9. +-commutativeN/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(1 + \mathsf{fma}\left(\alpha, \alpha, -1\right) \cdot \left(cosTheta \cdot cosTheta\right)\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    10. lift-fma.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\alpha \cdot \alpha + -1\right)} \cdot \left(cosTheta \cdot cosTheta\right)\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    11. difference-of-sqr--1N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\left(\alpha + 1\right) \cdot \left(\alpha - 1\right)\right)} \cdot \left(cosTheta \cdot cosTheta\right)\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    12. difference-of-sqr-1N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\alpha \cdot \alpha - 1\right)} \cdot \left(cosTheta \cdot cosTheta\right)\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    13. lift-*.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \left(\color{blue}{\alpha \cdot \alpha} - 1\right) \cdot \left(cosTheta \cdot cosTheta\right)\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    14. lift--.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\alpha \cdot \alpha - 1\right)} \cdot \left(cosTheta \cdot cosTheta\right)\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    15. lift-*.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \left(\alpha \cdot \alpha - 1\right) \cdot \color{blue}{\left(cosTheta \cdot cosTheta\right)}\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    16. associate-*r*N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta}\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    17. lift-*.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right)} \cdot cosTheta\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    18. lift-*.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta}\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    19. lift-+.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)} \]
    20. lift-*.f32N/A

      \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right)}} \]
  9. Applied rewrites98.6%

    \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(\mathsf{fma}\left(cosTheta \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(2 \cdot \log \alpha\right)}} \]
  10. Add Preprocessing

Alternative 2: 98.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (/
  (fma alpha alpha -1.0)
  (*
   (* (PI) (* (log alpha) 2.0))
   (fma (fma alpha alpha -1.0) (* cosTheta cosTheta) 1.0))))
\begin{array}{l}

\\
\frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)}
\end{array}
Derivation
  1. Initial program 98.5%

    \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-+.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)}} \]
    2. +-commutativeN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta + 1\right)}} \]
    3. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(\color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta} + 1\right)} \]
    4. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(\color{blue}{\left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right)} \cdot cosTheta + 1\right)} \]
    5. associate-*l*N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(\color{blue}{\left(\alpha \cdot \alpha - 1\right) \cdot \left(cosTheta \cdot cosTheta\right)} + 1\right)} \]
    6. lower-fma.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\mathsf{fma}\left(\alpha \cdot \alpha - 1, cosTheta \cdot cosTheta, 1\right)}} \]
    7. lift--.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\alpha \cdot \alpha - 1}, cosTheta \cdot cosTheta, 1\right)} \]
    8. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\alpha \cdot \alpha} - 1, cosTheta \cdot cosTheta, 1\right)} \]
    9. difference-of-sqr-1N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\left(\alpha + 1\right) \cdot \left(\alpha - 1\right)}, cosTheta \cdot cosTheta, 1\right)} \]
    10. difference-of-sqr--1-revN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\alpha \cdot \alpha + -1}, cosTheta \cdot cosTheta, 1\right)} \]
    11. lower-fma.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1\right)}, cosTheta \cdot cosTheta, 1\right)} \]
    12. lower-*.f3298.5

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), \color{blue}{cosTheta \cdot cosTheta}, 1\right)} \]
  4. Applied rewrites98.5%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)}} \]
  5. Taylor expanded in alpha around 0

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(2 \cdot \log \alpha\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  6. Step-by-step derivation
    1. *-commutativeN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha \cdot 2\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    2. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha \cdot 2\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    3. lower-log.f3298.4

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \left(\color{blue}{\log \alpha} \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  7. Applied rewrites98.4%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha \cdot 2\right)}\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  8. Step-by-step derivation
    1. lift--.f32N/A

      \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha - 1}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    2. lift-*.f32N/A

      \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha} - 1}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    3. difference-of-sqr-1N/A

      \[\leadsto \frac{\color{blue}{\left(\alpha + 1\right) \cdot \left(\alpha - 1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    4. difference-of-sqr--1N/A

      \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha + -1}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
    5. lift-fma.f3298.6

      \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  9. Applied rewrites98.6%

    \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot 2\right)\right) \cdot \mathsf{fma}\left(\mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta \cdot cosTheta, 1\right)} \]
  10. Add Preprocessing

Alternative 3: 97.4% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 - cosTheta \cdot cosTheta\right)} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (/
  (- (* alpha alpha) 1.0)
  (* (* (PI) (log (* alpha alpha))) (- 1.0 (* cosTheta cosTheta)))))
\begin{array}{l}

\\
\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 - cosTheta \cdot cosTheta\right)}
\end{array}
Derivation
  1. Initial program 98.5%

    \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  2. Add Preprocessing
  3. Taylor expanded in alpha around 0

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
  4. Step-by-step derivation
    1. fp-cancel-sign-sub-invN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(1 - \left(\mathsf{neg}\left(-1\right)\right) \cdot {cosTheta}^{2}\right)}} \]
    2. metadata-evalN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 - \color{blue}{1} \cdot {cosTheta}^{2}\right)} \]
    3. *-lft-identityN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 - \color{blue}{{cosTheta}^{2}}\right)} \]
    4. lower--.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(1 - {cosTheta}^{2}\right)}} \]
    5. unpow2N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 - \color{blue}{cosTheta \cdot cosTheta}\right)} \]
    6. lower-*.f3297.5

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 - \color{blue}{cosTheta \cdot cosTheta}\right)} \]
  5. Applied rewrites97.5%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \color{blue}{\left(1 - cosTheta \cdot cosTheta\right)}} \]
  6. Add Preprocessing

Alternative 4: 97.4% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - cosTheta \cdot cosTheta\right) \cdot \log \alpha\right)} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (/
  (- (* alpha alpha) 1.0)
  (* (* 2.0 (PI)) (* (- 1.0 (* cosTheta cosTheta)) (log alpha)))))
\begin{array}{l}

\\
\frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - cosTheta \cdot cosTheta\right) \cdot \log \alpha\right)}
\end{array}
Derivation
  1. Initial program 98.5%

    \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    2. lift-log.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\log \left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    3. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \color{blue}{\left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    4. log-prodN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha + \log \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    5. distribute-rgt-inN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\log \alpha \cdot \mathsf{PI}\left(\right) + \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    6. lift-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    7. add-cube-cbrtN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    8. associate-*r*N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\color{blue}{\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    9. lower-fma.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    10. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    11. lower-log.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha} \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    12. pow2N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    13. lower-pow.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    14. lift-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    15. lower-cbrt.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    16. lift-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    17. lower-cbrt.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \color{blue}{\sqrt[3]{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    18. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    19. lower-log.f3298.5

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha} \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  4. Applied rewrites98.5%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  5. Taylor expanded in alpha around 0

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{2 \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)\right)}} \]
  6. Step-by-step derivation
    1. associate-*r*N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)}} \]
    2. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)}} \]
    3. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)} \]
    4. lower-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)} \]
    5. *-commutativeN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha\right)}} \]
    6. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha\right)}} \]
    7. fp-cancel-sign-sub-invN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\color{blue}{\left(1 - \left(\mathsf{neg}\left(-1\right)\right) \cdot {cosTheta}^{2}\right)} \cdot \log \alpha\right)} \]
    8. metadata-evalN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - \color{blue}{1} \cdot {cosTheta}^{2}\right) \cdot \log \alpha\right)} \]
    9. *-lft-identityN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - \color{blue}{{cosTheta}^{2}}\right) \cdot \log \alpha\right)} \]
    10. lower--.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\color{blue}{\left(1 - {cosTheta}^{2}\right)} \cdot \log \alpha\right)} \]
    11. unpow2N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha\right)} \]
    12. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha\right)} \]
    13. lower-log.f3297.4

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - cosTheta \cdot cosTheta\right) \cdot \color{blue}{\log \alpha}\right)} \]
  7. Applied rewrites97.4%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(1 - cosTheta \cdot cosTheta\right) \cdot \log \alpha\right)}} \]
  8. Add Preprocessing

Alternative 5: 95.2% accurate, 1.2× speedup?

\[\begin{array}{l} \\ \frac{0.5 \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right)}{\log \alpha \cdot \mathsf{PI}\left(\right)} \end{array} \]
(FPCore (cosTheta alpha)
 :precision binary32
 (/ (* 0.5 (fma alpha alpha -1.0)) (* (log alpha) (PI))))
\begin{array}{l}

\\
\frac{0.5 \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right)}{\log \alpha \cdot \mathsf{PI}\left(\right)}
\end{array}
Derivation
  1. Initial program 98.5%

    \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    2. lift-log.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\log \left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    3. lift-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \color{blue}{\left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    4. log-prodN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha + \log \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    5. distribute-rgt-inN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\log \alpha \cdot \mathsf{PI}\left(\right) + \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    6. lift-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    7. add-cube-cbrtN/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    8. associate-*r*N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\color{blue}{\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    9. lower-fma.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    10. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    11. lower-log.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha} \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    12. pow2N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    13. lower-pow.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    14. lift-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    15. lower-cbrt.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    16. lift-PI.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    17. lower-cbrt.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \color{blue}{\sqrt[3]{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    18. lower-*.f32N/A

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    19. lower-log.f3298.5

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha} \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  4. Applied rewrites98.5%

    \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
  5. Taylor expanded in cosTheta around 0

    \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{{\alpha}^{2} - 1}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
  6. Step-by-step derivation
    1. associate-*r/N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \left({\alpha}^{2} - 1\right)}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
    2. *-commutativeN/A

      \[\leadsto \frac{\frac{1}{2} \cdot \left({\alpha}^{2} - 1\right)}{\color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}} \]
    3. times-fracN/A

      \[\leadsto \color{blue}{\frac{\frac{1}{2}}{\log \alpha} \cdot \frac{{\alpha}^{2} - 1}{\mathsf{PI}\left(\right)}} \]
    4. lower-*.f32N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{2}}{\log \alpha} \cdot \frac{{\alpha}^{2} - 1}{\mathsf{PI}\left(\right)}} \]
    5. lower-/.f32N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{2}}{\log \alpha}} \cdot \frac{{\alpha}^{2} - 1}{\mathsf{PI}\left(\right)} \]
    6. lower-log.f32N/A

      \[\leadsto \frac{\frac{1}{2}}{\color{blue}{\log \alpha}} \cdot \frac{{\alpha}^{2} - 1}{\mathsf{PI}\left(\right)} \]
    7. lower-/.f32N/A

      \[\leadsto \frac{\frac{1}{2}}{\log \alpha} \cdot \color{blue}{\frac{{\alpha}^{2} - 1}{\mathsf{PI}\left(\right)}} \]
    8. lower--.f32N/A

      \[\leadsto \frac{\frac{1}{2}}{\log \alpha} \cdot \frac{\color{blue}{{\alpha}^{2} - 1}}{\mathsf{PI}\left(\right)} \]
    9. unpow2N/A

      \[\leadsto \frac{\frac{1}{2}}{\log \alpha} \cdot \frac{\color{blue}{\alpha \cdot \alpha} - 1}{\mathsf{PI}\left(\right)} \]
    10. lower-*.f32N/A

      \[\leadsto \frac{\frac{1}{2}}{\log \alpha} \cdot \frac{\color{blue}{\alpha \cdot \alpha} - 1}{\mathsf{PI}\left(\right)} \]
    11. lower-PI.f3294.4

      \[\leadsto \frac{0.5}{\log \alpha} \cdot \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{PI}\left(\right)}} \]
  7. Applied rewrites94.4%

    \[\leadsto \color{blue}{\frac{0.5}{\log \alpha} \cdot \frac{\alpha \cdot \alpha - 1}{\mathsf{PI}\left(\right)}} \]
  8. Step-by-step derivation
    1. Applied rewrites95.0%

      \[\leadsto \frac{0.5 \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}} \]
    2. Add Preprocessing

    Alternative 6: 66.5% accurate, 1.2× speedup?

    \[\begin{array}{l} \\ \frac{\mathsf{fma}\left(-0.5 \cdot cosTheta, cosTheta, -0.5\right)}{\mathsf{PI}\left(\right) \cdot \log \alpha} \end{array} \]
    (FPCore (cosTheta alpha)
     :precision binary32
     (/ (fma (* -0.5 cosTheta) cosTheta -0.5) (* (PI) (log alpha))))
    \begin{array}{l}
    
    \\
    \frac{\mathsf{fma}\left(-0.5 \cdot cosTheta, cosTheta, -0.5\right)}{\mathsf{PI}\left(\right) \cdot \log \alpha}
    \end{array}
    
    Derivation
    1. Initial program 98.5%

      \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      2. lift-log.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\log \left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \color{blue}{\left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      4. log-prodN/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha + \log \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      5. distribute-rgt-inN/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\log \alpha \cdot \mathsf{PI}\left(\right) + \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      6. lift-PI.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      7. add-cube-cbrtN/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      8. associate-*r*N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\color{blue}{\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      9. lower-fma.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      10. lower-*.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      11. lower-log.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha} \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      12. pow2N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      13. lower-pow.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      14. lift-PI.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      15. lower-cbrt.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      16. lift-PI.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      17. lower-cbrt.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \color{blue}{\sqrt[3]{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      18. lower-*.f32N/A

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      19. lower-log.f3298.5

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha} \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    4. Applied rewrites98.5%

      \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
    5. Taylor expanded in alpha around 0

      \[\leadsto \color{blue}{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)}} \]
    6. Step-by-step derivation
      1. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
      2. lower-/.f32N/A

        \[\leadsto \color{blue}{\frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
      3. lower-/.f32N/A

        \[\leadsto \frac{\color{blue}{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)} \]
      4. lower-PI.f32N/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\color{blue}{\mathsf{PI}\left(\right)}}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)} \]
      5. *-commutativeN/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha}} \]
      6. lower-*.f32N/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha}} \]
      7. fp-cancel-sign-sub-invN/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 - \left(\mathsf{neg}\left(-1\right)\right) \cdot {cosTheta}^{2}\right)} \cdot \log \alpha} \]
      8. metadata-evalN/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{1} \cdot {cosTheta}^{2}\right) \cdot \log \alpha} \]
      9. *-lft-identityN/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{{cosTheta}^{2}}\right) \cdot \log \alpha} \]
      10. lower--.f32N/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 - {cosTheta}^{2}\right)} \cdot \log \alpha} \]
      11. unpow2N/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha} \]
      12. lower-*.f32N/A

        \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha} \]
      13. lower-log.f3268.0

        \[\leadsto \frac{\frac{-0.5}{\mathsf{PI}\left(\right)}}{\left(1 - cosTheta \cdot cosTheta\right) \cdot \color{blue}{\log \alpha}} \]
    7. Applied rewrites68.0%

      \[\leadsto \color{blue}{\frac{\frac{-0.5}{\mathsf{PI}\left(\right)}}{\left(1 - cosTheta \cdot cosTheta\right) \cdot \log \alpha}} \]
    8. Taylor expanded in cosTheta around 0

      \[\leadsto \frac{-1}{2} \cdot \frac{{cosTheta}^{2}}{\mathsf{PI}\left(\right) \cdot \log \alpha} - \color{blue}{\frac{1}{2} \cdot \frac{1}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
    9. Step-by-step derivation
      1. Applied rewrites67.4%

        \[\leadsto \frac{\mathsf{fma}\left(-0.5 \cdot cosTheta, cosTheta, -0.5\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
      2. Add Preprocessing

      Alternative 7: 65.8% accurate, 1.3× speedup?

      \[\begin{array}{l} \\ \frac{\frac{-0.5}{\log \alpha}}{\mathsf{PI}\left(\right)} \end{array} \]
      (FPCore (cosTheta alpha) :precision binary32 (/ (/ -0.5 (log alpha)) (PI)))
      \begin{array}{l}
      
      \\
      \frac{\frac{-0.5}{\log \alpha}}{\mathsf{PI}\left(\right)}
      \end{array}
      
      Derivation
      1. Initial program 98.5%

        \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        2. lift-log.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\log \left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \color{blue}{\left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        4. log-prodN/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha + \log \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        5. distribute-rgt-inN/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\log \alpha \cdot \mathsf{PI}\left(\right) + \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        6. lift-PI.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        7. add-cube-cbrtN/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        8. associate-*r*N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\color{blue}{\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        9. lower-fma.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        10. lower-*.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        11. lower-log.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha} \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        12. pow2N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        13. lower-pow.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        14. lift-PI.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        15. lower-cbrt.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        16. lift-PI.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        17. lower-cbrt.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \color{blue}{\sqrt[3]{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        18. lower-*.f32N/A

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
        19. lower-log.f3298.5

          \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha} \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      4. Applied rewrites98.5%

        \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
      5. Taylor expanded in alpha around 0

        \[\leadsto \color{blue}{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)}} \]
      6. Step-by-step derivation
        1. associate-/r*N/A

          \[\leadsto \color{blue}{\frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
        2. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
        3. lower-/.f32N/A

          \[\leadsto \frac{\color{blue}{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)} \]
        4. lower-PI.f32N/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\color{blue}{\mathsf{PI}\left(\right)}}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)} \]
        5. *-commutativeN/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha}} \]
        6. lower-*.f32N/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha}} \]
        7. fp-cancel-sign-sub-invN/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 - \left(\mathsf{neg}\left(-1\right)\right) \cdot {cosTheta}^{2}\right)} \cdot \log \alpha} \]
        8. metadata-evalN/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{1} \cdot {cosTheta}^{2}\right) \cdot \log \alpha} \]
        9. *-lft-identityN/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{{cosTheta}^{2}}\right) \cdot \log \alpha} \]
        10. lower--.f32N/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 - {cosTheta}^{2}\right)} \cdot \log \alpha} \]
        11. unpow2N/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha} \]
        12. lower-*.f32N/A

          \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha} \]
        13. lower-log.f3268.0

          \[\leadsto \frac{\frac{-0.5}{\mathsf{PI}\left(\right)}}{\left(1 - cosTheta \cdot cosTheta\right) \cdot \color{blue}{\log \alpha}} \]
      7. Applied rewrites68.0%

        \[\leadsto \color{blue}{\frac{\frac{-0.5}{\mathsf{PI}\left(\right)}}{\left(1 - cosTheta \cdot cosTheta\right) \cdot \log \alpha}} \]
      8. Taylor expanded in cosTheta around 0

        \[\leadsto \frac{\frac{-1}{2}}{\color{blue}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
      9. Step-by-step derivation
        1. Applied rewrites66.7%

          \[\leadsto \frac{-0.5}{\color{blue}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
        2. Step-by-step derivation
          1. Applied rewrites66.8%

            \[\leadsto \frac{\frac{-0.5}{\log \alpha}}{\mathsf{PI}\left(\right)} \]
          2. Add Preprocessing

          Alternative 8: 65.8% accurate, 1.3× speedup?

          \[\begin{array}{l} \\ \frac{-0.5}{\mathsf{PI}\left(\right) \cdot \log \alpha} \end{array} \]
          (FPCore (cosTheta alpha) :precision binary32 (/ -0.5 (* (PI) (log alpha))))
          \begin{array}{l}
          
          \\
          \frac{-0.5}{\mathsf{PI}\left(\right) \cdot \log \alpha}
          \end{array}
          
          Derivation
          1. Initial program 98.5%

            \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            2. lift-log.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\log \left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            3. lift-*.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \color{blue}{\left(\alpha \cdot \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            4. log-prodN/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\log \alpha + \log \alpha\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            5. distribute-rgt-inN/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\left(\log \alpha \cdot \mathsf{PI}\left(\right) + \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            6. lift-PI.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            7. add-cube-cbrtN/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\log \alpha \cdot \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            8. associate-*r*N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\left(\color{blue}{\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}} + \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            9. lower-fma.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            10. lower-*.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            11. lower-log.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\color{blue}{\log \alpha} \cdot \left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right), \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            12. pow2N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            13. lower-pow.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot \color{blue}{{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            14. lift-PI.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            15. lower-cbrt.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            16. lift-PI.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\color{blue}{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            17. lower-cbrt.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \color{blue}{\sqrt[3]{\mathsf{PI}\left(\right)}}, \log \alpha \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            18. lower-*.f32N/A

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha \cdot \mathsf{PI}\left(\right)}\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            19. lower-log.f3298.5

              \[\leadsto \frac{\alpha \cdot \alpha - 1}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \color{blue}{\log \alpha} \cdot \mathsf{PI}\left(\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
          4. Applied rewrites98.5%

            \[\leadsto \frac{\alpha \cdot \alpha - 1}{\color{blue}{\mathsf{fma}\left(\log \alpha \cdot {\left(\sqrt[3]{\mathsf{PI}\left(\right)}\right)}^{2}, \sqrt[3]{\mathsf{PI}\left(\right)}, \log \alpha \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
          5. Taylor expanded in alpha around 0

            \[\leadsto \color{blue}{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right) \cdot \left(\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)\right)}} \]
          6. Step-by-step derivation
            1. associate-/r*N/A

              \[\leadsto \color{blue}{\frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
            2. lower-/.f32N/A

              \[\leadsto \color{blue}{\frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)}} \]
            3. lower-/.f32N/A

              \[\leadsto \frac{\color{blue}{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)} \]
            4. lower-PI.f32N/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\color{blue}{\mathsf{PI}\left(\right)}}}{\log \alpha \cdot \left(1 + -1 \cdot {cosTheta}^{2}\right)} \]
            5. *-commutativeN/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha}} \]
            6. lower-*.f32N/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 + -1 \cdot {cosTheta}^{2}\right) \cdot \log \alpha}} \]
            7. fp-cancel-sign-sub-invN/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 - \left(\mathsf{neg}\left(-1\right)\right) \cdot {cosTheta}^{2}\right)} \cdot \log \alpha} \]
            8. metadata-evalN/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{1} \cdot {cosTheta}^{2}\right) \cdot \log \alpha} \]
            9. *-lft-identityN/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{{cosTheta}^{2}}\right) \cdot \log \alpha} \]
            10. lower--.f32N/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\color{blue}{\left(1 - {cosTheta}^{2}\right)} \cdot \log \alpha} \]
            11. unpow2N/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha} \]
            12. lower-*.f32N/A

              \[\leadsto \frac{\frac{\frac{-1}{2}}{\mathsf{PI}\left(\right)}}{\left(1 - \color{blue}{cosTheta \cdot cosTheta}\right) \cdot \log \alpha} \]
            13. lower-log.f3268.0

              \[\leadsto \frac{\frac{-0.5}{\mathsf{PI}\left(\right)}}{\left(1 - cosTheta \cdot cosTheta\right) \cdot \color{blue}{\log \alpha}} \]
          7. Applied rewrites68.0%

            \[\leadsto \color{blue}{\frac{\frac{-0.5}{\mathsf{PI}\left(\right)}}{\left(1 - cosTheta \cdot cosTheta\right) \cdot \log \alpha}} \]
          8. Taylor expanded in cosTheta around 0

            \[\leadsto \frac{\frac{-1}{2}}{\color{blue}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
          9. Step-by-step derivation
            1. Applied rewrites66.7%

              \[\leadsto \frac{-0.5}{\color{blue}{\mathsf{PI}\left(\right) \cdot \log \alpha}} \]
            2. Add Preprocessing

            Alternative 9: -0.0% accurate, 6.8× speedup?

            \[\begin{array}{l} \\ \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\mathsf{NAN}\left(\right) \cdot \mathsf{PI}\left(\right)} \end{array} \]
            (FPCore (cosTheta alpha)
             :precision binary32
             (/ (fma alpha alpha -1.0) (* (NAN) (PI))))
            \begin{array}{l}
            
            \\
            \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\mathsf{NAN}\left(\right) \cdot \mathsf{PI}\left(\right)}
            \end{array}
            
            Derivation
            1. Initial program 98.5%

              \[\frac{\alpha \cdot \alpha - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift--.f32N/A

                \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha - 1}}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
              2. lift-*.f32N/A

                \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha} - 1}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
              3. difference-of-sqr-1N/A

                \[\leadsto \frac{\color{blue}{\left(\alpha + 1\right) \cdot \left(\alpha - 1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
              4. difference-of-sqr--1-revN/A

                \[\leadsto \frac{\color{blue}{\alpha \cdot \alpha + -1}}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
              5. lower-fma.f3298.4

                \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1\right)}}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
              6. lift-*.f32N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)}} \]
              7. lift-*.f32N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)} \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)} \]
              8. associate-*l*N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \left(\log \left(\alpha \cdot \alpha\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)\right)}} \]
              9. *-commutativeN/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{\left(\left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right) \cdot \log \left(\alpha \cdot \alpha\right)\right)}} \]
              10. associate-*r*N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)\right) \cdot \log \left(\alpha \cdot \alpha\right)}} \]
              11. lower-*.f32N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \left(1 + \left(\left(\alpha \cdot \alpha - 1\right) \cdot cosTheta\right) \cdot cosTheta\right)\right) \cdot \log \left(\alpha \cdot \alpha\right)}} \]
            4. Applied rewrites-0.0%

              \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\left(\mathsf{PI}\left(\right) \cdot \mathsf{fma}\left(cosTheta \cdot \mathsf{fma}\left(\alpha, \alpha, -1\right), cosTheta, 1\right)\right) \cdot \frac{0}{0}}} \]
            5. Taylor expanded in cosTheta around 0

              \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\mathsf{NAN}\left(\right) \cdot \mathsf{PI}\left(\right)}} \]
            6. Step-by-step derivation
              1. lower-*.f32N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\mathsf{NAN}\left(\right) \cdot \mathsf{PI}\left(\right)}} \]
              2. lower-NAN.f32N/A

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\mathsf{NAN}\left(\right)} \cdot \mathsf{PI}\left(\right)} \]
              3. lower-PI.f32-0.0

                \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\mathsf{NAN}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}} \]
            7. Applied rewrites-0.0%

              \[\leadsto \frac{\mathsf{fma}\left(\alpha, \alpha, -1\right)}{\color{blue}{\mathsf{NAN}\left(\right) \cdot \mathsf{PI}\left(\right)}} \]
            8. Add Preprocessing

            Reproduce

            ?
            herbie shell --seed 2024352 
            (FPCore (cosTheta alpha)
              :name "GTR1 distribution"
              :precision binary32
              :pre (and (and (<= 0.0 cosTheta) (<= cosTheta 1.0)) (and (<= 0.0001 alpha) (<= alpha 1.0)))
              (/ (- (* alpha alpha) 1.0) (* (* (PI) (log (* alpha alpha))) (+ 1.0 (* (* (- (* alpha alpha) 1.0) cosTheta) cosTheta)))))