(/ (- x lo) (- hi lo))

Average Error: 62.0 → 50.4

Time: 10.3s

Precision: binary64

Cost: 62080

\[lo < -1 \cdot 10^{+308} \land hi > 10^{+308}\]

Math

\[\frac{x - lo}{hi - lo} \]

↓

\[\begin{array}{l} t_0 := \frac{x}{{lo}^{3}}\\ \sqrt{\frac{\mathsf{fma}\left(1 - \frac{x}{lo} \cdot \frac{x}{lo}, 1 - \frac{x}{lo}, \left(hi \cdot \left(hi \cdot \left(2 \cdot t_0 + \left(t_0 - {lo}^{-2}\right)\right)\right) - {\left(\frac{hi}{lo}\right)}^{3}\right) + hi \cdot \left(\left(\frac{1}{lo} - \frac{x}{\frac{{lo}^{3}}{x}}\right) + 2 \cdot \left(x \cdot \left({lo}^{-2} - t_0\right)\right)\right)\right)}{1 + \frac{x - hi}{lo}}} \end{array} \]

FPCore

(FPCore (lo hi x) :precision binary64 (/ (- x lo) (- hi lo)))

↓

(FPCore (lo hi x)
 :precision binary64
 (let* ((t_0 (/ x (pow lo 3.0))))
   (sqrt
    (/
     (fma
      (- 1.0 (* (/ x lo) (/ x lo)))
      (- 1.0 (/ x lo))
      (+
       (-
        (* hi (* hi (+ (* 2.0 t_0) (- t_0 (pow lo -2.0)))))
        (pow (/ hi lo) 3.0))
       (*
        hi
        (+
         (- (/ 1.0 lo) (/ x (/ (pow lo 3.0) x)))
         (* 2.0 (* x (- (pow lo -2.0) t_0)))))))
     (+ 1.0 (/ (- x hi) lo))))))

C

double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}

↓

double code(double lo, double hi, double x) {
	double t_0 = x / pow(lo, 3.0);
	return sqrt((fma((1.0 - ((x / lo) * (x / lo))), (1.0 - (x / lo)), (((hi * (hi * ((2.0 * t_0) + (t_0 - pow(lo, -2.0))))) - pow((hi / lo), 3.0)) + (hi * (((1.0 / lo) - (x / (pow(lo, 3.0) / x))) + (2.0 * (x * (pow(lo, -2.0) - t_0))))))) / (1.0 + ((x - hi) / lo))));
}

Julia

function code(lo, hi, x)
	return Float64(Float64(x - lo) / Float64(hi - lo))
end

↓

function code(lo, hi, x)
	t_0 = Float64(x / (lo ^ 3.0))
	return sqrt(Float64(fma(Float64(1.0 - Float64(Float64(x / lo) * Float64(x / lo))), Float64(1.0 - Float64(x / lo)), Float64(Float64(Float64(hi * Float64(hi * Float64(Float64(2.0 * t_0) + Float64(t_0 - (lo ^ -2.0))))) - (Float64(hi / lo) ^ 3.0)) + Float64(hi * Float64(Float64(Float64(1.0 / lo) - Float64(x / Float64((lo ^ 3.0) / x))) + Float64(2.0 * Float64(x * Float64((lo ^ -2.0) - t_0))))))) / Float64(1.0 + Float64(Float64(x - hi) / lo))))
end

Wolfram

code[lo_, hi_, x_] := N[(N[(x - lo), $MachinePrecision] / N[(hi - lo), $MachinePrecision]), $MachinePrecision]

↓

code[lo_, hi_, x_] := Block[{t$95$0 = N[(x / N[Power[lo, 3.0], $MachinePrecision]), $MachinePrecision]}, N[Sqrt[N[(N[(N[(1.0 - N[(N[(x / lo), $MachinePrecision] * N[(x / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(x / lo), $MachinePrecision]), $MachinePrecision] + N[(N[(N[(hi * N[(hi * N[(N[(2.0 * t$95$0), $MachinePrecision] + N[(t$95$0 - N[Power[lo, -2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Power[N[(hi / lo), $MachinePrecision], 3.0], $MachinePrecision]), $MachinePrecision] + N[(hi * N[(N[(N[(1.0 / lo), $MachinePrecision] - N[(x / N[(N[Power[lo, 3.0], $MachinePrecision] / x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(2.0 * N[(x * N[(N[Power[lo, -2.0], $MachinePrecision] - t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(1.0 + N[(N[(x - hi), $MachinePrecision] / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]

Derivation

1. Initial program 62.0

   \[\frac{x - lo}{hi - lo} \]

2. Taylor expanded in lo around inf 58.0

   \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{lo} + 1\right) - -1 \cdot \frac{hi}{lo}} \]

3. Simplified 58.0

   \[\leadsto \color{blue}{1 - \frac{x - hi}{lo}} \]
   Proof
   (-.f64 1 (/.f64 (-.f64 x hi) lo)): 0 points increase in error, 0 points decrease in error
   (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (/.f64 (-.f64 x hi) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 1 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 1 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 x hi)) lo))): 0 points increase in error, 0 points decrease in error
   (+.f64 1 (/.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) lo)): 0 points increase in error, 0 points decrease in error
   (+.f64 1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 -1 x) lo) (/.f64 (*.f64 -1 hi) lo)))): 2 points increase in error, 1 points decrease in error
   (+.f64 1 (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 x lo))) (/.f64 (*.f64 -1 hi) lo))): 0 points increase in error, 0 points decrease in error
   (+.f64 1 (-.f64 (*.f64 -1 (/.f64 x lo)) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 1 (*.f64 -1 (/.f64 x lo))) (*.f64 -1 (/.f64 hi lo)))): 1 points increase in error, 1 points decrease in error
   (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 x lo)) 1)) (*.f64 -1 (/.f64 hi lo))): 0 points increase in error, 0 points decrease in error

4. Applied egg-rr 52.5

   \[\leadsto \color{blue}{\sqrt{{\left(1 - \frac{x - hi}{lo}\right)}^{2}}} \]

5. Applied egg-rr 52.5

   \[\leadsto \sqrt{\color{blue}{\frac{\left(1 - {\left(\frac{x - hi}{lo}\right)}^{2}\right) \cdot \left(1 - \frac{x - hi}{lo}\right)}{1 + \frac{x - hi}{lo}}}} \]

6. Taylor expanded in hi around -inf 64.0

   \[\leadsto \sqrt{\frac{\color{blue}{\left(1 - \frac{{x}^{2}}{{lo}^{2}}\right) \cdot \left(1 - \frac{x}{lo}\right) + \left(-1 \cdot \frac{{hi}^{3}}{{lo}^{3}} + \left(\left(2 \cdot \frac{x}{{lo}^{3}} + -1 \cdot \frac{1 - \frac{x}{lo}}{{lo}^{2}}\right) \cdot {hi}^{2} + -1 \cdot \left(\left(-2 \cdot \frac{\left(1 - \frac{x}{lo}\right) \cdot x}{{lo}^{2}} + -1 \cdot \frac{1 - \frac{{x}^{2}}{{lo}^{2}}}{lo}\right) \cdot hi\right)\right)\right)}}{1 + \frac{x - hi}{lo}}} \]

7. Simplified 50.4

   \[\leadsto \sqrt{\frac{\color{blue}{\mathsf{fma}\left(1 - \frac{x}{lo} \cdot \frac{x}{lo}, 1 - \frac{x}{lo}, \left(hi \cdot \left(hi \cdot \left(2 \cdot \frac{x}{{lo}^{3}} - \left({lo}^{-2} - \frac{x}{{lo}^{3}}\right)\right)\right) - {\left(\frac{hi}{lo}\right)}^{3}\right) - hi \cdot \left(-2 \cdot \left(\left({lo}^{-2} - \frac{x}{{lo}^{3}}\right) \cdot x\right) - \left(\frac{1}{lo} - \frac{x}{\frac{{lo}^{3}}{x}}\right)\right)\right)}}{1 + \frac{x - hi}{lo}}} \]
   Proof
   (fma.f64 (-.f64 1 (*.f64 (/.f64 x lo) (/.f64 x lo))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 x x) (*.f64 lo lo)))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 61 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (*.f64 lo lo))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (Rewrite<= unpow2_binary64 (pow.f64 lo 2)))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (pow.f64 lo (Rewrite<= metadata-eval (*.f64 2 -1))) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 lo -1) (pow.f64 lo -1))) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (*.f64 (Rewrite=> unpow-1_binary64 (/.f64 1 lo)) (pow.f64 lo -1)) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (pow.f64 lo -1)) lo)) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (/.f64 (Rewrite=> *-lft-identity_binary64 (pow.f64 lo -1)) lo) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (/.f64 (Rewrite=> unpow-1_binary64 (/.f64 1 lo)) lo) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 lo lo))) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (/.f64 1 (Rewrite<= unpow2_binary64 (pow.f64 lo 2))) (/.f64 x (pow.f64 lo 3)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (/.f64 1 (pow.f64 lo 2)) (/.f64 x (Rewrite=> unpow3_binary64 (*.f64 (*.f64 lo lo) lo))))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (/.f64 1 (pow.f64 lo 2)) (/.f64 x (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 lo 2)) lo)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (-.f64 (/.f64 1 (pow.f64 lo 2)) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 x lo) (pow.f64 lo 2))))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (-.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (neg.f64 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2))))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 hi (*.f64 hi (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2))))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 hi hi) (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 195 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 hi 2)) (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2))))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (pow.f64 (/.f64 hi lo) 3)) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (Rewrite<= cube-unmult_binary64 (*.f64 (/.f64 hi lo) (*.f64 (/.f64 hi lo) (/.f64 hi lo))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (*.f64 (/.f64 hi lo) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi hi) (*.f64 lo lo))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (*.f64 (/.f64 hi lo) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 hi 2)) (*.f64 lo lo)))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (*.f64 (/.f64 hi lo) (/.f64 (pow.f64 hi 2) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (pow.f64 hi 2)) (*.f64 lo (pow.f64 lo 2))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (/.f64 (*.f64 hi (Rewrite=> unpow2_binary64 (*.f64 hi hi))) (*.f64 lo (pow.f64 lo 2)))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (/.f64 (Rewrite<= cube-mult_binary64 (pow.f64 hi 3)) (*.f64 lo (pow.f64 lo 2)))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (/.f64 (pow.f64 hi 3) (*.f64 lo (Rewrite=> unpow2_binary64 (*.f64 lo lo))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (-.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (/.f64 (pow.f64 hi 3) (Rewrite<= cube-mult_binary64 (pow.f64 lo 3)))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (neg.f64 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo -2) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (pow.f64 lo (Rewrite<= metadata-eval (*.f64 2 -1))) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 lo -1) (pow.f64 lo -1))) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (*.f64 (Rewrite=> unpow-1_binary64 (/.f64 1 lo)) (pow.f64 lo -1)) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (pow.f64 lo -1)) lo)) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (/.f64 (Rewrite=> *-lft-identity_binary64 (pow.f64 lo -1)) lo) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (/.f64 (Rewrite=> unpow-1_binary64 (/.f64 1 lo)) lo) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 lo lo))) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (/.f64 1 (Rewrite<= unpow2_binary64 (pow.f64 lo 2))) (/.f64 x (pow.f64 lo 3))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (/.f64 1 (pow.f64 lo 2)) (/.f64 x (Rewrite=> unpow3_binary64 (*.f64 (*.f64 lo lo) lo)))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (/.f64 1 (pow.f64 lo 2)) (/.f64 x (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 lo 2)) lo))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (-.f64 (/.f64 1 (pow.f64 lo 2)) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 x lo) (pow.f64 lo 2)))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (*.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2))) x)) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 1 (/.f64 x lo)) (/.f64 (pow.f64 lo 2) x)))) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2)))) (-.f64 (/.f64 1 lo) (/.f64 x (/.f64 (pow.f64 lo 3) x))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (-.f64 (/.f64 1 lo) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x x) (pow.f64 lo 3)))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (-.f64 (/.f64 1 lo) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (pow.f64 lo 3))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (-.f64 (/.f64 1 lo) (/.f64 (pow.f64 x 2) (Rewrite=> cube-mult_binary64 (*.f64 lo (*.f64 lo lo))))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (-.f64 (/.f64 1 lo) (/.f64 (pow.f64 x 2) (*.f64 lo (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (-.f64 (/.f64 1 lo) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (pow.f64 x 2) (pow.f64 lo 2)) lo))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (-.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo)))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (neg.f64 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (*.f64 hi (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (-.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))) hi)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (neg.f64 (*.f64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))) hi))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (+.f64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))) hi))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo)) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (+.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (*.f64 -1 (*.f64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))) hi)))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) (-.f64 1 (/.f64 x lo))) (+.f64 (*.f64 -1 (/.f64 (pow.f64 hi 3) (pow.f64 lo 3))) (+.f64 (*.f64 (+.f64 (*.f64 2 (/.f64 x (pow.f64 lo 3))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 x lo)) (pow.f64 lo 2)))) (pow.f64 hi 2)) (*.f64 -1 (*.f64 (+.f64 (*.f64 -2 (/.f64 (*.f64 (-.f64 1 (/.f64 x lo)) x) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 1 (/.f64 (pow.f64 x 2) (pow.f64 lo 2))) lo))) hi)))))): 0 points increase in error, 0 points decrease in error

8. Final simplification 50.4

   \[\leadsto \sqrt{\frac{\mathsf{fma}\left(1 - \frac{x}{lo} \cdot \frac{x}{lo}, 1 - \frac{x}{lo}, \left(hi \cdot \left(hi \cdot \left(2 \cdot \frac{x}{{lo}^{3}} + \left(\frac{x}{{lo}^{3}} - {lo}^{-2}\right)\right)\right) - {\left(\frac{hi}{lo}\right)}^{3}\right) + hi \cdot \left(\left(\frac{1}{lo} - \frac{x}{\frac{{lo}^{3}}{x}}\right) + 2 \cdot \left(x \cdot \left({lo}^{-2} - \frac{x}{{lo}^{3}}\right)\right)\right)\right)}{1 + \frac{x - hi}{lo}}} \]

Alternatives

Alternative 1
Error	50.6
Cost	13696

\[\begin{array}{l} t_0 := \frac{x - hi}{lo}\\ \sqrt{\frac{{t_0}^{3}}{1 + t_0}} \end{array} \]

Alternative 2
Error	50.6
Cost	13632

\[\sqrt{\frac{-{\left(\frac{hi}{lo}\right)}^{3}}{1 + \frac{x - hi}{lo}}} \]

Alternative 3
Error	50.9
Cost	7872

\[\sqrt{\frac{\left(1 - \frac{x}{lo} \cdot \frac{x}{lo}\right) \cdot \left(1 - \frac{x}{lo}\right)}{1 + \frac{x - hi}{lo}}} \]

Alternative 4
Error	51.5
Cost	576

\[\frac{hi}{lo} \cdot \frac{hi - x}{lo} \]

Alternative 5
Error	51.5
Cost	448

\[\frac{hi}{lo} \cdot \frac{hi}{lo} \]

Alternative 6
Error	52.0
Cost	256

\[\frac{-lo}{hi} \]

Alternative 7
Error	52.0
Cost	64

\[1 \]

Reproduce

herbie shell --seed 2022331 
(FPCore (lo hi x)
  :name "(/ (- x lo) (- hi lo))"
  :precision binary64
  :pre (and (< lo -1e+308) (> hi 1e+308))
  (/ (- x lo) (- hi lo)))