Beckmann Distribution sample, tan2theta, alphax == alphay

Percentage Accurate: 55.7% → 99.0%
Time: 10.5s
Alternatives: 16
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 16 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.7% 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: 99.0% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\alpha \cdot \left(-\alpha\right)\right) \cdot \mathsf{log1p}\left(-u0\right) \end{array} \]
(FPCore (alpha u0) :precision binary32 (* (* alpha (- alpha)) (log1p (- u0))))
float code(float alpha, float u0) {
	return (alpha * -alpha) * log1pf(-u0);
}
function code(alpha, u0)
	return Float32(Float32(alpha * Float32(-alpha)) * log1p(Float32(-u0)))
end
\begin{array}{l}

\\
\left(\alpha \cdot \left(-\alpha\right)\right) \cdot \mathsf{log1p}\left(-u0\right)
\end{array}
Derivation
  1. Initial program 60.0%

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

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

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

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

      \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u0\right)\right)} \]
    5. lower-neg.f3298.8

      \[\leadsto \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \mathsf{log1p}\left(\color{blue}{-u0}\right) \]
  4. Applied rewrites98.8%

    \[\leadsto \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \color{blue}{\mathsf{log1p}\left(-u0\right)} \]
  5. Final simplification98.8%

    \[\leadsto \left(\alpha \cdot \left(-\alpha\right)\right) \cdot \mathsf{log1p}\left(-u0\right) \]
  6. Add Preprocessing

Alternative 2: 93.6% accurate, 2.6× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(\alpha \cdot u0, \alpha, \left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right)\right)\right) \end{array} \]
(FPCore (alpha u0)
 :precision binary32
 (fma
  (* alpha u0)
  alpha
  (*
   (* u0 (* alpha alpha))
   (* u0 (fma u0 (fma u0 0.25 0.3333333333333333) 0.5)))))
float code(float alpha, float u0) {
	return fmaf((alpha * u0), alpha, ((u0 * (alpha * alpha)) * (u0 * fmaf(u0, fmaf(u0, 0.25f, 0.3333333333333333f), 0.5f))));
}
function code(alpha, u0)
	return fma(Float32(alpha * u0), alpha, Float32(Float32(u0 * Float32(alpha * alpha)) * Float32(u0 * fma(u0, fma(u0, Float32(0.25), Float32(0.3333333333333333)), Float32(0.5)))))
end
\begin{array}{l}

\\
\mathsf{fma}\left(\alpha \cdot u0, \alpha, \left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right)\right)\right)
\end{array}
Derivation
  1. Initial program 60.0%

    \[\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}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
  4. Step-by-step derivation
    1. lower-*.f32N/A

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

      \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right), {\alpha}^{2}\right)} \]
  5. Applied rewrites94.4%

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

      \[\leadsto \mathsf{fma}\left(\alpha \cdot u0, \color{blue}{\alpha}, \left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \left(\mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right) \cdot u0\right)\right) \]
    2. Final simplification94.5%

      \[\leadsto \mathsf{fma}\left(\alpha \cdot u0, \alpha, \left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right)\right)\right) \]
    3. Add Preprocessing

    Alternative 3: 93.6% accurate, 3.0× speedup?

    \[\begin{array}{l} \\ u0 \cdot \mathsf{fma}\left(\alpha, \alpha, \left(\alpha \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right)\right)\right) \end{array} \]
    (FPCore (alpha u0)
     :precision binary32
     (*
      u0
      (fma
       alpha
       alpha
       (* (* alpha alpha) (* u0 (fma u0 (fma u0 0.25 0.3333333333333333) 0.5))))))
    float code(float alpha, float u0) {
    	return u0 * fmaf(alpha, alpha, ((alpha * alpha) * (u0 * fmaf(u0, fmaf(u0, 0.25f, 0.3333333333333333f), 0.5f))));
    }
    
    function code(alpha, u0)
    	return Float32(u0 * fma(alpha, alpha, Float32(Float32(alpha * alpha) * Float32(u0 * fma(u0, fma(u0, Float32(0.25), Float32(0.3333333333333333)), Float32(0.5))))))
    end
    
    \begin{array}{l}
    
    \\
    u0 \cdot \mathsf{fma}\left(\alpha, \alpha, \left(\alpha \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right)\right)\right)
    \end{array}
    
    Derivation
    1. Initial program 60.0%

      \[\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}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
    4. Step-by-step derivation
      1. lower-*.f32N/A

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

        \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right), {\alpha}^{2}\right)} \]
    5. Applied rewrites94.4%

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

        \[\leadsto u0 \cdot \mathsf{fma}\left(\alpha, \color{blue}{\alpha}, \left(\alpha \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right)\right)\right) \]
      2. Add Preprocessing

      Alternative 4: 93.4% accurate, 3.4× speedup?

      \[\begin{array}{l} \\ u0 \cdot \left(\alpha \cdot \mathsf{fma}\left(\alpha, u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), \alpha\right)\right) \end{array} \]
      (FPCore (alpha u0)
       :precision binary32
       (*
        u0
        (*
         alpha
         (fma alpha (* u0 (fma u0 (fma u0 0.25 0.3333333333333333) 0.5)) alpha))))
      float code(float alpha, float u0) {
      	return u0 * (alpha * fmaf(alpha, (u0 * fmaf(u0, fmaf(u0, 0.25f, 0.3333333333333333f), 0.5f)), alpha));
      }
      
      function code(alpha, u0)
      	return Float32(u0 * Float32(alpha * fma(alpha, Float32(u0 * fma(u0, fma(u0, Float32(0.25), Float32(0.3333333333333333)), Float32(0.5))), alpha)))
      end
      
      \begin{array}{l}
      
      \\
      u0 \cdot \left(\alpha \cdot \mathsf{fma}\left(\alpha, u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), \alpha\right)\right)
      \end{array}
      
      Derivation
      1. Initial program 60.0%

        \[\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}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
      4. Step-by-step derivation
        1. lower-*.f32N/A

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

          \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right), {\alpha}^{2}\right)} \]
      5. Applied rewrites94.4%

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

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

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

            \[\leadsto u0 \cdot \left(\mathsf{fma}\left(\alpha, u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), \alpha\right) \cdot \alpha\right) \]
          2. Final simplification94.4%

            \[\leadsto u0 \cdot \left(\alpha \cdot \mathsf{fma}\left(\alpha, u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), \alpha\right)\right) \]
          3. Add Preprocessing

          Alternative 5: 93.4% accurate, 3.4× speedup?

          \[\begin{array}{l} \\ \alpha \cdot \left(\alpha \cdot \mathsf{fma}\left(u0 \cdot u0, \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), u0\right)\right) \end{array} \]
          (FPCore (alpha u0)
           :precision binary32
           (*
            alpha
            (* alpha (fma (* u0 u0) (fma u0 (fma u0 0.25 0.3333333333333333) 0.5) u0))))
          float code(float alpha, float u0) {
          	return alpha * (alpha * fmaf((u0 * u0), fmaf(u0, fmaf(u0, 0.25f, 0.3333333333333333f), 0.5f), u0));
          }
          
          function code(alpha, u0)
          	return Float32(alpha * Float32(alpha * fma(Float32(u0 * u0), fma(u0, fma(u0, Float32(0.25), Float32(0.3333333333333333)), Float32(0.5)), u0)))
          end
          
          \begin{array}{l}
          
          \\
          \alpha \cdot \left(\alpha \cdot \mathsf{fma}\left(u0 \cdot u0, \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), u0\right)\right)
          \end{array}
          
          Derivation
          1. Initial program 60.0%

            \[\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. *-commutativeN/A

              \[\leadsto \color{blue}{u0 \cdot {\alpha}^{2}} \]
            2. lower-*.f32N/A

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

              \[\leadsto u0 \cdot \color{blue}{\left(\alpha \cdot \alpha\right)} \]
            4. lower-*.f3273.0

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

            \[\leadsto \color{blue}{u0 \cdot \left(\alpha \cdot \alpha\right)} \]
          6. Taylor expanded in u0 around 0

            \[\leadsto \color{blue}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
          7. Applied rewrites94.3%

            \[\leadsto \color{blue}{\alpha \cdot \left(\alpha \cdot \mathsf{fma}\left(u0 \cdot u0, \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), u0\right)\right)} \]
          8. Add Preprocessing

          Alternative 6: 91.6% accurate, 3.5× speedup?

          \[\begin{array}{l} \\ u0 \cdot \mathsf{fma}\left(\alpha, \alpha, \alpha \cdot \left(\left(\alpha \cdot u0\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right)\right)\right) \end{array} \]
          (FPCore (alpha u0)
           :precision binary32
           (*
            u0
            (fma
             alpha
             alpha
             (* alpha (* (* alpha u0) (fma 0.3333333333333333 u0 0.5))))))
          float code(float alpha, float u0) {
          	return u0 * fmaf(alpha, alpha, (alpha * ((alpha * u0) * fmaf(0.3333333333333333f, u0, 0.5f))));
          }
          
          function code(alpha, u0)
          	return Float32(u0 * fma(alpha, alpha, Float32(alpha * Float32(Float32(alpha * u0) * fma(Float32(0.3333333333333333), u0, Float32(0.5))))))
          end
          
          \begin{array}{l}
          
          \\
          u0 \cdot \mathsf{fma}\left(\alpha, \alpha, \alpha \cdot \left(\left(\alpha \cdot u0\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right)\right)\right)
          \end{array}
          
          Derivation
          1. Initial program 60.0%

            \[\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}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
          4. Step-by-step derivation
            1. lower-*.f32N/A

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

              \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right), {\alpha}^{2}\right)} \]
          5. Applied rewrites94.4%

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

            \[\leadsto u0 \cdot \mathsf{fma}\left(u0, \left(\alpha \cdot \alpha\right) \cdot \left(\frac{1}{2} + \color{blue}{\frac{1}{3} \cdot u0}\right), \alpha \cdot \alpha\right) \]
          7. Step-by-step derivation
            1. Applied rewrites92.3%

              \[\leadsto u0 \cdot \mathsf{fma}\left(u0, \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \color{blue}{0.3333333333333333}, 0.5\right), \alpha \cdot \alpha\right) \]
            2. Applied rewrites92.4%

              \[\leadsto u0 \cdot \mathsf{fma}\left(\alpha, \color{blue}{\alpha}, \alpha \cdot \left(\left(\alpha \cdot u0\right) \cdot \mathsf{fma}\left(0.3333333333333333, u0, 0.5\right)\right)\right) \]
            3. Add Preprocessing

            Alternative 7: 91.2% accurate, 3.9× speedup?

            \[\begin{array}{l} \\ \left(\alpha \cdot \left(-\alpha\right)\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, -0.3333333333333333, -0.5\right), -1\right)\right) \end{array} \]
            (FPCore (alpha u0)
             :precision binary32
             (*
              (* alpha (- alpha))
              (* u0 (fma u0 (fma u0 -0.3333333333333333 -0.5) -1.0))))
            float code(float alpha, float u0) {
            	return (alpha * -alpha) * (u0 * fmaf(u0, fmaf(u0, -0.3333333333333333f, -0.5f), -1.0f));
            }
            
            function code(alpha, u0)
            	return Float32(Float32(alpha * Float32(-alpha)) * Float32(u0 * fma(u0, fma(u0, Float32(-0.3333333333333333), Float32(-0.5)), Float32(-1.0))))
            end
            
            \begin{array}{l}
            
            \\
            \left(\alpha \cdot \left(-\alpha\right)\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, -0.3333333333333333, -0.5\right), -1\right)\right)
            \end{array}
            
            Derivation
            1. Initial program 60.0%

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

              \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \color{blue}{\left(u0 \cdot \left(u0 \cdot \left(\frac{-1}{3} \cdot u0 - \frac{1}{2}\right) - 1\right)\right)} \]
            4. Step-by-step derivation
              1. lower-*.f32N/A

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \color{blue}{\left(u0 \cdot \left(u0 \cdot \left(\frac{-1}{3} \cdot u0 - \frac{1}{2}\right) - 1\right)\right)} \]
              2. sub-negN/A

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \left(u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{-1}{3} \cdot u0 - \frac{1}{2}, -1\right)}\right) \]
              5. sub-negN/A

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, u0 \cdot \frac{-1}{3} + \color{blue}{\frac{-1}{2}}, -1\right)\right) \]
              8. lower-fma.f3292.2

                \[\leadsto \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \color{blue}{\mathsf{fma}\left(u0, -0.3333333333333333, -0.5\right)}, -1\right)\right) \]
            5. Applied rewrites92.2%

              \[\leadsto \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \color{blue}{\left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, -0.3333333333333333, -0.5\right), -1\right)\right)} \]
            6. Final simplification92.2%

              \[\leadsto \left(\alpha \cdot \left(-\alpha\right)\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, -0.3333333333333333, -0.5\right), -1\right)\right) \]
            7. Add Preprocessing

            Alternative 8: 91.4% accurate, 4.1× speedup?

            \[\begin{array}{l} \\ \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, u0 \cdot \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), u0\right) \end{array} \]
            (FPCore (alpha u0)
             :precision binary32
             (* (* alpha alpha) (fma u0 (* u0 (fma u0 0.3333333333333333 0.5)) u0)))
            float code(float alpha, float u0) {
            	return (alpha * alpha) * fmaf(u0, (u0 * fmaf(u0, 0.3333333333333333f, 0.5f)), u0);
            }
            
            function code(alpha, u0)
            	return Float32(Float32(alpha * alpha) * fma(u0, Float32(u0 * fma(u0, Float32(0.3333333333333333), Float32(0.5))), u0))
            end
            
            \begin{array}{l}
            
            \\
            \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, u0 \cdot \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), u0\right)
            \end{array}
            
            Derivation
            1. Initial program 60.0%

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

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

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u0\right)\right)} \]
              5. lower-neg.f3298.8

                \[\leadsto \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \mathsf{log1p}\left(\color{blue}{-u0}\right) \]
            4. Applied rewrites98.8%

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

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

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

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

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

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

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

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \left(\mathsf{neg}\left(\log \left(\frac{\color{blue}{\left(1 - 0\right)} + u0}{1 \cdot 1 - u0 \cdot u0}\right)\right)\right) \]
              10. associate--r-N/A

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

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

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

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \left(\mathsf{neg}\left(\log \left(\frac{1 - \color{blue}{\left(0 - u0\right)}}{1 \cdot 1 - u0 \cdot u0}\right)\right)\right) \]
              16. associate--r-N/A

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

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

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

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

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

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

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

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \left(\mathsf{neg}\left(u0 \cdot \color{blue}{\left(u0 \cdot \left(\frac{1}{2} + \frac{1}{3} \cdot u0\right) + 1\right)}\right)\right) \]
              2. distribute-lft-inN/A

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

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

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

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

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

                \[\leadsto \left(\left(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right) \cdot \left(\mathsf{neg}\left(\mathsf{fma}\left(u0, u0 \cdot \left(\color{blue}{u0 \cdot \frac{1}{3}} + \frac{1}{2}\right), u0\right)\right)\right) \]
              8. lower-fma.f3292.3

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

              \[\leadsto \left(\left(-\alpha\right) \cdot \alpha\right) \cdot \left(-\color{blue}{\mathsf{fma}\left(u0, u0 \cdot \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), u0\right)}\right) \]
            10. Final simplification92.3%

              \[\leadsto \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, u0 \cdot \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), u0\right) \]
            11. Add Preprocessing

            Alternative 9: 91.2% accurate, 4.1× speedup?

            \[\begin{array}{l} \\ \left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), 1\right) \end{array} \]
            (FPCore (alpha u0)
             :precision binary32
             (* (* u0 (* alpha alpha)) (fma u0 (fma u0 0.3333333333333333 0.5) 1.0)))
            float code(float alpha, float u0) {
            	return (u0 * (alpha * alpha)) * fmaf(u0, fmaf(u0, 0.3333333333333333f, 0.5f), 1.0f);
            }
            
            function code(alpha, u0)
            	return Float32(Float32(u0 * Float32(alpha * alpha)) * fma(u0, fma(u0, Float32(0.3333333333333333), Float32(0.5)), Float32(1.0)))
            end
            
            \begin{array}{l}
            
            \\
            \left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), 1\right)
            \end{array}
            
            Derivation
            1. Initial program 60.0%

              \[\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(\mathsf{neg}\left(\alpha\right)\right) \cdot \alpha\right)} \cdot \log \left(1 - u0\right) \]
              2. *-commutativeN/A

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

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

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

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

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

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

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

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

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

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

                \[\leadsto \frac{\alpha}{\frac{\color{blue}{\alpha \cdot \alpha}}{{0}^{3} - {\alpha}^{3}}} \cdot \log \left(1 - u0\right) \]
              13. clear-numN/A

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

                \[\leadsto \frac{\alpha}{\frac{1}{\frac{{0}^{3} - {\alpha}^{3}}{\color{blue}{\alpha \cdot \alpha + 0}}}} \cdot \log \left(1 - u0\right) \]
              15. mul0-lftN/A

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

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

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

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

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

                \[\leadsto \frac{\alpha}{\frac{1}{\color{blue}{\mathsf{neg}\left(\alpha\right)}}} \cdot \log \left(1 - u0\right) \]
              21. lower-/.f3259.9

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

              \[\leadsto \color{blue}{\frac{\alpha}{\frac{1}{-\alpha}}} \cdot \log \left(1 - u0\right) \]
            5. 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)} \]
            6. Step-by-step derivation
              1. distribute-lft-inN/A

                \[\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)\right) + u0 \cdot {\alpha}^{2}} \]
              2. *-commutativeN/A

                \[\leadsto u0 \cdot \left(u0 \cdot \left(\frac{1}{3} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{2} \cdot {\alpha}^{2}\right)\right) + \color{blue}{{\alpha}^{2} \cdot u0} \]
            7. Applied rewrites92.1%

              \[\leadsto \color{blue}{\left(u0 \cdot \left(\alpha \cdot \alpha\right)\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), 1\right)} \]
            8. Add Preprocessing

            Alternative 10: 91.2% accurate, 4.1× speedup?

            \[\begin{array}{l} \\ u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), 1\right)\right) \end{array} \]
            (FPCore (alpha u0)
             :precision binary32
             (* u0 (* (* alpha alpha) (fma u0 (fma u0 0.3333333333333333 0.5) 1.0))))
            float code(float alpha, float u0) {
            	return u0 * ((alpha * alpha) * fmaf(u0, fmaf(u0, 0.3333333333333333f, 0.5f), 1.0f));
            }
            
            function code(alpha, u0)
            	return Float32(u0 * Float32(Float32(alpha * alpha) * fma(u0, fma(u0, Float32(0.3333333333333333), Float32(0.5)), Float32(1.0))))
            end
            
            \begin{array}{l}
            
            \\
            u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), 1\right)\right)
            \end{array}
            
            Derivation
            1. Initial program 60.0%

              \[\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}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
            4. Step-by-step derivation
              1. lower-*.f32N/A

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

                \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right), {\alpha}^{2}\right)} \]
            5. Applied rewrites94.4%

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

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

                \[\leadsto u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot \color{blue}{\mathsf{fma}\left(u0, \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.25, 0.3333333333333333\right), 0.5\right), 1\right)}\right) \]
              2. Taylor expanded in u0 around 0

                \[\leadsto u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, \frac{1}{3}, \frac{1}{2}\right), 1\right)\right) \]
              3. Step-by-step derivation
                1. Applied rewrites92.1%

                  \[\leadsto u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \mathsf{fma}\left(u0, 0.3333333333333333, 0.5\right), 1\right)\right) \]
                2. Add Preprocessing

                Alternative 11: 87.4% accurate, 4.3× speedup?

                \[\begin{array}{l} \\ u0 \cdot \mathsf{fma}\left(\alpha, \alpha, u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot 0.5\right)\right) \end{array} \]
                (FPCore (alpha u0)
                 :precision binary32
                 (* u0 (fma alpha alpha (* u0 (* (* alpha alpha) 0.5)))))
                float code(float alpha, float u0) {
                	return u0 * fmaf(alpha, alpha, (u0 * ((alpha * alpha) * 0.5f)));
                }
                
                function code(alpha, u0)
                	return Float32(u0 * fma(alpha, alpha, Float32(u0 * Float32(Float32(alpha * alpha) * Float32(0.5)))))
                end
                
                \begin{array}{l}
                
                \\
                u0 \cdot \mathsf{fma}\left(\alpha, \alpha, u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot 0.5\right)\right)
                \end{array}
                
                Derivation
                1. Initial program 60.0%

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

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

                  \[\leadsto \color{blue}{u0 \cdot \left(\frac{1}{2} \cdot \left({\alpha}^{2} \cdot u0\right) + {\alpha}^{2}\right)} \]
                5. Step-by-step derivation
                  1. distribute-lft-inN/A

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

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

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

                    \[\leadsto \left(u0 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(\frac{-1}{2}\right)\right)} \cdot {\alpha}^{2}\right)\right) \cdot u0 + u0 \cdot {\alpha}^{2} \]
                  5. distribute-lft-neg-inN/A

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

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

                    \[\leadsto \left(u0 \cdot \left(\mathsf{neg}\left({\alpha}^{2} \cdot \color{blue}{\left(-1 - \frac{-1}{2}\right)}\right)\right)\right) \cdot u0 + u0 \cdot {\alpha}^{2} \]
                  8. distribute-rgt-out--N/A

                    \[\leadsto \left(u0 \cdot \left(\mathsf{neg}\left(\color{blue}{\left(-1 \cdot {\alpha}^{2} - \frac{-1}{2} \cdot {\alpha}^{2}\right)}\right)\right)\right) \cdot u0 + u0 \cdot {\alpha}^{2} \]
                  9. distribute-rgt-neg-inN/A

                    \[\leadsto \color{blue}{\left(\mathsf{neg}\left(u0 \cdot \left(-1 \cdot {\alpha}^{2} - \frac{-1}{2} \cdot {\alpha}^{2}\right)\right)\right)} \cdot u0 + u0 \cdot {\alpha}^{2} \]
                  10. mul-1-negN/A

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

                    \[\leadsto \left(-1 \cdot \left(u0 \cdot \left(-1 \cdot {\alpha}^{2} - \frac{-1}{2} \cdot {\alpha}^{2}\right)\right)\right) \cdot u0 + \color{blue}{{\alpha}^{2} \cdot u0} \]
                  12. distribute-rgt-inN/A

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

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

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

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

                    \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(\alpha, \alpha, -1 \cdot \left(u0 \cdot \left(-1 \cdot {\alpha}^{2} - \frac{-1}{2} \cdot {\alpha}^{2}\right)\right)\right)} \]
                6. Applied rewrites87.5%

                  \[\leadsto \color{blue}{u0 \cdot \mathsf{fma}\left(\alpha, \alpha, u0 \cdot \left(\left(\alpha \cdot \alpha\right) \cdot 0.5\right)\right)} \]
                7. Add Preprocessing

                Alternative 12: 87.3% accurate, 4.3× speedup?

                \[\begin{array}{l} \\ u0 \cdot \mathsf{fma}\left(u0, \left(\alpha \cdot \alpha\right) \cdot 0.5, \alpha \cdot \alpha\right) \end{array} \]
                (FPCore (alpha u0)
                 :precision binary32
                 (* u0 (fma u0 (* (* alpha alpha) 0.5) (* alpha alpha))))
                float code(float alpha, float u0) {
                	return u0 * fmaf(u0, ((alpha * alpha) * 0.5f), (alpha * alpha));
                }
                
                function code(alpha, u0)
                	return Float32(u0 * fma(u0, Float32(Float32(alpha * alpha) * Float32(0.5)), Float32(alpha * alpha)))
                end
                
                \begin{array}{l}
                
                \\
                u0 \cdot \mathsf{fma}\left(u0, \left(\alpha \cdot \alpha\right) \cdot 0.5, \alpha \cdot \alpha\right)
                \end{array}
                
                Derivation
                1. Initial program 60.0%

                  \[\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}{u0 \cdot \left(u0 \cdot \left(\frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right)\right) + {\alpha}^{2}\right)} \]
                4. Step-by-step derivation
                  1. lower-*.f32N/A

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

                    \[\leadsto u0 \cdot \color{blue}{\mathsf{fma}\left(u0, \frac{1}{2} \cdot {\alpha}^{2} + u0 \cdot \left(\frac{1}{4} \cdot \left({\alpha}^{2} \cdot u0\right) + \frac{1}{3} \cdot {\alpha}^{2}\right), {\alpha}^{2}\right)} \]
                5. Applied rewrites94.4%

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

                  \[\leadsto u0 \cdot \mathsf{fma}\left(u0, \left(\alpha \cdot \alpha\right) \cdot \frac{1}{2}, \alpha \cdot \alpha\right) \]
                7. Step-by-step derivation
                  1. Applied rewrites87.5%

                    \[\leadsto u0 \cdot \mathsf{fma}\left(u0, \left(\alpha \cdot \alpha\right) \cdot 0.5, \alpha \cdot \alpha\right) \]
                  2. Add Preprocessing

                  Alternative 13: 87.3% accurate, 5.3× speedup?

                  \[\begin{array}{l} \\ \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, u0 \cdot 0.5, u0\right) \end{array} \]
                  (FPCore (alpha u0)
                   :precision binary32
                   (* (* alpha alpha) (fma u0 (* u0 0.5) u0)))
                  float code(float alpha, float u0) {
                  	return (alpha * alpha) * fmaf(u0, (u0 * 0.5f), u0);
                  }
                  
                  function code(alpha, u0)
                  	return Float32(Float32(alpha * alpha) * fma(u0, Float32(u0 * Float32(0.5)), u0))
                  end
                  
                  \begin{array}{l}
                  
                  \\
                  \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, u0 \cdot 0.5, u0\right)
                  \end{array}
                  
                  Derivation
                  1. Initial program 60.0%

                    \[\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}{u0 \cdot \left(\frac{1}{2} \cdot \left({\alpha}^{2} \cdot u0\right) + {\alpha}^{2}\right)} \]
                  4. Step-by-step derivation
                    1. distribute-lft-inN/A

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

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

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

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

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

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

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

                      \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right)} \cdot \left(\left(u0 \cdot \frac{1}{2}\right) \cdot u0 + u0\right) \]
                    9. associate-*r*N/A

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

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

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

                      \[\leadsto \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \color{blue}{u0 \cdot 0.5}, u0\right) \]
                  5. Applied rewrites87.4%

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

                  Alternative 14: 87.1% accurate, 5.3× speedup?

                  \[\begin{array}{l} \\ \left(\alpha \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, 0.5, 1\right)\right) \end{array} \]
                  (FPCore (alpha u0)
                   :precision binary32
                   (* (* alpha alpha) (* u0 (fma u0 0.5 1.0))))
                  float code(float alpha, float u0) {
                  	return (alpha * alpha) * (u0 * fmaf(u0, 0.5f, 1.0f));
                  }
                  
                  function code(alpha, u0)
                  	return Float32(Float32(alpha * alpha) * Float32(u0 * fma(u0, Float32(0.5), Float32(1.0))))
                  end
                  
                  \begin{array}{l}
                  
                  \\
                  \left(\alpha \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, 0.5, 1\right)\right)
                  \end{array}
                  
                  Derivation
                  1. Initial program 60.0%

                    \[\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}{u0 \cdot \left(\frac{1}{2} \cdot \left({\alpha}^{2} \cdot u0\right) + {\alpha}^{2}\right)} \]
                  4. Step-by-step derivation
                    1. distribute-lft-inN/A

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

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

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

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

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

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

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

                      \[\leadsto \color{blue}{\left(\alpha \cdot \alpha\right)} \cdot \left(\left(u0 \cdot \frac{1}{2}\right) \cdot u0 + u0\right) \]
                    9. associate-*r*N/A

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

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

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

                      \[\leadsto \left(\alpha \cdot \alpha\right) \cdot \mathsf{fma}\left(u0, \color{blue}{u0 \cdot 0.5}, u0\right) \]
                  5. Applied rewrites87.4%

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

                      \[\leadsto \left(\alpha \cdot \alpha\right) \cdot \left(\mathsf{fma}\left(u0, 0.5, 1\right) \cdot \color{blue}{u0}\right) \]
                    2. Final simplification87.3%

                      \[\leadsto \left(\alpha \cdot \alpha\right) \cdot \left(u0 \cdot \mathsf{fma}\left(u0, 0.5, 1\right)\right) \]
                    3. Add Preprocessing

                    Alternative 15: 74.5% accurate, 10.5× speedup?

                    \[\begin{array}{l} \\ \alpha \cdot \left(\alpha \cdot u0\right) \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(alpha * Float32(alpha * u0))
                    end
                    
                    function tmp = code(alpha, u0)
                    	tmp = alpha * (alpha * u0);
                    end
                    
                    \begin{array}{l}
                    
                    \\
                    \alpha \cdot \left(\alpha \cdot u0\right)
                    \end{array}
                    
                    Derivation
                    1. Initial program 60.0%

                      \[\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. *-commutativeN/A

                        \[\leadsto \color{blue}{u0 \cdot {\alpha}^{2}} \]
                      2. lower-*.f32N/A

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

                        \[\leadsto u0 \cdot \color{blue}{\left(\alpha \cdot \alpha\right)} \]
                      4. lower-*.f3273.0

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

                      \[\leadsto \color{blue}{u0 \cdot \left(\alpha \cdot \alpha\right)} \]
                    6. Step-by-step derivation
                      1. Applied rewrites73.0%

                        \[\leadsto \left(\alpha \cdot u0\right) \cdot \color{blue}{\alpha} \]
                      2. Final simplification73.0%

                        \[\leadsto \alpha \cdot \left(\alpha \cdot u0\right) \]
                      3. Add Preprocessing

                      Alternative 16: 74.5% accurate, 10.5× speedup?

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

                        \[\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. *-commutativeN/A

                          \[\leadsto \color{blue}{u0 \cdot {\alpha}^{2}} \]
                        2. lower-*.f32N/A

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

                          \[\leadsto u0 \cdot \color{blue}{\left(\alpha \cdot \alpha\right)} \]
                        4. lower-*.f3273.0

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

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

                      Reproduce

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