Average Error: 62.0 → 48.4
Time: 12.2s
Precision: binary64
Cost: 61184
\[lo < -1 \cdot 10^{+308} \land hi > 10^{+308}\]
\[\frac{x - lo}{hi - lo} \]
\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := \sqrt[3]{t_0}\\ 1 + \frac{{\left({t_1}^{2}\right)}^{4} \cdot {t_1}^{4} - {\left(hi \cdot \left(\left(hi - x\right) \cdot {lo}^{-2}\right)\right)}^{4}}{{t_0}^{2} \cdot \left(1 + {\left(\frac{hi}{lo}\right)}^{2}\right)} \cdot \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)} \end{array} \]
(FPCore (lo hi x) :precision binary64 (/ (- x lo) (- hi lo)))
(FPCore (lo hi x)
 :precision binary64
 (let* ((t_0 (/ (- hi x) lo)) (t_1 (cbrt t_0)))
   (+
    1.0
    (*
     (/
      (-
       (* (pow (pow t_1 2.0) 4.0) (pow t_1 4.0))
       (pow (* hi (* (- hi x) (pow lo -2.0))) 4.0))
      (* (pow t_0 2.0) (+ 1.0 (pow (/ hi lo) 2.0))))
     (/ 1.0 (* (- hi x) (- (/ 1.0 lo) (/ hi (* lo lo)))))))))
double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}
double code(double lo, double hi, double x) {
	double t_0 = (hi - x) / lo;
	double t_1 = cbrt(t_0);
	return 1.0 + ((((pow(pow(t_1, 2.0), 4.0) * pow(t_1, 4.0)) - pow((hi * ((hi - x) * pow(lo, -2.0))), 4.0)) / (pow(t_0, 2.0) * (1.0 + pow((hi / lo), 2.0)))) * (1.0 / ((hi - x) * ((1.0 / lo) - (hi / (lo * lo))))));
}
public static double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}
public static double code(double lo, double hi, double x) {
	double t_0 = (hi - x) / lo;
	double t_1 = Math.cbrt(t_0);
	return 1.0 + ((((Math.pow(Math.pow(t_1, 2.0), 4.0) * Math.pow(t_1, 4.0)) - Math.pow((hi * ((hi - x) * Math.pow(lo, -2.0))), 4.0)) / (Math.pow(t_0, 2.0) * (1.0 + Math.pow((hi / lo), 2.0)))) * (1.0 / ((hi - x) * ((1.0 / lo) - (hi / (lo * lo))))));
}
function code(lo, hi, x)
	return Float64(Float64(x - lo) / Float64(hi - lo))
end
function code(lo, hi, x)
	t_0 = Float64(Float64(hi - x) / lo)
	t_1 = cbrt(t_0)
	return Float64(1.0 + Float64(Float64(Float64(Float64(((t_1 ^ 2.0) ^ 4.0) * (t_1 ^ 4.0)) - (Float64(hi * Float64(Float64(hi - x) * (lo ^ -2.0))) ^ 4.0)) / Float64((t_0 ^ 2.0) * Float64(1.0 + (Float64(hi / lo) ^ 2.0)))) * Float64(1.0 / Float64(Float64(hi - x) * Float64(Float64(1.0 / lo) - Float64(hi / Float64(lo * lo)))))))
end
code[lo_, hi_, x_] := N[(N[(x - lo), $MachinePrecision] / N[(hi - lo), $MachinePrecision]), $MachinePrecision]
code[lo_, hi_, x_] := Block[{t$95$0 = N[(N[(hi - x), $MachinePrecision] / lo), $MachinePrecision]}, Block[{t$95$1 = N[Power[t$95$0, 1/3], $MachinePrecision]}, N[(1.0 + N[(N[(N[(N[(N[Power[N[Power[t$95$1, 2.0], $MachinePrecision], 4.0], $MachinePrecision] * N[Power[t$95$1, 4.0], $MachinePrecision]), $MachinePrecision] - N[Power[N[(hi * N[(N[(hi - x), $MachinePrecision] * N[Power[lo, -2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 4.0], $MachinePrecision]), $MachinePrecision] / N[(N[Power[t$95$0, 2.0], $MachinePrecision] * N[(1.0 + N[Power[N[(hi / lo), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(1.0 / N[(N[(hi - x), $MachinePrecision] * N[(N[(1.0 / lo), $MachinePrecision] - N[(hi / N[(lo * lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\frac{x - lo}{hi - lo}
\begin{array}{l}
t_0 := \frac{hi - x}{lo}\\
t_1 := \sqrt[3]{t_0}\\
1 + \frac{{\left({t_1}^{2}\right)}^{4} \cdot {t_1}^{4} - {\left(hi \cdot \left(\left(hi - x\right) \cdot {lo}^{-2}\right)\right)}^{4}}{{t_0}^{2} \cdot \left(1 + {\left(\frac{hi}{lo}\right)}^{2}\right)} \cdot \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)}
\end{array}

Error

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 62.0

    \[\frac{x - lo}{hi - lo} \]
  2. Taylor expanded in lo around inf 64.0

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

    \[\leadsto \color{blue}{1 + \left(\frac{hi - x}{lo} + \frac{hi - x}{\frac{lo}{\frac{hi}{lo}}}\right)} \]
    Proof
    (+.f64 1 (+.f64 (/.f64 (-.f64 hi x) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 hi (neg.f64 x))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (+.f64 hi (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 x) hi)) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (+.f64 (*.f64 -1 x) (Rewrite<= *-lft-identity_binary64 (*.f64 1 hi))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (+.f64 (*.f64 -1 x) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) hi)) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (/.f64 (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 x hi))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 x hi) lo))) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 hi (neg.f64 x))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (+.f64 hi (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 x) hi)) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (+.f64 (*.f64 -1 x) (Rewrite<= *-lft-identity_binary64 (*.f64 1 hi))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (+.f64 (*.f64 -1 x) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) hi)) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 x hi))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 -1 (-.f64 x hi)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 lo lo) hi))))): 191 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 -1 (-.f64 x hi)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 lo 2)) hi)))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 x hi) (/.f64 (pow.f64 lo 2) hi)))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 -1 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 256 points increase in error, 0 points decrease in error
    (+.f64 1 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))) (*.f64 -1 (/.f64 (-.f64 x hi) lo)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (*.f64 (-.f64 x hi) hi)) (pow.f64 lo 2)))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 -1 (-.f64 x hi)) hi)) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (/.f64 (*.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) hi) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi)))) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1)) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 x hi)) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 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 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 -1 x) lo) (/.f64 (*.f64 -1 hi) lo)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 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 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 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 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (*.f64 -1 (/.f64 x lo))) (*.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 x lo)) (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1))) (*.f64 -1 (/.f64 hi lo))): 0 points increase in error, 0 points decrease in error
  4. Applied egg-rr51.5

    \[\leadsto 1 + \color{blue}{\left({\left(\frac{hi - x}{lo}\right)}^{2} - {\left(\frac{hi}{lo} \cdot \frac{hi - x}{lo}\right)}^{2}\right) \cdot \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)}} \]
  5. Applied egg-rr64.0

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

    \[\leadsto 1 + \color{blue}{\frac{{\left(\frac{hi - x}{lo}\right)}^{4} - {\left(hi \cdot \left(\left(hi - x\right) \cdot {lo}^{-2}\right)\right)}^{4}}{{\left(\frac{hi - x}{lo}\right)}^{2} \cdot \left(1 + {\left(\frac{hi}{lo}\right)}^{2}\right)}} \cdot \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)} \]
    Proof
    (/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 hi (*.f64 (-.f64 hi x) (pow.f64 lo -2))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 0 points increase in error, 0 points decrease in error
    (/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 256 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) 1)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 0 points increase in error, 0 points decrease in error
    (/.f64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) 1) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (/.f64 hi lo) 2) 1)))): 0 points increase in error, 0 points decrease in error
    (/.f64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) 1) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (pow.f64 (/.f64 hi lo) 2) 1) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) (/.f64 1 (*.f64 (+.f64 (pow.f64 (/.f64 hi lo) 2) 1) (pow.f64 (/.f64 (-.f64 hi x) lo) 2))))): 0 points increase in error, 0 points decrease in error
  7. Applied egg-rr48.4

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

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

Alternatives

Alternative 1
Error48.4
Cost47872
\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ 1 + \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)} \cdot \frac{\log \left(e^{{t_0}^{4}}\right) - {\left(hi \cdot \left(\left(hi - x\right) \cdot {lo}^{-2}\right)\right)}^{4}}{{t_0}^{2} \cdot \left(1 + {\left(\frac{hi}{lo}\right)}^{2}\right)} \end{array} \]
Alternative 2
Error48.4
Cost28608
\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := \frac{hi}{lo \cdot lo}\\ 1 + \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - t_1\right)} \cdot \frac{{t_0}^{4} - {\left(hi \cdot t_1\right)}^{4}}{{t_0}^{2} \cdot \left(1 + {\left(\frac{hi}{lo}\right)}^{2}\right)} \end{array} \]
Alternative 3
Error51.5
Cost8960
\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ 1 + \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)} \cdot \left(t_0 \cdot t_0 - {\left(t_0 \cdot \frac{hi}{lo}\right)}^{2}\right) \end{array} \]
Alternative 4
Error52.0
Cost576
\[\frac{lo \cdot \left(\frac{x}{hi} + -1\right)}{hi} \]
Alternative 5
Error52.0
Cost256
\[\frac{-lo}{hi} \]
Alternative 6
Error52.0
Cost64
\[1 \]

Error

Reproduce

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