xlohi (overflows)

Average Error: 62.0 → 48.5

Time: 12.5s

Precision: binary64

Cost: 28672

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

Math

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

↓

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ 1 + \frac{{t_0}^{4} - {\left(\frac{hi}{lo} \cdot \frac{-x}{lo}\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

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

↓

(FPCore (lo hi x)
 :precision binary64
 (let* ((t_0 (/ (- hi x) lo)))
   (+
    1.0
    (*
     (/
      (- (pow t_0 4.0) (pow (* (/ hi lo) (/ (- x) lo)) 4.0))
      (* (pow t_0 2.0) (+ 1.0 (pow (/ hi lo) 2.0))))
     (/ 1.0 (* (- hi x) (- (/ 1.0 lo) (/ hi (* lo 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 = (hi - x) / lo;
	return 1.0 + (((pow(t_0, 4.0) - pow(((hi / lo) * (-x / lo)), 4.0)) / (pow(t_0, 2.0) * (1.0 + pow((hi / lo), 2.0)))) * (1.0 / ((hi - x) * ((1.0 / lo) - (hi / (lo * lo))))));
}

Fortran

real(8) function code(lo, hi, x)
    real(8), intent (in) :: lo
    real(8), intent (in) :: hi
    real(8), intent (in) :: x
    code = (x - lo) / (hi - lo)
end function

↓

real(8) function code(lo, hi, x)
    real(8), intent (in) :: lo
    real(8), intent (in) :: hi
    real(8), intent (in) :: x
    real(8) :: t_0
    t_0 = (hi - x) / lo
    code = 1.0d0 + ((((t_0 ** 4.0d0) - (((hi / lo) * (-x / lo)) ** 4.0d0)) / ((t_0 ** 2.0d0) * (1.0d0 + ((hi / lo) ** 2.0d0)))) * (1.0d0 / ((hi - x) * ((1.0d0 / lo) - (hi / (lo * lo))))))
end function

Java

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;
	return 1.0 + (((Math.pow(t_0, 4.0) - Math.pow(((hi / lo) * (-x / lo)), 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))))));
}

Python

def code(lo, hi, x):
	return (x - lo) / (hi - lo)

↓

def code(lo, hi, x):
	t_0 = (hi - x) / lo
	return 1.0 + (((math.pow(t_0, 4.0) - math.pow(((hi / lo) * (-x / lo)), 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))))))

Julia

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)
	return Float64(1.0 + Float64(Float64(Float64((t_0 ^ 4.0) - (Float64(Float64(hi / lo) * Float64(Float64(-x) / lo)) ^ 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

MATLAB

function tmp = code(lo, hi, x)
	tmp = (x - lo) / (hi - lo);
end

↓

function tmp = code(lo, hi, x)
	t_0 = (hi - x) / lo;
	tmp = 1.0 + ((((t_0 ^ 4.0) - (((hi / lo) * (-x / lo)) ^ 4.0)) / ((t_0 ^ 2.0) * (1.0 + ((hi / lo) ^ 2.0)))) * (1.0 / ((hi - x) * ((1.0 / lo) - (hi / (lo * 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[(N[(hi - x), $MachinePrecision] / lo), $MachinePrecision]}, N[(1.0 + N[(N[(N[(N[Power[t$95$0, 4.0], $MachinePrecision] - N[Power[N[(N[(hi / lo), $MachinePrecision] * N[((-x) / lo), $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]]

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. Simplified 52.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-rr 51.6

   \[\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-rr 64.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. Simplified 48.4

   \[\leadsto 1 + \color{blue}{\frac{{\left(\frac{hi - x}{lo}\right)}^{4} - {\left(\frac{hi}{lo \cdot lo} \cdot \left(hi - x\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 (/.f64 hi (*.f64 lo lo)) (-.f64 hi x)) 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 (*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 hi lo) lo)) (-.f64 hi x)) 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 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (/.f64 hi lo) (/.f64 lo (-.f64 hi x)))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 102 points increase in error, 95 points decrease in error
   (/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (/.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 hi)) lo) (/.f64 lo (-.f64 hi x))) 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 (/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 lo) hi)) (/.f64 lo (-.f64 hi x))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 93 points increase in error, 96 points decrease in error
   (/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (/.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 lo hi))) (/.f64 lo (-.f64 hi x))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 99 points increase in error, 80 points decrease in error
   (/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 (/.f64 lo hi) (/.f64 lo (-.f64 hi x))))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 42 points increase in error, 55 points decrease in error
   (/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (/.f64 1 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 lo lo) (*.f64 hi (-.f64 hi x))))) 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 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 (*.f64 lo lo)) (*.f64 hi (-.f64 hi x)))) 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 (*.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 lo) lo)) (*.f64 hi (-.f64 hi x))) 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 (*.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 lo))) lo) (*.f64 hi (-.f64 hi x))) 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 (*.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 lo) (/.f64 1 lo))) (*.f64 hi (-.f64 hi x))) 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 (*.f64 (*.f64 (Rewrite<= unpow-1_binary64 (pow.f64 lo -1)) (/.f64 1 lo)) (*.f64 hi (-.f64 hi x))) 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 (*.f64 (*.f64 (pow.f64 lo -1) (Rewrite<= unpow-1_binary64 (pow.f64 lo -1))) (*.f64 hi (-.f64 hi x))) 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 (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 lo (*.f64 2 -1))) (*.f64 hi (-.f64 hi x))) 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 (*.f64 (pow.f64 lo (Rewrite=> metadata-eval -2)) (*.f64 hi (-.f64 hi x))) 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<= *-commutative_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)))): 0 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. Taylor expanded in hi around 0 56.2

   \[\leadsto 1 + \frac{{\left(\frac{hi - x}{lo}\right)}^{4} - {\color{blue}{\left(-1 \cdot \frac{hi \cdot x}{{lo}^{2}}\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. Simplified 48.5

   \[\leadsto 1 + \frac{{\left(\frac{hi - x}{lo}\right)}^{4} - {\color{blue}{\left(\frac{hi}{lo} \cdot \frac{-x}{lo}\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 hi lo) (/.f64 (neg.f64 x) lo)): 0 points increase in error, 0 points decrease in error
   (*.f64 (/.f64 hi lo) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 x lo)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 hi lo) (/.f64 x lo)))): 0 points increase in error, 0 points decrease in error
   (neg.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi x) (*.f64 lo lo)))): 142 points increase in error, 4 points decrease in error
   (neg.f64 (/.f64 (*.f64 hi x) (Rewrite<= unpow2_binary64 (pow.f64 lo 2)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 hi x) (pow.f64 lo 2)))): 0 points increase in error, 0 points decrease in error

9. Final simplification 48.5

   \[\leadsto 1 + \frac{{\left(\frac{hi - x}{lo}\right)}^{4} - {\left(\frac{hi}{lo} \cdot \frac{-x}{lo}\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
Error	50.4
Cost	14272

\[\frac{x}{hi} - \mathsf{log1p}\left(\mathsf{fma}\left(0.5, \frac{lo}{hi} \cdot \frac{lo}{hi}, \frac{lo}{hi}\right) - \frac{x}{hi} \cdot \frac{lo}{hi}\right) \]

Alternative 2
Error	51.9
Cost	7552

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

Alternative 3
Error	51.9
Cost	832

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

Alternative 4
Error	52.0
Cost	576

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

Alternative 5
Error	52.0
Cost	256

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

Alternative 6
Error	52.0
Cost	64

\[1 \]

Reproduce

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