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

Average Error: 62.0 → 0.4

Time: 11.0s

Precision: binary64

Cost: 55872

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

Math

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

↓

\[\begin{array}{l} t_0 := \frac{x - lo}{hi}\\ t_1 := {t_0}^{2}\\ t_2 := \frac{x - lo}{hi \cdot hi}\\ t_3 := lo \cdot t_2\\ t_4 := {t_3}^{2}\\ \frac{\mathsf{fma}\left(t_0, t_0 - t_3, t_4\right) \cdot \mathsf{fma}\left(lo, t_2, t_0\right)}{\log \left(e^{t_1}\right) + \left(t_4 - t_1 \cdot \frac{lo}{hi}\right)} \end{array} \]

FPCore

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

↓

(FPCore (lo hi x)
 :precision binary64
 (let* ((t_0 (/ (- x lo) hi))
        (t_1 (pow t_0 2.0))
        (t_2 (/ (- x lo) (* hi hi)))
        (t_3 (* lo t_2))
        (t_4 (pow t_3 2.0)))
   (/
    (* (fma t_0 (- t_0 t_3) t_4) (fma lo t_2 t_0))
    (+ (log (exp t_1)) (- t_4 (* t_1 (/ lo hi)))))))

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 - lo) / hi;
	double t_1 = pow(t_0, 2.0);
	double t_2 = (x - lo) / (hi * hi);
	double t_3 = lo * t_2;
	double t_4 = pow(t_3, 2.0);
	return (fma(t_0, (t_0 - t_3), t_4) * fma(lo, t_2, t_0)) / (log(exp(t_1)) + (t_4 - (t_1 * (lo / hi))));
}

Julia

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

↓

function code(lo, hi, x)
	t_0 = Float64(Float64(x - lo) / hi)
	t_1 = t_0 ^ 2.0
	t_2 = Float64(Float64(x - lo) / Float64(hi * hi))
	t_3 = Float64(lo * t_2)
	t_4 = t_3 ^ 2.0
	return Float64(Float64(fma(t_0, Float64(t_0 - t_3), t_4) * fma(lo, t_2, t_0)) / Float64(log(exp(t_1)) + Float64(t_4 - Float64(t_1 * Float64(lo / hi)))))
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[(N[(x - lo), $MachinePrecision] / hi), $MachinePrecision]}, Block[{t$95$1 = N[Power[t$95$0, 2.0], $MachinePrecision]}, Block[{t$95$2 = N[(N[(x - lo), $MachinePrecision] / N[(hi * hi), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(lo * t$95$2), $MachinePrecision]}, Block[{t$95$4 = N[Power[t$95$3, 2.0], $MachinePrecision]}, N[(N[(N[(t$95$0 * N[(t$95$0 - t$95$3), $MachinePrecision] + t$95$4), $MachinePrecision] * N[(lo * t$95$2 + t$95$0), $MachinePrecision]), $MachinePrecision] / N[(N[Log[N[Exp[t$95$1], $MachinePrecision]], $MachinePrecision] + N[(t$95$4 - N[(t$95$1 * N[(lo / hi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]]

Derivation

1. Initial program 62.0

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

2. Taylor expanded in hi around inf 64.0

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

3. Simplified 57.9

   \[\leadsto \color{blue}{\frac{x - lo}{hi} \cdot \frac{lo}{hi} + \frac{x - lo}{hi}} \]
   Proof
   (+.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) (/.f64 (-.f64 x lo) hi)): 0 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 x lo) lo) (*.f64 hi hi))) (/.f64 (-.f64 x lo) hi)): 255 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 lo (-.f64 x lo))) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi)): 0 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 (*.f64 lo (-.f64 x lo)) (Rewrite<= unpow2_binary64 (pow.f64 hi 2))) (/.f64 (-.f64 x lo) hi)): 0 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 (*.f64 lo (-.f64 x lo)) (pow.f64 hi 2)) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x hi) (/.f64 lo hi)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (*.f64 lo (-.f64 x lo)) (pow.f64 hi 2)) (/.f64 x hi)) (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 x hi) (/.f64 (*.f64 lo (-.f64 x lo)) (pow.f64 hi 2)))) (/.f64 lo hi)): 0 points increase in error, 0 points decrease in error

4. Applied egg-rr 57.9

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

5. Simplified 0.5

   \[\leadsto \color{blue}{\frac{{\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{3} + {\left(\frac{x - lo}{hi}\right)}^{3}}{{\left(\frac{x - lo}{hi}\right)}^{2} + \left({\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{2} - \frac{lo}{hi} \cdot {\left(\frac{x - lo}{hi}\right)}^{2}\right)}} \]
   Proof
   (/.f64 (+.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (pow.f64 (*.f64 lo (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) hi))) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 255 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (pow.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 lo (/.f64 (-.f64 x lo) hi)) hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 145 points increase in error, 70 points decrease in error
   (/.f64 (+.f64 (pow.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 x lo) hi) lo)) hi) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi))) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 32 points increase in error, 108 points decrease in error
   (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1)) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (*.f64 lo (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 125 points increase in error, 130 points decrease in error
   (/.f64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 lo (/.f64 (-.f64 x lo) hi)) hi)) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 51 points increase in error, 110 points decrease in error
   (/.f64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 x lo) hi) lo)) hi) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1) (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (-.f64 (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi))) 2) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 82 points increase in error, 14 points decrease in error
   (/.f64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1) (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2)) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))))): 20 points increase in error, 32 points decrease in error
   (/.f64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) 1) (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2))) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate-*r/_binary64 (*.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 3) (pow.f64 (/.f64 (-.f64 x lo) hi) 3)) (/.f64 1 (-.f64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (*.f64 (/.f64 lo hi) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)))))): 29 points increase in error, 40 points decrease in error

6. Applied egg-rr 0.4

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

7. Simplified 0.4

   \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{x - lo}{hi}, \frac{x - lo}{hi} - lo \cdot \frac{x - lo}{hi \cdot hi}, {\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{2}\right) \cdot \mathsf{fma}\left(lo, \frac{x - lo}{hi \cdot hi}, \frac{x - lo}{hi}\right)}}{{\left(\frac{x - lo}{hi}\right)}^{2} + \left({\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{2} - \frac{lo}{hi} \cdot {\left(\frac{x - lo}{hi}\right)}^{2}\right)} \]
   Proof
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) hi)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 244 points increase in error, 11 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 x lo) hi))) hi))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 hi) (/.f64 (-.f64 x lo) hi))))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 35 points increase in error, 37 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (*.f64 (/.f64 1 hi) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 x lo))) hi)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (*.f64 (/.f64 1 hi) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 hi) (-.f64 x lo)))))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 35 points increase in error, 25 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 1 hi) (/.f64 1 hi)) (-.f64 x lo))))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 11 points increase in error, 244 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (*.f64 (*.f64 (Rewrite<= unpow-1_binary64 (pow.f64 hi -1)) (/.f64 1 hi)) (-.f64 x lo)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (*.f64 (*.f64 (pow.f64 hi -1) (Rewrite<= unpow-1_binary64 (pow.f64 hi -1))) (-.f64 x lo)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 hi (*.f64 2 -1))) (-.f64 x lo)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (*.f64 (pow.f64 hi (Rewrite=> metadata-eval -2)) (-.f64 x lo)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 lo (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 x lo) (pow.f64 hi -2))))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (-.f64 x lo) (pow.f64 hi -2)) lo))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (Rewrite<= associate-*r*_binary64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)))) (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 239 points increase in error, 16 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 x lo) hi))) hi)) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 hi) (/.f64 (-.f64 x lo) hi)))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 38 points increase in error, 36 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (*.f64 (/.f64 1 hi) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 x lo))) hi))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (*.f64 (/.f64 1 hi) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 hi) (-.f64 x lo))))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 36 points increase in error, 27 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 1 hi) (/.f64 1 hi)) (-.f64 x lo)))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 16 points increase in error, 239 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (*.f64 (*.f64 (Rewrite<= unpow-1_binary64 (pow.f64 hi -1)) (/.f64 1 hi)) (-.f64 x lo))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (*.f64 (*.f64 (pow.f64 hi -1) (Rewrite<= unpow-1_binary64 (pow.f64 hi -1))) (-.f64 x lo))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 hi (*.f64 2 -1))) (-.f64 x lo))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (*.f64 (pow.f64 hi (Rewrite=> metadata-eval -2)) (-.f64 x lo))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 lo (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 x lo) (pow.f64 hi -2)))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (-.f64 x lo) (pow.f64 hi -2)) lo)) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) 2)) (fma.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) hi)) (/.f64 (-.f64 x lo) hi))): 254 points increase in error, 1 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 x lo) hi))) hi) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 hi) (/.f64 (-.f64 x lo) hi))) (/.f64 (-.f64 x lo) hi))): 38 points increase in error, 36 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (*.f64 (/.f64 1 hi) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 x lo))) hi)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (*.f64 (/.f64 1 hi) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 hi) (-.f64 x lo)))) (/.f64 (-.f64 x lo) hi))): 37 points increase in error, 26 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 1 hi) (/.f64 1 hi)) (-.f64 x lo))) (/.f64 (-.f64 x lo) hi))): 1 points increase in error, 254 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (*.f64 (*.f64 (Rewrite<= unpow-1_binary64 (pow.f64 hi -1)) (/.f64 1 hi)) (-.f64 x lo)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (*.f64 (*.f64 (pow.f64 hi -1) (Rewrite<= unpow-1_binary64 (pow.f64 hi -1))) (-.f64 x lo)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 hi (*.f64 2 -1))) (-.f64 x lo)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (*.f64 (pow.f64 hi (Rewrite=> metadata-eval -2)) (-.f64 x lo)) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error
   (*.f64 (fma.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 (-.f64 x lo) hi) (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo))) (pow.f64 (*.f64 (-.f64 x lo) (*.f64 (pow.f64 hi -2) lo)) 2)) (fma.f64 lo (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 x lo) (pow.f64 hi -2))) (/.f64 (-.f64 x lo) hi))): 0 points increase in error, 0 points decrease in error

8. Applied egg-rr 0.4

   \[\leadsto \frac{\mathsf{fma}\left(\frac{x - lo}{hi}, \frac{x - lo}{hi} - lo \cdot \frac{x - lo}{hi \cdot hi}, {\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{2}\right) \cdot \mathsf{fma}\left(lo, \frac{x - lo}{hi \cdot hi}, \frac{x - lo}{hi}\right)}{\color{blue}{\log \left(e^{{\left(\frac{x - lo}{hi}\right)}^{2}}\right)} + \left({\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{2} - \frac{lo}{hi} \cdot {\left(\frac{x - lo}{hi}\right)}^{2}\right)} \]

9. Final simplification 0.4

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

Alternatives

Alternative 1
Error	0.4
Cost	36160

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

Alternative 2
Error	0.5
Cost	27840

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

Alternative 3
Error	0.5
Cost	14656

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

Alternative 4
Error	51.6
Cost	448

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

Alternative 5
Error	52.0
Cost	256

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

Alternative 6
Error	52.0
Cost	64

\[1 \]

Reproduce

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