Beckmann Sample, near normal, slope_y

Percentage Accurate: 57.5% → 98.3%
Time: 9.7s
Alternatives: 10
Speedup: 8.9×

Specification

?
\[\left(\left(cosTheta\_i > 0.9999 \land cosTheta\_i \leq 1\right) \land \left(2.328306437 \cdot 10^{-10} \leq u1 \land u1 \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq u2 \land u2 \leq 1\right)\]
\[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log (- 1.0 u1)))) (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\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 10 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: 57.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log (- 1.0 u1)))) (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\end{array}

Alternative 1: 98.3% accurate, 0.7× speedup?

\[\begin{array}{l} \\ \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (+ (- (log1p (* (- u1) u1))) (log1p u1))) (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\end{array}
Derivation
  1. Initial program 63.1%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-neg.f32N/A

      \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    2. lift-log.f32N/A

      \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    3. neg-logN/A

      \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    4. lift--.f32N/A

      \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    5. flip--N/A

      \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    6. associate-/r/N/A

      \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    7. log-prodN/A

      \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    8. lower-+.f32N/A

      \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    9. log-recN/A

      \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    10. lower-neg.f32N/A

      \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    11. metadata-evalN/A

      \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    12. fp-cancel-sub-sign-invN/A

      \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    13. lower-log1p.f32N/A

      \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    14. lower-*.f32N/A

      \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    15. lower-neg.f32N/A

      \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    16. lower-log1p.f3298.4

      \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  4. Applied rewrites98.4%

    \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  5. Add Preprocessing

Alternative 2: 98.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log1p (- u1)))) (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\end{array}
Derivation
  1. Initial program 63.1%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-log.f32N/A

      \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    2. lift--.f32N/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    3. *-lft-identityN/A

      \[\leadsto \sqrt{-\log \left(1 - \color{blue}{1 \cdot u1}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    4. fp-cancel-sub-sign-invN/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(1\right)\right) \cdot u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    5. distribute-lft-neg-inN/A

      \[\leadsto \sqrt{-\log \left(1 + \color{blue}{\left(\mathsf{neg}\left(1 \cdot u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    6. *-lft-identityN/A

      \[\leadsto \sqrt{-\log \left(1 + \left(\mathsf{neg}\left(\color{blue}{u1}\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    7. lower-log1p.f32N/A

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    8. lower-neg.f3298.4

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  4. Applied rewrites98.4%

    \[\leadsto \color{blue}{\sqrt{-\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  5. Add Preprocessing

Alternative 3: 93.6% accurate, 1.6× speedup?

\[\begin{array}{l} \\ \sqrt{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.25, u1, 0.3333333333333333\right), u1, 0.5\right), u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (*
  (sqrt (* (fma (fma (fma 0.25 u1 0.3333333333333333) u1 0.5) u1 1.0) u1))
  (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.25, u1, 0.3333333333333333\right), u1, 0.5\right), u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\end{array}
Derivation
  1. Initial program 63.1%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  2. Add Preprocessing
  3. Taylor expanded in u1 around 0

    \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  4. Step-by-step derivation
    1. *-commutativeN/A

      \[\leadsto \sqrt{\color{blue}{\left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    2. lower-*.f32N/A

      \[\leadsto \sqrt{\color{blue}{\left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    3. +-commutativeN/A

      \[\leadsto \sqrt{\color{blue}{\left(u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right) + 1\right)} \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    4. *-commutativeN/A

      \[\leadsto \sqrt{\left(\color{blue}{\left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right) \cdot u1} + 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    5. lower-fma.f32N/A

      \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right), u1, 1\right)} \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    6. +-commutativeN/A

      \[\leadsto \sqrt{\mathsf{fma}\left(\color{blue}{u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right) + \frac{1}{2}}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    7. *-commutativeN/A

      \[\leadsto \sqrt{\mathsf{fma}\left(\color{blue}{\left(\frac{1}{3} + \frac{1}{4} \cdot u1\right) \cdot u1} + \frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    8. lower-fma.f32N/A

      \[\leadsto \sqrt{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{1}{3} + \frac{1}{4} \cdot u1, u1, \frac{1}{2}\right)}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    9. +-commutativeN/A

      \[\leadsto \sqrt{\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\frac{1}{4} \cdot u1 + \frac{1}{3}}, u1, \frac{1}{2}\right), u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    10. lower-fma.f3294.0

      \[\leadsto \sqrt{\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(0.25, u1, 0.3333333333333333\right)}, u1, 0.5\right), u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  5. Applied rewrites94.0%

    \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.25, u1, 0.3333333333333333\right), u1, 0.5\right), u1, 1\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  6. Add Preprocessing

Alternative 4: 91.9% accurate, 1.6× speedup?

\[\begin{array}{l} \\ \sqrt{\mathsf{fma}\left(\mathsf{fma}\left(0.3333333333333333, u1, 0.5\right), u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (*
  (sqrt (* (fma (fma 0.3333333333333333 u1 0.5) u1 1.0) u1))
  (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{\mathsf{fma}\left(\mathsf{fma}\left(0.3333333333333333, u1, 0.5\right), u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\end{array}
Derivation
  1. Initial program 63.1%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  2. Add Preprocessing
  3. Taylor expanded in u1 around 0

    \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + \frac{1}{3} \cdot u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  4. Step-by-step derivation
    1. *-commutativeN/A

      \[\leadsto \sqrt{\color{blue}{\left(1 + u1 \cdot \left(\frac{1}{2} + \frac{1}{3} \cdot u1\right)\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    2. lower-*.f32N/A

      \[\leadsto \sqrt{\color{blue}{\left(1 + u1 \cdot \left(\frac{1}{2} + \frac{1}{3} \cdot u1\right)\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    3. +-commutativeN/A

      \[\leadsto \sqrt{\color{blue}{\left(u1 \cdot \left(\frac{1}{2} + \frac{1}{3} \cdot u1\right) + 1\right)} \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    4. *-commutativeN/A

      \[\leadsto \sqrt{\left(\color{blue}{\left(\frac{1}{2} + \frac{1}{3} \cdot u1\right) \cdot u1} + 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    5. lower-fma.f32N/A

      \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(\frac{1}{2} + \frac{1}{3} \cdot u1, u1, 1\right)} \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    6. +-commutativeN/A

      \[\leadsto \sqrt{\mathsf{fma}\left(\color{blue}{\frac{1}{3} \cdot u1 + \frac{1}{2}}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    7. lower-fma.f3292.3

      \[\leadsto \sqrt{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(0.3333333333333333, u1, 0.5\right)}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  5. Applied rewrites92.3%

    \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(0.3333333333333333, u1, 0.5\right), u1, 1\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  6. Add Preprocessing

Alternative 5: 88.2% accurate, 1.7× speedup?

\[\begin{array}{l} \\ \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (* (fma 0.5 u1 1.0) u1)) (sin (* (* 2.0 (PI)) u2))))
\begin{array}{l}

\\
\sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)
\end{array}
Derivation
  1. Initial program 63.1%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  2. Add Preprocessing
  3. Taylor expanded in u1 around 0

    \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + \frac{1}{2} \cdot u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  4. Step-by-step derivation
    1. *-commutativeN/A

      \[\leadsto \sqrt{\color{blue}{\left(1 + \frac{1}{2} \cdot u1\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    2. lower-*.f32N/A

      \[\leadsto \sqrt{\color{blue}{\left(1 + \frac{1}{2} \cdot u1\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    3. +-commutativeN/A

      \[\leadsto \sqrt{\color{blue}{\left(\frac{1}{2} \cdot u1 + 1\right)} \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    4. lower-fma.f3288.8

      \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(0.5, u1, 1\right)} \cdot u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  5. Applied rewrites88.8%

    \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
  6. Add Preprocessing

Alternative 6: 85.6% accurate, 1.7× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u2 \leq 0.00139999995008111:\\ \;\;\;\;\mathsf{fma}\left(\left(2 \cdot \sqrt{u1}\right) \cdot u2, \mathsf{PI}\left(\right), \left(\left(\mathsf{PI}\left(\right) \cdot u2\right) \cdot \mathsf{fma}\left(0.5, \sqrt{\frac{1}{u1}}, 0.3333333333333333 \cdot \sqrt{u1}\right)\right) \cdot \left(u1 \cdot u1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)\\ \end{array} \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (if (<= u2 0.00139999995008111)
   (fma
    (* (* 2.0 (sqrt u1)) u2)
    (PI)
    (*
     (*
      (* (PI) u2)
      (fma 0.5 (sqrt (/ 1.0 u1)) (* 0.3333333333333333 (sqrt u1))))
     (* u1 u1)))
   (* (sqrt u1) (sin (* (* 2.0 (PI)) u2)))))
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;u2 \leq 0.00139999995008111:\\
\;\;\;\;\mathsf{fma}\left(\left(2 \cdot \sqrt{u1}\right) \cdot u2, \mathsf{PI}\left(\right), \left(\left(\mathsf{PI}\left(\right) \cdot u2\right) \cdot \mathsf{fma}\left(0.5, \sqrt{\frac{1}{u1}}, 0.3333333333333333 \cdot \sqrt{u1}\right)\right) \cdot \left(u1 \cdot u1\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{u1} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if u2 < 0.00139999995

    1. Initial program 64.2%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-neg.f32N/A

        \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      2. lift-log.f32N/A

        \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      3. neg-logN/A

        \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      4. lift--.f32N/A

        \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      5. flip--N/A

        \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      6. associate-/r/N/A

        \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      7. log-prodN/A

        \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      8. lower-+.f32N/A

        \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      9. log-recN/A

        \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      10. lower-neg.f32N/A

        \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      12. fp-cancel-sub-sign-invN/A

        \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      13. lower-log1p.f32N/A

        \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      14. lower-*.f32N/A

        \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      15. lower-neg.f32N/A

        \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      16. lower-log1p.f3298.6

        \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    4. Applied rewrites98.6%

      \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
    5. Taylor expanded in u2 around 0

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

        \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
      2. count-2-revN/A

        \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      3. distribute-lft-inN/A

        \[\leadsto \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      4. count-2-revN/A

        \[\leadsto \left(u2 \cdot \color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      5. lower-*.f32N/A

        \[\leadsto \color{blue}{\left(u2 \cdot \left(2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
      6. count-2-revN/A

        \[\leadsto \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      7. distribute-lft-inN/A

        \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      8. count-2-revN/A

        \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      9. *-commutativeN/A

        \[\leadsto \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot u2\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      10. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      11. lower-*.f32N/A

        \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      12. *-commutativeN/A

        \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      13. lower-*.f32N/A

        \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      14. lower-PI.f32N/A

        \[\leadsto \left(\left(\color{blue}{\mathsf{PI}\left(\right)} \cdot 2\right) \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      15. lower-sqrt.f32N/A

        \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \color{blue}{\sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
      16. lower--.f32N/A

        \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
      17. lower-log1p.f32N/A

        \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(u1\right)} - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
      18. mul-1-negN/A

        \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \log \left(1 + \color{blue}{\left(\mathsf{neg}\left({u1}^{2}\right)\right)}\right)} \]
    7. Applied rewrites96.8%

      \[\leadsto \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)}} \]
    8. Taylor expanded in u1 around 0

      \[\leadsto 2 \cdot \color{blue}{\left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
    9. Step-by-step derivation
      1. Applied rewrites74.3%

        \[\leadsto \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{u2} \]
      2. Taylor expanded in u1 around 0

        \[\leadsto 2 \cdot \left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) + \color{blue}{{u1}^{2} \cdot \left(\frac{1}{3} \cdot \left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) + \frac{1}{2} \cdot \left(\sqrt{\frac{1}{u1}} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
      3. Step-by-step derivation
        1. Applied rewrites90.5%

          \[\leadsto \mathsf{fma}\left(\left(2 \cdot \sqrt{u1}\right) \cdot u2, \color{blue}{\mathsf{PI}\left(\right)}, \left(\left(\mathsf{PI}\left(\right) \cdot u2\right) \cdot \mathsf{fma}\left(0.5, \sqrt{\frac{1}{u1}}, 0.3333333333333333 \cdot \sqrt{u1}\right)\right) \cdot \left(u1 \cdot u1\right)\right) \]

        if 0.00139999995 < u2

        1. Initial program 60.4%

          \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-neg.f32N/A

            \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          2. lift-log.f32N/A

            \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          3. neg-logN/A

            \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          4. lift--.f32N/A

            \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          5. flip--N/A

            \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          6. associate-/r/N/A

            \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          7. log-prodN/A

            \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          8. lower-+.f32N/A

            \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          9. log-recN/A

            \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          10. lower-neg.f32N/A

            \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          11. metadata-evalN/A

            \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          12. fp-cancel-sub-sign-invN/A

            \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          13. lower-log1p.f32N/A

            \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          14. lower-*.f32N/A

            \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          15. lower-neg.f32N/A

            \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          16. lower-log1p.f3298.1

            \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        4. Applied rewrites98.1%

          \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        5. Taylor expanded in u1 around 0

          \[\leadsto \color{blue}{\sqrt{u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        6. Step-by-step derivation
          1. lower-sqrt.f3276.0

            \[\leadsto \color{blue}{\sqrt{u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        7. Applied rewrites76.0%

          \[\leadsto \color{blue}{\sqrt{u1}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      4. Recombined 2 regimes into one program.
      5. Add Preprocessing

      Alternative 7: 76.3% accurate, 2.6× speedup?

      \[\begin{array}{l} \\ \mathsf{fma}\left(\left(2 \cdot \sqrt{u1}\right) \cdot u2, \mathsf{PI}\left(\right), \left(\left(\mathsf{PI}\left(\right) \cdot u2\right) \cdot \mathsf{fma}\left(0.5, \sqrt{\frac{1}{u1}}, 0.3333333333333333 \cdot \sqrt{u1}\right)\right) \cdot \left(u1 \cdot u1\right)\right) \end{array} \]
      (FPCore (cosTheta_i u1 u2)
       :precision binary32
       (fma
        (* (* 2.0 (sqrt u1)) u2)
        (PI)
        (*
         (* (* (PI) u2) (fma 0.5 (sqrt (/ 1.0 u1)) (* 0.3333333333333333 (sqrt u1))))
         (* u1 u1))))
      \begin{array}{l}
      
      \\
      \mathsf{fma}\left(\left(2 \cdot \sqrt{u1}\right) \cdot u2, \mathsf{PI}\left(\right), \left(\left(\mathsf{PI}\left(\right) \cdot u2\right) \cdot \mathsf{fma}\left(0.5, \sqrt{\frac{1}{u1}}, 0.3333333333333333 \cdot \sqrt{u1}\right)\right) \cdot \left(u1 \cdot u1\right)\right)
      \end{array}
      
      Derivation
      1. Initial program 63.1%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-neg.f32N/A

          \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        2. lift-log.f32N/A

          \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        3. neg-logN/A

          \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        4. lift--.f32N/A

          \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        5. flip--N/A

          \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        6. associate-/r/N/A

          \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        7. log-prodN/A

          \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        8. lower-+.f32N/A

          \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        9. log-recN/A

          \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        10. lower-neg.f32N/A

          \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        11. metadata-evalN/A

          \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        12. fp-cancel-sub-sign-invN/A

          \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        13. lower-log1p.f32N/A

          \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        14. lower-*.f32N/A

          \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        15. lower-neg.f32N/A

          \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
        16. lower-log1p.f3298.4

          \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      4. Applied rewrites98.4%

        \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      5. Taylor expanded in u2 around 0

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

          \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
        2. count-2-revN/A

          \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        3. distribute-lft-inN/A

          \[\leadsto \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        4. count-2-revN/A

          \[\leadsto \left(u2 \cdot \color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        5. lower-*.f32N/A

          \[\leadsto \color{blue}{\left(u2 \cdot \left(2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
        6. count-2-revN/A

          \[\leadsto \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        7. distribute-lft-inN/A

          \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        8. count-2-revN/A

          \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        9. *-commutativeN/A

          \[\leadsto \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot u2\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        10. associate-*r*N/A

          \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        11. lower-*.f32N/A

          \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        12. *-commutativeN/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        13. lower-*.f32N/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        14. lower-PI.f32N/A

          \[\leadsto \left(\left(\color{blue}{\mathsf{PI}\left(\right)} \cdot 2\right) \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        15. lower-sqrt.f32N/A

          \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \color{blue}{\sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
        16. lower--.f32N/A

          \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
        17. lower-log1p.f32N/A

          \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(u1\right)} - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
        18. mul-1-negN/A

          \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \log \left(1 + \color{blue}{\left(\mathsf{neg}\left({u1}^{2}\right)\right)}\right)} \]
      7. Applied rewrites82.0%

        \[\leadsto \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)}} \]
      8. Taylor expanded in u1 around 0

        \[\leadsto 2 \cdot \color{blue}{\left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
      9. Step-by-step derivation
        1. Applied rewrites65.7%

          \[\leadsto \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{u2} \]
        2. Taylor expanded in u1 around 0

          \[\leadsto 2 \cdot \left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) + \color{blue}{{u1}^{2} \cdot \left(\frac{1}{3} \cdot \left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) + \frac{1}{2} \cdot \left(\sqrt{\frac{1}{u1}} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
        3. Step-by-step derivation
          1. Applied rewrites77.4%

            \[\leadsto \mathsf{fma}\left(\left(2 \cdot \sqrt{u1}\right) \cdot u2, \color{blue}{\mathsf{PI}\left(\right)}, \left(\left(\mathsf{PI}\left(\right) \cdot u2\right) \cdot \mathsf{fma}\left(0.5, \sqrt{\frac{1}{u1}}, 0.3333333333333333 \cdot \sqrt{u1}\right)\right) \cdot \left(u1 \cdot u1\right)\right) \]
          2. Add Preprocessing

          Alternative 8: 66.7% accurate, 8.9× speedup?

          \[\begin{array}{l} \\ \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2 \end{array} \]
          (FPCore (cosTheta_i u1 u2)
           :precision binary32
           (* (* (* 2.0 (sqrt u1)) (PI)) u2))
          \begin{array}{l}
          
          \\
          \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2
          \end{array}
          
          Derivation
          1. Initial program 63.1%

            \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-neg.f32N/A

              \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            2. lift-log.f32N/A

              \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            3. neg-logN/A

              \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            4. lift--.f32N/A

              \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            5. flip--N/A

              \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            6. associate-/r/N/A

              \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            7. log-prodN/A

              \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            8. lower-+.f32N/A

              \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            9. log-recN/A

              \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            10. lower-neg.f32N/A

              \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            11. metadata-evalN/A

              \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            12. fp-cancel-sub-sign-invN/A

              \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            13. lower-log1p.f32N/A

              \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            14. lower-*.f32N/A

              \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            15. lower-neg.f32N/A

              \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            16. lower-log1p.f3298.4

              \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          4. Applied rewrites98.4%

            \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
          5. Taylor expanded in u2 around 0

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

              \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
            2. count-2-revN/A

              \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            3. distribute-lft-inN/A

              \[\leadsto \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            4. count-2-revN/A

              \[\leadsto \left(u2 \cdot \color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            5. lower-*.f32N/A

              \[\leadsto \color{blue}{\left(u2 \cdot \left(2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
            6. count-2-revN/A

              \[\leadsto \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            7. distribute-lft-inN/A

              \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            8. count-2-revN/A

              \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            9. *-commutativeN/A

              \[\leadsto \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot u2\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            10. associate-*r*N/A

              \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            11. lower-*.f32N/A

              \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            12. *-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            13. lower-*.f32N/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            14. lower-PI.f32N/A

              \[\leadsto \left(\left(\color{blue}{\mathsf{PI}\left(\right)} \cdot 2\right) \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            15. lower-sqrt.f32N/A

              \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \color{blue}{\sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
            16. lower--.f32N/A

              \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
            17. lower-log1p.f32N/A

              \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(u1\right)} - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
            18. mul-1-negN/A

              \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \log \left(1 + \color{blue}{\left(\mathsf{neg}\left({u1}^{2}\right)\right)}\right)} \]
          7. Applied rewrites82.0%

            \[\leadsto \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)}} \]
          8. Taylor expanded in u1 around 0

            \[\leadsto 2 \cdot \color{blue}{\left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
          9. Step-by-step derivation
            1. Applied rewrites65.7%

              \[\leadsto \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{u2} \]
            2. Add Preprocessing

            Alternative 9: 66.7% accurate, 8.9× speedup?

            \[\begin{array}{l} \\ \left(\left(2 \cdot \sqrt{u1}\right) \cdot u2\right) \cdot \mathsf{PI}\left(\right) \end{array} \]
            (FPCore (cosTheta_i u1 u2)
             :precision binary32
             (* (* (* 2.0 (sqrt u1)) u2) (PI)))
            \begin{array}{l}
            
            \\
            \left(\left(2 \cdot \sqrt{u1}\right) \cdot u2\right) \cdot \mathsf{PI}\left(\right)
            \end{array}
            
            Derivation
            1. Initial program 63.1%

              \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-neg.f32N/A

                \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              2. lift-log.f32N/A

                \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              3. neg-logN/A

                \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              4. lift--.f32N/A

                \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              5. flip--N/A

                \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              6. associate-/r/N/A

                \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              7. log-prodN/A

                \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              8. lower-+.f32N/A

                \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              9. log-recN/A

                \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              10. lower-neg.f32N/A

                \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              11. metadata-evalN/A

                \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              12. fp-cancel-sub-sign-invN/A

                \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              13. lower-log1p.f32N/A

                \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              14. lower-*.f32N/A

                \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              15. lower-neg.f32N/A

                \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
              16. lower-log1p.f3298.4

                \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            4. Applied rewrites98.4%

              \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
            5. Taylor expanded in u2 around 0

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

                \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
              2. count-2-revN/A

                \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              3. distribute-lft-inN/A

                \[\leadsto \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              4. count-2-revN/A

                \[\leadsto \left(u2 \cdot \color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              5. lower-*.f32N/A

                \[\leadsto \color{blue}{\left(u2 \cdot \left(2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
              6. count-2-revN/A

                \[\leadsto \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              7. distribute-lft-inN/A

                \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              8. count-2-revN/A

                \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              9. *-commutativeN/A

                \[\leadsto \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot u2\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              10. associate-*r*N/A

                \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              11. lower-*.f32N/A

                \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              12. *-commutativeN/A

                \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              13. lower-*.f32N/A

                \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              14. lower-PI.f32N/A

                \[\leadsto \left(\left(\color{blue}{\mathsf{PI}\left(\right)} \cdot 2\right) \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              15. lower-sqrt.f32N/A

                \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \color{blue}{\sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
              16. lower--.f32N/A

                \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
              17. lower-log1p.f32N/A

                \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(u1\right)} - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
              18. mul-1-negN/A

                \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \log \left(1 + \color{blue}{\left(\mathsf{neg}\left({u1}^{2}\right)\right)}\right)} \]
            7. Applied rewrites82.0%

              \[\leadsto \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)}} \]
            8. Taylor expanded in u1 around 0

              \[\leadsto 2 \cdot \color{blue}{\left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
            9. Step-by-step derivation
              1. Applied rewrites65.7%

                \[\leadsto \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{u2} \]
              2. Taylor expanded in u1 around 0

                \[\leadsto 2 \cdot \color{blue}{\left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
              3. Step-by-step derivation
                1. Applied rewrites65.7%

                  \[\leadsto \left(\left(2 \cdot \sqrt{u1}\right) \cdot u2\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} \]
                2. Add Preprocessing

                Alternative 10: 66.7% accurate, 8.9× speedup?

                \[\begin{array}{l} \\ \left(\sqrt{u1} \cdot 2\right) \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right) \end{array} \]
                (FPCore (cosTheta_i u1 u2)
                 :precision binary32
                 (* (* (sqrt u1) 2.0) (* u2 (PI))))
                \begin{array}{l}
                
                \\
                \left(\sqrt{u1} \cdot 2\right) \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)
                \end{array}
                
                Derivation
                1. Initial program 63.1%

                  \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-neg.f32N/A

                    \[\leadsto \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  2. lift-log.f32N/A

                    \[\leadsto \sqrt{\mathsf{neg}\left(\color{blue}{\log \left(1 - u1\right)}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  3. neg-logN/A

                    \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 - u1}\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  4. lift--.f32N/A

                    \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{1 - u1}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  5. flip--N/A

                    \[\leadsto \sqrt{\log \left(\frac{1}{\color{blue}{\frac{1 \cdot 1 - u1 \cdot u1}{1 + u1}}}\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  6. associate-/r/N/A

                    \[\leadsto \sqrt{\log \color{blue}{\left(\frac{1}{1 \cdot 1 - u1 \cdot u1} \cdot \left(1 + u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  7. log-prodN/A

                    \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  8. lower-+.f32N/A

                    \[\leadsto \sqrt{\color{blue}{\log \left(\frac{1}{1 \cdot 1 - u1 \cdot u1}\right) + \log \left(1 + u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  9. log-recN/A

                    \[\leadsto \sqrt{\color{blue}{\left(\mathsf{neg}\left(\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  10. lower-neg.f32N/A

                    \[\leadsto \sqrt{\color{blue}{\left(-\log \left(1 \cdot 1 - u1 \cdot u1\right)\right)} + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  11. metadata-evalN/A

                    \[\leadsto \sqrt{\left(-\log \left(\color{blue}{1} - u1 \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  12. fp-cancel-sub-sign-invN/A

                    \[\leadsto \sqrt{\left(-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  13. lower-log1p.f32N/A

                    \[\leadsto \sqrt{\left(-\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u1\right)\right) \cdot u1\right)}\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  14. lower-*.f32N/A

                    \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot u1}\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  15. lower-neg.f32N/A

                    \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot u1\right)\right) + \log \left(1 + u1\right)} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                  16. lower-log1p.f3298.4

                    \[\leadsto \sqrt{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \color{blue}{\mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                4. Applied rewrites98.4%

                  \[\leadsto \sqrt{\color{blue}{\left(-\mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)\right) + \mathsf{log1p}\left(u1\right)}} \cdot \sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
                5. Taylor expanded in u2 around 0

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

                    \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
                  2. count-2-revN/A

                    \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  3. distribute-lft-inN/A

                    \[\leadsto \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  4. count-2-revN/A

                    \[\leadsto \left(u2 \cdot \color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  5. lower-*.f32N/A

                    \[\leadsto \color{blue}{\left(u2 \cdot \left(2 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
                  6. count-2-revN/A

                    \[\leadsto \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  7. distribute-lft-inN/A

                    \[\leadsto \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right) + u2 \cdot \mathsf{PI}\left(\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  8. count-2-revN/A

                    \[\leadsto \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  9. *-commutativeN/A

                    \[\leadsto \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot u2\right)}\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  10. associate-*r*N/A

                    \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  11. lower-*.f32N/A

                    \[\leadsto \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  12. *-commutativeN/A

                    \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  13. lower-*.f32N/A

                    \[\leadsto \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot 2\right)} \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  14. lower-PI.f32N/A

                    \[\leadsto \left(\left(\color{blue}{\mathsf{PI}\left(\right)} \cdot 2\right) \cdot u2\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  15. lower-sqrt.f32N/A

                    \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \color{blue}{\sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
                  16. lower--.f32N/A

                    \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}} \]
                  17. lower-log1p.f32N/A

                    \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(u1\right)} - \log \left(1 + -1 \cdot {u1}^{2}\right)} \]
                  18. mul-1-negN/A

                    \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \log \left(1 + \color{blue}{\left(\mathsf{neg}\left({u1}^{2}\right)\right)}\right)} \]
                7. Applied rewrites82.0%

                  \[\leadsto \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot 2\right) \cdot u2\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\left(-u1\right) \cdot u1\right)}} \]
                8. Taylor expanded in u1 around 0

                  \[\leadsto 2 \cdot \color{blue}{\left(\sqrt{u1} \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
                9. Step-by-step derivation
                  1. Applied rewrites65.7%

                    \[\leadsto \left(\left(2 \cdot \sqrt{u1}\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{u2} \]
                  2. Step-by-step derivation
                    1. Applied rewrites65.7%

                      \[\leadsto \left(\sqrt{u1} \cdot 2\right) \cdot \left(u2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \]
                    2. Add Preprocessing

                    Reproduce

                    ?
                    herbie shell --seed 2025006 
                    (FPCore (cosTheta_i u1 u2)
                      :name "Beckmann Sample, near normal, slope_y"
                      :precision binary32
                      :pre (and (and (and (> cosTheta_i 0.9999) (<= cosTheta_i 1.0)) (and (<= 2.328306437e-10 u1) (<= u1 1.0))) (and (<= 2.328306437e-10 u2) (<= u2 1.0)))
                      (* (sqrt (- (log (- 1.0 u1)))) (sin (* (* 2.0 (PI)) u2))))