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

Average Error: 62.0 → 15.5

Time: 10.5s

Precision: binary64

Cost: 21256

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

Math

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

↓

\[\begin{array}{l} t_0 := \frac{x - hi}{lo}\\ t_1 := 1 + {\left(\left(-1 - \frac{hi}{lo}\right) \cdot t_0\right)}^{3}\\ t_2 := 1 + t_0 \cdot \left(1 + \frac{hi}{lo}\right)\\ \mathbf{if}\;x \leq -8.565711362251411 \cdot 10^{+111}:\\ \;\;\;\;\frac{t_1}{\left(-1 + \left(1 + {t_0}^{2}\right)\right) + t_2}\\ \mathbf{elif}\;x \leq 1.687909615090524 \cdot 10^{+79}:\\ \;\;\;\;\frac{1 - \frac{{x}^{3}}{{lo}^{3}}}{t_2 + {\left(\frac{hi - x}{lo}\right)}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_1}{t_2 + \frac{hi}{lo} \cdot \frac{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 hi) lo))
        (t_1 (+ 1.0 (pow (* (- -1.0 (/ hi lo)) t_0) 3.0)))
        (t_2 (+ 1.0 (* t_0 (+ 1.0 (/ hi lo))))))
   (if (<= x -8.565711362251411e+111)
     (/ t_1 (+ (+ -1.0 (+ 1.0 (pow t_0 2.0))) t_2))
     (if (<= x 1.687909615090524e+79)
       (/
        (- 1.0 (/ (pow x 3.0) (pow lo 3.0)))
        (+ t_2 (pow (/ (- hi x) lo) 2.0)))
       (/ t_1 (+ t_2 (* (/ hi lo) (/ 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 - hi) / lo;
	double t_1 = 1.0 + pow(((-1.0 - (hi / lo)) * t_0), 3.0);
	double t_2 = 1.0 + (t_0 * (1.0 + (hi / lo)));
	double tmp;
	if (x <= -8.565711362251411e+111) {
		tmp = t_1 / ((-1.0 + (1.0 + pow(t_0, 2.0))) + t_2);
	} else if (x <= 1.687909615090524e+79) {
		tmp = (1.0 - (pow(x, 3.0) / pow(lo, 3.0))) / (t_2 + pow(((hi - x) / lo), 2.0));
	} else {
		tmp = t_1 / (t_2 + ((hi / lo) * (hi / lo)));
	}
	return tmp;
}

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
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: tmp
    t_0 = (x - hi) / lo
    t_1 = 1.0d0 + ((((-1.0d0) - (hi / lo)) * t_0) ** 3.0d0)
    t_2 = 1.0d0 + (t_0 * (1.0d0 + (hi / lo)))
    if (x <= (-8.565711362251411d+111)) then
        tmp = t_1 / (((-1.0d0) + (1.0d0 + (t_0 ** 2.0d0))) + t_2)
    else if (x <= 1.687909615090524d+79) then
        tmp = (1.0d0 - ((x ** 3.0d0) / (lo ** 3.0d0))) / (t_2 + (((hi - x) / lo) ** 2.0d0))
    else
        tmp = t_1 / (t_2 + ((hi / lo) * (hi / lo)))
    end if
    code = tmp
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 = (x - hi) / lo;
	double t_1 = 1.0 + Math.pow(((-1.0 - (hi / lo)) * t_0), 3.0);
	double t_2 = 1.0 + (t_0 * (1.0 + (hi / lo)));
	double tmp;
	if (x <= -8.565711362251411e+111) {
		tmp = t_1 / ((-1.0 + (1.0 + Math.pow(t_0, 2.0))) + t_2);
	} else if (x <= 1.687909615090524e+79) {
		tmp = (1.0 - (Math.pow(x, 3.0) / Math.pow(lo, 3.0))) / (t_2 + Math.pow(((hi - x) / lo), 2.0));
	} else {
		tmp = t_1 / (t_2 + ((hi / lo) * (hi / lo)));
	}
	return tmp;
}

Python

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

↓

def code(lo, hi, x):
	t_0 = (x - hi) / lo
	t_1 = 1.0 + math.pow(((-1.0 - (hi / lo)) * t_0), 3.0)
	t_2 = 1.0 + (t_0 * (1.0 + (hi / lo)))
	tmp = 0
	if x <= -8.565711362251411e+111:
		tmp = t_1 / ((-1.0 + (1.0 + math.pow(t_0, 2.0))) + t_2)
	elif x <= 1.687909615090524e+79:
		tmp = (1.0 - (math.pow(x, 3.0) / math.pow(lo, 3.0))) / (t_2 + math.pow(((hi - x) / lo), 2.0))
	else:
		tmp = t_1 / (t_2 + ((hi / lo) * (hi / lo)))
	return tmp

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 - hi) / lo)
	t_1 = Float64(1.0 + (Float64(Float64(-1.0 - Float64(hi / lo)) * t_0) ^ 3.0))
	t_2 = Float64(1.0 + Float64(t_0 * Float64(1.0 + Float64(hi / lo))))
	tmp = 0.0
	if (x <= -8.565711362251411e+111)
		tmp = Float64(t_1 / Float64(Float64(-1.0 + Float64(1.0 + (t_0 ^ 2.0))) + t_2));
	elseif (x <= 1.687909615090524e+79)
		tmp = Float64(Float64(1.0 - Float64((x ^ 3.0) / (lo ^ 3.0))) / Float64(t_2 + (Float64(Float64(hi - x) / lo) ^ 2.0)));
	else
		tmp = Float64(t_1 / Float64(t_2 + Float64(Float64(hi / lo) * Float64(hi / lo))));
	end
	return tmp
end

MATLAB

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

↓

function tmp_2 = code(lo, hi, x)
	t_0 = (x - hi) / lo;
	t_1 = 1.0 + (((-1.0 - (hi / lo)) * t_0) ^ 3.0);
	t_2 = 1.0 + (t_0 * (1.0 + (hi / lo)));
	tmp = 0.0;
	if (x <= -8.565711362251411e+111)
		tmp = t_1 / ((-1.0 + (1.0 + (t_0 ^ 2.0))) + t_2);
	elseif (x <= 1.687909615090524e+79)
		tmp = (1.0 - ((x ^ 3.0) / (lo ^ 3.0))) / (t_2 + (((hi - x) / lo) ^ 2.0));
	else
		tmp = t_1 / (t_2 + ((hi / lo) * (hi / lo)));
	end
	tmp_2 = tmp;
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 - hi), $MachinePrecision] / lo), $MachinePrecision]}, Block[{t$95$1 = N[(1.0 + N[Power[N[(N[(-1.0 - N[(hi / lo), $MachinePrecision]), $MachinePrecision] * t$95$0), $MachinePrecision], 3.0], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(1.0 + N[(t$95$0 * N[(1.0 + N[(hi / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[x, -8.565711362251411e+111], N[(t$95$1 / N[(N[(-1.0 + N[(1.0 + N[Power[t$95$0, 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$2), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 1.687909615090524e+79], N[(N[(1.0 - N[(N[Power[x, 3.0], $MachinePrecision] / N[Power[lo, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(t$95$2 + N[Power[N[(N[(hi - x), $MachinePrecision] / lo), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(t$95$1 / N[(t$95$2 + N[(N[(hi / lo), $MachinePrecision] * N[(hi / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]]

Derivation

1. Split input into 3 regimes

2. if x < -8.565711362251411e111

   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 51.9

      \[\leadsto \color{blue}{1 + \frac{x - hi}{lo} \cdot \left(-1 - \frac{hi}{lo}\right)} \]
      Proof
      (+.f64 1 (*.f64 (/.f64 (-.f64 x hi) lo) (-.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 (/.f64 hi lo) (/.f64 (-.f64 x hi) lo))))): 15 points increase in error, 13 points decrease in error
      (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (-.f64 x hi)) (*.f64 lo lo))))): 256 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 x hi) hi)) (*.f64 lo lo)))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 (-.f64 x hi) hi) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (neg.f64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 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) (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x lo) (/.f64 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<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 x lo)) (*.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.9

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

   5. Taylor expanded in hi around 0 43.8

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

   6. Applied egg-rr 43.8

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

   if -8.565711362251411e111 < x < 1.6879096150905239e79

   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 51.9

      \[\leadsto \color{blue}{1 + \frac{x - hi}{lo} \cdot \left(-1 - \frac{hi}{lo}\right)} \]
      Proof
      (+.f64 1 (*.f64 (/.f64 (-.f64 x hi) lo) (-.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 (/.f64 hi lo) (/.f64 (-.f64 x hi) lo))))): 15 points increase in error, 13 points decrease in error
      (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (-.f64 x hi)) (*.f64 lo lo))))): 256 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 x hi) hi)) (*.f64 lo lo)))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 (-.f64 x hi) hi) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (neg.f64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 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) (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x lo) (/.f64 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<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 x lo)) (*.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.9

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

   5. Taylor expanded in hi around 0 43.7

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

   6. Taylor expanded in hi around 0 0.9

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

   7. Simplified 0.9

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

   if 1.6879096150905239e79 < x

   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 51.9

      \[\leadsto \color{blue}{1 + \frac{x - hi}{lo} \cdot \left(-1 - \frac{hi}{lo}\right)} \]
      Proof
      (+.f64 1 (*.f64 (/.f64 (-.f64 x hi) lo) (-.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 (/.f64 hi lo) (/.f64 (-.f64 x hi) lo))))): 15 points increase in error, 13 points decrease in error
      (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (-.f64 x hi)) (*.f64 lo lo))))): 256 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 x hi) hi)) (*.f64 lo lo)))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 (-.f64 x hi) hi) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (neg.f64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 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) (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x lo) (/.f64 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<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 x lo)) (*.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.9

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

   5. Taylor expanded in hi around 0 43.6

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

   6. Taylor expanded in x around 0 64.0

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

   7. Simplified 43.7

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

4. Final simplification 15.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -8.565711362251411 \cdot 10^{+111}:\\ \;\;\;\;\frac{1 + {\left(\left(-1 - \frac{hi}{lo}\right) \cdot \frac{x - hi}{lo}\right)}^{3}}{\left(-1 + \left(1 + {\left(\frac{x - hi}{lo}\right)}^{2}\right)\right) + \left(1 + \frac{x - hi}{lo} \cdot \left(1 + \frac{hi}{lo}\right)\right)}\\ \mathbf{elif}\;x \leq 1.687909615090524 \cdot 10^{+79}:\\ \;\;\;\;\frac{1 - \frac{{x}^{3}}{{lo}^{3}}}{\left(1 + \frac{x - hi}{lo} \cdot \left(1 + \frac{hi}{lo}\right)\right) + {\left(\frac{hi - x}{lo}\right)}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1 + {\left(\left(-1 - \frac{hi}{lo}\right) \cdot \frac{x - hi}{lo}\right)}^{3}}{\left(1 + \frac{x - hi}{lo} \cdot \left(1 + \frac{hi}{lo}\right)\right) + \frac{hi}{lo} \cdot \frac{hi}{lo}}\\ \end{array} \]

Alternatives

Alternative 1
Error	51.6
Cost	448

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

Alternative 2
Error	52.0
Cost	256

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

Alternative 3
Error	52.1
Cost	64

\[1 \]

Reproduce

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