Average Error: 62.0 → 1.2
Time: 8.6s
Precision: 64
\[lo \lt -1 \cdot 10^{308} \land hi \gt 10^{308}\]
\[\frac{x - lo}{hi - lo}\]
↓
\[\frac{x}{hi - lo} - \frac{1}{{\left(\frac{hi}{lo}\right)}^{3} + -1} \cdot \left(\left(--1\right) + \frac{{\left(\frac{hi}{lo}\right)}^{6} + {\left(\frac{hi}{lo}\right)}^{3}}{\left({\left(\frac{hi}{lo}\right)}^{4} - {\left(\frac{hi}{lo}\right)}^{3}\right) + {\left(\frac{hi}{lo}\right)}^{2}}\right)\]
\frac{x - lo}{hi - lo}
↓
\frac{x}{hi - lo} - \frac{1}{{\left(\frac{hi}{lo}\right)}^{3} + -1} \cdot \left(\left(--1\right) + \frac{{\left(\frac{hi}{lo}\right)}^{6} + {\left(\frac{hi}{lo}\right)}^{3}}{\left({\left(\frac{hi}{lo}\right)}^{4} - {\left(\frac{hi}{lo}\right)}^{3}\right) + {\left(\frac{hi}{lo}\right)}^{2}}\right)
double f(double lo, double hi, double x) {
        double r20392 = x;
        double r20393 = lo;
        double r20394 = r20392 - r20393;
        double r20395 = hi;
        double r20396 = r20395 - r20393;
        double r20397 = r20394 / r20396;
        return r20397;
}
↓
double f(double lo, double hi, double x) {
        double r20398 = x;
        double r20399 = hi;
        double r20400 = lo;
        double r20401 = r20399 - r20400;
        double r20402 = r20398 / r20401;
        double r20403 = 1.0;
        double r20404 = r20399 / r20400;
        double r20405 = 3.0;
        double r20406 = pow(r20404, r20405);
        double r20407 = -1.0;
        double r20408 = r20406 + r20407;
        double r20409 = r20403 / r20408;
        double r20410 = -r20407;
        double r20411 = 6.0;
        double r20412 = pow(r20404, r20411);
        double r20413 = r20412 + r20406;
        double r20414 = 4.0;
        double r20415 = pow(r20404, r20414);
        double r20416 = r20415 - r20406;
        double r20417 = 2.0;
        double r20418 = pow(r20404, r20417);
        double r20419 = r20416 + r20418;
        double r20420 = r20413 / r20419;
        double r20421 = r20410 + r20420;
        double r20422 = r20409 * r20421;
        double r20423 = r20402 - r20422;
        return r20423;
}

Error

Bits error versus lo

Bits error versus hi

Bits error versus x

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. Using strategy rm

  3. Applied div-sub62.0

    \[\leadsto \color{blue}{\frac{x}{hi - lo} - \frac{lo}{hi - lo}}\]
  4. Using strategy rm

  5. Applied clear-num62.0

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1}{\frac{hi - lo}{lo}}}\]

  6. Simplified1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\color{blue}{-1 + \frac{hi}{lo}}}\]
  7. Using strategy rm

  8. Applied flip3-+1.2

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

  9. Applied associate-/r/1.2

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

  10. Simplified1.2

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1}{{\left(\frac{hi}{lo}\right)}^{3} + -1}} \cdot \left(-1 \cdot -1 + \left(\frac{hi}{lo} \cdot \frac{hi}{lo} - -1 \cdot \frac{hi}{lo}\right)\right)\]
  11. Using strategy rm

  12. Applied flip3--1.2

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

  13. Simplified1.2

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

  14. Simplified1.2

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

  15. Final simplification1.2

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

Reproduce

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