Beckmann Distribution sample, tan2theta, alphax == alphay

Percentage Accurate: 55.8% → 97.6%
Time: 6.9s
Alternatives: 5
Speedup: 10.5×

Specification

?
\[\left(0.0001 \leq \alpha \land \alpha \leq 1\right) \land \left(2.328306437 \cdot 10^{-10} \leq u0 \land u0 \leq 1\right)\]
\[\begin{array}{l} \\ \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \end{array} \]
(FPCore (alpha u0)
 :precision binary32
 (* (* (- alpha) alpha) (log (- 1.0 u0))))
float code(float alpha, float u0) {
	return (-alpha * alpha) * logf((1.0f - u0));
}
real(4) function code(alpha, u0)
    real(4), intent (in) :: alpha
    real(4), intent (in) :: u0
    code = (-alpha * alpha) * log((1.0e0 - u0))
end function
function code(alpha, u0)
	return Float32(Float32(Float32(-alpha) * alpha) * log(Float32(Float32(1.0) - u0)))
end
function tmp = code(alpha, u0)
	tmp = (-alpha * alpha) * log((single(1.0) - u0));
end
\begin{array}{l}

\\
\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\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 5 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: 55.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \end{array} \]
(FPCore (alpha u0)
 :precision binary32
 (* (* (- alpha) alpha) (log (- 1.0 u0))))
float code(float alpha, float u0) {
	return (-alpha * alpha) * logf((1.0f - u0));
}
real(4) function code(alpha, u0)
    real(4), intent (in) :: alpha
    real(4), intent (in) :: u0
    code = (-alpha * alpha) * log((1.0e0 - u0))
end function
function code(alpha, u0)
	return Float32(Float32(Float32(-alpha) * alpha) * log(Float32(Float32(1.0) - u0)))
end
function tmp = code(alpha, u0)
	tmp = (-alpha * alpha) * log((single(1.0) - u0));
end
\begin{array}{l}

\\
\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right)
\end{array}

Alternative 1: 97.6% accurate, 0.8× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9869999885559082:\\ \;\;\;\;\left(\left(\left(\alpha \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{-1}{\alpha}\right) \cdot \log \left(1 - u0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0\\ \end{array} \end{array} \]
(FPCore (alpha u0)
 :precision binary32
 (if (<= (- 1.0 u0) 0.9869999885559082)
   (* (* (* (* alpha alpha) alpha) (/ -1.0 alpha)) (log (- 1.0 u0)))
   (*
    (*
     (*
      (-
       (* 0.3333333333333333 (* alpha alpha))
       (/ (* (* alpha alpha) (+ -0.5 (/ -1.0 u0))) u0))
      u0)
     u0)
    u0)))
float code(float alpha, float u0) {
	float tmp;
	if ((1.0f - u0) <= 0.9869999885559082f) {
		tmp = (((alpha * alpha) * alpha) * (-1.0f / alpha)) * logf((1.0f - u0));
	} else {
		tmp = ((((0.3333333333333333f * (alpha * alpha)) - (((alpha * alpha) * (-0.5f + (-1.0f / u0))) / u0)) * u0) * u0) * u0;
	}
	return tmp;
}
real(4) function code(alpha, u0)
    real(4), intent (in) :: alpha
    real(4), intent (in) :: u0
    real(4) :: tmp
    if ((1.0e0 - u0) <= 0.9869999885559082e0) then
        tmp = (((alpha * alpha) * alpha) * ((-1.0e0) / alpha)) * log((1.0e0 - u0))
    else
        tmp = ((((0.3333333333333333e0 * (alpha * alpha)) - (((alpha * alpha) * ((-0.5e0) + ((-1.0e0) / u0))) / u0)) * u0) * u0) * u0
    end if
    code = tmp
end function
function code(alpha, u0)
	tmp = Float32(0.0)
	if (Float32(Float32(1.0) - u0) <= Float32(0.9869999885559082))
		tmp = Float32(Float32(Float32(Float32(alpha * alpha) * alpha) * Float32(Float32(-1.0) / alpha)) * log(Float32(Float32(1.0) - u0)));
	else
		tmp = Float32(Float32(Float32(Float32(Float32(Float32(0.3333333333333333) * Float32(alpha * alpha)) - Float32(Float32(Float32(alpha * alpha) * Float32(Float32(-0.5) + Float32(Float32(-1.0) / u0))) / u0)) * u0) * u0) * u0);
	end
	return tmp
end
function tmp_2 = code(alpha, u0)
	tmp = single(0.0);
	if ((single(1.0) - u0) <= single(0.9869999885559082))
		tmp = (((alpha * alpha) * alpha) * (single(-1.0) / alpha)) * log((single(1.0) - u0));
	else
		tmp = ((((single(0.3333333333333333) * (alpha * alpha)) - (((alpha * alpha) * (single(-0.5) + (single(-1.0) / u0))) / u0)) * u0) * u0) * u0;
	end
	tmp_2 = tmp;
end
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;1 - u0 \leq 0.9869999885559082:\\
\;\;\;\;\left(\left(\left(\alpha \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{-1}{\alpha}\right) \cdot \log \left(1 - u0\right)\\

\mathbf{else}:\\
\;\;\;\;\left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (-.f32 #s(literal 1 binary32) u0) < 0.986999989

    1. Initial program 95.6%

      \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \color{blue}{\left(\left(-\alpha\right) \cdot \alpha\right)} \cdot \log \left(1 - u0\right) \]
      2. lift-neg.f32N/A

        \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      3. neg-sub0N/A

        \[\leadsto \left(\color{blue}{\left(0 - \alpha\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      4. flip--N/A

        \[\leadsto \left(\color{blue}{\frac{0 \cdot 0 - \alpha \cdot \alpha}{0 + \alpha}} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      5. metadata-evalN/A

        \[\leadsto \left(\frac{\color{blue}{0} - \alpha \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      6. neg-sub0N/A

        \[\leadsto \left(\frac{\color{blue}{\mathsf{neg}\left(\alpha \cdot \alpha\right)}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      7. distribute-lft-neg-outN/A

        \[\leadsto \left(\frac{\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      8. lift-neg.f32N/A

        \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right)} \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      9. lift-*.f32N/A

        \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      10. +-lft-identityN/A

        \[\leadsto \left(\frac{\left(-\alpha\right) \cdot \alpha}{\color{blue}{\alpha}} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      11. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha}{\alpha}} \cdot \log \left(1 - u0\right) \]
      12. div-invN/A

        \[\leadsto \color{blue}{\left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right)} \cdot \log \left(1 - u0\right) \]
      13. +-lft-identityN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{1}{\color{blue}{0 + \alpha}}\right) \cdot \log \left(1 - u0\right) \]
      14. lower-*.f32N/A

        \[\leadsto \color{blue}{\left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{1}{0 + \alpha}\right)} \cdot \log \left(1 - u0\right) \]
      15. lower-*.f32N/A

        \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right)} \cdot \frac{1}{0 + \alpha}\right) \cdot \log \left(1 - u0\right) \]
      16. +-lft-identityN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{1}{\color{blue}{\alpha}}\right) \cdot \log \left(1 - u0\right) \]
      17. lower-/.f3295.7

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right) \cdot \color{blue}{\frac{1}{\alpha}}\right) \cdot \log \left(1 - u0\right) \]
    4. Applied rewrites95.7%

      \[\leadsto \color{blue}{\left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right)} \cdot \log \left(1 - u0\right) \]

    if 0.986999989 < (-.f32 #s(literal 1 binary32) u0)

    1. Initial program 44.4%

      \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-neg.f32N/A

        \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      2. neg-sub0N/A

        \[\leadsto \left(\color{blue}{\left(0 - \alpha\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      3. flip--N/A

        \[\leadsto \left(\color{blue}{\frac{0 \cdot 0 - \alpha \cdot \alpha}{0 + \alpha}} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      4. metadata-evalN/A

        \[\leadsto \left(\frac{\color{blue}{0} - \alpha \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      5. neg-sub0N/A

        \[\leadsto \left(\frac{\color{blue}{\mathsf{neg}\left(\alpha \cdot \alpha\right)}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      6. distribute-lft-neg-outN/A

        \[\leadsto \left(\frac{\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      7. lift-neg.f32N/A

        \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right)} \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      8. lift-*.f32N/A

        \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      9. div-invN/A

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

        \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{0 + \alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      11. +-lft-identityN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\color{blue}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      12. lower-/.f3244.4

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \color{blue}{\frac{1}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
    4. Applied rewrites44.4%

      \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
    5. Step-by-step derivation
      1. lift-log.f32N/A

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

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(1 - u0\right)} \]
      3. flip--N/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(\frac{1 \cdot 1 - u0 \cdot u0}{1 + u0}\right)} \]
      4. log-divN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - u0 \cdot u0\right) - \log \left(1 + u0\right)\right)} \]
      5. sqr-negN/A

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

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

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

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right)} \]
      9. metadata-evalN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(\color{blue}{1} - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right) \]
      10. lift-neg.f32N/A

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

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \left(\mathsf{neg}\left(u0\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(u0\right)\right)}\right) - \log \left(1 + u0\right)\right) \]
      12. sqr-negN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \color{blue}{u0 \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
      13. cancel-sign-sub-invN/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
      14. lower-log1p.f32N/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
      15. lift-neg.f32N/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right)} \cdot u0\right) - \log \left(1 + u0\right)\right) \]
      16. lower-*.f32N/A

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right) \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
      17. lower-log1p.f3281.7

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \color{blue}{\mathsf{log1p}\left(u0\right)}\right) \]
    6. Applied rewrites83.6%

      \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \mathsf{log1p}\left(u0\right)\right)} \]
    7. Taylor expanded in u0 around 0

      \[\leadsto \color{blue}{u0 \cdot \left(u0 \cdot \left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) + {\alpha}^{2}\right)} \]
    8. Step-by-step derivation
      1. *-commutativeN/A

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

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

        \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) \cdot u0} + {\alpha}^{2}\right) \cdot u0 \]
      4. lower-fma.f32N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right)} \cdot u0 \]
      5. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{3} \cdot \color{blue}{\left(u0 \cdot {\alpha}^{2}\right)} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
      6. associate-*r*N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\frac{1}{3} \cdot u0\right) \cdot {\alpha}^{2}} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
      7. distribute-rgt-outN/A

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{{\alpha}^{2} \cdot \left(\frac{1}{3} \cdot u0 + \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
      9. unpow2N/A

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

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

        \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
      12. unpow2N/A

        \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
      13. lower-*.f3284.3

        \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
    9. Applied rewrites83.8%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \alpha \cdot \alpha\right) \cdot u0} \]
    10. Taylor expanded in u0 around -inf

      \[\leadsto \left({u0}^{2} \cdot \left(-1 \cdot \frac{-1 \cdot \frac{{\alpha}^{2}}{u0} + \frac{-1}{2} \cdot {\alpha}^{2}}{u0} + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) \cdot u0 \]
    11. Step-by-step derivation
      1. Applied rewrites98.2%

        \[\leadsto \left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0 \]
    12. Recombined 2 regimes into one program.
    13. Final simplification97.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9869999885559082:\\ \;\;\;\;\left(\left(\left(\alpha \cdot \alpha\right) \cdot \alpha\right) \cdot \frac{-1}{\alpha}\right) \cdot \log \left(1 - u0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0\\ \end{array} \]
    14. Add Preprocessing

    Alternative 2: 97.6% accurate, 0.9× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9869999885559082:\\ \;\;\;\;\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0\\ \end{array} \end{array} \]
    (FPCore (alpha u0)
     :precision binary32
     (if (<= (- 1.0 u0) 0.9869999885559082)
       (* (* (- alpha) alpha) (log (- 1.0 u0)))
       (*
        (*
         (*
          (-
           (* 0.3333333333333333 (* alpha alpha))
           (/ (* (* alpha alpha) (+ -0.5 (/ -1.0 u0))) u0))
          u0)
         u0)
        u0)))
    float code(float alpha, float u0) {
    	float tmp;
    	if ((1.0f - u0) <= 0.9869999885559082f) {
    		tmp = (-alpha * alpha) * logf((1.0f - u0));
    	} else {
    		tmp = ((((0.3333333333333333f * (alpha * alpha)) - (((alpha * alpha) * (-0.5f + (-1.0f / u0))) / u0)) * u0) * u0) * u0;
    	}
    	return tmp;
    }
    
    real(4) function code(alpha, u0)
        real(4), intent (in) :: alpha
        real(4), intent (in) :: u0
        real(4) :: tmp
        if ((1.0e0 - u0) <= 0.9869999885559082e0) then
            tmp = (-alpha * alpha) * log((1.0e0 - u0))
        else
            tmp = ((((0.3333333333333333e0 * (alpha * alpha)) - (((alpha * alpha) * ((-0.5e0) + ((-1.0e0) / u0))) / u0)) * u0) * u0) * u0
        end if
        code = tmp
    end function
    
    function code(alpha, u0)
    	tmp = Float32(0.0)
    	if (Float32(Float32(1.0) - u0) <= Float32(0.9869999885559082))
    		tmp = Float32(Float32(Float32(-alpha) * alpha) * log(Float32(Float32(1.0) - u0)));
    	else
    		tmp = Float32(Float32(Float32(Float32(Float32(Float32(0.3333333333333333) * Float32(alpha * alpha)) - Float32(Float32(Float32(alpha * alpha) * Float32(Float32(-0.5) + Float32(Float32(-1.0) / u0))) / u0)) * u0) * u0) * u0);
    	end
    	return tmp
    end
    
    function tmp_2 = code(alpha, u0)
    	tmp = single(0.0);
    	if ((single(1.0) - u0) <= single(0.9869999885559082))
    		tmp = (-alpha * alpha) * log((single(1.0) - u0));
    	else
    		tmp = ((((single(0.3333333333333333) * (alpha * alpha)) - (((alpha * alpha) * (single(-0.5) + (single(-1.0) / u0))) / u0)) * u0) * u0) * u0;
    	end
    	tmp_2 = tmp;
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;1 - u0 \leq 0.9869999885559082:\\
    \;\;\;\;\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (-.f32 #s(literal 1 binary32) u0) < 0.986999989

      1. Initial program 95.6%

        \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      2. Add Preprocessing

      if 0.986999989 < (-.f32 #s(literal 1 binary32) u0)

      1. Initial program 44.4%

        \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-neg.f32N/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        2. neg-sub0N/A

          \[\leadsto \left(\color{blue}{\left(0 - \alpha\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        3. flip--N/A

          \[\leadsto \left(\color{blue}{\frac{0 \cdot 0 - \alpha \cdot \alpha}{0 + \alpha}} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        4. metadata-evalN/A

          \[\leadsto \left(\frac{\color{blue}{0} - \alpha \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        5. neg-sub0N/A

          \[\leadsto \left(\frac{\color{blue}{\mathsf{neg}\left(\alpha \cdot \alpha\right)}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        6. distribute-lft-neg-outN/A

          \[\leadsto \left(\frac{\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        7. lift-neg.f32N/A

          \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right)} \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        8. lift-*.f32N/A

          \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        9. div-invN/A

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

          \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{0 + \alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        11. +-lft-identityN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\color{blue}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        12. lower-/.f3244.4

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \color{blue}{\frac{1}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      4. Applied rewrites44.4%

        \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      5. Step-by-step derivation
        1. lift-log.f32N/A

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

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(1 - u0\right)} \]
        3. flip--N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(\frac{1 \cdot 1 - u0 \cdot u0}{1 + u0}\right)} \]
        4. log-divN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - u0 \cdot u0\right) - \log \left(1 + u0\right)\right)} \]
        5. sqr-negN/A

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

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

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

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right)} \]
        9. metadata-evalN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(\color{blue}{1} - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right) \]
        10. lift-neg.f32N/A

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

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \left(\mathsf{neg}\left(u0\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(u0\right)\right)}\right) - \log \left(1 + u0\right)\right) \]
        12. sqr-negN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \color{blue}{u0 \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
        13. cancel-sign-sub-invN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
        14. lower-log1p.f32N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
        15. lift-neg.f32N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right)} \cdot u0\right) - \log \left(1 + u0\right)\right) \]
        16. lower-*.f32N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right) \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
        17. lower-log1p.f3283.4

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \color{blue}{\mathsf{log1p}\left(u0\right)}\right) \]
      6. Applied rewrites76.9%

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \mathsf{log1p}\left(u0\right)\right)} \]
      7. Taylor expanded in u0 around 0

        \[\leadsto \color{blue}{u0 \cdot \left(u0 \cdot \left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) + {\alpha}^{2}\right)} \]
      8. Step-by-step derivation
        1. *-commutativeN/A

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

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

          \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) \cdot u0} + {\alpha}^{2}\right) \cdot u0 \]
        4. lower-fma.f32N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right)} \cdot u0 \]
        5. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{3} \cdot \color{blue}{\left(u0 \cdot {\alpha}^{2}\right)} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
        6. associate-*r*N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\frac{1}{3} \cdot u0\right) \cdot {\alpha}^{2}} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
        7. distribute-rgt-outN/A

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

          \[\leadsto \mathsf{fma}\left(\color{blue}{{\alpha}^{2} \cdot \left(\frac{1}{3} \cdot u0 + \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
        9. unpow2N/A

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

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

          \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
        12. unpow2N/A

          \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
        13. lower-*.f3284.3

          \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
      9. Applied rewrites83.8%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \alpha \cdot \alpha\right) \cdot u0} \]
      10. Taylor expanded in u0 around -inf

        \[\leadsto \left({u0}^{2} \cdot \left(-1 \cdot \frac{-1 \cdot \frac{{\alpha}^{2}}{u0} + \frac{-1}{2} \cdot {\alpha}^{2}}{u0} + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) \cdot u0 \]
      11. Step-by-step derivation
        1. Applied rewrites98.2%

          \[\leadsto \left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0 \]
      12. Recombined 2 regimes into one program.
      13. Add Preprocessing

      Alternative 3: 90.6% accurate, 1.8× speedup?

      \[\begin{array}{l} \\ \left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0 \end{array} \]
      (FPCore (alpha u0)
       :precision binary32
       (*
        (*
         (*
          (-
           (* 0.3333333333333333 (* alpha alpha))
           (/ (* (* alpha alpha) (+ -0.5 (/ -1.0 u0))) u0))
          u0)
         u0)
        u0))
      float code(float alpha, float u0) {
      	return ((((0.3333333333333333f * (alpha * alpha)) - (((alpha * alpha) * (-0.5f + (-1.0f / u0))) / u0)) * u0) * u0) * u0;
      }
      
      real(4) function code(alpha, u0)
          real(4), intent (in) :: alpha
          real(4), intent (in) :: u0
          code = ((((0.3333333333333333e0 * (alpha * alpha)) - (((alpha * alpha) * ((-0.5e0) + ((-1.0e0) / u0))) / u0)) * u0) * u0) * u0
      end function
      
      function code(alpha, u0)
      	return Float32(Float32(Float32(Float32(Float32(Float32(0.3333333333333333) * Float32(alpha * alpha)) - Float32(Float32(Float32(alpha * alpha) * Float32(Float32(-0.5) + Float32(Float32(-1.0) / u0))) / u0)) * u0) * u0) * u0)
      end
      
      function tmp = code(alpha, u0)
      	tmp = ((((single(0.3333333333333333) * (alpha * alpha)) - (((alpha * alpha) * (single(-0.5) + (single(-1.0) / u0))) / u0)) * u0) * u0) * u0;
      end
      
      \begin{array}{l}
      
      \\
      \left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0
      \end{array}
      
      Derivation
      1. Initial program 56.8%

        \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-neg.f32N/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        2. neg-sub0N/A

          \[\leadsto \left(\color{blue}{\left(0 - \alpha\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        3. flip--N/A

          \[\leadsto \left(\color{blue}{\frac{0 \cdot 0 - \alpha \cdot \alpha}{0 + \alpha}} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        4. metadata-evalN/A

          \[\leadsto \left(\frac{\color{blue}{0} - \alpha \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        5. neg-sub0N/A

          \[\leadsto \left(\frac{\color{blue}{\mathsf{neg}\left(\alpha \cdot \alpha\right)}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        6. distribute-lft-neg-outN/A

          \[\leadsto \left(\frac{\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        7. lift-neg.f32N/A

          \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right)} \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        8. lift-*.f32N/A

          \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        9. div-invN/A

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

          \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{0 + \alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        11. +-lft-identityN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\color{blue}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
        12. lower-/.f3256.8

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \color{blue}{\frac{1}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      4. Applied rewrites56.8%

        \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
      5. Step-by-step derivation
        1. lift-log.f32N/A

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

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(1 - u0\right)} \]
        3. flip--N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(\frac{1 \cdot 1 - u0 \cdot u0}{1 + u0}\right)} \]
        4. log-divN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - u0 \cdot u0\right) - \log \left(1 + u0\right)\right)} \]
        5. sqr-negN/A

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

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

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

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right)} \]
        9. metadata-evalN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(\color{blue}{1} - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right) \]
        10. lift-neg.f32N/A

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

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \left(\mathsf{neg}\left(u0\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(u0\right)\right)}\right) - \log \left(1 + u0\right)\right) \]
        12. sqr-negN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \color{blue}{u0 \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
        13. cancel-sign-sub-invN/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
        14. lower-log1p.f32N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
        15. lift-neg.f32N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right)} \cdot u0\right) - \log \left(1 + u0\right)\right) \]
        16. lower-*.f32N/A

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right) \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
        17. lower-log1p.f3273.1

          \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \color{blue}{\mathsf{log1p}\left(u0\right)}\right) \]
      6. Applied rewrites72.4%

        \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \mathsf{log1p}\left(u0\right)\right)} \]
      7. Taylor expanded in u0 around 0

        \[\leadsto \color{blue}{u0 \cdot \left(u0 \cdot \left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) + {\alpha}^{2}\right)} \]
      8. Step-by-step derivation
        1. *-commutativeN/A

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

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

          \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) \cdot u0} + {\alpha}^{2}\right) \cdot u0 \]
        4. lower-fma.f32N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right)} \cdot u0 \]
        5. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{3} \cdot \color{blue}{\left(u0 \cdot {\alpha}^{2}\right)} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
        6. associate-*r*N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\frac{1}{3} \cdot u0\right) \cdot {\alpha}^{2}} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
        7. distribute-rgt-outN/A

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

          \[\leadsto \mathsf{fma}\left(\color{blue}{{\alpha}^{2} \cdot \left(\frac{1}{3} \cdot u0 + \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
        9. unpow2N/A

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

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

          \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
        12. unpow2N/A

          \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
        13. lower-*.f3272.9

          \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
      9. Applied rewrites72.6%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \alpha \cdot \alpha\right) \cdot u0} \]
      10. Taylor expanded in u0 around -inf

        \[\leadsto \left({u0}^{2} \cdot \left(-1 \cdot \frac{-1 \cdot \frac{{\alpha}^{2}}{u0} + \frac{-1}{2} \cdot {\alpha}^{2}}{u0} + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) \cdot u0 \]
      11. Step-by-step derivation
        1. Applied rewrites88.4%

          \[\leadsto \left(\left(\left(0.3333333333333333 \cdot \left(\alpha \cdot \alpha\right) - \frac{\left(\alpha \cdot \alpha\right) \cdot \left(-0.5 + \frac{-1}{u0}\right)}{u0}\right) \cdot u0\right) \cdot u0\right) \cdot u0 \]
        2. Add Preprocessing

        Alternative 4: 65.0% accurate, 2.6× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9999780058860779:\\ \;\;\;\;\left(\left(u0 \cdot \alpha\right) \cdot \left(\mathsf{fma}\left(0.3333333333333333, u0, 0.5\right) \cdot \alpha\right) + \alpha \cdot \alpha\right) \cdot u0\\ \mathbf{else}:\\ \;\;\;\;\left(\alpha \cdot \alpha\right) \cdot u0\\ \end{array} \end{array} \]
        (FPCore (alpha u0)
         :precision binary32
         (if (<= (- 1.0 u0) 0.9999780058860779)
           (*
            (+
             (* (* u0 alpha) (* (fma 0.3333333333333333 u0 0.5) alpha))
             (* alpha alpha))
            u0)
           (* (* alpha alpha) u0)))
        float code(float alpha, float u0) {
        	float tmp;
        	if ((1.0f - u0) <= 0.9999780058860779f) {
        		tmp = (((u0 * alpha) * (fmaf(0.3333333333333333f, u0, 0.5f) * alpha)) + (alpha * alpha)) * u0;
        	} else {
        		tmp = (alpha * alpha) * u0;
        	}
        	return tmp;
        }
        
        function code(alpha, u0)
        	tmp = Float32(0.0)
        	if (Float32(Float32(1.0) - u0) <= Float32(0.9999780058860779))
        		tmp = Float32(Float32(Float32(Float32(u0 * alpha) * Float32(fma(Float32(0.3333333333333333), u0, Float32(0.5)) * alpha)) + Float32(alpha * alpha)) * u0);
        	else
        		tmp = Float32(Float32(alpha * alpha) * u0);
        	end
        	return tmp
        end
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;1 - u0 \leq 0.9999780058860779:\\
        \;\;\;\;\left(\left(u0 \cdot \alpha\right) \cdot \left(\mathsf{fma}\left(0.3333333333333333, u0, 0.5\right) \cdot \alpha\right) + \alpha \cdot \alpha\right) \cdot u0\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(\alpha \cdot \alpha\right) \cdot u0\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (-.f32 #s(literal 1 binary32) u0) < 0.999978006

          1. Initial program 84.5%

            \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-neg.f32N/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            2. neg-sub0N/A

              \[\leadsto \left(\color{blue}{\left(0 - \alpha\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            3. flip--N/A

              \[\leadsto \left(\color{blue}{\frac{0 \cdot 0 - \alpha \cdot \alpha}{0 + \alpha}} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            4. metadata-evalN/A

              \[\leadsto \left(\frac{\color{blue}{0} - \alpha \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            5. neg-sub0N/A

              \[\leadsto \left(\frac{\color{blue}{\mathsf{neg}\left(\alpha \cdot \alpha\right)}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            6. distribute-lft-neg-outN/A

              \[\leadsto \left(\frac{\color{blue}{\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            7. lift-neg.f32N/A

              \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right)} \cdot \alpha}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            8. lift-*.f32N/A

              \[\leadsto \left(\frac{\color{blue}{\left(-\alpha\right) \cdot \alpha}}{0 + \alpha} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            9. div-invN/A

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

              \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{0 + \alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            11. +-lft-identityN/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\color{blue}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            12. lower-/.f3284.5

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \color{blue}{\frac{1}{\alpha}}\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
          4. Applied rewrites84.5%

            \[\leadsto \left(\color{blue}{\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right)} \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
          5. Step-by-step derivation
            1. lift-log.f32N/A

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

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(1 - u0\right)} \]
            3. flip--N/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \log \color{blue}{\left(\frac{1 \cdot 1 - u0 \cdot u0}{1 + u0}\right)} \]
            4. log-divN/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - u0 \cdot u0\right) - \log \left(1 + u0\right)\right)} \]
            5. sqr-negN/A

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

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

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

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\log \left(1 \cdot 1 - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right)} \]
            9. metadata-evalN/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(\color{blue}{1} - \left(-u0\right) \cdot \left(-u0\right)\right) - \log \left(1 + u0\right)\right) \]
            10. lift-neg.f32N/A

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

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \left(\mathsf{neg}\left(u0\right)\right) \cdot \color{blue}{\left(\mathsf{neg}\left(u0\right)\right)}\right) - \log \left(1 + u0\right)\right) \]
            12. sqr-negN/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \left(1 - \color{blue}{u0 \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
            13. cancel-sign-sub-invN/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
            14. lower-log1p.f32N/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\color{blue}{\mathsf{log1p}\left(\left(\mathsf{neg}\left(u0\right)\right) \cdot u0\right)} - \log \left(1 + u0\right)\right) \]
            15. lift-neg.f32N/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right)} \cdot u0\right) - \log \left(1 + u0\right)\right) \]
            16. lower-*.f32N/A

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\color{blue}{\left(-u0\right) \cdot u0}\right) - \log \left(1 + u0\right)\right) \]
            17. lower-log1p.f3249.6

              \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \color{blue}{\mathsf{log1p}\left(u0\right)}\right) \]
          6. Applied rewrites52.0%

            \[\leadsto \left(\left(\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \frac{1}{\alpha}\right) \cdot \alpha\right) \cdot \color{blue}{\left(\mathsf{log1p}\left(\left(-u0\right) \cdot u0\right) - \mathsf{log1p}\left(u0\right)\right)} \]
          7. Taylor expanded in u0 around 0

            \[\leadsto \color{blue}{u0 \cdot \left(u0 \cdot \left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) + {\alpha}^{2}\right)} \]
          8. Step-by-step derivation
            1. *-commutativeN/A

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

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

              \[\leadsto \left(\color{blue}{\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right) \cdot u0} + {\alpha}^{2}\right) \cdot u0 \]
            4. lower-fma.f32N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right)} \cdot u0 \]
            5. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(\frac{1}{3} \cdot \color{blue}{\left(u0 \cdot {\alpha}^{2}\right)} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
            6. associate-*r*N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\frac{1}{3} \cdot u0\right) \cdot {\alpha}^{2}} + \frac{1}{2} \cdot {\alpha}^{2}, u0, {\alpha}^{2}\right) \cdot u0 \]
            7. distribute-rgt-outN/A

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

              \[\leadsto \mathsf{fma}\left(\color{blue}{{\alpha}^{2} \cdot \left(\frac{1}{3} \cdot u0 + \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
            9. unpow2N/A

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

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

              \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right)}, u0, {\alpha}^{2}\right) \cdot u0 \]
            12. unpow2N/A

              \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(\frac{1}{3}, u0, \frac{1}{2}\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
            13. lower-*.f3251.4

              \[\leadsto \mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \color{blue}{\alpha \cdot \alpha}\right) \cdot u0 \]
          9. Applied rewrites51.0%

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right), u0, \alpha \cdot \alpha\right) \cdot u0} \]
          10. Step-by-step derivation
            1. Applied rewrites69.7%

              \[\leadsto \left(\left(u0 \cdot \alpha\right) \cdot \left(\mathsf{fma}\left(0.3333333333333333, u0, 0.5\right) \cdot \alpha\right) + \alpha \cdot \alpha\right) \cdot u0 \]

            if 0.999978006 < (-.f32 #s(literal 1 binary32) u0)

            1. Initial program 28.6%

              \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
            2. Add Preprocessing
            3. Taylor expanded in u0 around 0

              \[\leadsto \color{blue}{{\alpha}^{2} \cdot u0} \]
            4. Step-by-step derivation
              1. lower-*.f32N/A

                \[\leadsto \color{blue}{{\alpha}^{2} \cdot u0} \]
              2. unpow2N/A

                \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right)} \cdot u0 \]
              3. lower-*.f3294.9

                \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right)} \cdot u0 \]
            5. Applied rewrites94.9%

              \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right) \cdot u0} \]
          11. Recombined 2 regimes into one program.
          12. Add Preprocessing

          Alternative 5: 74.5% accurate, 10.5× speedup?

          \[\begin{array}{l} \\ \left(\alpha \cdot \alpha\right) \cdot u0 \end{array} \]
          (FPCore (alpha u0) :precision binary32 (* (* alpha alpha) u0))
          float code(float alpha, float u0) {
          	return (alpha * alpha) * u0;
          }
          
          real(4) function code(alpha, u0)
              real(4), intent (in) :: alpha
              real(4), intent (in) :: u0
              code = (alpha * alpha) * u0
          end function
          
          function code(alpha, u0)
          	return Float32(Float32(alpha * alpha) * u0)
          end
          
          function tmp = code(alpha, u0)
          	tmp = (alpha * alpha) * u0;
          end
          
          \begin{array}{l}
          
          \\
          \left(\alpha \cdot \alpha\right) \cdot u0
          \end{array}
          
          Derivation
          1. Initial program 56.8%

            \[\left(\left(-\alpha\right) \cdot \alpha\right) \cdot \log \left(1 - u0\right) \]
          2. Add Preprocessing
          3. Taylor expanded in u0 around 0

            \[\leadsto \color{blue}{{\alpha}^{2} \cdot u0} \]
          4. Step-by-step derivation
            1. lower-*.f32N/A

              \[\leadsto \color{blue}{{\alpha}^{2} \cdot u0} \]
            2. unpow2N/A

              \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right)} \cdot u0 \]
            3. lower-*.f3272.9

              \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right)} \cdot u0 \]
          5. Applied rewrites72.9%

            \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right) \cdot u0} \]
          6. Add Preprocessing

          Reproduce

          ?
          herbie shell --seed 2024322 
          (FPCore (alpha u0)
            :name "Beckmann Distribution sample, tan2theta, alphax == alphay"
            :precision binary32
            :pre (and (and (<= 0.0001 alpha) (<= alpha 1.0)) (and (<= 2.328306437e-10 u0) (<= u0 1.0)))
            (* (* (- alpha) alpha) (log (- 1.0 u0))))