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

Average Error: 62.0 → 0.6

Time: 10.8s

Precision: binary64

Cost: 7680

\[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}^{2}}{t_0 \cdot \left(\frac{hi}{lo} + -1\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 2.0) (* t_0 (+ (/ hi lo) -1.0))))))

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, 2.0) / (t_0 * ((hi / lo) + -1.0)));
}

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 ** 2.0d0) / (t_0 * ((hi / lo) + (-1.0d0))))
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, 2.0) / (t_0 * ((hi / lo) + -1.0)));
}

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, 2.0) / (t_0 * ((hi / lo) + -1.0)))

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((t_0 ^ 2.0) / Float64(t_0 * Float64(Float64(hi / lo) + -1.0))))
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 ^ 2.0) / (t_0 * ((hi / lo) + -1.0)));
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[Power[t$95$0, 2.0], $MachinePrecision] / N[(t$95$0 * N[(N[(hi / lo), $MachinePrecision] + -1.0), $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))))): 179 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 55.0

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

5. Applied egg-rr 52.0

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

6. Simplified 0.6

   \[\leadsto 1 + \color{blue}{\frac{{\left(hi \cdot \frac{hi - x}{lo \cdot lo}\right)}^{2} - {\left(\frac{hi - x}{lo}\right)}^{2}}{\frac{hi - x}{lo} \cdot \left(\frac{hi}{lo} + -1\right)}} \]
   Proof
   (/.f64 (-.f64 (pow.f64 (*.f64 hi (/.f64 (-.f64 hi x) (*.f64 lo lo))) 2) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (pow.f64 (*.f64 hi (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (-.f64 hi x) lo) lo))) 2) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 256 points decrease in error
   (/.f64 (-.f64 (pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (/.f64 (-.f64 hi x) lo) lo) hi)) 2) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (pow.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (/.f64 (-.f64 hi x) lo) hi) lo)) 2) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 134 points increase in error, 75 points decrease in error
   (/.f64 (-.f64 (pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo))) 2) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 43 points increase in error, 101 points decrease in error
   (/.f64 (Rewrite=> sub-neg_binary64 (+.f64 (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2) (neg.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2)))) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2)) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (pow.f64 (/.f64 (-.f64 hi x) lo) 2))) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2)) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2)))) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2)))) (*.f64 (/.f64 (-.f64 hi x) lo) (+.f64 (/.f64 hi lo) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (/.f64 hi lo) (/.f64 (-.f64 hi x) lo)) (*.f64 -1 (/.f64 (-.f64 hi x) lo))))): 48 points increase in error, 41 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo))) (*.f64 -1 (/.f64 (-.f64 hi x) lo)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (+.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (-.f64 hi x) lo))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (/.f64 (-.f64 hi x) lo)) (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 (-.f64 hi x) lo))) (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 (-.f64 hi x) lo) (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)))))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (-.f64 0 (-.f64 (/.f64 (-.f64 hi x) lo) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (/.f64 (-.f64 hi x) lo) hi) lo))))): 86 points increase in error, 12 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (-.f64 0 (-.f64 (/.f64 (-.f64 hi x) lo) (/.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 hi x) hi) lo)) lo)))): 57 points increase in error, 129 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (-.f64 0 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (-.f64 hi x) (/.f64 (*.f64 (-.f64 hi x) hi) lo)) lo)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (neg.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (pow.f64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 hi lo)) 2))) (Rewrite<= neg-sub0_binary64 (neg.f64 (/.f64 (-.f64 (-.f64 hi x) (/.f64 (*.f64 (-.f64 hi x) hi) lo)) lo)))): 0 points increase in error, 0 points decrease in error

7. Taylor expanded in lo around inf 64.0

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

8. Simplified 0.6

   \[\leadsto 1 + \frac{\color{blue}{-{\left(\frac{hi - x}{lo}\right)}^{2}}}{\frac{hi - x}{lo} \cdot \left(\frac{hi}{lo} + -1\right)} \]
   Proof
   (neg.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2)): 0 points increase in error, 0 points decrease in error
   (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (pow.f64 (/.f64 (-.f64 hi x) lo) 2))): 0 points increase in error, 0 points decrease in error
   (*.f64 -1 (Rewrite=> unpow2_binary64 (*.f64 (/.f64 (-.f64 hi x) lo) (/.f64 (-.f64 hi x) lo)))): 0 points increase in error, 0 points decrease in error
   (*.f64 -1 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 hi x) (-.f64 hi x)) (*.f64 lo lo)))): 256 points increase in error, 0 points decrease in error
   (*.f64 -1 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 hi x) 2)) (*.f64 lo lo))): 0 points increase in error, 0 points decrease in error
   (*.f64 -1 (/.f64 (pow.f64 (-.f64 hi x) 2) (Rewrite<= unpow2_binary64 (pow.f64 lo 2)))): 0 points increase in error, 0 points decrease in error

9. Final simplification 0.6

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

Alternatives

Alternative 1
Error	51.9
Cost	832

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

Alternative 2
Error	52.0
Cost	576

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

Alternative 3
Error	52.0
Cost	256

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

Alternative 4
Error	52.0
Cost	64

\[1 \]

Reproduce

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