Average Error: 1.0 → 1.0
Time: 6.1m
Precision: 64
\[\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]
↓
\[\frac{1}{x + 1} + \left(\frac{1}{x - 1} - \frac{2}{x}\right)\]
\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}
↓
\frac{1}{x + 1} + \left(\frac{1}{x - 1} - \frac{2}{x}\right)
double f(double x) {
        double r5719210 = 1.0;
        double r5719211 = /* ERROR: no posit support in C */;
        double r5719212 = x;
        double r5719213 = r5719212 + r5719211;
        double r5719214 = r5719211 / r5719213;
        double r5719215 = 2.0;
        double r5719216 = /* ERROR: no posit support in C */;
        double r5719217 = r5719216 / r5719212;
        double r5719218 = r5719214 - r5719217;
        double r5719219 = r5719212 - r5719211;
        double r5719220 = r5719211 / r5719219;
        double r5719221 = r5719218 + r5719220;
        return r5719221;
}
↓
double f(double x) {
        double r5719222 = 1.0;
        double r5719223 = x;
        double r5719224 = r5719223 + r5719222;
        double r5719225 = r5719222 / r5719224;
        double r5719226 = r5719223 - r5719222;
        double r5719227 = r5719222 / r5719226;
        double r5719228 = 2.0;
        double r5719229 = r5719228 / r5719223;
        double r5719230 = r5719227 - r5719229;
        double r5719231 = r5719225 + r5719230;
        return r5719231;
}

Error

Bits error versus x

Derivation

  1. Initial program 1.0

    \[\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]
  2. Using strategy rm

  3. Applied +p16-rgt-identity-expand1.0

    \[\leadsto \frac{\left(\color{blue}{\left(\frac{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}{\left(0.0\right)}\right)} - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]

  4. Applied associate--l+1.0

    \[\leadsto \frac{\color{blue}{\left(\frac{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}{\left(\left(0.0\right) - \left(\frac{\left(2\right)}{x}\right)\right)}\right)}}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]

  5. Applied associate-+l+1.0

    \[\leadsto \color{blue}{\frac{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}{\left(\frac{\left(\left(0.0\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\right)}}\]

  6. Simplified1.0

    \[\leadsto \frac{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}{\color{blue}{\left(\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}}\]

  7. Final simplification1.0

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

Reproduce

herbie shell --seed 2019158 
(FPCore (x)
  :name "3frac (problem 3.3.3)"
  (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))