Average Error: 0.6 → 0.7
Time: 25.5s
Precision: 64
\[\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(1\right)}{x}\right)\]
↓
\[\frac{\frac{1}{x} + \frac{1}{x + 1}}{1.0} \cdot \left(\frac{\frac{1}{x + 1} - \frac{1}{x}}{1.0} \cdot \frac{1.0}{\frac{1}{x} + \frac{1}{x + 1}}\right)\]
\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(1\right)}{x}\right)
↓
\frac{\frac{1}{x} + \frac{1}{x + 1}}{1.0} \cdot \left(\frac{\frac{1}{x + 1} - \frac{1}{x}}{1.0} \cdot \frac{1.0}{\frac{1}{x} + \frac{1}{x + 1}}\right)
double f(double x) {
        double r5113129 = 1.0;
        double r5113130 = /* ERROR: no posit support in C */;
        double r5113131 = x;
        double r5113132 = r5113131 + r5113130;
        double r5113133 = r5113130 / r5113132;
        double r5113134 = r5113130 / r5113131;
        double r5113135 = r5113133 - r5113134;
        return r5113135;
}
↓
double f(double x) {
        double r5113136 = 1.0;
        double r5113137 = x;
        double r5113138 = r5113136 / r5113137;
        double r5113139 = r5113137 + r5113136;
        double r5113140 = r5113136 / r5113139;
        double r5113141 = r5113138 + r5113140;
        double r5113142 = 1.0;
        double r5113143 = r5113141 / r5113142;
        double r5113144 = r5113140 - r5113138;
        double r5113145 = r5113144 / r5113142;
        double r5113146 = r5113142 / r5113141;
        double r5113147 = r5113145 * r5113146;
        double r5113148 = r5113143 * r5113147;
        return r5113148;
}

Error

Bits error versus x

Derivation

  1. Initial program 0.6

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

  3. Applied p16-flip--1.3

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

  4. Simplified1.0

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

  5. Simplified1.0

    \[\leadsto \frac{\left(\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(1\right)}{x}\right)\right) \cdot \left(\frac{\left(\frac{\left(1\right)}{x}\right)}{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}\right)\right)}{\color{blue}{\left(\frac{\left(\frac{\left(1\right)}{x}\right)}{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}\right)}}\]
  6. Using strategy rm

  7. Applied p16-*-un-lft-identity1.0

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

  8. Applied p16-*-un-lft-identity1.0

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

  9. Applied distribute-lft-out1.0

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

  10. Applied *-commutative1.0

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

  11. Applied p16-times-frac0.7

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{x}\right)}{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(1\right)}{x}\right)\right)}{\left(\frac{\left(\frac{\left(1\right)}{x}\right)}{\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)}\right)}\right)}\]
  12. Using strategy rm

  13. Applied p16-*-un-lft-identity0.7

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

  14. Applied p16-*-un-lft-identity0.7

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

  15. Applied distribute-lft-out0.7

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

  16. Applied *p16-rgt-identity-expand0.7

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

  17. Applied p16-times-frac0.7

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

  18. Final simplification0.7

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

Reproduce

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