b parameter of renormalized beta distribution

Percentage Accurate: 99.9% → 99.8%
Time: 6.9s
Alternatives: 16
Speedup: N/A×

Specification

?
\[\left(0 < m \land 0 < v\right) \land v < 0.25\]
\[\begin{array}{l} \\ \left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \end{array} \]
(FPCore (m v) :precision binary64 (* (- (/ (* m (- 1.0 m)) v) 1.0) (- 1.0 m)))
double code(double m, double v) {
	return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
real(8) function code(m, v)
    real(8), intent (in) :: m
    real(8), intent (in) :: v
    code = (((m * (1.0d0 - m)) / v) - 1.0d0) * (1.0d0 - m)
end function
public static double code(double m, double v) {
	return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
def code(m, v):
	return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m)
function code(m, v)
	return Float64(Float64(Float64(Float64(m * Float64(1.0 - m)) / v) - 1.0) * Float64(1.0 - m))
end
function tmp = code(m, v)
	tmp = (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
end
code[m_, v_] := N[(N[(N[(N[(m * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right)
\end{array}

Sampling outcomes in binary64 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: 99.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \end{array} \]
(FPCore (m v) :precision binary64 (* (- (/ (* m (- 1.0 m)) v) 1.0) (- 1.0 m)))
double code(double m, double v) {
	return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
real(8) function code(m, v)
    real(8), intent (in) :: m
    real(8), intent (in) :: v
    code = (((m * (1.0d0 - m)) / v) - 1.0d0) * (1.0d0 - m)
end function
public static double code(double m, double v) {
	return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
def code(m, v):
	return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m)
function code(m, v)
	return Float64(Float64(Float64(Float64(m * Float64(1.0 - m)) / v) - 1.0) * Float64(1.0 - m))
end
function tmp = code(m, v)
	tmp = (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
end
code[m_, v_] := N[(N[(N[(N[(m * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right)
\end{array}

Alternative 1: 99.8% accurate, 0.9× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;m \leq 1.5 \cdot 10^{-11}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{1 - m}{v} \cdot m\right) \cdot \left(1 - m\right)\\ \end{array} \end{array} \]
(FPCore (m v)
 :precision binary64
 (if (<= m 1.5e-11)
   (fma (fma -2.0 m 1.0) (/ m v) -1.0)
   (* (* (/ (- 1.0 m) v) m) (- 1.0 m))))
double code(double m, double v) {
	double tmp;
	if (m <= 1.5e-11) {
		tmp = fma(fma(-2.0, m, 1.0), (m / v), -1.0);
	} else {
		tmp = (((1.0 - m) / v) * m) * (1.0 - m);
	}
	return tmp;
}
function code(m, v)
	tmp = 0.0
	if (m <= 1.5e-11)
		tmp = fma(fma(-2.0, m, 1.0), Float64(m / v), -1.0);
	else
		tmp = Float64(Float64(Float64(Float64(1.0 - m) / v) * m) * Float64(1.0 - m));
	end
	return tmp
end
code[m_, v_] := If[LessEqual[m, 1.5e-11], N[(N[(-2.0 * m + 1.0), $MachinePrecision] * N[(m / v), $MachinePrecision] + -1.0), $MachinePrecision], N[(N[(N[(N[(1.0 - m), $MachinePrecision] / v), $MachinePrecision] * m), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;m \leq 1.5 \cdot 10^{-11}:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\

\mathbf{else}:\\
\;\;\;\;\left(\frac{1 - m}{v} \cdot m\right) \cdot \left(1 - m\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if m < 1.5e-11

    1. Initial program 99.9%

      \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
    2. Add Preprocessing
    3. Taylor expanded in m around 0

      \[\leadsto \color{blue}{m \cdot \left(1 + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right)\right) - 1} \]
    4. Step-by-step derivation
      1. distribute-rgt-inN/A

        \[\leadsto \color{blue}{\left(1 \cdot m + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right)} - 1 \]
      2. *-lft-identityN/A

        \[\leadsto \left(\color{blue}{m} + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right) - 1 \]
      3. associate--l+N/A

        \[\leadsto \color{blue}{m + \left(\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - 1\right)} \]
      4. +-commutativeN/A

        \[\leadsto \color{blue}{\left(\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - 1\right) + m} \]
      5. associate-+l-N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - \left(1 - m\right)} \]
      6. unsub-negN/A

        \[\leadsto \color{blue}{\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m + \left(\mathsf{neg}\left(\left(1 - m\right)\right)\right)} \]
      7. mul-1-negN/A

        \[\leadsto \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m + \color{blue}{-1 \cdot \left(1 - m\right)} \]
      8. *-commutativeN/A

        \[\leadsto \color{blue}{m \cdot \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right)} + -1 \cdot \left(1 - m\right) \]
      9. distribute-lft-inN/A

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

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

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

        \[\leadsto \left(\left(-2 \cdot m\right) \cdot \frac{m}{v} + \color{blue}{\frac{m \cdot 1}{v}}\right) + -1 \cdot \left(1 - m\right) \]
      13. *-rgt-identityN/A

        \[\leadsto \left(\left(-2 \cdot m\right) \cdot \frac{m}{v} + \frac{\color{blue}{m}}{v}\right) + -1 \cdot \left(1 - m\right) \]
      14. distribute-lft1-inN/A

        \[\leadsto \color{blue}{\left(-2 \cdot m + 1\right) \cdot \frac{m}{v}} + -1 \cdot \left(1 - m\right) \]
      15. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(-2 \cdot m + 1, \frac{m}{v}, -1 \cdot \left(1 - m\right)\right)} \]
      16. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(-2, m, 1\right)}, \frac{m}{v}, -1 \cdot \left(1 - m\right)\right) \]
      17. lower-/.f64N/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \color{blue}{\frac{m}{v}}, -1 \cdot \left(1 - m\right)\right) \]
      18. mul-1-negN/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{\mathsf{neg}\left(\left(1 - m\right)\right)}\right) \]
      19. neg-sub0N/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{0 - \left(1 - m\right)}\right) \]
      20. associate--r-N/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{\left(0 - 1\right) + m}\right) \]
      21. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{-1} + m\right) \]
      22. +-commutativeN/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{m + -1}\right) \]
      23. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, m + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \]
    5. Applied rewrites100.0%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, m - 1\right)} \]
    6. Taylor expanded in m around 0

      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right) \]
    7. Step-by-step derivation
      1. Applied rewrites100.0%

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right) \]

      if 1.5e-11 < m

      1. Initial program 99.8%

        \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
      2. Add Preprocessing
      3. Taylor expanded in v around 0

        \[\leadsto \color{blue}{\frac{m \cdot \left(1 - m\right)}{v}} \cdot \left(1 - m\right) \]
      4. Step-by-step derivation
        1. associate-/l*N/A

          \[\leadsto \color{blue}{\left(m \cdot \frac{1 - m}{v}\right)} \cdot \left(1 - m\right) \]
        2. div-subN/A

          \[\leadsto \left(m \cdot \color{blue}{\left(\frac{1}{v} - \frac{m}{v}\right)}\right) \cdot \left(1 - m\right) \]
        3. unsub-negN/A

          \[\leadsto \left(m \cdot \color{blue}{\left(\frac{1}{v} + \left(\mathsf{neg}\left(\frac{m}{v}\right)\right)\right)}\right) \cdot \left(1 - m\right) \]
        4. mul-1-negN/A

          \[\leadsto \left(m \cdot \left(\frac{1}{v} + \color{blue}{-1 \cdot \frac{m}{v}}\right)\right) \cdot \left(1 - m\right) \]
        5. +-commutativeN/A

          \[\leadsto \left(m \cdot \color{blue}{\left(-1 \cdot \frac{m}{v} + \frac{1}{v}\right)}\right) \cdot \left(1 - m\right) \]
        6. *-commutativeN/A

          \[\leadsto \color{blue}{\left(\left(-1 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right)} \cdot \left(1 - m\right) \]
        7. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\left(-1 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right)} \cdot \left(1 - m\right) \]
        8. +-commutativeN/A

          \[\leadsto \left(\color{blue}{\left(\frac{1}{v} + -1 \cdot \frac{m}{v}\right)} \cdot m\right) \cdot \left(1 - m\right) \]
        9. mul-1-negN/A

          \[\leadsto \left(\left(\frac{1}{v} + \color{blue}{\left(\mathsf{neg}\left(\frac{m}{v}\right)\right)}\right) \cdot m\right) \cdot \left(1 - m\right) \]
        10. unsub-negN/A

          \[\leadsto \left(\color{blue}{\left(\frac{1}{v} - \frac{m}{v}\right)} \cdot m\right) \cdot \left(1 - m\right) \]
        11. div-subN/A

          \[\leadsto \left(\color{blue}{\frac{1 - m}{v}} \cdot m\right) \cdot \left(1 - m\right) \]
        12. lower-/.f64N/A

          \[\leadsto \left(\color{blue}{\frac{1 - m}{v}} \cdot m\right) \cdot \left(1 - m\right) \]
        13. lower--.f6499.9

          \[\leadsto \left(\frac{\color{blue}{1 - m}}{v} \cdot m\right) \cdot \left(1 - m\right) \]
      5. Applied rewrites99.9%

        \[\leadsto \color{blue}{\left(\frac{1 - m}{v} \cdot m\right)} \cdot \left(1 - m\right) \]
    8. Recombined 2 regimes into one program.
    9. Add Preprocessing

    Alternative 2: 73.3% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\left(\frac{\left(1 - m\right) \cdot m}{v} - 1\right) \cdot \left(1 - m\right) \leq -0.2:\\ \;\;\;\;-1\\ \mathbf{else}:\\ \;\;\;\;\frac{m}{v} + m\\ \end{array} \end{array} \]
    (FPCore (m v)
     :precision binary64
     (if (<= (* (- (/ (* (- 1.0 m) m) v) 1.0) (- 1.0 m)) -0.2) -1.0 (+ (/ m v) m)))
    double code(double m, double v) {
    	double tmp;
    	if ((((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2) {
    		tmp = -1.0;
    	} else {
    		tmp = (m / v) + m;
    	}
    	return tmp;
    }
    
    real(8) function code(m, v)
        real(8), intent (in) :: m
        real(8), intent (in) :: v
        real(8) :: tmp
        if ((((((1.0d0 - m) * m) / v) - 1.0d0) * (1.0d0 - m)) <= (-0.2d0)) then
            tmp = -1.0d0
        else
            tmp = (m / v) + m
        end if
        code = tmp
    end function
    
    public static double code(double m, double v) {
    	double tmp;
    	if ((((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2) {
    		tmp = -1.0;
    	} else {
    		tmp = (m / v) + m;
    	}
    	return tmp;
    }
    
    def code(m, v):
    	tmp = 0
    	if (((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2:
    		tmp = -1.0
    	else:
    		tmp = (m / v) + m
    	return tmp
    
    function code(m, v)
    	tmp = 0.0
    	if (Float64(Float64(Float64(Float64(Float64(1.0 - m) * m) / v) - 1.0) * Float64(1.0 - m)) <= -0.2)
    		tmp = -1.0;
    	else
    		tmp = Float64(Float64(m / v) + m);
    	end
    	return tmp
    end
    
    function tmp_2 = code(m, v)
    	tmp = 0.0;
    	if ((((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2)
    		tmp = -1.0;
    	else
    		tmp = (m / v) + m;
    	end
    	tmp_2 = tmp;
    end
    
    code[m_, v_] := If[LessEqual[N[(N[(N[(N[(N[(1.0 - m), $MachinePrecision] * m), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision], -0.2], -1.0, N[(N[(m / v), $MachinePrecision] + m), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\left(\frac{\left(1 - m\right) \cdot m}{v} - 1\right) \cdot \left(1 - m\right) \leq -0.2:\\
    \;\;\;\;-1\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{m}{v} + m\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) (-.f64 #s(literal 1 binary64) m)) < -0.20000000000000001

      1. Initial program 100.0%

        \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
      2. Add Preprocessing
      3. Taylor expanded in m around 0

        \[\leadsto \color{blue}{-1} \]
      4. Step-by-step derivation
        1. Applied rewrites97.4%

          \[\leadsto \color{blue}{-1} \]

        if -0.20000000000000001 < (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) (-.f64 #s(literal 1 binary64) m))

        1. Initial program 99.9%

          \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
          2. lift--.f64N/A

            \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
          3. flip3--N/A

            \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          4. clear-numN/A

            \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          5. un-div-invN/A

            \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          6. lower-/.f64N/A

            \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          7. clear-numN/A

            \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          8. flip3--N/A

            \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          9. lift--.f64N/A

            \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
          10. lower-/.f6499.9

            \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
        4. Applied rewrites99.9%

          \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
        5. Taylor expanded in m around 0

          \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
        6. Step-by-step derivation
          1. lower--.f64N/A

            \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
          2. +-commutativeN/A

            \[\leadsto m \cdot \color{blue}{\left(\frac{1}{v} + 1\right)} - 1 \]
          3. distribute-rgt-inN/A

            \[\leadsto \color{blue}{\left(\frac{1}{v} \cdot m + 1 \cdot m\right)} - 1 \]
          4. associate-*l/N/A

            \[\leadsto \left(\color{blue}{\frac{1 \cdot m}{v}} + 1 \cdot m\right) - 1 \]
          5. *-lft-identityN/A

            \[\leadsto \left(\frac{\color{blue}{m}}{v} + 1 \cdot m\right) - 1 \]
          6. *-lft-identityN/A

            \[\leadsto \left(\frac{m}{v} + \color{blue}{m}\right) - 1 \]
          7. lower-+.f64N/A

            \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right)} - 1 \]
          8. lower-/.f6467.2

            \[\leadsto \left(\color{blue}{\frac{m}{v}} + m\right) - 1 \]
        7. Applied rewrites67.2%

          \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right) - 1} \]
        8. Taylor expanded in m around inf

          \[\leadsto m \cdot \color{blue}{\left(1 + \frac{1}{v}\right)} \]
        9. Step-by-step derivation
          1. Applied rewrites66.1%

            \[\leadsto \frac{m}{v} + \color{blue}{m} \]
        10. Recombined 2 regimes into one program.
        11. Final simplification73.4%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\frac{\left(1 - m\right) \cdot m}{v} - 1\right) \cdot \left(1 - m\right) \leq -0.2:\\ \;\;\;\;-1\\ \mathbf{else}:\\ \;\;\;\;\frac{m}{v} + m\\ \end{array} \]
        12. Add Preprocessing

        Alternative 3: 73.3% accurate, 0.6× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\left(\frac{\left(1 - m\right) \cdot m}{v} - 1\right) \cdot \left(1 - m\right) \leq -0.2:\\ \;\;\;\;-1\\ \mathbf{else}:\\ \;\;\;\;\frac{m}{v}\\ \end{array} \end{array} \]
        (FPCore (m v)
         :precision binary64
         (if (<= (* (- (/ (* (- 1.0 m) m) v) 1.0) (- 1.0 m)) -0.2) -1.0 (/ m v)))
        double code(double m, double v) {
        	double tmp;
        	if ((((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2) {
        		tmp = -1.0;
        	} else {
        		tmp = m / v;
        	}
        	return tmp;
        }
        
        real(8) function code(m, v)
            real(8), intent (in) :: m
            real(8), intent (in) :: v
            real(8) :: tmp
            if ((((((1.0d0 - m) * m) / v) - 1.0d0) * (1.0d0 - m)) <= (-0.2d0)) then
                tmp = -1.0d0
            else
                tmp = m / v
            end if
            code = tmp
        end function
        
        public static double code(double m, double v) {
        	double tmp;
        	if ((((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2) {
        		tmp = -1.0;
        	} else {
        		tmp = m / v;
        	}
        	return tmp;
        }
        
        def code(m, v):
        	tmp = 0
        	if (((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2:
        		tmp = -1.0
        	else:
        		tmp = m / v
        	return tmp
        
        function code(m, v)
        	tmp = 0.0
        	if (Float64(Float64(Float64(Float64(Float64(1.0 - m) * m) / v) - 1.0) * Float64(1.0 - m)) <= -0.2)
        		tmp = -1.0;
        	else
        		tmp = Float64(m / v);
        	end
        	return tmp
        end
        
        function tmp_2 = code(m, v)
        	tmp = 0.0;
        	if ((((((1.0 - m) * m) / v) - 1.0) * (1.0 - m)) <= -0.2)
        		tmp = -1.0;
        	else
        		tmp = m / v;
        	end
        	tmp_2 = tmp;
        end
        
        code[m_, v_] := If[LessEqual[N[(N[(N[(N[(N[(1.0 - m), $MachinePrecision] * m), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision], -0.2], -1.0, N[(m / v), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;\left(\frac{\left(1 - m\right) \cdot m}{v} - 1\right) \cdot \left(1 - m\right) \leq -0.2:\\
        \;\;\;\;-1\\
        
        \mathbf{else}:\\
        \;\;\;\;\frac{m}{v}\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) (-.f64 #s(literal 1 binary64) m)) < -0.20000000000000001

          1. Initial program 100.0%

            \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
          2. Add Preprocessing
          3. Taylor expanded in m around 0

            \[\leadsto \color{blue}{-1} \]
          4. Step-by-step derivation
            1. Applied rewrites97.4%

              \[\leadsto \color{blue}{-1} \]

            if -0.20000000000000001 < (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) (-.f64 #s(literal 1 binary64) m))

            1. Initial program 99.9%

              \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
              2. lift--.f64N/A

                \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
              3. flip3--N/A

                \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              4. clear-numN/A

                \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              5. un-div-invN/A

                \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              6. lower-/.f64N/A

                \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              7. clear-numN/A

                \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              8. flip3--N/A

                \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              9. lift--.f64N/A

                \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              10. lower-/.f6499.9

                \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
            4. Applied rewrites99.9%

              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
            5. Taylor expanded in m around 0

              \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
            6. Step-by-step derivation
              1. lower--.f64N/A

                \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
              2. +-commutativeN/A

                \[\leadsto m \cdot \color{blue}{\left(\frac{1}{v} + 1\right)} - 1 \]
              3. distribute-rgt-inN/A

                \[\leadsto \color{blue}{\left(\frac{1}{v} \cdot m + 1 \cdot m\right)} - 1 \]
              4. associate-*l/N/A

                \[\leadsto \left(\color{blue}{\frac{1 \cdot m}{v}} + 1 \cdot m\right) - 1 \]
              5. *-lft-identityN/A

                \[\leadsto \left(\frac{\color{blue}{m}}{v} + 1 \cdot m\right) - 1 \]
              6. *-lft-identityN/A

                \[\leadsto \left(\frac{m}{v} + \color{blue}{m}\right) - 1 \]
              7. lower-+.f64N/A

                \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right)} - 1 \]
              8. lower-/.f6467.2

                \[\leadsto \left(\color{blue}{\frac{m}{v}} + m\right) - 1 \]
            7. Applied rewrites67.2%

              \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right) - 1} \]
            8. Taylor expanded in v around 0

              \[\leadsto \frac{m}{\color{blue}{v}} \]
            9. Step-by-step derivation
              1. Applied rewrites66.1%

                \[\leadsto \frac{m}{\color{blue}{v}} \]
            10. Recombined 2 regimes into one program.
            11. Final simplification73.4%

              \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\frac{\left(1 - m\right) \cdot m}{v} - 1\right) \cdot \left(1 - m\right) \leq -0.2:\\ \;\;\;\;-1\\ \mathbf{else}:\\ \;\;\;\;\frac{m}{v}\\ \end{array} \]
            12. Add Preprocessing

            Alternative 4: 99.9% accurate, 0.6× speedup?

            \[\begin{array}{l} \\ \left(\frac{\frac{m}{\frac{1}{1 - m}}}{v} - 1\right) \cdot \left(1 - m\right) \end{array} \]
            (FPCore (m v)
             :precision binary64
             (* (- (/ (/ m (/ 1.0 (- 1.0 m))) v) 1.0) (- 1.0 m)))
            double code(double m, double v) {
            	return (((m / (1.0 / (1.0 - m))) / v) - 1.0) * (1.0 - m);
            }
            
            real(8) function code(m, v)
                real(8), intent (in) :: m
                real(8), intent (in) :: v
                code = (((m / (1.0d0 / (1.0d0 - m))) / v) - 1.0d0) * (1.0d0 - m)
            end function
            
            public static double code(double m, double v) {
            	return (((m / (1.0 / (1.0 - m))) / v) - 1.0) * (1.0 - m);
            }
            
            def code(m, v):
            	return (((m / (1.0 / (1.0 - m))) / v) - 1.0) * (1.0 - m)
            
            function code(m, v)
            	return Float64(Float64(Float64(Float64(m / Float64(1.0 / Float64(1.0 - m))) / v) - 1.0) * Float64(1.0 - m))
            end
            
            function tmp = code(m, v)
            	tmp = (((m / (1.0 / (1.0 - m))) / v) - 1.0) * (1.0 - m);
            end
            
            code[m_, v_] := N[(N[(N[(N[(m / N[(1.0 / N[(1.0 - m), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            \left(\frac{\frac{m}{\frac{1}{1 - m}}}{v} - 1\right) \cdot \left(1 - m\right)
            \end{array}
            
            Derivation
            1. Initial program 99.9%

              \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
              2. lift--.f64N/A

                \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
              3. flip3--N/A

                \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              4. clear-numN/A

                \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              5. un-div-invN/A

                \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              6. lower-/.f64N/A

                \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              7. clear-numN/A

                \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              8. flip3--N/A

                \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              9. lift--.f64N/A

                \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
              10. lower-/.f6499.9

                \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
            4. Applied rewrites99.9%

              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
            5. Add Preprocessing

            Alternative 5: 99.9% accurate, 0.9× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;m \leq 2.75 \cdot 10^{-8}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\left(1 - m\right) \cdot m\right) \cdot \left(1 - m\right)}{v}\\ \end{array} \end{array} \]
            (FPCore (m v)
             :precision binary64
             (if (<= m 2.75e-8)
               (fma (fma -2.0 m 1.0) (/ m v) -1.0)
               (/ (* (* (- 1.0 m) m) (- 1.0 m)) v)))
            double code(double m, double v) {
            	double tmp;
            	if (m <= 2.75e-8) {
            		tmp = fma(fma(-2.0, m, 1.0), (m / v), -1.0);
            	} else {
            		tmp = (((1.0 - m) * m) * (1.0 - m)) / v;
            	}
            	return tmp;
            }
            
            function code(m, v)
            	tmp = 0.0
            	if (m <= 2.75e-8)
            		tmp = fma(fma(-2.0, m, 1.0), Float64(m / v), -1.0);
            	else
            		tmp = Float64(Float64(Float64(Float64(1.0 - m) * m) * Float64(1.0 - m)) / v);
            	end
            	return tmp
            end
            
            code[m_, v_] := If[LessEqual[m, 2.75e-8], N[(N[(-2.0 * m + 1.0), $MachinePrecision] * N[(m / v), $MachinePrecision] + -1.0), $MachinePrecision], N[(N[(N[(N[(1.0 - m), $MachinePrecision] * m), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;m \leq 2.75 \cdot 10^{-8}:\\
            \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\
            
            \mathbf{else}:\\
            \;\;\;\;\frac{\left(\left(1 - m\right) \cdot m\right) \cdot \left(1 - m\right)}{v}\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if m < 2.7500000000000001e-8

              1. Initial program 99.9%

                \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
              2. Add Preprocessing
              3. Taylor expanded in m around 0

                \[\leadsto \color{blue}{m \cdot \left(1 + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right)\right) - 1} \]
              4. Step-by-step derivation
                1. distribute-rgt-inN/A

                  \[\leadsto \color{blue}{\left(1 \cdot m + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right)} - 1 \]
                2. *-lft-identityN/A

                  \[\leadsto \left(\color{blue}{m} + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right) - 1 \]
                3. associate--l+N/A

                  \[\leadsto \color{blue}{m + \left(\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - 1\right)} \]
                4. +-commutativeN/A

                  \[\leadsto \color{blue}{\left(\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - 1\right) + m} \]
                5. associate-+l-N/A

                  \[\leadsto \color{blue}{\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - \left(1 - m\right)} \]
                6. unsub-negN/A

                  \[\leadsto \color{blue}{\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m + \left(\mathsf{neg}\left(\left(1 - m\right)\right)\right)} \]
                7. mul-1-negN/A

                  \[\leadsto \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m + \color{blue}{-1 \cdot \left(1 - m\right)} \]
                8. *-commutativeN/A

                  \[\leadsto \color{blue}{m \cdot \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right)} + -1 \cdot \left(1 - m\right) \]
                9. distribute-lft-inN/A

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

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

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

                  \[\leadsto \left(\left(-2 \cdot m\right) \cdot \frac{m}{v} + \color{blue}{\frac{m \cdot 1}{v}}\right) + -1 \cdot \left(1 - m\right) \]
                13. *-rgt-identityN/A

                  \[\leadsto \left(\left(-2 \cdot m\right) \cdot \frac{m}{v} + \frac{\color{blue}{m}}{v}\right) + -1 \cdot \left(1 - m\right) \]
                14. distribute-lft1-inN/A

                  \[\leadsto \color{blue}{\left(-2 \cdot m + 1\right) \cdot \frac{m}{v}} + -1 \cdot \left(1 - m\right) \]
                15. lower-fma.f64N/A

                  \[\leadsto \color{blue}{\mathsf{fma}\left(-2 \cdot m + 1, \frac{m}{v}, -1 \cdot \left(1 - m\right)\right)} \]
                16. lower-fma.f64N/A

                  \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(-2, m, 1\right)}, \frac{m}{v}, -1 \cdot \left(1 - m\right)\right) \]
                17. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \color{blue}{\frac{m}{v}}, -1 \cdot \left(1 - m\right)\right) \]
                18. mul-1-negN/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{\mathsf{neg}\left(\left(1 - m\right)\right)}\right) \]
                19. neg-sub0N/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{0 - \left(1 - m\right)}\right) \]
                20. associate--r-N/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{\left(0 - 1\right) + m}\right) \]
                21. metadata-evalN/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{-1} + m\right) \]
                22. +-commutativeN/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{m + -1}\right) \]
                23. metadata-evalN/A

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, m + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \]
              5. Applied rewrites99.9%

                \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, m - 1\right)} \]
              6. Taylor expanded in m around 0

                \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right) \]
              7. Step-by-step derivation
                1. Applied rewrites99.9%

                  \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right) \]

                if 2.7500000000000001e-8 < m

                1. Initial program 99.9%

                  \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-*.f64N/A

                    \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  2. lift--.f64N/A

                    \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  3. flip3--N/A

                    \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  4. clear-numN/A

                    \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  5. un-div-invN/A

                    \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  6. lower-/.f64N/A

                    \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  7. clear-numN/A

                    \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  8. flip3--N/A

                    \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  9. lift--.f64N/A

                    \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  10. lower-/.f6499.9

                    \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                4. Applied rewrites99.9%

                  \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                5. Taylor expanded in v around 0

                  \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                6. Step-by-step derivation
                  1. lower-/.f64N/A

                    \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                7. Applied rewrites99.9%

                  \[\leadsto \color{blue}{\frac{\left(1 - m\right) \cdot \left(m - \mathsf{fma}\left(m, m, v\right)\right)}{v}} \]
                8. Taylor expanded in v around 0

                  \[\leadsto \frac{\left(1 - m\right) \cdot \left(m - {m}^{2}\right)}{v} \]
                9. Step-by-step derivation
                  1. Applied rewrites99.9%

                    \[\leadsto \frac{\left(1 - m\right) \cdot \left(\left(1 - m\right) \cdot m\right)}{v} \]
                10. Recombined 2 regimes into one program.
                11. Final simplification99.9%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;m \leq 2.75 \cdot 10^{-8}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\left(1 - m\right) \cdot m\right) \cdot \left(1 - m\right)}{v}\\ \end{array} \]
                12. Add Preprocessing

                Alternative 6: 98.3% accurate, 1.0× speedup?

                \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;m \leq 0.41:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{m}{v} \cdot m\right) \cdot m\\ \end{array} \end{array} \]
                (FPCore (m v)
                 :precision binary64
                 (if (<= m 0.41) (fma (fma -2.0 m 1.0) (/ m v) -1.0) (* (* (/ m v) m) m)))
                double code(double m, double v) {
                	double tmp;
                	if (m <= 0.41) {
                		tmp = fma(fma(-2.0, m, 1.0), (m / v), -1.0);
                	} else {
                		tmp = ((m / v) * m) * m;
                	}
                	return tmp;
                }
                
                function code(m, v)
                	tmp = 0.0
                	if (m <= 0.41)
                		tmp = fma(fma(-2.0, m, 1.0), Float64(m / v), -1.0);
                	else
                		tmp = Float64(Float64(Float64(m / v) * m) * m);
                	end
                	return tmp
                end
                
                code[m_, v_] := If[LessEqual[m, 0.41], N[(N[(-2.0 * m + 1.0), $MachinePrecision] * N[(m / v), $MachinePrecision] + -1.0), $MachinePrecision], N[(N[(N[(m / v), $MachinePrecision] * m), $MachinePrecision] * m), $MachinePrecision]]
                
                \begin{array}{l}
                
                \\
                \begin{array}{l}
                \mathbf{if}\;m \leq 0.41:\\
                \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right)\\
                
                \mathbf{else}:\\
                \;\;\;\;\left(\frac{m}{v} \cdot m\right) \cdot m\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 2 regimes
                2. if m < 0.409999999999999976

                  1. Initial program 99.9%

                    \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                  2. Add Preprocessing
                  3. Taylor expanded in m around 0

                    \[\leadsto \color{blue}{m \cdot \left(1 + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right)\right) - 1} \]
                  4. Step-by-step derivation
                    1. distribute-rgt-inN/A

                      \[\leadsto \color{blue}{\left(1 \cdot m + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right)} - 1 \]
                    2. *-lft-identityN/A

                      \[\leadsto \left(\color{blue}{m} + \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m\right) - 1 \]
                    3. associate--l+N/A

                      \[\leadsto \color{blue}{m + \left(\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - 1\right)} \]
                    4. +-commutativeN/A

                      \[\leadsto \color{blue}{\left(\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - 1\right) + m} \]
                    5. associate-+l-N/A

                      \[\leadsto \color{blue}{\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m - \left(1 - m\right)} \]
                    6. unsub-negN/A

                      \[\leadsto \color{blue}{\left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m + \left(\mathsf{neg}\left(\left(1 - m\right)\right)\right)} \]
                    7. mul-1-negN/A

                      \[\leadsto \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right) \cdot m + \color{blue}{-1 \cdot \left(1 - m\right)} \]
                    8. *-commutativeN/A

                      \[\leadsto \color{blue}{m \cdot \left(-2 \cdot \frac{m}{v} + \frac{1}{v}\right)} + -1 \cdot \left(1 - m\right) \]
                    9. distribute-lft-inN/A

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

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

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

                      \[\leadsto \left(\left(-2 \cdot m\right) \cdot \frac{m}{v} + \color{blue}{\frac{m \cdot 1}{v}}\right) + -1 \cdot \left(1 - m\right) \]
                    13. *-rgt-identityN/A

                      \[\leadsto \left(\left(-2 \cdot m\right) \cdot \frac{m}{v} + \frac{\color{blue}{m}}{v}\right) + -1 \cdot \left(1 - m\right) \]
                    14. distribute-lft1-inN/A

                      \[\leadsto \color{blue}{\left(-2 \cdot m + 1\right) \cdot \frac{m}{v}} + -1 \cdot \left(1 - m\right) \]
                    15. lower-fma.f64N/A

                      \[\leadsto \color{blue}{\mathsf{fma}\left(-2 \cdot m + 1, \frac{m}{v}, -1 \cdot \left(1 - m\right)\right)} \]
                    16. lower-fma.f64N/A

                      \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(-2, m, 1\right)}, \frac{m}{v}, -1 \cdot \left(1 - m\right)\right) \]
                    17. lower-/.f64N/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \color{blue}{\frac{m}{v}}, -1 \cdot \left(1 - m\right)\right) \]
                    18. mul-1-negN/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{\mathsf{neg}\left(\left(1 - m\right)\right)}\right) \]
                    19. neg-sub0N/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{0 - \left(1 - m\right)}\right) \]
                    20. associate--r-N/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{\left(0 - 1\right) + m}\right) \]
                    21. metadata-evalN/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{-1} + m\right) \]
                    22. +-commutativeN/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, \color{blue}{m + -1}\right) \]
                    23. metadata-evalN/A

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, m + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \]
                  5. Applied rewrites99.5%

                    \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, m - 1\right)} \]
                  6. Taylor expanded in m around 0

                    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right) \]
                  7. Step-by-step derivation
                    1. Applied rewrites99.5%

                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, m, 1\right), \frac{m}{v}, -1\right) \]

                    if 0.409999999999999976 < m

                    1. Initial program 99.9%

                      \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                    2. Add Preprocessing
                    3. Taylor expanded in m around inf

                      \[\leadsto \color{blue}{\frac{{m}^{3}}{v}} \]
                    4. Step-by-step derivation
                      1. unpow3N/A

                        \[\leadsto \frac{\color{blue}{\left(m \cdot m\right) \cdot m}}{v} \]
                      2. unpow2N/A

                        \[\leadsto \frac{\color{blue}{{m}^{2}} \cdot m}{v} \]
                      3. associate-*l/N/A

                        \[\leadsto \color{blue}{\frac{{m}^{2}}{v} \cdot m} \]
                      4. lower-*.f64N/A

                        \[\leadsto \color{blue}{\frac{{m}^{2}}{v} \cdot m} \]
                      5. unpow2N/A

                        \[\leadsto \frac{\color{blue}{m \cdot m}}{v} \cdot m \]
                      6. associate-*l/N/A

                        \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right)} \cdot m \]
                      7. lower-*.f64N/A

                        \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right)} \cdot m \]
                      8. lower-/.f6496.4

                        \[\leadsto \left(\color{blue}{\frac{m}{v}} \cdot m\right) \cdot m \]
                    5. Applied rewrites96.4%

                      \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right) \cdot m} \]
                  8. Recombined 2 regimes into one program.
                  9. Add Preprocessing

                  Alternative 7: 97.8% accurate, 1.1× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;m \leq 1:\\ \;\;\;\;\left(\frac{m}{v} - 1\right) \cdot \left(1 - m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{m}{v} \cdot m\right) \cdot m\\ \end{array} \end{array} \]
                  (FPCore (m v)
                   :precision binary64
                   (if (<= m 1.0) (* (- (/ m v) 1.0) (- 1.0 m)) (* (* (/ m v) m) m)))
                  double code(double m, double v) {
                  	double tmp;
                  	if (m <= 1.0) {
                  		tmp = ((m / v) - 1.0) * (1.0 - m);
                  	} else {
                  		tmp = ((m / v) * m) * m;
                  	}
                  	return tmp;
                  }
                  
                  real(8) function code(m, v)
                      real(8), intent (in) :: m
                      real(8), intent (in) :: v
                      real(8) :: tmp
                      if (m <= 1.0d0) then
                          tmp = ((m / v) - 1.0d0) * (1.0d0 - m)
                      else
                          tmp = ((m / v) * m) * m
                      end if
                      code = tmp
                  end function
                  
                  public static double code(double m, double v) {
                  	double tmp;
                  	if (m <= 1.0) {
                  		tmp = ((m / v) - 1.0) * (1.0 - m);
                  	} else {
                  		tmp = ((m / v) * m) * m;
                  	}
                  	return tmp;
                  }
                  
                  def code(m, v):
                  	tmp = 0
                  	if m <= 1.0:
                  		tmp = ((m / v) - 1.0) * (1.0 - m)
                  	else:
                  		tmp = ((m / v) * m) * m
                  	return tmp
                  
                  function code(m, v)
                  	tmp = 0.0
                  	if (m <= 1.0)
                  		tmp = Float64(Float64(Float64(m / v) - 1.0) * Float64(1.0 - m));
                  	else
                  		tmp = Float64(Float64(Float64(m / v) * m) * m);
                  	end
                  	return tmp
                  end
                  
                  function tmp_2 = code(m, v)
                  	tmp = 0.0;
                  	if (m <= 1.0)
                  		tmp = ((m / v) - 1.0) * (1.0 - m);
                  	else
                  		tmp = ((m / v) * m) * m;
                  	end
                  	tmp_2 = tmp;
                  end
                  
                  code[m_, v_] := If[LessEqual[m, 1.0], N[(N[(N[(m / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision], N[(N[(N[(m / v), $MachinePrecision] * m), $MachinePrecision] * m), $MachinePrecision]]
                  
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  \mathbf{if}\;m \leq 1:\\
                  \;\;\;\;\left(\frac{m}{v} - 1\right) \cdot \left(1 - m\right)\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\left(\frac{m}{v} \cdot m\right) \cdot m\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 2 regimes
                  2. if m < 1

                    1. Initial program 99.9%

                      \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                    2. Add Preprocessing
                    3. Taylor expanded in m around 0

                      \[\leadsto \left(\color{blue}{\frac{m}{v}} - 1\right) \cdot \left(1 - m\right) \]
                    4. Step-by-step derivation
                      1. lower-/.f6497.5

                        \[\leadsto \left(\color{blue}{\frac{m}{v}} - 1\right) \cdot \left(1 - m\right) \]
                    5. Applied rewrites97.5%

                      \[\leadsto \left(\color{blue}{\frac{m}{v}} - 1\right) \cdot \left(1 - m\right) \]

                    if 1 < m

                    1. Initial program 99.9%

                      \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                    2. Add Preprocessing
                    3. Taylor expanded in m around inf

                      \[\leadsto \color{blue}{\frac{{m}^{3}}{v}} \]
                    4. Step-by-step derivation
                      1. unpow3N/A

                        \[\leadsto \frac{\color{blue}{\left(m \cdot m\right) \cdot m}}{v} \]
                      2. unpow2N/A

                        \[\leadsto \frac{\color{blue}{{m}^{2}} \cdot m}{v} \]
                      3. associate-*l/N/A

                        \[\leadsto \color{blue}{\frac{{m}^{2}}{v} \cdot m} \]
                      4. lower-*.f64N/A

                        \[\leadsto \color{blue}{\frac{{m}^{2}}{v} \cdot m} \]
                      5. unpow2N/A

                        \[\leadsto \frac{\color{blue}{m \cdot m}}{v} \cdot m \]
                      6. associate-*l/N/A

                        \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right)} \cdot m \]
                      7. lower-*.f64N/A

                        \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right)} \cdot m \]
                      8. lower-/.f6497.0

                        \[\leadsto \left(\color{blue}{\frac{m}{v}} \cdot m\right) \cdot m \]
                    5. Applied rewrites97.0%

                      \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right) \cdot m} \]
                  3. Recombined 2 regimes into one program.
                  4. Add Preprocessing

                  Alternative 8: 99.9% accurate, 1.1× speedup?

                  \[\begin{array}{l} \\ \frac{\left(m - \mathsf{fma}\left(m, m, v\right)\right) \cdot \left(1 - m\right)}{v} \end{array} \]
                  (FPCore (m v) :precision binary64 (/ (* (- m (fma m m v)) (- 1.0 m)) v))
                  double code(double m, double v) {
                  	return ((m - fma(m, m, v)) * (1.0 - m)) / v;
                  }
                  
                  function code(m, v)
                  	return Float64(Float64(Float64(m - fma(m, m, v)) * Float64(1.0 - m)) / v)
                  end
                  
                  code[m_, v_] := N[(N[(N[(m - N[(m * m + v), $MachinePrecision]), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision]
                  
                  \begin{array}{l}
                  
                  \\
                  \frac{\left(m - \mathsf{fma}\left(m, m, v\right)\right) \cdot \left(1 - m\right)}{v}
                  \end{array}
                  
                  Derivation
                  1. Initial program 99.9%

                    \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-*.f64N/A

                      \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    2. lift--.f64N/A

                      \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    3. flip3--N/A

                      \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    4. clear-numN/A

                      \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    5. un-div-invN/A

                      \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    6. lower-/.f64N/A

                      \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    7. clear-numN/A

                      \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    8. flip3--N/A

                      \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    9. lift--.f64N/A

                      \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    10. lower-/.f6499.9

                      \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  4. Applied rewrites99.9%

                    \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                  5. Taylor expanded in v around 0

                    \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                  6. Step-by-step derivation
                    1. lower-/.f64N/A

                      \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                  7. Applied rewrites99.9%

                    \[\leadsto \color{blue}{\frac{\left(1 - m\right) \cdot \left(m - \mathsf{fma}\left(m, m, v\right)\right)}{v}} \]
                  8. Final simplification99.9%

                    \[\leadsto \frac{\left(m - \mathsf{fma}\left(m, m, v\right)\right) \cdot \left(1 - m\right)}{v} \]
                  9. Add Preprocessing

                  Alternative 9: 97.8% accurate, 1.1× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;m \leq 2.6:\\ \;\;\;\;\frac{\mathsf{fma}\left(-1, v, m\right)}{v}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{m}{v} \cdot m\right) \cdot m\\ \end{array} \end{array} \]
                  (FPCore (m v)
                   :precision binary64
                   (if (<= m 2.6) (/ (fma -1.0 v m) v) (* (* (/ m v) m) m)))
                  double code(double m, double v) {
                  	double tmp;
                  	if (m <= 2.6) {
                  		tmp = fma(-1.0, v, m) / v;
                  	} else {
                  		tmp = ((m / v) * m) * m;
                  	}
                  	return tmp;
                  }
                  
                  function code(m, v)
                  	tmp = 0.0
                  	if (m <= 2.6)
                  		tmp = Float64(fma(-1.0, v, m) / v);
                  	else
                  		tmp = Float64(Float64(Float64(m / v) * m) * m);
                  	end
                  	return tmp
                  end
                  
                  code[m_, v_] := If[LessEqual[m, 2.6], N[(N[(-1.0 * v + m), $MachinePrecision] / v), $MachinePrecision], N[(N[(N[(m / v), $MachinePrecision] * m), $MachinePrecision] * m), $MachinePrecision]]
                  
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  \mathbf{if}\;m \leq 2.6:\\
                  \;\;\;\;\frac{\mathsf{fma}\left(-1, v, m\right)}{v}\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\left(\frac{m}{v} \cdot m\right) \cdot m\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 2 regimes
                  2. if m < 2.60000000000000009

                    1. Initial program 99.9%

                      \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                    2. Add Preprocessing
                    3. Step-by-step derivation
                      1. lift-*.f64N/A

                        \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      2. lift--.f64N/A

                        \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      3. flip3--N/A

                        \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      4. clear-numN/A

                        \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      5. un-div-invN/A

                        \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      6. lower-/.f64N/A

                        \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      7. clear-numN/A

                        \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      8. flip3--N/A

                        \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      9. lift--.f64N/A

                        \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                      10. lower-/.f6499.9

                        \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    4. Applied rewrites99.9%

                      \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                    5. Taylor expanded in v around 0

                      \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                    6. Step-by-step derivation
                      1. lower-/.f64N/A

                        \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                    7. Applied rewrites99.9%

                      \[\leadsto \color{blue}{\frac{\left(1 - m\right) \cdot \left(m - \mathsf{fma}\left(m, m, v\right)\right)}{v}} \]
                    8. Taylor expanded in m around 0

                      \[\leadsto \frac{-1 \cdot v + m \cdot \left(1 + v\right)}{v} \]
                    9. Step-by-step derivation
                      1. Applied rewrites96.8%

                        \[\leadsto \frac{\mathsf{fma}\left(m - 1, v, m\right)}{v} \]
                      2. Taylor expanded in m around 0

                        \[\leadsto \frac{\mathsf{fma}\left(-1, v, m\right)}{v} \]
                      3. Step-by-step derivation
                        1. Applied rewrites96.8%

                          \[\leadsto \frac{\mathsf{fma}\left(-1, v, m\right)}{v} \]

                        if 2.60000000000000009 < m

                        1. Initial program 99.9%

                          \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                        2. Add Preprocessing
                        3. Taylor expanded in m around inf

                          \[\leadsto \color{blue}{\frac{{m}^{3}}{v}} \]
                        4. Step-by-step derivation
                          1. unpow3N/A

                            \[\leadsto \frac{\color{blue}{\left(m \cdot m\right) \cdot m}}{v} \]
                          2. unpow2N/A

                            \[\leadsto \frac{\color{blue}{{m}^{2}} \cdot m}{v} \]
                          3. associate-*l/N/A

                            \[\leadsto \color{blue}{\frac{{m}^{2}}{v} \cdot m} \]
                          4. lower-*.f64N/A

                            \[\leadsto \color{blue}{\frac{{m}^{2}}{v} \cdot m} \]
                          5. unpow2N/A

                            \[\leadsto \frac{\color{blue}{m \cdot m}}{v} \cdot m \]
                          6. associate-*l/N/A

                            \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right)} \cdot m \]
                          7. lower-*.f64N/A

                            \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right)} \cdot m \]
                          8. lower-/.f6497.7

                            \[\leadsto \left(\color{blue}{\frac{m}{v}} \cdot m\right) \cdot m \]
                        5. Applied rewrites97.7%

                          \[\leadsto \color{blue}{\left(\frac{m}{v} \cdot m\right) \cdot m} \]
                      4. Recombined 2 regimes into one program.
                      5. Add Preprocessing

                      Alternative 10: 81.5% accurate, 1.1× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;m \leq 1.35 \cdot 10^{+154}:\\ \;\;\;\;\frac{\mathsf{fma}\left(m - 1, v, m\right)}{v}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{fma}\left(m, m, -1\right)}{m - -1}\\ \end{array} \end{array} \]
                      (FPCore (m v)
                       :precision binary64
                       (if (<= m 1.35e+154) (/ (fma (- m 1.0) v m) v) (/ (fma m m -1.0) (- m -1.0))))
                      double code(double m, double v) {
                      	double tmp;
                      	if (m <= 1.35e+154) {
                      		tmp = fma((m - 1.0), v, m) / v;
                      	} else {
                      		tmp = fma(m, m, -1.0) / (m - -1.0);
                      	}
                      	return tmp;
                      }
                      
                      function code(m, v)
                      	tmp = 0.0
                      	if (m <= 1.35e+154)
                      		tmp = Float64(fma(Float64(m - 1.0), v, m) / v);
                      	else
                      		tmp = Float64(fma(m, m, -1.0) / Float64(m - -1.0));
                      	end
                      	return tmp
                      end
                      
                      code[m_, v_] := If[LessEqual[m, 1.35e+154], N[(N[(N[(m - 1.0), $MachinePrecision] * v + m), $MachinePrecision] / v), $MachinePrecision], N[(N[(m * m + -1.0), $MachinePrecision] / N[(m - -1.0), $MachinePrecision]), $MachinePrecision]]
                      
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      \mathbf{if}\;m \leq 1.35 \cdot 10^{+154}:\\
                      \;\;\;\;\frac{\mathsf{fma}\left(m - 1, v, m\right)}{v}\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;\frac{\mathsf{fma}\left(m, m, -1\right)}{m - -1}\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if m < 1.35000000000000003e154

                        1. Initial program 99.9%

                          \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                        2. Add Preprocessing
                        3. Step-by-step derivation
                          1. lift-*.f64N/A

                            \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          2. lift--.f64N/A

                            \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          3. flip3--N/A

                            \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          4. clear-numN/A

                            \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          5. un-div-invN/A

                            \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          6. lower-/.f64N/A

                            \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          7. clear-numN/A

                            \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          8. flip3--N/A

                            \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          9. lift--.f64N/A

                            \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          10. lower-/.f6499.9

                            \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                        4. Applied rewrites99.9%

                          \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                        5. Taylor expanded in v around 0

                          \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                        6. Step-by-step derivation
                          1. lower-/.f64N/A

                            \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                        7. Applied rewrites99.9%

                          \[\leadsto \color{blue}{\frac{\left(1 - m\right) \cdot \left(m - \mathsf{fma}\left(m, m, v\right)\right)}{v}} \]
                        8. Taylor expanded in m around 0

                          \[\leadsto \frac{-1 \cdot v + m \cdot \left(1 + v\right)}{v} \]
                        9. Step-by-step derivation
                          1. Applied rewrites73.0%

                            \[\leadsto \frac{\mathsf{fma}\left(m - 1, v, m\right)}{v} \]

                          if 1.35000000000000003e154 < m

                          1. Initial program 100.0%

                            \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                          2. Add Preprocessing
                          3. Step-by-step derivation
                            1. lift-*.f64N/A

                              \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            2. lift--.f64N/A

                              \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            3. flip3--N/A

                              \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            4. clear-numN/A

                              \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            5. un-div-invN/A

                              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            6. lower-/.f64N/A

                              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            7. clear-numN/A

                              \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            8. flip3--N/A

                              \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            9. lift--.f64N/A

                              \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            10. lower-/.f64100.0

                              \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          4. Applied rewrites100.0%

                            \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          5. Taylor expanded in v around inf

                            \[\leadsto \color{blue}{-1 \cdot \left(1 - m\right)} \]
                          6. Step-by-step derivation
                            1. mul-1-negN/A

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

                              \[\leadsto \color{blue}{0 - \left(1 - m\right)} \]
                            3. associate--r-N/A

                              \[\leadsto \color{blue}{\left(0 - 1\right) + m} \]
                            4. metadata-evalN/A

                              \[\leadsto \color{blue}{-1} + m \]
                            5. +-commutativeN/A

                              \[\leadsto \color{blue}{m + -1} \]
                            6. metadata-evalN/A

                              \[\leadsto m + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \]
                            7. sub-negN/A

                              \[\leadsto \color{blue}{m - 1} \]
                            8. lower--.f647.2

                              \[\leadsto \color{blue}{m - 1} \]
                          7. Applied rewrites7.2%

                            \[\leadsto \color{blue}{m - 1} \]
                          8. Step-by-step derivation
                            1. Applied rewrites100.0%

                              \[\leadsto \frac{\mathsf{fma}\left(m, m, -1\right)}{\color{blue}{m - -1}} \]
                          9. Recombined 2 regimes into one program.
                          10. Add Preprocessing

                          Alternative 11: 75.4% accurate, 1.5× speedup?

                          \[\begin{array}{l} \\ \frac{\mathsf{fma}\left(m - 1, v, m\right)}{v} \end{array} \]
                          (FPCore (m v) :precision binary64 (/ (fma (- m 1.0) v m) v))
                          double code(double m, double v) {
                          	return fma((m - 1.0), v, m) / v;
                          }
                          
                          function code(m, v)
                          	return Float64(fma(Float64(m - 1.0), v, m) / v)
                          end
                          
                          code[m_, v_] := N[(N[(N[(m - 1.0), $MachinePrecision] * v + m), $MachinePrecision] / v), $MachinePrecision]
                          
                          \begin{array}{l}
                          
                          \\
                          \frac{\mathsf{fma}\left(m - 1, v, m\right)}{v}
                          \end{array}
                          
                          Derivation
                          1. Initial program 99.9%

                            \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                          2. Add Preprocessing
                          3. Step-by-step derivation
                            1. lift-*.f64N/A

                              \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            2. lift--.f64N/A

                              \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            3. flip3--N/A

                              \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            4. clear-numN/A

                              \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            5. un-div-invN/A

                              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            6. lower-/.f64N/A

                              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            7. clear-numN/A

                              \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            8. flip3--N/A

                              \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            9. lift--.f64N/A

                              \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            10. lower-/.f6499.9

                              \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          4. Applied rewrites99.9%

                            \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                          5. Taylor expanded in v around 0

                            \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                          6. Step-by-step derivation
                            1. lower-/.f64N/A

                              \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                          7. Applied rewrites99.9%

                            \[\leadsto \color{blue}{\frac{\left(1 - m\right) \cdot \left(m - \mathsf{fma}\left(m, m, v\right)\right)}{v}} \]
                          8. Taylor expanded in m around 0

                            \[\leadsto \frac{-1 \cdot v + m \cdot \left(1 + v\right)}{v} \]
                          9. Step-by-step derivation
                            1. Applied rewrites74.9%

                              \[\leadsto \frac{\mathsf{fma}\left(m - 1, v, m\right)}{v} \]
                            2. Add Preprocessing

                            Alternative 12: 75.4% accurate, 1.7× speedup?

                            \[\begin{array}{l} \\ \frac{\mathsf{fma}\left(-1, v, m\right)}{v} \end{array} \]
                            (FPCore (m v) :precision binary64 (/ (fma -1.0 v m) v))
                            double code(double m, double v) {
                            	return fma(-1.0, v, m) / v;
                            }
                            
                            function code(m, v)
                            	return Float64(fma(-1.0, v, m) / v)
                            end
                            
                            code[m_, v_] := N[(N[(-1.0 * v + m), $MachinePrecision] / v), $MachinePrecision]
                            
                            \begin{array}{l}
                            
                            \\
                            \frac{\mathsf{fma}\left(-1, v, m\right)}{v}
                            \end{array}
                            
                            Derivation
                            1. Initial program 99.9%

                              \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                            2. Add Preprocessing
                            3. Step-by-step derivation
                              1. lift-*.f64N/A

                                \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              2. lift--.f64N/A

                                \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              3. flip3--N/A

                                \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              4. clear-numN/A

                                \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              5. un-div-invN/A

                                \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              6. lower-/.f64N/A

                                \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              7. clear-numN/A

                                \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              8. flip3--N/A

                                \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              9. lift--.f64N/A

                                \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                              10. lower-/.f6499.9

                                \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            4. Applied rewrites99.9%

                              \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                            5. Taylor expanded in v around 0

                              \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                            6. Step-by-step derivation
                              1. lower-/.f64N/A

                                \[\leadsto \color{blue}{\frac{-1 \cdot \left(v \cdot \left(1 - m\right)\right) + m \cdot {\left(1 - m\right)}^{2}}{v}} \]
                            7. Applied rewrites99.9%

                              \[\leadsto \color{blue}{\frac{\left(1 - m\right) \cdot \left(m - \mathsf{fma}\left(m, m, v\right)\right)}{v}} \]
                            8. Taylor expanded in m around 0

                              \[\leadsto \frac{-1 \cdot v + m \cdot \left(1 + v\right)}{v} \]
                            9. Step-by-step derivation
                              1. Applied rewrites74.9%

                                \[\leadsto \frac{\mathsf{fma}\left(m - 1, v, m\right)}{v} \]
                              2. Taylor expanded in m around 0

                                \[\leadsto \frac{\mathsf{fma}\left(-1, v, m\right)}{v} \]
                              3. Step-by-step derivation
                                1. Applied rewrites74.9%

                                  \[\leadsto \frac{\mathsf{fma}\left(-1, v, m\right)}{v} \]
                                2. Add Preprocessing

                                Alternative 13: 75.4% accurate, 1.7× speedup?

                                \[\begin{array}{l} \\ \left(\frac{m}{v} + m\right) - 1 \end{array} \]
                                (FPCore (m v) :precision binary64 (- (+ (/ m v) m) 1.0))
                                double code(double m, double v) {
                                	return ((m / v) + m) - 1.0;
                                }
                                
                                real(8) function code(m, v)
                                    real(8), intent (in) :: m
                                    real(8), intent (in) :: v
                                    code = ((m / v) + m) - 1.0d0
                                end function
                                
                                public static double code(double m, double v) {
                                	return ((m / v) + m) - 1.0;
                                }
                                
                                def code(m, v):
                                	return ((m / v) + m) - 1.0
                                
                                function code(m, v)
                                	return Float64(Float64(Float64(m / v) + m) - 1.0)
                                end
                                
                                function tmp = code(m, v)
                                	tmp = ((m / v) + m) - 1.0;
                                end
                                
                                code[m_, v_] := N[(N[(N[(m / v), $MachinePrecision] + m), $MachinePrecision] - 1.0), $MachinePrecision]
                                
                                \begin{array}{l}
                                
                                \\
                                \left(\frac{m}{v} + m\right) - 1
                                \end{array}
                                
                                Derivation
                                1. Initial program 99.9%

                                  \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                                2. Add Preprocessing
                                3. Taylor expanded in m around 0

                                  \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
                                4. Step-by-step derivation
                                  1. lower--.f64N/A

                                    \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
                                  2. +-commutativeN/A

                                    \[\leadsto m \cdot \color{blue}{\left(\frac{1}{v} + 1\right)} - 1 \]
                                  3. distribute-rgt-inN/A

                                    \[\leadsto \color{blue}{\left(\frac{1}{v} \cdot m + 1 \cdot m\right)} - 1 \]
                                  4. associate-*l/N/A

                                    \[\leadsto \left(\color{blue}{\frac{1 \cdot m}{v}} + 1 \cdot m\right) - 1 \]
                                  5. *-lft-identityN/A

                                    \[\leadsto \left(\frac{\color{blue}{m}}{v} + 1 \cdot m\right) - 1 \]
                                  6. *-lft-identityN/A

                                    \[\leadsto \left(\frac{m}{v} + \color{blue}{m}\right) - 1 \]
                                  7. lower-+.f64N/A

                                    \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right)} - 1 \]
                                  8. lower-/.f6474.9

                                    \[\leadsto \left(\color{blue}{\frac{m}{v}} + m\right) - 1 \]
                                5. Applied rewrites74.9%

                                  \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right) - 1} \]
                                6. Add Preprocessing

                                Alternative 14: 75.4% accurate, 2.1× speedup?

                                \[\begin{array}{l} \\ \frac{m}{v} - 1 \end{array} \]
                                (FPCore (m v) :precision binary64 (- (/ m v) 1.0))
                                double code(double m, double v) {
                                	return (m / v) - 1.0;
                                }
                                
                                real(8) function code(m, v)
                                    real(8), intent (in) :: m
                                    real(8), intent (in) :: v
                                    code = (m / v) - 1.0d0
                                end function
                                
                                public static double code(double m, double v) {
                                	return (m / v) - 1.0;
                                }
                                
                                def code(m, v):
                                	return (m / v) - 1.0
                                
                                function code(m, v)
                                	return Float64(Float64(m / v) - 1.0)
                                end
                                
                                function tmp = code(m, v)
                                	tmp = (m / v) - 1.0;
                                end
                                
                                code[m_, v_] := N[(N[(m / v), $MachinePrecision] - 1.0), $MachinePrecision]
                                
                                \begin{array}{l}
                                
                                \\
                                \frac{m}{v} - 1
                                \end{array}
                                
                                Derivation
                                1. Initial program 99.9%

                                  \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                                2. Add Preprocessing
                                3. Step-by-step derivation
                                  1. lift-*.f64N/A

                                    \[\leadsto \left(\frac{\color{blue}{m \cdot \left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  2. lift--.f64N/A

                                    \[\leadsto \left(\frac{m \cdot \color{blue}{\left(1 - m\right)}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  3. flip3--N/A

                                    \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  4. clear-numN/A

                                    \[\leadsto \left(\frac{m \cdot \color{blue}{\frac{1}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  5. un-div-invN/A

                                    \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  6. lower-/.f64N/A

                                    \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}{{1}^{3} - {m}^{3}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  7. clear-numN/A

                                    \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{\frac{{1}^{3} - {m}^{3}}{1 \cdot 1 + \left(m \cdot m + 1 \cdot m\right)}}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  8. flip3--N/A

                                    \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  9. lift--.f64N/A

                                    \[\leadsto \left(\frac{\frac{m}{\frac{1}{\color{blue}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  10. lower-/.f6499.9

                                    \[\leadsto \left(\frac{\frac{m}{\color{blue}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                4. Applied rewrites99.9%

                                  \[\leadsto \left(\frac{\color{blue}{\frac{m}{\frac{1}{1 - m}}}}{v} - 1\right) \cdot \left(1 - m\right) \]
                                5. Taylor expanded in m around 0

                                  \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
                                6. Step-by-step derivation
                                  1. lower--.f64N/A

                                    \[\leadsto \color{blue}{m \cdot \left(1 + \frac{1}{v}\right) - 1} \]
                                  2. +-commutativeN/A

                                    \[\leadsto m \cdot \color{blue}{\left(\frac{1}{v} + 1\right)} - 1 \]
                                  3. distribute-rgt-inN/A

                                    \[\leadsto \color{blue}{\left(\frac{1}{v} \cdot m + 1 \cdot m\right)} - 1 \]
                                  4. associate-*l/N/A

                                    \[\leadsto \left(\color{blue}{\frac{1 \cdot m}{v}} + 1 \cdot m\right) - 1 \]
                                  5. *-lft-identityN/A

                                    \[\leadsto \left(\frac{\color{blue}{m}}{v} + 1 \cdot m\right) - 1 \]
                                  6. *-lft-identityN/A

                                    \[\leadsto \left(\frac{m}{v} + \color{blue}{m}\right) - 1 \]
                                  7. lower-+.f64N/A

                                    \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right)} - 1 \]
                                  8. lower-/.f6474.9

                                    \[\leadsto \left(\color{blue}{\frac{m}{v}} + m\right) - 1 \]
                                7. Applied rewrites74.9%

                                  \[\leadsto \color{blue}{\left(\frac{m}{v} + m\right) - 1} \]
                                8. Taylor expanded in v around 0

                                  \[\leadsto \frac{m}{v} - 1 \]
                                9. Step-by-step derivation
                                  1. Applied rewrites74.9%

                                    \[\leadsto \frac{m}{v} - 1 \]
                                  2. Add Preprocessing

                                  Alternative 15: 27.7% accurate, 7.8× speedup?

                                  \[\begin{array}{l} \\ m - 1 \end{array} \]
                                  (FPCore (m v) :precision binary64 (- m 1.0))
                                  double code(double m, double v) {
                                  	return m - 1.0;
                                  }
                                  
                                  real(8) function code(m, v)
                                      real(8), intent (in) :: m
                                      real(8), intent (in) :: v
                                      code = m - 1.0d0
                                  end function
                                  
                                  public static double code(double m, double v) {
                                  	return m - 1.0;
                                  }
                                  
                                  def code(m, v):
                                  	return m - 1.0
                                  
                                  function code(m, v)
                                  	return Float64(m - 1.0)
                                  end
                                  
                                  function tmp = code(m, v)
                                  	tmp = m - 1.0;
                                  end
                                  
                                  code[m_, v_] := N[(m - 1.0), $MachinePrecision]
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  m - 1
                                  \end{array}
                                  
                                  Derivation
                                  1. Initial program 99.9%

                                    \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in v around inf

                                    \[\leadsto \color{blue}{-1 \cdot \left(1 - m\right)} \]
                                  4. Step-by-step derivation
                                    1. mul-1-negN/A

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

                                      \[\leadsto \color{blue}{0 - \left(1 - m\right)} \]
                                    3. associate--r-N/A

                                      \[\leadsto \color{blue}{\left(0 - 1\right) + m} \]
                                    4. metadata-evalN/A

                                      \[\leadsto \color{blue}{-1} + m \]
                                    5. +-commutativeN/A

                                      \[\leadsto \color{blue}{m + -1} \]
                                    6. metadata-evalN/A

                                      \[\leadsto m + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \]
                                    7. sub-negN/A

                                      \[\leadsto \color{blue}{m - 1} \]
                                    8. lower--.f6425.7

                                      \[\leadsto \color{blue}{m - 1} \]
                                  5. Applied rewrites25.7%

                                    \[\leadsto \color{blue}{m - 1} \]
                                  6. Add Preprocessing

                                  Alternative 16: 25.2% accurate, 31.0× speedup?

                                  \[\begin{array}{l} \\ -1 \end{array} \]
                                  (FPCore (m v) :precision binary64 -1.0)
                                  double code(double m, double v) {
                                  	return -1.0;
                                  }
                                  
                                  real(8) function code(m, v)
                                      real(8), intent (in) :: m
                                      real(8), intent (in) :: v
                                      code = -1.0d0
                                  end function
                                  
                                  public static double code(double m, double v) {
                                  	return -1.0;
                                  }
                                  
                                  def code(m, v):
                                  	return -1.0
                                  
                                  function code(m, v)
                                  	return -1.0
                                  end
                                  
                                  function tmp = code(m, v)
                                  	tmp = -1.0;
                                  end
                                  
                                  code[m_, v_] := -1.0
                                  
                                  \begin{array}{l}
                                  
                                  \\
                                  -1
                                  \end{array}
                                  
                                  Derivation
                                  1. Initial program 99.9%

                                    \[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right) \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in m around 0

                                    \[\leadsto \color{blue}{-1} \]
                                  4. Step-by-step derivation
                                    1. Applied rewrites23.5%

                                      \[\leadsto \color{blue}{-1} \]
                                    2. Add Preprocessing

                                    Reproduce

                                    ?
                                    herbie shell --seed 2024240 
                                    (FPCore (m v)
                                      :name "b parameter of renormalized beta distribution"
                                      :precision binary64
                                      :pre (and (and (< 0.0 m) (< 0.0 v)) (< v 0.25))
                                      (* (- (/ (* m (- 1.0 m)) v) 1.0) (- 1.0 m)))