Henrywood and Agarwal, Equation (13)

Percentage Accurate: 24.9% → 45.8%
Time: 17.7s
Alternatives: 8
Speedup: 156.0×

Specification

?
\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \frac{c0}{2 \cdot w} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \end{array} \end{array} \]
(FPCore (c0 w h D d M)
 :precision binary64
 (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
   (* (/ c0 (* 2.0 w)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))))
double code(double c0, double w, double h, double D, double d, double M) {
	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
	return (c0 / (2.0 * w)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))));
}
real(8) function code(c0, w, h, d, d_1, m)
    real(8), intent (in) :: c0
    real(8), intent (in) :: w
    real(8), intent (in) :: h
    real(8), intent (in) :: d
    real(8), intent (in) :: d_1
    real(8), intent (in) :: m
    real(8) :: t_0
    t_0 = (c0 * (d_1 * d_1)) / ((w * h) * (d * d))
    code = (c0 / (2.0d0 * w)) * (t_0 + sqrt(((t_0 * t_0) - (m * m))))
end function
public static double code(double c0, double w, double h, double D, double d, double M) {
	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
	return (c0 / (2.0 * w)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))));
}
def code(c0, w, h, D, d, M):
	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
	return (c0 / (2.0 * w)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))
function code(c0, w, h, D, d, M)
	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
	return Float64(Float64(c0 / Float64(2.0 * w)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M)))))
end
function tmp = code(c0, w, h, D, d, M)
	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
	tmp = (c0 / (2.0 * w)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))));
end
code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(N[(c0 / N[(2.0 * w), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
\frac{c0}{2 \cdot w} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right)
\end{array}
\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 8 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: 24.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \frac{c0}{2 \cdot w} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \end{array} \end{array} \]
(FPCore (c0 w h D d M)
 :precision binary64
 (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
   (* (/ c0 (* 2.0 w)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))))
double code(double c0, double w, double h, double D, double d, double M) {
	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
	return (c0 / (2.0 * w)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))));
}
real(8) function code(c0, w, h, d, d_1, m)
    real(8), intent (in) :: c0
    real(8), intent (in) :: w
    real(8), intent (in) :: h
    real(8), intent (in) :: d
    real(8), intent (in) :: d_1
    real(8), intent (in) :: m
    real(8) :: t_0
    t_0 = (c0 * (d_1 * d_1)) / ((w * h) * (d * d))
    code = (c0 / (2.0d0 * w)) * (t_0 + sqrt(((t_0 * t_0) - (m * m))))
end function
public static double code(double c0, double w, double h, double D, double d, double M) {
	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
	return (c0 / (2.0 * w)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))));
}
def code(c0, w, h, D, d, M):
	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
	return (c0 / (2.0 * w)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))
function code(c0, w, h, D, d, M)
	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
	return Float64(Float64(c0 / Float64(2.0 * w)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M)))))
end
function tmp = code(c0, w, h, D, d, M)
	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
	tmp = (c0 / (2.0 * w)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))));
end
code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(N[(c0 / N[(2.0 * w), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
\frac{c0}{2 \cdot w} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right)
\end{array}
\end{array}

Alternative 1: 45.8% accurate, 1.9× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;w \leq -4100:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{c0}{w \cdot 2} \cdot \left(\frac{d}{D} \cdot \left(\frac{d}{D} \cdot \frac{c0 \cdot 2}{w \cdot h}\right)\right)\\ \end{array} \end{array} \]
(FPCore (c0 w h D d M)
 :precision binary64
 (if (<= w -4100.0)
   0.0
   (* (/ c0 (* w 2.0)) (* (/ d D) (* (/ d D) (/ (* c0 2.0) (* w h)))))))
double code(double c0, double w, double h, double D, double d, double M) {
	double tmp;
	if (w <= -4100.0) {
		tmp = 0.0;
	} else {
		tmp = (c0 / (w * 2.0)) * ((d / D) * ((d / D) * ((c0 * 2.0) / (w * h))));
	}
	return tmp;
}
real(8) function code(c0, w, h, d, d_1, m)
    real(8), intent (in) :: c0
    real(8), intent (in) :: w
    real(8), intent (in) :: h
    real(8), intent (in) :: d
    real(8), intent (in) :: d_1
    real(8), intent (in) :: m
    real(8) :: tmp
    if (w <= (-4100.0d0)) then
        tmp = 0.0d0
    else
        tmp = (c0 / (w * 2.0d0)) * ((d_1 / d) * ((d_1 / d) * ((c0 * 2.0d0) / (w * h))))
    end if
    code = tmp
end function
public static double code(double c0, double w, double h, double D, double d, double M) {
	double tmp;
	if (w <= -4100.0) {
		tmp = 0.0;
	} else {
		tmp = (c0 / (w * 2.0)) * ((d / D) * ((d / D) * ((c0 * 2.0) / (w * h))));
	}
	return tmp;
}
def code(c0, w, h, D, d, M):
	tmp = 0
	if w <= -4100.0:
		tmp = 0.0
	else:
		tmp = (c0 / (w * 2.0)) * ((d / D) * ((d / D) * ((c0 * 2.0) / (w * h))))
	return tmp
function code(c0, w, h, D, d, M)
	tmp = 0.0
	if (w <= -4100.0)
		tmp = 0.0;
	else
		tmp = Float64(Float64(c0 / Float64(w * 2.0)) * Float64(Float64(d / D) * Float64(Float64(d / D) * Float64(Float64(c0 * 2.0) / Float64(w * h)))));
	end
	return tmp
end
function tmp_2 = code(c0, w, h, D, d, M)
	tmp = 0.0;
	if (w <= -4100.0)
		tmp = 0.0;
	else
		tmp = (c0 / (w * 2.0)) * ((d / D) * ((d / D) * ((c0 * 2.0) / (w * h))));
	end
	tmp_2 = tmp;
end
code[c0_, w_, h_, D_, d_, M_] := If[LessEqual[w, -4100.0], 0.0, N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(N[(d / D), $MachinePrecision] * N[(N[(d / D), $MachinePrecision] * N[(N[(c0 * 2.0), $MachinePrecision] / N[(w * h), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;w \leq -4100:\\
\;\;\;\;0\\

\mathbf{else}:\\
\;\;\;\;\frac{c0}{w \cdot 2} \cdot \left(\frac{d}{D} \cdot \left(\frac{d}{D} \cdot \frac{c0 \cdot 2}{w \cdot h}\right)\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if w < -4100

    1. Initial program 12.8%

      \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
    2. Add Preprocessing
    3. Taylor expanded in c0 around -inf

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
    4. Step-by-step derivation
      1. associate-/l*N/A

        \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
      2. distribute-lft1-inN/A

        \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
      3. metadata-evalN/A

        \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
      4. mul0-lftN/A

        \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
      5. div0N/A

        \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
      6. mul0-rgtN/A

        \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
      7. metadata-eval48.6

        \[\leadsto \color{blue}{0} \]
    5. Applied rewrites48.6%

      \[\leadsto \color{blue}{0} \]

    if -4100 < w

    1. Initial program 28.1%

      \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
    2. Add Preprocessing
    3. Taylor expanded in c0 around inf

      \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\left(2 \cdot \frac{c0 \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)} \]
    4. Step-by-step derivation
      1. associate-*r/N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\frac{2 \cdot \left(c0 \cdot {d}^{2}\right)}{{D}^{2} \cdot \left(h \cdot w\right)}} \]
      2. lower-/.f64N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\frac{2 \cdot \left(c0 \cdot {d}^{2}\right)}{{D}^{2} \cdot \left(h \cdot w\right)}} \]
      3. lower-*.f64N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{\color{blue}{2 \cdot \left(c0 \cdot {d}^{2}\right)}}{{D}^{2} \cdot \left(h \cdot w\right)} \]
      4. lower-*.f64N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \color{blue}{\left(c0 \cdot {d}^{2}\right)}}{{D}^{2} \cdot \left(h \cdot w\right)} \]
      5. unpow2N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \left(c0 \cdot \color{blue}{\left(d \cdot d\right)}\right)}{{D}^{2} \cdot \left(h \cdot w\right)} \]
      6. lower-*.f64N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \left(c0 \cdot \color{blue}{\left(d \cdot d\right)}\right)}{{D}^{2} \cdot \left(h \cdot w\right)} \]
      7. lower-*.f64N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \left(c0 \cdot \left(d \cdot d\right)\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot w\right)}} \]
      8. unpow2N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \left(c0 \cdot \left(d \cdot d\right)\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot w\right)} \]
      9. lower-*.f64N/A

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \left(c0 \cdot \left(d \cdot d\right)\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot w\right)} \]
      10. lower-*.f6437.0

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \frac{2 \cdot \left(c0 \cdot \left(d \cdot d\right)\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot w\right)}} \]
    5. Applied rewrites37.0%

      \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\frac{2 \cdot \left(c0 \cdot \left(d \cdot d\right)\right)}{\left(D \cdot D\right) \cdot \left(h \cdot w\right)}} \]
    6. Step-by-step derivation
      1. Applied rewrites39.6%

        \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot 2}{w \cdot h} \cdot \color{blue}{\frac{d \cdot d}{D \cdot D}}\right) \]
      2. Step-by-step derivation
        1. Applied rewrites57.3%

          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{d}{D} \cdot \color{blue}{\left(\frac{d}{D} \cdot \frac{c0 \cdot 2}{w \cdot h}\right)}\right) \]
      3. Recombined 2 regimes into one program.
      4. Final simplification56.2%

        \[\leadsto \begin{array}{l} \mathbf{if}\;w \leq -4100:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{c0}{w \cdot 2} \cdot \left(\frac{d}{D} \cdot \left(\frac{d}{D} \cdot \frac{c0 \cdot 2}{w \cdot h}\right)\right)\\ \end{array} \]
      5. Add Preprocessing

      Alternative 2: 57.0% accurate, 0.7× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\left(c0 \cdot d\right) \cdot \frac{d \cdot \frac{c0}{h \cdot \left(w \cdot D\right)}}{w \cdot D}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \end{array} \]
      (FPCore (c0 w h D d M)
       :precision binary64
       (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
         (if (<=
              (* (/ c0 (* w 2.0)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))
              INFINITY)
           (* (* c0 d) (/ (* d (/ c0 (* h (* w D)))) (* w D)))
           0.0)))
      double code(double c0, double w, double h, double D, double d, double M) {
      	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
      	double tmp;
      	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= ((double) INFINITY)) {
      		tmp = (c0 * d) * ((d * (c0 / (h * (w * D)))) / (w * D));
      	} else {
      		tmp = 0.0;
      	}
      	return tmp;
      }
      
      public static double code(double c0, double w, double h, double D, double d, double M) {
      	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
      	double tmp;
      	if (((c0 / (w * 2.0)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))))) <= Double.POSITIVE_INFINITY) {
      		tmp = (c0 * d) * ((d * (c0 / (h * (w * D)))) / (w * D));
      	} else {
      		tmp = 0.0;
      	}
      	return tmp;
      }
      
      def code(c0, w, h, D, d, M):
      	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
      	tmp = 0
      	if ((c0 / (w * 2.0)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))) <= math.inf:
      		tmp = (c0 * d) * ((d * (c0 / (h * (w * D)))) / (w * D))
      	else:
      		tmp = 0.0
      	return tmp
      
      function code(c0, w, h, D, d, M)
      	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
      	tmp = 0.0
      	if (Float64(Float64(c0 / Float64(w * 2.0)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M))))) <= Inf)
      		tmp = Float64(Float64(c0 * d) * Float64(Float64(d * Float64(c0 / Float64(h * Float64(w * D)))) / Float64(w * D)));
      	else
      		tmp = 0.0;
      	end
      	return tmp
      end
      
      function tmp_2 = code(c0, w, h, D, d, M)
      	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
      	tmp = 0.0;
      	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= Inf)
      		tmp = (c0 * d) * ((d * (c0 / (h * (w * D)))) / (w * D));
      	else
      		tmp = 0.0;
      	end
      	tmp_2 = tmp;
      end
      
      code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(N[(c0 * d), $MachinePrecision] * N[(N[(d * N[(c0 / N[(h * N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.0]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
      \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\
      \;\;\;\;\left(c0 \cdot d\right) \cdot \frac{d \cdot \frac{c0}{h \cdot \left(w \cdot D\right)}}{w \cdot D}\\
      
      \mathbf{else}:\\
      \;\;\;\;0\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < +inf.0

        1. Initial program 79.8%

          \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
          2. lift-*.f64N/A

            \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \color{blue}{\left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
          3. associate-*r*N/A

            \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
          4. lower-*.f64N/A

            \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
          5. lower-*.f6478.8

            \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right)} \cdot D} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
        4. Applied rewrites78.8%

          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
        5. Taylor expanded in c0 around inf

          \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
        6. Step-by-step derivation
          1. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
          2. *-commutativeN/A

            \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
          3. lower-*.f64N/A

            \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
          4. unpow2N/A

            \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
          5. lower-*.f64N/A

            \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
          6. unpow2N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
          7. lower-*.f64N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
          8. lower-*.f64N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
          9. unpow2N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
          10. lower-*.f64N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
          11. lower-*.f64N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot {w}^{2}\right)}} \]
          12. unpow2N/A

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
          13. lower-*.f6458.6

            \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
        7. Applied rewrites58.6%

          \[\leadsto \color{blue}{\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}} \]
        8. Step-by-step derivation
          1. Applied rewrites81.4%

            \[\leadsto \left(c0 \cdot d\right) \cdot \color{blue}{\frac{c0 \cdot d}{\left(D \cdot w\right) \cdot \left(h \cdot \left(D \cdot w\right)\right)}} \]
          2. Step-by-step derivation
            1. Applied rewrites85.7%

              \[\leadsto \left(c0 \cdot d\right) \cdot \frac{d \cdot \frac{c0}{h \cdot \left(w \cdot D\right)}}{\color{blue}{w \cdot D}} \]

            if +inf.0 < (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))

            1. Initial program 0.0%

              \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
            2. Add Preprocessing
            3. Taylor expanded in c0 around -inf

              \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
            4. Step-by-step derivation
              1. associate-/l*N/A

                \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
              2. distribute-lft1-inN/A

                \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
              3. metadata-evalN/A

                \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
              4. mul0-lftN/A

                \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
              5. div0N/A

                \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
              6. mul0-rgtN/A

                \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
              7. metadata-eval38.1

                \[\leadsto \color{blue}{0} \]
            5. Applied rewrites38.1%

              \[\leadsto \color{blue}{0} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification53.7%

            \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\left(c0 \cdot d\right) \cdot \frac{d \cdot \frac{c0}{h \cdot \left(w \cdot D\right)}}{w \cdot D}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
          5. Add Preprocessing

          Alternative 3: 55.8% accurate, 0.7× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\ \;\;\;\;d \cdot \left(\left(c0 \cdot \frac{c0}{w \cdot D}\right) \cdot \frac{d}{h \cdot \left(w \cdot D\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \end{array} \]
          (FPCore (c0 w h D d M)
           :precision binary64
           (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
             (if (<=
                  (* (/ c0 (* w 2.0)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))
                  INFINITY)
               (* d (* (* c0 (/ c0 (* w D))) (/ d (* h (* w D)))))
               0.0)))
          double code(double c0, double w, double h, double D, double d, double M) {
          	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
          	double tmp;
          	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= ((double) INFINITY)) {
          		tmp = d * ((c0 * (c0 / (w * D))) * (d / (h * (w * D))));
          	} else {
          		tmp = 0.0;
          	}
          	return tmp;
          }
          
          public static double code(double c0, double w, double h, double D, double d, double M) {
          	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
          	double tmp;
          	if (((c0 / (w * 2.0)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))))) <= Double.POSITIVE_INFINITY) {
          		tmp = d * ((c0 * (c0 / (w * D))) * (d / (h * (w * D))));
          	} else {
          		tmp = 0.0;
          	}
          	return tmp;
          }
          
          def code(c0, w, h, D, d, M):
          	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
          	tmp = 0
          	if ((c0 / (w * 2.0)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))) <= math.inf:
          		tmp = d * ((c0 * (c0 / (w * D))) * (d / (h * (w * D))))
          	else:
          		tmp = 0.0
          	return tmp
          
          function code(c0, w, h, D, d, M)
          	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
          	tmp = 0.0
          	if (Float64(Float64(c0 / Float64(w * 2.0)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M))))) <= Inf)
          		tmp = Float64(d * Float64(Float64(c0 * Float64(c0 / Float64(w * D))) * Float64(d / Float64(h * Float64(w * D)))));
          	else
          		tmp = 0.0;
          	end
          	return tmp
          end
          
          function tmp_2 = code(c0, w, h, D, d, M)
          	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
          	tmp = 0.0;
          	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= Inf)
          		tmp = d * ((c0 * (c0 / (w * D))) * (d / (h * (w * D))));
          	else
          		tmp = 0.0;
          	end
          	tmp_2 = tmp;
          end
          
          code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(d * N[(N[(c0 * N[(c0 / N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(d / N[(h * N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.0]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
          \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\
          \;\;\;\;d \cdot \left(\left(c0 \cdot \frac{c0}{w \cdot D}\right) \cdot \frac{d}{h \cdot \left(w \cdot D\right)}\right)\\
          
          \mathbf{else}:\\
          \;\;\;\;0\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < +inf.0

            1. Initial program 79.8%

              \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
              2. lift-*.f64N/A

                \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \color{blue}{\left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
              3. associate-*r*N/A

                \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
              4. lower-*.f64N/A

                \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
              5. lower-*.f6478.8

                \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right)} \cdot D} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
            4. Applied rewrites78.8%

              \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
            5. Taylor expanded in c0 around inf

              \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
            6. Step-by-step derivation
              1. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
              2. *-commutativeN/A

                \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
              3. lower-*.f64N/A

                \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
              4. unpow2N/A

                \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
              5. lower-*.f64N/A

                \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
              6. unpow2N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
              7. lower-*.f64N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
              8. lower-*.f64N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
              9. unpow2N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
              10. lower-*.f64N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
              11. lower-*.f64N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot {w}^{2}\right)}} \]
              12. unpow2N/A

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
              13. lower-*.f6458.6

                \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
            7. Applied rewrites58.6%

              \[\leadsto \color{blue}{\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}} \]
            8. Step-by-step derivation
              1. Applied rewrites77.9%

                \[\leadsto d \cdot \color{blue}{\frac{c0 \cdot \left(c0 \cdot d\right)}{\left(D \cdot w\right) \cdot \left(h \cdot \left(D \cdot w\right)\right)}} \]
              2. Step-by-step derivation
                1. Applied rewrites82.3%

                  \[\leadsto d \cdot \left(\left(c0 \cdot \frac{c0}{w \cdot D}\right) \cdot \color{blue}{\frac{d}{h \cdot \left(w \cdot D\right)}}\right) \]

                if +inf.0 < (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))

                1. Initial program 0.0%

                  \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                2. Add Preprocessing
                3. Taylor expanded in c0 around -inf

                  \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
                4. Step-by-step derivation
                  1. associate-/l*N/A

                    \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
                  2. distribute-lft1-inN/A

                    \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
                  3. metadata-evalN/A

                    \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
                  4. mul0-lftN/A

                    \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
                  5. div0N/A

                    \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
                  6. mul0-rgtN/A

                    \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
                  7. metadata-eval38.1

                    \[\leadsto \color{blue}{0} \]
                5. Applied rewrites38.1%

                  \[\leadsto \color{blue}{0} \]
              3. Recombined 2 regimes into one program.
              4. Final simplification52.6%

                \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \leq \infty:\\ \;\;\;\;d \cdot \left(\left(c0 \cdot \frac{c0}{w \cdot D}\right) \cdot \frac{d}{h \cdot \left(w \cdot D\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
              5. Add Preprocessing

              Alternative 4: 56.2% accurate, 0.7× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\left(c0 \cdot d\right) \cdot \frac{c0 \cdot d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \end{array} \]
              (FPCore (c0 w h D d M)
               :precision binary64
               (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
                 (if (<=
                      (* (/ c0 (* w 2.0)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))
                      INFINITY)
                   (* (* c0 d) (/ (* c0 d) (* (* w D) (* h (* w D)))))
                   0.0)))
              double code(double c0, double w, double h, double D, double d, double M) {
              	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
              	double tmp;
              	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= ((double) INFINITY)) {
              		tmp = (c0 * d) * ((c0 * d) / ((w * D) * (h * (w * D))));
              	} else {
              		tmp = 0.0;
              	}
              	return tmp;
              }
              
              public static double code(double c0, double w, double h, double D, double d, double M) {
              	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
              	double tmp;
              	if (((c0 / (w * 2.0)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))))) <= Double.POSITIVE_INFINITY) {
              		tmp = (c0 * d) * ((c0 * d) / ((w * D) * (h * (w * D))));
              	} else {
              		tmp = 0.0;
              	}
              	return tmp;
              }
              
              def code(c0, w, h, D, d, M):
              	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
              	tmp = 0
              	if ((c0 / (w * 2.0)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))) <= math.inf:
              		tmp = (c0 * d) * ((c0 * d) / ((w * D) * (h * (w * D))))
              	else:
              		tmp = 0.0
              	return tmp
              
              function code(c0, w, h, D, d, M)
              	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
              	tmp = 0.0
              	if (Float64(Float64(c0 / Float64(w * 2.0)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M))))) <= Inf)
              		tmp = Float64(Float64(c0 * d) * Float64(Float64(c0 * d) / Float64(Float64(w * D) * Float64(h * Float64(w * D)))));
              	else
              		tmp = 0.0;
              	end
              	return tmp
              end
              
              function tmp_2 = code(c0, w, h, D, d, M)
              	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
              	tmp = 0.0;
              	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= Inf)
              		tmp = (c0 * d) * ((c0 * d) / ((w * D) * (h * (w * D))));
              	else
              		tmp = 0.0;
              	end
              	tmp_2 = tmp;
              end
              
              code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(N[(c0 * d), $MachinePrecision] * N[(N[(c0 * d), $MachinePrecision] / N[(N[(w * D), $MachinePrecision] * N[(h * N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.0]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
              \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\
              \;\;\;\;\left(c0 \cdot d\right) \cdot \frac{c0 \cdot d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\\
              
              \mathbf{else}:\\
              \;\;\;\;0\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < +inf.0

                1. Initial program 79.8%

                  \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-*.f64N/A

                    \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  2. lift-*.f64N/A

                    \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \color{blue}{\left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  3. associate-*r*N/A

                    \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  4. lower-*.f64N/A

                    \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  5. lower-*.f6478.8

                    \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right)} \cdot D} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                4. Applied rewrites78.8%

                  \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                5. Taylor expanded in c0 around inf

                  \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                6. Step-by-step derivation
                  1. lower-/.f64N/A

                    \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                  2. *-commutativeN/A

                    \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                  3. lower-*.f64N/A

                    \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                  4. unpow2N/A

                    \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                  5. lower-*.f64N/A

                    \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                  6. unpow2N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                  7. lower-*.f64N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                  8. lower-*.f64N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                  9. unpow2N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                  10. lower-*.f64N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                  11. lower-*.f64N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot {w}^{2}\right)}} \]
                  12. unpow2N/A

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                  13. lower-*.f6458.6

                    \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                7. Applied rewrites58.6%

                  \[\leadsto \color{blue}{\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}} \]
                8. Step-by-step derivation
                  1. Applied rewrites81.4%

                    \[\leadsto \left(c0 \cdot d\right) \cdot \color{blue}{\frac{c0 \cdot d}{\left(D \cdot w\right) \cdot \left(h \cdot \left(D \cdot w\right)\right)}} \]

                  if +inf.0 < (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))

                  1. Initial program 0.0%

                    \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  2. Add Preprocessing
                  3. Taylor expanded in c0 around -inf

                    \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
                  4. Step-by-step derivation
                    1. associate-/l*N/A

                      \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
                    2. distribute-lft1-inN/A

                      \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
                    3. metadata-evalN/A

                      \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
                    4. mul0-lftN/A

                      \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
                    5. div0N/A

                      \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
                    6. mul0-rgtN/A

                      \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
                    7. metadata-eval38.1

                      \[\leadsto \color{blue}{0} \]
                  5. Applied rewrites38.1%

                    \[\leadsto \color{blue}{0} \]
                9. Recombined 2 regimes into one program.
                10. Final simplification52.3%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\left(c0 \cdot d\right) \cdot \frac{c0 \cdot d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
                11. Add Preprocessing

                Alternative 5: 55.6% accurate, 0.7× speedup?

                \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\left(c0 \cdot d\right) \cdot \left(c0 \cdot \frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \end{array} \]
                (FPCore (c0 w h D d M)
                 :precision binary64
                 (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
                   (if (<=
                        (* (/ c0 (* w 2.0)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))
                        INFINITY)
                     (* (* c0 d) (* c0 (/ d (* (* w D) (* h (* w D))))))
                     0.0)))
                double code(double c0, double w, double h, double D, double d, double M) {
                	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                	double tmp;
                	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= ((double) INFINITY)) {
                		tmp = (c0 * d) * (c0 * (d / ((w * D) * (h * (w * D)))));
                	} else {
                		tmp = 0.0;
                	}
                	return tmp;
                }
                
                public static double code(double c0, double w, double h, double D, double d, double M) {
                	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                	double tmp;
                	if (((c0 / (w * 2.0)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))))) <= Double.POSITIVE_INFINITY) {
                		tmp = (c0 * d) * (c0 * (d / ((w * D) * (h * (w * D)))));
                	} else {
                		tmp = 0.0;
                	}
                	return tmp;
                }
                
                def code(c0, w, h, D, d, M):
                	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
                	tmp = 0
                	if ((c0 / (w * 2.0)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))) <= math.inf:
                		tmp = (c0 * d) * (c0 * (d / ((w * D) * (h * (w * D)))))
                	else:
                		tmp = 0.0
                	return tmp
                
                function code(c0, w, h, D, d, M)
                	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
                	tmp = 0.0
                	if (Float64(Float64(c0 / Float64(w * 2.0)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M))))) <= Inf)
                		tmp = Float64(Float64(c0 * d) * Float64(c0 * Float64(d / Float64(Float64(w * D) * Float64(h * Float64(w * D))))));
                	else
                		tmp = 0.0;
                	end
                	return tmp
                end
                
                function tmp_2 = code(c0, w, h, D, d, M)
                	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                	tmp = 0.0;
                	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= Inf)
                		tmp = (c0 * d) * (c0 * (d / ((w * D) * (h * (w * D)))));
                	else
                		tmp = 0.0;
                	end
                	tmp_2 = tmp;
                end
                
                code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(N[(c0 * d), $MachinePrecision] * N[(c0 * N[(d / N[(N[(w * D), $MachinePrecision] * N[(h * N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.0]]
                
                \begin{array}{l}
                
                \\
                \begin{array}{l}
                t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
                \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\
                \;\;\;\;\left(c0 \cdot d\right) \cdot \left(c0 \cdot \frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\right)\\
                
                \mathbf{else}:\\
                \;\;\;\;0\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 2 regimes
                2. if (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < +inf.0

                  1. Initial program 79.8%

                    \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-*.f64N/A

                      \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                    2. lift-*.f64N/A

                      \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \color{blue}{\left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                    3. associate-*r*N/A

                      \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                    4. lower-*.f64N/A

                      \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                    5. lower-*.f6478.8

                      \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right)} \cdot D} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  4. Applied rewrites78.8%

                    \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                  5. Taylor expanded in c0 around inf

                    \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                  6. Step-by-step derivation
                    1. lower-/.f64N/A

                      \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                    2. *-commutativeN/A

                      \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                    3. lower-*.f64N/A

                      \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                    4. unpow2N/A

                      \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                    5. lower-*.f64N/A

                      \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                    6. unpow2N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                    7. lower-*.f64N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                    8. lower-*.f64N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                    9. unpow2N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                    10. lower-*.f64N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                    11. lower-*.f64N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot {w}^{2}\right)}} \]
                    12. unpow2N/A

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                    13. lower-*.f6458.6

                      \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                  7. Applied rewrites58.6%

                    \[\leadsto \color{blue}{\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}} \]
                  8. Step-by-step derivation
                    1. Applied rewrites81.4%

                      \[\leadsto \left(c0 \cdot d\right) \cdot \color{blue}{\frac{c0 \cdot d}{\left(D \cdot w\right) \cdot \left(h \cdot \left(D \cdot w\right)\right)}} \]
                    2. Step-by-step derivation
                      1. Applied rewrites80.3%

                        \[\leadsto \left(c0 \cdot d\right) \cdot \left(\frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)} \cdot \color{blue}{c0}\right) \]

                      if +inf.0 < (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))

                      1. Initial program 0.0%

                        \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                      2. Add Preprocessing
                      3. Taylor expanded in c0 around -inf

                        \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
                      4. Step-by-step derivation
                        1. associate-/l*N/A

                          \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
                        2. distribute-lft1-inN/A

                          \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
                        3. metadata-evalN/A

                          \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
                        4. mul0-lftN/A

                          \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
                        5. div0N/A

                          \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
                        6. mul0-rgtN/A

                          \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
                        7. metadata-eval38.1

                          \[\leadsto \color{blue}{0} \]
                      5. Applied rewrites38.1%

                        \[\leadsto \color{blue}{0} \]
                    3. Recombined 2 regimes into one program.
                    4. Final simplification52.0%

                      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\left(c0 \cdot d\right) \cdot \left(c0 \cdot \frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
                    5. Add Preprocessing

                    Alternative 6: 55.4% accurate, 0.7× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\ \;\;\;\;c0 \cdot \left(\left(c0 \cdot d\right) \cdot \frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \end{array} \]
                    (FPCore (c0 w h D d M)
                     :precision binary64
                     (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
                       (if (<=
                            (* (/ c0 (* w 2.0)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))
                            INFINITY)
                         (* c0 (* (* c0 d) (/ d (* (* w D) (* h (* w D))))))
                         0.0)))
                    double code(double c0, double w, double h, double D, double d, double M) {
                    	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                    	double tmp;
                    	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= ((double) INFINITY)) {
                    		tmp = c0 * ((c0 * d) * (d / ((w * D) * (h * (w * D)))));
                    	} else {
                    		tmp = 0.0;
                    	}
                    	return tmp;
                    }
                    
                    public static double code(double c0, double w, double h, double D, double d, double M) {
                    	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                    	double tmp;
                    	if (((c0 / (w * 2.0)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))))) <= Double.POSITIVE_INFINITY) {
                    		tmp = c0 * ((c0 * d) * (d / ((w * D) * (h * (w * D)))));
                    	} else {
                    		tmp = 0.0;
                    	}
                    	return tmp;
                    }
                    
                    def code(c0, w, h, D, d, M):
                    	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
                    	tmp = 0
                    	if ((c0 / (w * 2.0)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))) <= math.inf:
                    		tmp = c0 * ((c0 * d) * (d / ((w * D) * (h * (w * D)))))
                    	else:
                    		tmp = 0.0
                    	return tmp
                    
                    function code(c0, w, h, D, d, M)
                    	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
                    	tmp = 0.0
                    	if (Float64(Float64(c0 / Float64(w * 2.0)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M))))) <= Inf)
                    		tmp = Float64(c0 * Float64(Float64(c0 * d) * Float64(d / Float64(Float64(w * D) * Float64(h * Float64(w * D))))));
                    	else
                    		tmp = 0.0;
                    	end
                    	return tmp
                    end
                    
                    function tmp_2 = code(c0, w, h, D, d, M)
                    	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                    	tmp = 0.0;
                    	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= Inf)
                    		tmp = c0 * ((c0 * d) * (d / ((w * D) * (h * (w * D)))));
                    	else
                    		tmp = 0.0;
                    	end
                    	tmp_2 = tmp;
                    end
                    
                    code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(c0 * N[(N[(c0 * d), $MachinePrecision] * N[(d / N[(N[(w * D), $MachinePrecision] * N[(h * N[(w * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.0]]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
                    \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\
                    \;\;\;\;c0 \cdot \left(\left(c0 \cdot d\right) \cdot \frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\right)\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;0\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < +inf.0

                      1. Initial program 79.8%

                        \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. lift-*.f64N/A

                          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                        2. lift-*.f64N/A

                          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \color{blue}{\left(D \cdot D\right)}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                        3. associate-*r*N/A

                          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                        4. lower-*.f64N/A

                          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                        5. lower-*.f6478.8

                          \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right)} \cdot D} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                      4. Applied rewrites78.8%

                        \[\leadsto \frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\color{blue}{\left(\left(w \cdot h\right) \cdot D\right) \cdot D}} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                      5. Taylor expanded in c0 around inf

                        \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                      6. Step-by-step derivation
                        1. lower-/.f64N/A

                          \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                        2. *-commutativeN/A

                          \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                        3. lower-*.f64N/A

                          \[\leadsto \frac{\color{blue}{{d}^{2} \cdot {c0}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                        4. unpow2N/A

                          \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                        5. lower-*.f64N/A

                          \[\leadsto \frac{\color{blue}{\left(d \cdot d\right)} \cdot {c0}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                        6. unpow2N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                        7. lower-*.f64N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \color{blue}{\left(c0 \cdot c0\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                        8. lower-*.f64N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                        9. unpow2N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                        10. lower-*.f64N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                        11. lower-*.f64N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot {w}^{2}\right)}} \]
                        12. unpow2N/A

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                        13. lower-*.f6458.6

                          \[\leadsto \frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                      7. Applied rewrites58.6%

                        \[\leadsto \color{blue}{\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}} \]
                      8. Step-by-step derivation
                        1. Applied rewrites81.4%

                          \[\leadsto \left(c0 \cdot d\right) \cdot \color{blue}{\frac{c0 \cdot d}{\left(D \cdot w\right) \cdot \left(h \cdot \left(D \cdot w\right)\right)}} \]
                        2. Step-by-step derivation
                          1. Applied rewrites80.3%

                            \[\leadsto c0 \cdot \color{blue}{\left(\frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)} \cdot \left(c0 \cdot d\right)\right)} \]

                          if +inf.0 < (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))

                          1. Initial program 0.0%

                            \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                          2. Add Preprocessing
                          3. Taylor expanded in c0 around -inf

                            \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
                          4. Step-by-step derivation
                            1. associate-/l*N/A

                              \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
                            2. distribute-lft1-inN/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
                            3. metadata-evalN/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
                            4. mul0-lftN/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
                            5. div0N/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
                            6. mul0-rgtN/A

                              \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
                            7. metadata-eval38.1

                              \[\leadsto \color{blue}{0} \]
                          5. Applied rewrites38.1%

                            \[\leadsto \color{blue}{0} \]
                        3. Recombined 2 regimes into one program.
                        4. Final simplification51.9%

                          \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \leq \infty:\\ \;\;\;\;c0 \cdot \left(\left(c0 \cdot d\right) \cdot \frac{d}{\left(w \cdot D\right) \cdot \left(h \cdot \left(w \cdot D\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
                        5. Add Preprocessing

                        Alternative 7: 48.8% accurate, 0.7× speedup?

                        \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\ \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \end{array} \]
                        (FPCore (c0 w h D d M)
                         :precision binary64
                         (let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
                           (if (<=
                                (* (/ c0 (* w 2.0)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M)))))
                                INFINITY)
                             (/ (* (* d d) (* c0 c0)) (* (* D D) (* h (* w w))))
                             0.0)))
                        double code(double c0, double w, double h, double D, double d, double M) {
                        	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                        	double tmp;
                        	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= ((double) INFINITY)) {
                        		tmp = ((d * d) * (c0 * c0)) / ((D * D) * (h * (w * w)));
                        	} else {
                        		tmp = 0.0;
                        	}
                        	return tmp;
                        }
                        
                        public static double code(double c0, double w, double h, double D, double d, double M) {
                        	double t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                        	double tmp;
                        	if (((c0 / (w * 2.0)) * (t_0 + Math.sqrt(((t_0 * t_0) - (M * M))))) <= Double.POSITIVE_INFINITY) {
                        		tmp = ((d * d) * (c0 * c0)) / ((D * D) * (h * (w * w)));
                        	} else {
                        		tmp = 0.0;
                        	}
                        	return tmp;
                        }
                        
                        def code(c0, w, h, D, d, M):
                        	t_0 = (c0 * (d * d)) / ((w * h) * (D * D))
                        	tmp = 0
                        	if ((c0 / (w * 2.0)) * (t_0 + math.sqrt(((t_0 * t_0) - (M * M))))) <= math.inf:
                        		tmp = ((d * d) * (c0 * c0)) / ((D * D) * (h * (w * w)))
                        	else:
                        		tmp = 0.0
                        	return tmp
                        
                        function code(c0, w, h, D, d, M)
                        	t_0 = Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))
                        	tmp = 0.0
                        	if (Float64(Float64(c0 / Float64(w * 2.0)) * Float64(t_0 + sqrt(Float64(Float64(t_0 * t_0) - Float64(M * M))))) <= Inf)
                        		tmp = Float64(Float64(Float64(d * d) * Float64(c0 * c0)) / Float64(Float64(D * D) * Float64(h * Float64(w * w))));
                        	else
                        		tmp = 0.0;
                        	end
                        	return tmp
                        end
                        
                        function tmp_2 = code(c0, w, h, D, d, M)
                        	t_0 = (c0 * (d * d)) / ((w * h) * (D * D));
                        	tmp = 0.0;
                        	if (((c0 / (w * 2.0)) * (t_0 + sqrt(((t_0 * t_0) - (M * M))))) <= Inf)
                        		tmp = ((d * d) * (c0 * c0)) / ((D * D) * (h * (w * w)));
                        	else
                        		tmp = 0.0;
                        	end
                        	tmp_2 = tmp;
                        end
                        
                        code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(c0 / N[(w * 2.0), $MachinePrecision]), $MachinePrecision] * N[(t$95$0 + N[Sqrt[N[(N[(t$95$0 * t$95$0), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(N[(N[(d * d), $MachinePrecision] * N[(c0 * c0), $MachinePrecision]), $MachinePrecision] / N[(N[(D * D), $MachinePrecision] * N[(h * N[(w * w), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.0]]
                        
                        \begin{array}{l}
                        
                        \\
                        \begin{array}{l}
                        t_0 := \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)}\\
                        \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(t\_0 + \sqrt{t\_0 \cdot t\_0 - M \cdot M}\right) \leq \infty:\\
                        \;\;\;\;\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}\\
                        
                        \mathbf{else}:\\
                        \;\;\;\;0\\
                        
                        
                        \end{array}
                        \end{array}
                        
                        Derivation
                        1. Split input into 2 regimes
                        2. if (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < +inf.0

                          1. Initial program 79.8%

                            \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                          2. Add Preprocessing
                          3. Taylor expanded in c0 around inf

                            \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                          4. Step-by-step derivation
                            1. lower-/.f64N/A

                              \[\leadsto \color{blue}{\frac{{c0}^{2} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                            2. lower-*.f64N/A

                              \[\leadsto \frac{\color{blue}{{c0}^{2} \cdot {d}^{2}}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                            3. unpow2N/A

                              \[\leadsto \frac{\color{blue}{\left(c0 \cdot c0\right)} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                            4. lower-*.f64N/A

                              \[\leadsto \frac{\color{blue}{\left(c0 \cdot c0\right)} \cdot {d}^{2}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                            5. unpow2N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \color{blue}{\left(d \cdot d\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                            6. lower-*.f64N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \color{blue}{\left(d \cdot d\right)}}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)} \]
                            7. lower-*.f64N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\color{blue}{{D}^{2} \cdot \left(h \cdot {w}^{2}\right)}} \]
                            8. unpow2N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                            9. lower-*.f64N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\color{blue}{\left(D \cdot D\right)} \cdot \left(h \cdot {w}^{2}\right)} \]
                            10. lower-*.f64N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \color{blue}{\left(h \cdot {w}^{2}\right)}} \]
                            11. unpow2N/A

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                            12. lower-*.f6458.6

                              \[\leadsto \frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \color{blue}{\left(w \cdot w\right)}\right)} \]
                          5. Applied rewrites58.6%

                            \[\leadsto \color{blue}{\frac{\left(c0 \cdot c0\right) \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}} \]

                          if +inf.0 < (*.f64 (/.f64 c0 (*.f64 #s(literal 2 binary64) w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))

                          1. Initial program 0.0%

                            \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                          2. Add Preprocessing
                          3. Taylor expanded in c0 around -inf

                            \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
                          4. Step-by-step derivation
                            1. associate-/l*N/A

                              \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
                            2. distribute-lft1-inN/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
                            3. metadata-evalN/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
                            4. mul0-lftN/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
                            5. div0N/A

                              \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
                            6. mul0-rgtN/A

                              \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
                            7. metadata-eval38.1

                              \[\leadsto \color{blue}{0} \]
                          5. Applied rewrites38.1%

                            \[\leadsto \color{blue}{0} \]
                        3. Recombined 2 regimes into one program.
                        4. Final simplification44.8%

                          \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{w \cdot 2} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \leq \infty:\\ \;\;\;\;\frac{\left(d \cdot d\right) \cdot \left(c0 \cdot c0\right)}{\left(D \cdot D\right) \cdot \left(h \cdot \left(w \cdot w\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
                        5. Add Preprocessing

                        Alternative 8: 33.4% accurate, 156.0× speedup?

                        \[\begin{array}{l} \\ 0 \end{array} \]
                        (FPCore (c0 w h D d M) :precision binary64 0.0)
                        double code(double c0, double w, double h, double D, double d, double M) {
                        	return 0.0;
                        }
                        
                        real(8) function code(c0, w, h, d, d_1, m)
                            real(8), intent (in) :: c0
                            real(8), intent (in) :: w
                            real(8), intent (in) :: h
                            real(8), intent (in) :: d
                            real(8), intent (in) :: d_1
                            real(8), intent (in) :: m
                            code = 0.0d0
                        end function
                        
                        public static double code(double c0, double w, double h, double D, double d, double M) {
                        	return 0.0;
                        }
                        
                        def code(c0, w, h, D, d, M):
                        	return 0.0
                        
                        function code(c0, w, h, D, d, M)
                        	return 0.0
                        end
                        
                        function tmp = code(c0, w, h, D, d, M)
                        	tmp = 0.0;
                        end
                        
                        code[c0_, w_, h_, D_, d_, M_] := 0.0
                        
                        \begin{array}{l}
                        
                        \\
                        0
                        \end{array}
                        
                        Derivation
                        1. Initial program 26.2%

                          \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \]
                        2. Add Preprocessing
                        3. Taylor expanded in c0 around -inf

                          \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{{c0}^{2} \cdot \left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}\right)}{w}} \]
                        4. Step-by-step derivation
                          1. associate-/l*N/A

                            \[\leadsto \frac{-1}{2} \cdot \color{blue}{\left({c0}^{2} \cdot \frac{-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)} + \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right)} \]
                          2. distribute-lft1-inN/A

                            \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}}{w}\right) \]
                          3. metadata-evalN/A

                            \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0} \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(h \cdot w\right)}}{w}\right) \]
                          4. mul0-lftN/A

                            \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \frac{\color{blue}{0}}{w}\right) \]
                          5. div0N/A

                            \[\leadsto \frac{-1}{2} \cdot \left({c0}^{2} \cdot \color{blue}{0}\right) \]
                          6. mul0-rgtN/A

                            \[\leadsto \frac{-1}{2} \cdot \color{blue}{0} \]
                          7. metadata-eval28.3

                            \[\leadsto \color{blue}{0} \]
                        5. Applied rewrites28.3%

                          \[\leadsto \color{blue}{0} \]
                        6. Add Preprocessing

                        Reproduce

                        ?
                        herbie shell --seed 2024226 
                        (FPCore (c0 w h D d M)
                          :name "Henrywood and Agarwal, Equation (13)"
                          :precision binary64
                          (* (/ c0 (* 2.0 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M))))))