Henrywood and Agarwal, Equation (13)

Average Error: 59.6 → 25.7

Time: 46.6s

Precision: binary64

Cost: 75672

Math

\[\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) \]

↓

\[\begin{array}{l} t_0 := \frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h}\\ t_1 := \frac{0}{w} \cdot \left(c0 \cdot c0\right)\\ t_2 := \sqrt[3]{\left(w \cdot 2\right) \cdot \frac{t_0 - \sqrt{{t_0}^{2} - M \cdot M}}{c0}}\\ t_3 := \mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, t_1\right)\\ t_4 := \frac{{\left(M \cdot D\right)}^{2}}{d}\\ \mathbf{if}\;c0 \leq -2.8 \cdot 10^{+108}:\\ \;\;\;\;\frac{M}{\frac{{\left(\frac{\frac{d}{D}}{\sqrt{w \cdot h}}\right)}^{2} \cdot \left(c0 \cdot \left(w \cdot -4\right)\right)}{M}} \cdot \left(-c0\right)\\ \mathbf{elif}\;c0 \leq -1.05 \cdot 10^{-158}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;c0 \leq 5.5 \cdot 10^{-26}:\\ \;\;\;\;\mathsf{fma}\left(0.25, \frac{h \cdot t_4}{d}, t_1\right)\\ \mathbf{elif}\;c0 \leq 1.45 \cdot 10^{-9}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;c0 \leq 5:\\ \;\;\;\;\mathsf{fma}\left(0.25, t_4 \cdot \left(h \cdot \frac{1}{d}\right), t_1\right)\\ \mathbf{elif}\;c0 \leq 1.32 \cdot 10^{+154}:\\ \;\;\;\;t_3\\ \mathbf{else}:\\ \;\;\;\;\frac{M}{{t_2}^{2}} \cdot \frac{M}{t_2}\\ \end{array} \]

FPCore

(FPCore (c0 w h D d M)
 :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))))))

↓

(FPCore (c0 w h D d M)
 :precision binary64
 (let* ((t_0 (* (/ c0 w) (/ (pow (/ d D) 2.0) h)))
        (t_1 (* (/ 0.0 w) (* c0 c0)))
        (t_2
         (cbrt (* (* w 2.0) (/ (- t_0 (sqrt (- (pow t_0 2.0) (* M M)))) c0))))
        (t_3 (fma 0.25 (* h (pow (* M (/ D d)) 2.0)) t_1))
        (t_4 (/ (pow (* M D) 2.0) d)))
   (if (<= c0 -2.8e+108)
     (*
      (/ M (/ (* (pow (/ (/ d D) (sqrt (* w h))) 2.0) (* c0 (* w -4.0))) M))
      (- c0))
     (if (<= c0 -1.05e-158)
       t_3
       (if (<= c0 5.5e-26)
         (fma 0.25 (/ (* h t_4) d) t_1)
         (if (<= c0 1.45e-9)
           (* (/ (/ c0 2.0) w) (* 2.0 (* c0 (* (/ (/ d D) w) (/ (/ d D) h)))))
           (if (<= c0 5.0)
             (fma 0.25 (* t_4 (* h (/ 1.0 d))) t_1)
             (if (<= c0 1.32e+154)
               t_3
               (* (/ M (pow t_2 2.0)) (/ M t_2))))))))))

C

double code(double c0, double w, double h, double D, double d, double M) {
	return (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))));
}

↓

double code(double c0, double w, double h, double D, double d, double M) {
	double t_0 = (c0 / w) * (pow((d / D), 2.0) / h);
	double t_1 = (0.0 / w) * (c0 * c0);
	double t_2 = cbrt(((w * 2.0) * ((t_0 - sqrt((pow(t_0, 2.0) - (M * M)))) / c0)));
	double t_3 = fma(0.25, (h * pow((M * (D / d)), 2.0)), t_1);
	double t_4 = pow((M * D), 2.0) / d;
	double tmp;
	if (c0 <= -2.8e+108) {
		tmp = (M / ((pow(((d / D) / sqrt((w * h))), 2.0) * (c0 * (w * -4.0))) / M)) * -c0;
	} else if (c0 <= -1.05e-158) {
		tmp = t_3;
	} else if (c0 <= 5.5e-26) {
		tmp = fma(0.25, ((h * t_4) / d), t_1);
	} else if (c0 <= 1.45e-9) {
		tmp = ((c0 / 2.0) / w) * (2.0 * (c0 * (((d / D) / w) * ((d / D) / h))));
	} else if (c0 <= 5.0) {
		tmp = fma(0.25, (t_4 * (h * (1.0 / d))), t_1);
	} else if (c0 <= 1.32e+154) {
		tmp = t_3;
	} else {
		tmp = (M / pow(t_2, 2.0)) * (M / t_2);
	}
	return tmp;
}

Julia

function code(c0, w, h, D, d, M)
	return Float64(Float64(c0 / Float64(2.0 * w)) * Float64(Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D))) + sqrt(Float64(Float64(Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D))) * Float64(Float64(c0 * Float64(d * d)) / Float64(Float64(w * h) * Float64(D * D)))) - Float64(M * M)))))
end

↓

function code(c0, w, h, D, d, M)
	t_0 = Float64(Float64(c0 / w) * Float64((Float64(d / D) ^ 2.0) / h))
	t_1 = Float64(Float64(0.0 / w) * Float64(c0 * c0))
	t_2 = cbrt(Float64(Float64(w * 2.0) * Float64(Float64(t_0 - sqrt(Float64((t_0 ^ 2.0) - Float64(M * M)))) / c0)))
	t_3 = fma(0.25, Float64(h * (Float64(M * Float64(D / d)) ^ 2.0)), t_1)
	t_4 = Float64((Float64(M * D) ^ 2.0) / d)
	tmp = 0.0
	if (c0 <= -2.8e+108)
		tmp = Float64(Float64(M / Float64(Float64((Float64(Float64(d / D) / sqrt(Float64(w * h))) ^ 2.0) * Float64(c0 * Float64(w * -4.0))) / M)) * Float64(-c0));
	elseif (c0 <= -1.05e-158)
		tmp = t_3;
	elseif (c0 <= 5.5e-26)
		tmp = fma(0.25, Float64(Float64(h * t_4) / d), t_1);
	elseif (c0 <= 1.45e-9)
		tmp = Float64(Float64(Float64(c0 / 2.0) / w) * Float64(2.0 * Float64(c0 * Float64(Float64(Float64(d / D) / w) * Float64(Float64(d / D) / h)))));
	elseif (c0 <= 5.0)
		tmp = fma(0.25, Float64(t_4 * Float64(h * Float64(1.0 / d))), t_1);
	elseif (c0 <= 1.32e+154)
		tmp = t_3;
	else
		tmp = Float64(Float64(M / (t_2 ^ 2.0)) * Float64(M / t_2));
	end
	return tmp
end

Wolfram

code[c0_, w_, h_, D_, d_, M_] := N[(N[(c0 / N[(2.0 * w), $MachinePrecision]), $MachinePrecision] * N[(N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[Sqrt[N[(N[(N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[(c0 * N[(d * d), $MachinePrecision]), $MachinePrecision] / N[(N[(w * h), $MachinePrecision] * N[(D * D), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[c0_, w_, h_, D_, d_, M_] := Block[{t$95$0 = N[(N[(c0 / w), $MachinePrecision] * N[(N[Power[N[(d / D), $MachinePrecision], 2.0], $MachinePrecision] / h), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(0.0 / w), $MachinePrecision] * N[(c0 * c0), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[Power[N[(N[(w * 2.0), $MachinePrecision] * N[(N[(t$95$0 - N[Sqrt[N[(N[Power[t$95$0, 2.0], $MachinePrecision] - N[(M * M), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / c0), $MachinePrecision]), $MachinePrecision], 1/3], $MachinePrecision]}, Block[{t$95$3 = N[(0.25 * N[(h * N[Power[N[(M * N[(D / d), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision]}, Block[{t$95$4 = N[(N[Power[N[(M * D), $MachinePrecision], 2.0], $MachinePrecision] / d), $MachinePrecision]}, If[LessEqual[c0, -2.8e+108], N[(N[(M / N[(N[(N[Power[N[(N[(d / D), $MachinePrecision] / N[Sqrt[N[(w * h), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] * N[(c0 * N[(w * -4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / M), $MachinePrecision]), $MachinePrecision] * (-c0)), $MachinePrecision], If[LessEqual[c0, -1.05e-158], t$95$3, If[LessEqual[c0, 5.5e-26], N[(0.25 * N[(N[(h * t$95$4), $MachinePrecision] / d), $MachinePrecision] + t$95$1), $MachinePrecision], If[LessEqual[c0, 1.45e-9], N[(N[(N[(c0 / 2.0), $MachinePrecision] / w), $MachinePrecision] * N[(2.0 * N[(c0 * N[(N[(N[(d / D), $MachinePrecision] / w), $MachinePrecision] * N[(N[(d / D), $MachinePrecision] / h), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[c0, 5.0], N[(0.25 * N[(t$95$4 * N[(h * N[(1.0 / d), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision], If[LessEqual[c0, 1.32e+154], t$95$3, N[(N[(M / N[Power[t$95$2, 2.0], $MachinePrecision]), $MachinePrecision] * N[(M / t$95$2), $MachinePrecision]), $MachinePrecision]]]]]]]]]]]]

Derivation

1. Split input into 6 regimes

2. if c0 < -2.7999999999999998e108

   1. Initial program 61.5

      \[\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. Applied egg-rr 62.8

      \[\leadsto \color{blue}{\frac{{\left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)}\right)}^{2} - \left({\left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)}\right)}^{2} - M \cdot M\right)}{\left(2 \cdot \frac{w}{c0}\right) \cdot \left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)} - \sqrt{{\left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)}\right)}^{2} - M \cdot M}\right)}} \]

   3. Simplified 46.8

      \[\leadsto \color{blue}{\frac{0 + M \cdot M}{c0 \cdot \left(d \cdot \frac{\frac{\frac{d}{D}}{D}}{w \cdot h}\right) - \sqrt{{\left(c0 \cdot \left(d \cdot \frac{\frac{\frac{d}{D}}{D}}{w \cdot h}\right)\right)}^{2} - M \cdot M}} \cdot \frac{c0}{\frac{w}{0.5}}} \]
      Proof
      (*.f64 (/.f64 (+.f64 0 (*.f64 M M)) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (Rewrite<= +-inverses_binary64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2))) (*.f64 M M)) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 105 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2)) (Rewrite<= unpow2_binary64 (pow.f64 M 2))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (pow.f64 M 2)))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (Rewrite=> unpow2_binary64 (*.f64 M M)))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 D D))) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 (*.f64 D D) (*.f64 w h)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite<= associate-*r*_binary64 (*.f64 w (*.f64 h (*.f64 D D))))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 d 1)) (*.f64 w (*.f64 h (*.f64 D D)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-*r/_binary64 (*.f64 d (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 d d) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D))))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c0 (*.f64 d d)) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 c0 (*.f64 d d)) 1) (*.f64 w (*.f64 h (*.f64 D D))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (/.f64 (Rewrite=> *-rgt-identity_binary64 (*.f64 c0 (*.f64 d d))) (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (*.f64 c0 (*.f64 d d)) w) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 c0 w) (*.f64 d d))) (*.f64 h (*.f64 D D))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 D D))) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 4 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 (*.f64 D D) (*.f64 w h)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite<= associate-*r*_binary64 (*.f64 w (*.f64 h (*.f64 D D))))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 3 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 d 1)) (*.f64 w (*.f64 h (*.f64 D D)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-*r/_binary64 (*.f64 d (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 d d) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D))))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 5 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c0 (*.f64 d d)) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 c0 (*.f64 d d)) 1) (*.f64 w (*.f64 h (*.f64 D D))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 (Rewrite=> *-rgt-identity_binary64 (*.f64 c0 (*.f64 d d))) (*.f64 w (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (*.f64 c0 (*.f64 d d)) w) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 c0 w) (*.f64 d d))) (*.f64 h (*.f64 D D))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 3 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c0 1/2) w))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 1/2 c0)) w)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (Rewrite=> associate-/l*_binary64 (/.f64 1/2 (/.f64 w c0)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) (/.f64 w c0))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 2 (/.f64 w c0))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) 1) (*.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M)))) (*.f64 2 (/.f64 w c0))))): 1 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> *-rgt-identity_binary64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M)))) (*.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M)))) (*.f64 2 (/.f64 w c0)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 2 (/.f64 w c0)) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))))): 0 points increase in error, 0 points decrease in error

   4. Taylor expanded in c0 around -inf 49.6

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{{M}^{2}}{\left(-1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)} - \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)}\right) \cdot c0}\right)} \cdot \frac{c0}{\frac{w}{0.5}} \]

   5. Simplified 48.7

      \[\leadsto \color{blue}{\frac{M \cdot \left(-M\right)}{c0 \cdot \left(\frac{d \cdot d}{D \cdot \left(D \cdot \left(w \cdot h\right)\right)} \cdot -2\right)}} \cdot \frac{c0}{\frac{w}{0.5}} \]
      Proof
      (/.f64 (*.f64 M (neg.f64 M)) (*.f64 c0 (*.f64 (/.f64 (*.f64 d d) (*.f64 D (*.f64 D (*.f64 w h)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 M M))) (*.f64 c0 (*.f64 (/.f64 (*.f64 d d) (*.f64 D (*.f64 D (*.f64 w h)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 M M))) (*.f64 c0 (*.f64 (/.f64 (*.f64 d d) (*.f64 D (*.f64 D (*.f64 w h)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (*.f64 D (*.f64 D (*.f64 w h)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (pow.f64 d 2) (*.f64 D (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 w h) D)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (pow.f64 d 2) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (*.f64 w h) D) D))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (pow.f64 d 2) (Rewrite=> associate-*l*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))) -2))): 16 points increase in error, 4 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (pow.f64 d 2) (*.f64 (*.f64 w h) (Rewrite<= unpow2_binary64 (pow.f64 D 2)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (pow.f64 d 2) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 D 2) (*.f64 w h)))) -2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (*.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (Rewrite<= metadata-eval (+.f64 -1 -1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (+.f64 (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (Rewrite=> mul-1-neg_binary64 (neg.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (*.f64 c0 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (*.f64 M M)) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) c0))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 M M) (*.f64 (-.f64 (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) c0)))): 0 points increase in error, 0 points decrease in error
      (*.f64 -1 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 M 2)) (*.f64 (-.f64 (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) c0))): 0 points increase in error, 0 points decrease in error

   6. Applied egg-rr 37.7

      \[\leadsto \color{blue}{\frac{\left(M \cdot M\right) \cdot \left(-c0\right)}{\left(\left({\left(\frac{d}{D \cdot \sqrt{w \cdot h}}\right)}^{2} \cdot c0\right) \cdot 2\right) \cdot \left(w \cdot -2\right)}} \]

   7. Simplified 32.3

      \[\leadsto \color{blue}{\frac{M}{\frac{{\left(\frac{\frac{d}{D}}{\sqrt{w \cdot h}}\right)}^{2} \cdot \left(\left(-4 \cdot w\right) \cdot c0\right)}{M}} \cdot \left(-c0\right)} \]
      Proof
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (/.f64 (/.f64 d D) (sqrt.f64 (*.f64 w h))) 2) (*.f64 (*.f64 -4 w) c0)) M)) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h))))) 2) (*.f64 (*.f64 -4 w) c0)) M)) (neg.f64 c0)): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 (*.f64 (Rewrite<= metadata-eval (*.f64 -2 2)) w) c0)) M)) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -2 (*.f64 2 w))) c0)) M)) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 (*.f64 -2 (Rewrite<= *-commutative_binary64 (*.f64 w 2))) c0)) M)) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (Rewrite<= associate-*r*_binary64 (*.f64 -2 (*.f64 (*.f64 w 2) c0)))) M)) (neg.f64 c0)): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (/.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 -2 (Rewrite<= *-commutative_binary64 (*.f64 c0 (*.f64 w 2))))) M)) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) -2) (*.f64 c0 (*.f64 w 2)))) M)) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 M M) (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) -2) (*.f64 c0 (*.f64 w 2))))) (neg.f64 c0)): 18 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 -2 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2))) (*.f64 c0 (*.f64 w 2)))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (Rewrite=> associate-*l*_binary64 (*.f64 -2 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 c0 (*.f64 w 2)))))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (*.f64 -2 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 c0 (Rewrite=> *-commutative_binary64 (*.f64 2 w)))))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (*.f64 -2 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 c0 2) w))))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (*.f64 -2 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) (*.f64 c0 2)) w)))) (neg.f64 c0)): 1 points increase in error, 23 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (*.f64 -2 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) c0) 2)) w))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) c0) 2) w) -2))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (*.f64 M M) (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) c0) 2) (*.f64 w -2)))) (neg.f64 c0)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 M M) (/.f64 (*.f64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) c0) 2) (*.f64 w -2)) (neg.f64 c0)))): 3 points increase in error, 8 points decrease in error
      (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 M M) (neg.f64 c0)) (*.f64 (*.f64 (*.f64 (pow.f64 (/.f64 d (*.f64 D (sqrt.f64 (*.f64 w h)))) 2) c0) 2) (*.f64 w -2)))): 10 points increase in error, 4 points decrease in error

   if -2.7999999999999998e108 < c0 < -1.04999999999999996e-158 or 5 < c0 < 1.31999999999999998e154

   1. Initial program 58.7

      \[\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. Simplified 58.8

      \[\leadsto \color{blue}{\frac{c0}{2 \cdot w} \cdot \left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D} + \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, \frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, -M \cdot M\right)}\right)} \]
      Proof
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (sqrt.f64 (fma.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 7 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 1 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 7 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.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)))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in c0 around -inf 59.0

      \[\leadsto \color{blue}{-0.5 \cdot \frac{\left(\frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)} + -1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)}\right) \cdot {c0}^{2}}{w} + 0.25 \cdot \frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{{d}^{2}}} \]

   4. Simplified 33.2

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.25, \frac{\frac{D \cdot D}{d}}{d} \cdot \left(h \cdot \left(M \cdot M\right)\right), \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)} \]
      Proof
      (fma.f64 1/4 (*.f64 (/.f64 (/.f64 (*.f64 D D) d) d) (*.f64 h (*.f64 M M))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 D D) (*.f64 d d))) (*.f64 h (*.f64 M M))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 12 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (/.f64 (*.f64 D D) (*.f64 d d)) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (/.f64 (*.f64 D D) (*.f64 d d)) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 D D) (/.f64 (*.f64 d d) (*.f64 (pow.f64 M 2) h)))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 5 points increase in error, 2 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 D D) (/.f64 (*.f64 d d) (Rewrite=> *-commutative_binary64 (*.f64 h (pow.f64 M 2))))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D D) (*.f64 h (pow.f64 M 2))) (*.f64 d d))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 3 points increase in error, 5 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 h (pow.f64 M 2))) (*.f64 d d)) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 d d)) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 (/.f64 0 w) (Rewrite<= unpow2_binary64 (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-/r/_binary64 (/.f64 0 (/.f64 w (pow.f64 c0 2))))): 4 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (Rewrite<= metadata-eval (*.f64 -1/2 0)) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 0 (/.f64 w (pow.f64 c0 2)))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (Rewrite<= mul0-lft_binary64 (*.f64 0 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2))))): 86 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 w (pow.f64 c0 2))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))) (/.f64 w (pow.f64 c0 2))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error

   5. Taylor expanded in D around 0 35.7

      \[\leadsto \mathsf{fma}\left(0.25, \color{blue}{\frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{{d}^{2}}}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]

   6. Simplified 18.9

      \[\leadsto \mathsf{fma}\left(0.25, \color{blue}{h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]
      Proof
      (*.f64 h (pow.f64 (*.f64 M (/.f64 D d)) 2)): 0 points increase in error, 0 points decrease in error
      (*.f64 h (pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 D d) M)) 2)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (*.f64 (/.f64 D d) M) 2) h)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (*.f64 (/.f64 D d) M) (*.f64 (/.f64 D d) M))) h): 0 points increase in error, 0 points decrease in error
      (*.f64 (*.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 D M) d)) (*.f64 (/.f64 D d) M)) h): 10 points increase in error, 10 points decrease in error
      (*.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (*.f64 D M) (*.f64 (/.f64 D d) M)) d)) h): 21 points increase in error, 11 points decrease in error
      (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (*.f64 (*.f64 D M) (*.f64 (/.f64 D d) M)) h) d)): 17 points increase in error, 16 points decrease in error
      (/.f64 (*.f64 (*.f64 (*.f64 D M) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 D M) d))) h) d): 3 points increase in error, 12 points decrease in error
      (/.f64 (*.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 D M) (*.f64 D M)) d)) h) d): 21 points increase in error, 5 points decrease in error
      (/.f64 (*.f64 (/.f64 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 D D) (*.f64 M M))) d) h) d): 45 points increase in error, 5 points decrease in error
      (/.f64 (*.f64 (/.f64 (*.f64 (*.f64 D D) (Rewrite<= unpow2_binary64 (pow.f64 M 2))) d) h) d): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 M 2) (*.f64 D D))) d) h) d): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (pow.f64 M 2) (/.f64 (*.f64 D D) d))) h) d): 5 points increase in error, 9 points decrease in error
      (/.f64 (*.f64 (*.f64 (pow.f64 M 2) (Rewrite=> associate-/l*_binary64 (/.f64 D (/.f64 d D)))) h) d): 2 points increase in error, 18 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 (pow.f64 M 2) (/.f64 D (/.f64 d D))) (/.f64 h d))): 12 points increase in error, 10 points decrease in error
      (*.f64 (*.f64 (pow.f64 M 2) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 D D) d))) (/.f64 h d)): 21 points increase in error, 2 points decrease in error
      (*.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (pow.f64 M 2) (*.f64 D D)) d)) (/.f64 h d)): 9 points increase in error, 5 points decrease in error
      (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (pow.f64 M 2))) d) (/.f64 h d)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 (*.f64 D D) (pow.f64 M 2)) h) (*.f64 d d))): 33 points increase in error, 8 points decrease in error
      (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 D D) (*.f64 (pow.f64 M 2) h))) (*.f64 d d)): 8 points increase in error, 5 points decrease in error
      (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 (pow.f64 M 2) h)) (*.f64 d d)): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (Rewrite<= unpow2_binary64 (pow.f64 d 2))): 0 points increase in error, 0 points decrease in error

   if -1.04999999999999996e-158 < c0 < 5.5000000000000005e-26

   1. Initial program 58.4

      \[\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. Simplified 58.8

      \[\leadsto \color{blue}{\frac{c0}{2 \cdot w} \cdot \left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D} + \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, \frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, -M \cdot M\right)}\right)} \]
      Proof
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (sqrt.f64 (fma.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 7 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 1 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 7 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.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)))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in c0 around -inf 60.1

      \[\leadsto \color{blue}{-0.5 \cdot \frac{\left(\frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)} + -1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)}\right) \cdot {c0}^{2}}{w} + 0.25 \cdot \frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{{d}^{2}}} \]

   4. Simplified 32.7

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.25, \frac{\frac{D \cdot D}{d}}{d} \cdot \left(h \cdot \left(M \cdot M\right)\right), \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)} \]
      Proof
      (fma.f64 1/4 (*.f64 (/.f64 (/.f64 (*.f64 D D) d) d) (*.f64 h (*.f64 M M))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 D D) (*.f64 d d))) (*.f64 h (*.f64 M M))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 12 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (/.f64 (*.f64 D D) (*.f64 d d)) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (/.f64 (*.f64 D D) (*.f64 d d)) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 D D) (/.f64 (*.f64 d d) (*.f64 (pow.f64 M 2) h)))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 5 points increase in error, 2 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 D D) (/.f64 (*.f64 d d) (Rewrite=> *-commutative_binary64 (*.f64 h (pow.f64 M 2))))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D D) (*.f64 h (pow.f64 M 2))) (*.f64 d d))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 3 points increase in error, 5 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 h (pow.f64 M 2))) (*.f64 d d)) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 d d)) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 (/.f64 0 w) (Rewrite<= unpow2_binary64 (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-/r/_binary64 (/.f64 0 (/.f64 w (pow.f64 c0 2))))): 4 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (Rewrite<= metadata-eval (*.f64 -1/2 0)) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 0 (/.f64 w (pow.f64 c0 2)))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (Rewrite<= mul0-lft_binary64 (*.f64 0 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2))))): 86 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 w (pow.f64 c0 2))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))) (/.f64 w (pow.f64 c0 2))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error

   5. Applied egg-rr 44.0

      \[\leadsto \mathsf{fma}\left(0.25, \color{blue}{\frac{{\left(\frac{D}{\sqrt{d}} \cdot M\right)}^{2} \cdot h}{d}}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]

   6. Taylor expanded in D around 0 32.5

      \[\leadsto \mathsf{fma}\left(0.25, \frac{\color{blue}{\frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{d}}}{d}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]

   7. Simplified 25.6

      \[\leadsto \mathsf{fma}\left(0.25, \frac{\color{blue}{h \cdot \frac{{\left(D \cdot M\right)}^{2}}{d}}}{d}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]
      Proof
      (*.f64 h (/.f64 (pow.f64 (*.f64 D M) 2) d)): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 h (pow.f64 (*.f64 D M) 2)) d)): 28 points increase in error, 16 points decrease in error
      (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (*.f64 D M) 2) h)) d): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (*.f64 D M) (*.f64 D M))) h) d): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 D D) (*.f64 M M))) h) d): 43 points increase in error, 7 points decrease in error
      (/.f64 (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 M M)) h) d): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 (pow.f64 D 2) (Rewrite<= unpow2_binary64 (pow.f64 M 2))) h) d): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h))) d): 12 points increase in error, 6 points decrease in error

   if 5.5000000000000005e-26 < c0 < 1.44999999999999996e-9

   1. Initial program 58.9

      \[\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. Simplified 60.7

      \[\leadsto \color{blue}{\frac{\frac{c0}{2}}{w} \cdot \mathsf{fma}\left(d \cdot d, \frac{c0}{w \cdot \left(h \cdot \left(D \cdot D\right)\right)}, \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h}, \frac{c0}{w \cdot h} \cdot {\left(\frac{d}{D}\right)}^{4}, M \cdot \left(-M\right)\right)}\right)} \]
      Proof
      (*.f64 (/.f64 (/.f64 c0 2) w) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 c0 (*.f64 2 w))) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 2 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) (Rewrite<= metadata-eval (+.f64 3 1)))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 (/.f64 d D) 3) (/.f64 d D)))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (Rewrite=> unpow3_binary64 (*.f64 (*.f64 (/.f64 d D) (/.f64 d D)) (/.f64 d D))) (/.f64 d D))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))) (/.f64 d D)) (/.f64 d D))) (*.f64 M (neg.f64 M)))))): 3 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (*.f64 (/.f64 d D) (/.f64 d D))))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D)))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 M M))))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 c0 (*.f64 w h))) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M))))): 5 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M))))): 0 points increase in error, 10 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D)))) (*.f64 M M))))): 3 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))))) (*.f64 M M))))): 0 points increase in error, 7 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 d d) (/.f64 c0 (*.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)))))): 3 points increase in error, 5 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (*.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))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite=> associate-*l/_binary64 (/.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 points increase in error, 6 points decrease in error

   3. Taylor expanded in d around inf 58.3

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

   4. Simplified 46.2

      \[\leadsto \frac{\frac{c0}{2}}{w} \cdot \color{blue}{\left(2 \cdot \left(\frac{{\left(\frac{d}{D}\right)}^{2}}{w \cdot h} \cdot c0\right)\right)} \]
      Proof
      (*.f64 2 (*.f64 (/.f64 (pow.f64 (/.f64 d D) 2) (*.f64 w h)) c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (Rewrite=> unpow2_binary64 (*.f64 (/.f64 d D) (/.f64 d D))) (*.f64 w h)) c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 w h)) c0)): 37 points increase in error, 15 points decrease in error
      (*.f64 2 (*.f64 (/.f64 (/.f64 (*.f64 d d) (Rewrite<= unpow2_binary64 (pow.f64 D 2))) (*.f64 w h)) c0)): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 d d) (*.f64 (pow.f64 D 2) (*.f64 w h)))) c0)): 12 points increase in error, 7 points decrease in error
      (*.f64 2 (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 d d) (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w h)) c0)))): 10 points increase in error, 8 points decrease in error
      (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 d d) c0) (*.f64 (pow.f64 D 2) (*.f64 w h))))): 9 points increase in error, 13 points decrease in error
      (*.f64 2 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) c0) (*.f64 (pow.f64 D 2) (*.f64 w h)))): 0 points increase in error, 0 points decrease in error

   5. Applied egg-rr 43.1

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

   if 1.44999999999999996e-9 < c0 < 5

   1. Initial program 60.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. Simplified 60.8

      \[\leadsto \color{blue}{\frac{c0}{2 \cdot w} \cdot \left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D} + \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, \frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, -M \cdot M\right)}\right)} \]
      Proof
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (sqrt.f64 (fma.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 7 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (neg.f64 (*.f64 M M)))))): 1 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 7 points decrease in error
      (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.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)))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in c0 around -inf 58.7

      \[\leadsto \color{blue}{-0.5 \cdot \frac{\left(\frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)} + -1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)}\right) \cdot {c0}^{2}}{w} + 0.25 \cdot \frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{{d}^{2}}} \]

   4. Simplified 35.7

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.25, \frac{\frac{D \cdot D}{d}}{d} \cdot \left(h \cdot \left(M \cdot M\right)\right), \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)} \]
      Proof
      (fma.f64 1/4 (*.f64 (/.f64 (/.f64 (*.f64 D D) d) d) (*.f64 h (*.f64 M M))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 D D) (*.f64 d d))) (*.f64 h (*.f64 M M))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 12 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (/.f64 (*.f64 D D) (*.f64 d d)) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (*.f64 (/.f64 (*.f64 D D) (*.f64 d d)) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 D D) (/.f64 (*.f64 d d) (*.f64 (pow.f64 M 2) h)))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 5 points increase in error, 2 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 D D) (/.f64 (*.f64 d d) (Rewrite=> *-commutative_binary64 (*.f64 h (pow.f64 M 2))))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D D) (*.f64 h (pow.f64 M 2))) (*.f64 d d))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 3 points increase in error, 5 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 h (pow.f64 M 2))) (*.f64 d d)) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 d d)) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) (*.f64 (/.f64 0 w) (*.f64 c0 c0))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 (/.f64 0 w) (Rewrite<= unpow2_binary64 (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-/r/_binary64 (/.f64 0 (/.f64 w (pow.f64 c0 2))))): 4 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (Rewrite<= metadata-eval (*.f64 -1/2 0)) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 0 (/.f64 w (pow.f64 c0 2)))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (Rewrite<= mul0-lft_binary64 (*.f64 0 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2))))): 86 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 w (pow.f64 c0 2))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (/.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))) (/.f64 w (pow.f64 c0 2))))): 0 points increase in error, 0 points decrease in error
      (fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error

   5. Applied egg-rr 42.2

      \[\leadsto \mathsf{fma}\left(0.25, \color{blue}{\frac{{\left(\frac{D}{\sqrt{d}} \cdot M\right)}^{2} \cdot h}{d}}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]

   6. Applied egg-rr 25.5

      \[\leadsto \mathsf{fma}\left(0.25, \color{blue}{\frac{{\left(D \cdot M\right)}^{2}}{d} \cdot \left(h \cdot \frac{1}{d}\right)}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right) \]

   if 1.31999999999999998e154 < c0

   1. Initial program 62.7

      \[\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. Applied egg-rr 63.3

      \[\leadsto \color{blue}{\frac{{\left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)}\right)}^{2} - \left({\left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)}\right)}^{2} - M \cdot M\right)}{\left(2 \cdot \frac{w}{c0}\right) \cdot \left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)} - \sqrt{{\left(\frac{c0}{w} \cdot \frac{d \cdot d}{h \cdot \left(D \cdot D\right)}\right)}^{2} - M \cdot M}\right)}} \]

   3. Simplified 48.8

      \[\leadsto \color{blue}{\frac{0 + M \cdot M}{c0 \cdot \left(d \cdot \frac{\frac{\frac{d}{D}}{D}}{w \cdot h}\right) - \sqrt{{\left(c0 \cdot \left(d \cdot \frac{\frac{\frac{d}{D}}{D}}{w \cdot h}\right)\right)}^{2} - M \cdot M}} \cdot \frac{c0}{\frac{w}{0.5}}} \]
      Proof
      (*.f64 (/.f64 (+.f64 0 (*.f64 M M)) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (Rewrite<= +-inverses_binary64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2))) (*.f64 M M)) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 105 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2)) (Rewrite<= unpow2_binary64 (pow.f64 M 2))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (pow.f64 M 2)))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (Rewrite=> unpow2_binary64 (*.f64 M M)))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 D D))) (*.f64 w h)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 (*.f64 D D) (*.f64 w h)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite<= associate-*r*_binary64 (*.f64 w (*.f64 h (*.f64 D D))))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 d 1)) (*.f64 w (*.f64 h (*.f64 D D)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-*r/_binary64 (*.f64 d (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 d d) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D))))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c0 (*.f64 d d)) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 c0 (*.f64 d d)) 1) (*.f64 w (*.f64 h (*.f64 D D))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (/.f64 (Rewrite=> *-rgt-identity_binary64 (*.f64 c0 (*.f64 d d))) (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (*.f64 c0 (*.f64 d d)) w) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 c0 w) (*.f64 d d))) (*.f64 h (*.f64 D D))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D))))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (/.f64 (/.f64 d D) D) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 D D))) (*.f64 w h)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 4 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 (*.f64 D D) (*.f64 w h)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 d (Rewrite<= associate-*r*_binary64 (*.f64 w (*.f64 h (*.f64 D D))))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 3 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 d 1)) (*.f64 w (*.f64 h (*.f64 D D)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (*.f64 d (Rewrite<= associate-*r/_binary64 (*.f64 d (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 2 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 d d) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D))))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 5 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c0 (*.f64 d d)) (/.f64 1 (*.f64 w (*.f64 h (*.f64 D D)))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 c0 (*.f64 d d)) 1) (*.f64 w (*.f64 h (*.f64 D D))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 1 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 (Rewrite=> *-rgt-identity_binary64 (*.f64 c0 (*.f64 d d))) (*.f64 w (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (*.f64 c0 (*.f64 d d)) w) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 c0 w) (*.f64 d d))) (*.f64 h (*.f64 D D))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 3 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D))))) 2) (*.f64 M M))))) (/.f64 c0 (/.f64 w 1/2))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c0 1/2) w))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 1/2 c0)) w)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (Rewrite=> associate-/l*_binary64 (/.f64 1/2 (/.f64 w c0)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) (/.f64 w c0))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))) (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 2 (/.f64 w c0))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) 1) (*.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M)))) (*.f64 2 (/.f64 w c0))))): 1 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> *-rgt-identity_binary64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M)))) (*.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M)))) (*.f64 2 (/.f64 w c0)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 2 (/.f64 w c0)) (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (*.f64 d d) (*.f64 h (*.f64 D D)))) 2) (*.f64 M M))))))): 0 points increase in error, 0 points decrease in error

   4. Applied egg-rr 37.8

      \[\leadsto \color{blue}{\frac{M \cdot M}{\frac{\left(c0 \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{w \cdot h} - \sqrt{{\left(c0 \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{w \cdot h}\right)}^{2} - M \cdot M}\right) \cdot \left(w \cdot 2\right)}{c0}}} \]

   5. Applied egg-rr 36.9

      \[\leadsto \color{blue}{\frac{M}{{\left(\sqrt[3]{\frac{\frac{c0}{\frac{w \cdot h}{{\left(\frac{d}{D}\right)}^{2}}} - \sqrt{{\left(\frac{c0}{\frac{w \cdot h}{{\left(\frac{d}{D}\right)}^{2}}}\right)}^{2} - M \cdot M}}{c0} \cdot \left(2 \cdot w\right)}\right)}^{2}} \cdot \frac{M}{\sqrt[3]{\frac{\frac{c0}{\frac{w \cdot h}{{\left(\frac{d}{D}\right)}^{2}}} - \sqrt{{\left(\frac{c0}{\frac{w \cdot h}{{\left(\frac{d}{D}\right)}^{2}}}\right)}^{2} - M \cdot M}}{c0} \cdot \left(2 \cdot w\right)}}} \]

   6. Simplified 34.3

      \[\leadsto \color{blue}{\frac{M}{{\left(\sqrt[3]{\left(2 \cdot w\right) \cdot \frac{\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h} - \sqrt{{\left(\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h}\right)}^{2} - M \cdot M}}{c0}}\right)}^{2}} \cdot \frac{M}{\sqrt[3]{\left(2 \cdot w\right) \cdot \frac{\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h} - \sqrt{{\left(\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h}\right)}^{2} - M \cdot M}}{c0}}}} \]
      Proof
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (pow.f64 (/.f64 d D) 2)) (*.f64 w h))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 16 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (Rewrite=> associate-/l*_binary64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 1 points increase in error, 8 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (pow.f64 (/.f64 d D) 2)) (*.f64 w h))) 2) (*.f64 M M)))) c0))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 5 points increase in error, 3 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite=> associate-/l*_binary64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2)))) 2) (*.f64 M M)))) c0))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 2 points increase in error, 5 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w)))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (pow.f64 (/.f64 d D) 2)) (*.f64 w h))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 8 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (Rewrite=> associate-/l*_binary64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2)))) (sqrt.f64 (-.f64 (pow.f64 (*.f64 (/.f64 c0 w) (/.f64 (pow.f64 (/.f64 d D) 2) h)) 2) (*.f64 M M)))) c0))))): 0 points increase in error, 7 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (pow.f64 (/.f64 d D) 2)) (*.f64 w h))) 2) (*.f64 M M)))) c0))))): 4 points increase in error, 12 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w))) 2)) (/.f64 M (cbrt.f64 (*.f64 (*.f64 2 w) (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (Rewrite=> associate-/l*_binary64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2)))) 2) (*.f64 M M)))) c0))))): 1 points increase in error, 4 points decrease in error
      (*.f64 (/.f64 M (pow.f64 (cbrt.f64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w))) 2)) (/.f64 M (cbrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) (sqrt.f64 (-.f64 (pow.f64 (/.f64 c0 (/.f64 (*.f64 w h) (pow.f64 (/.f64 d D) 2))) 2) (*.f64 M M)))) c0) (*.f64 2 w)))))): 0 points increase in error, 0 points decrease in error
3. Recombined 6 regimes into one program.

4. Final simplification 25.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;c0 \leq -2.8 \cdot 10^{+108}:\\ \;\;\;\;\frac{M}{\frac{{\left(\frac{\frac{d}{D}}{\sqrt{w \cdot h}}\right)}^{2} \cdot \left(c0 \cdot \left(w \cdot -4\right)\right)}{M}} \cdot \left(-c0\right)\\ \mathbf{elif}\;c0 \leq -1.05 \cdot 10^{-158}:\\ \;\;\;\;\mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)\\ \mathbf{elif}\;c0 \leq 5.5 \cdot 10^{-26}:\\ \;\;\;\;\mathsf{fma}\left(0.25, \frac{h \cdot \frac{{\left(M \cdot D\right)}^{2}}{d}}{d}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)\\ \mathbf{elif}\;c0 \leq 1.45 \cdot 10^{-9}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;c0 \leq 5:\\ \;\;\;\;\mathsf{fma}\left(0.25, \frac{{\left(M \cdot D\right)}^{2}}{d} \cdot \left(h \cdot \frac{1}{d}\right), \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)\\ \mathbf{elif}\;c0 \leq 1.32 \cdot 10^{+154}:\\ \;\;\;\;\mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{M}{{\left(\sqrt[3]{\left(w \cdot 2\right) \cdot \frac{\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h} - \sqrt{{\left(\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h}\right)}^{2} - M \cdot M}}{c0}}\right)}^{2}} \cdot \frac{M}{\sqrt[3]{\left(w \cdot 2\right) \cdot \frac{\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h} - \sqrt{{\left(\frac{c0}{w} \cdot \frac{{\left(\frac{d}{D}\right)}^{2}}{h}\right)}^{2} - M \cdot M}}{c0}}}\\ \end{array} \]

Alternatives

Alternative 1
Error	25.3
Cost	14740

\[\begin{array}{l} t_0 := \frac{{\left(M \cdot D\right)}^{2}}{d}\\ t_1 := \frac{0}{w} \cdot \left(c0 \cdot c0\right)\\ t_2 := \mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, t_1\right)\\ \mathbf{if}\;c0 \leq -1.35 \cdot 10^{+154}:\\ \;\;\;\;0\\ \mathbf{elif}\;c0 \leq -5 \cdot 10^{-161}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;c0 \leq 5.5 \cdot 10^{-26}:\\ \;\;\;\;\mathsf{fma}\left(0.25, \frac{h \cdot t_0}{d}, t_1\right)\\ \mathbf{elif}\;c0 \leq 1.45 \cdot 10^{-9}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;c0 \leq 480:\\ \;\;\;\;\mathsf{fma}\left(0.25, t_0 \cdot \left(h \cdot \frac{1}{d}\right), t_1\right)\\ \mathbf{elif}\;c0 \leq 1.15 \cdot 10^{+149}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \end{array} \]

Alternative 2
Error	25.6
Cost	14740

\[\begin{array}{l} t_0 := \frac{0}{w} \cdot \left(c0 \cdot c0\right)\\ t_1 := \mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, t_0\right)\\ t_2 := \frac{{\left(M \cdot D\right)}^{2}}{d}\\ \mathbf{if}\;c0 \leq -2.8 \cdot 10^{+108}:\\ \;\;\;\;\frac{M}{\frac{{\left(\frac{\frac{d}{D}}{\sqrt{w \cdot h}}\right)}^{2} \cdot \left(c0 \cdot \left(w \cdot -4\right)\right)}{M}} \cdot \left(-c0\right)\\ \mathbf{elif}\;c0 \leq -2 \cdot 10^{-156}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;c0 \leq 3 \cdot 10^{-28}:\\ \;\;\;\;\mathsf{fma}\left(0.25, \frac{h \cdot t_2}{d}, t_0\right)\\ \mathbf{elif}\;c0 \leq 1.45 \cdot 10^{-9}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;c0 \leq 20000000:\\ \;\;\;\;\mathsf{fma}\left(0.25, t_2 \cdot \left(h \cdot \frac{1}{d}\right), t_0\right)\\ \mathbf{elif}\;c0 \leq 1.15 \cdot 10^{+149}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \end{array} \]

Alternative 3
Error	25.3
Cost	14616

\[\begin{array}{l} t_0 := \frac{{\left(M \cdot D\right)}^{2}}{d}\\ t_1 := \frac{0}{w} \cdot \left(c0 \cdot c0\right)\\ t_2 := \mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, t_1\right)\\ \mathbf{if}\;c0 \leq -1.35 \cdot 10^{+154}:\\ \;\;\;\;0\\ \mathbf{elif}\;c0 \leq -2.2 \cdot 10^{-160}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;c0 \leq 5.5 \cdot 10^{-26}:\\ \;\;\;\;\mathsf{fma}\left(0.25, \frac{h \cdot t_0}{d}, t_1\right)\\ \mathbf{elif}\;c0 \leq 1.45 \cdot 10^{-9}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;c0 \leq 4.5:\\ \;\;\;\;\mathsf{fma}\left(0.25, h \cdot \frac{t_0}{d}, t_1\right)\\ \mathbf{elif}\;c0 \leq 1.15 \cdot 10^{+149}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \end{array} \]

Alternative 4
Error	24.4
Cost	14352

\[\begin{array}{l} t_0 := \mathsf{fma}\left(0.25, h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}, \frac{0}{w} \cdot \left(c0 \cdot c0\right)\right)\\ \mathbf{if}\;c0 \leq -1.35 \cdot 10^{+154}:\\ \;\;\;\;0\\ \mathbf{elif}\;c0 \leq 8.5 \cdot 10^{-23}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;c0 \leq 1.45 \cdot 10^{-9}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;c0 \leq 1.15 \cdot 10^{+149}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \end{array} \]

Alternative 5
Error	29.4
Cost	7888

\[\begin{array}{l} t_0 := h \cdot \left(M \cdot M\right)\\ \mathbf{if}\;D \leq -1.25 \cdot 10^{+141}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;D \leq -9.2 \cdot 10^{-129}:\\ \;\;\;\;0.25 \cdot \frac{t_0}{d \cdot \frac{d}{D \cdot D}}\\ \mathbf{elif}\;D \leq 2.2 \cdot 10^{-110}:\\ \;\;\;\;0\\ \mathbf{elif}\;D \leq 1.35 \cdot 10^{+154}:\\ \;\;\;\;\mathsf{fma}\left(0.25, t_0 \cdot \frac{\frac{D \cdot D}{d}}{d}, 0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(0.5 \cdot \frac{D}{d \cdot \frac{d}{D}}\right) \cdot \frac{w}{\frac{c0}{t_0}}\right) \cdot \frac{c0}{\frac{w}{0.5}}\\ \end{array} \]

Alternative 6
Error	29.4
Cost	2128

\[\begin{array}{l} t_0 := h \cdot \left(M \cdot M\right)\\ t_1 := 0.25 \cdot \frac{t_0}{d \cdot \frac{d}{D \cdot D}}\\ \mathbf{if}\;D \leq -1.25 \cdot 10^{+141}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;D \leq -2.4 \cdot 10^{-135}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;D \leq 2.15 \cdot 10^{-112}:\\ \;\;\;\;0\\ \mathbf{elif}\;D \leq 1.35 \cdot 10^{+154}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\left(\left(0.5 \cdot \frac{D}{d \cdot \frac{d}{D}}\right) \cdot \frac{w}{\frac{c0}{t_0}}\right) \cdot \frac{c0}{\frac{w}{0.5}}\\ \end{array} \]

Alternative 7
Error	30.0
Cost	1488

\[\begin{array}{l} t_0 := 0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \mathbf{if}\;D \leq -1.25 \cdot 10^{+141}:\\ \;\;\;\;\frac{d}{\frac{\frac{\left(D \cdot w\right) \cdot \left(D \cdot w\right)}{\frac{c0 \cdot c0}{h}}}{d}}\\ \mathbf{elif}\;D \leq -7 \cdot 10^{-130}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;D \leq 1.9 \cdot 10^{-110}:\\ \;\;\;\;0\\ \mathbf{elif}\;D \leq 1.05 \cdot 10^{+89}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

Alternative 8
Error	29.6
Cost	1488

\[\begin{array}{l} t_0 := 0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \mathbf{if}\;D \leq -1.25 \cdot 10^{+141}:\\ \;\;\;\;\frac{\frac{c0}{2}}{w} \cdot \left(2 \cdot \left(c0 \cdot \left(\frac{\frac{d}{D}}{w} \cdot \frac{\frac{d}{D}}{h}\right)\right)\right)\\ \mathbf{elif}\;D \leq -9.5 \cdot 10^{-136}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;D \leq 5.2 \cdot 10^{-111}:\\ \;\;\;\;0\\ \mathbf{elif}\;D \leq 8.2 \cdot 10^{+91}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

Alternative 9
Error	29.4
Cost	1480

\[\begin{array}{l} \mathbf{if}\;D \cdot D \leq 8 \cdot 10^{-254}:\\ \;\;\;\;0\\ \mathbf{elif}\;D \cdot D \leq 4.8 \cdot 10^{+301}:\\ \;\;\;\;0.25 \cdot \frac{h \cdot \left(M \cdot M\right)}{d \cdot \frac{d}{D \cdot D}}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

Alternative 10
Error	31.9
Cost	64

\[0 \]

Reproduce

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