Average Error: 0.9 → 0.6
Time: 47.5s
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right) \land i \gt \left(0\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
↓
\[\frac{\frac{\frac{\beta + \alpha}{\beta + \left(\alpha + i \cdot 2\right)} \cdot \left(\beta - \alpha\right)}{2.0 + \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) + 0.0 \cdot i\right)} + 1.0}{2.0}\]
\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
↓
\frac{\frac{\frac{\beta + \alpha}{\beta + \left(\alpha + i \cdot 2\right)} \cdot \left(\beta - \alpha\right)}{2.0 + \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) + 0.0 \cdot i\right)} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r1111333 = alpha;
        double r1111334 = beta;
        double r1111335 = r1111333 + r1111334;
        double r1111336 = r1111334 - r1111333;
        double r1111337 = r1111335 * r1111336;
        double r1111338 = 2.0;
        double r1111339 = /* ERROR: no posit support in C */;
        double r1111340 = i;
        double r1111341 = r1111339 * r1111340;
        double r1111342 = r1111335 + r1111341;
        double r1111343 = r1111337 / r1111342;
        double r1111344 = 2.0;
        double r1111345 = /* ERROR: no posit support in C */;
        double r1111346 = r1111342 + r1111345;
        double r1111347 = r1111343 / r1111346;
        double r1111348 = 1.0;
        double r1111349 = /* ERROR: no posit support in C */;
        double r1111350 = r1111347 + r1111349;
        double r1111351 = r1111350 / r1111345;
        return r1111351;
}
↓
double f(double alpha, double beta, double i) {
        double r1111352 = beta;
        double r1111353 = alpha;
        double r1111354 = r1111352 + r1111353;
        double r1111355 = i;
        double r1111356 = 2.0;
        double r1111357 = r1111355 * r1111356;
        double r1111358 = r1111353 + r1111357;
        double r1111359 = r1111352 + r1111358;
        double r1111360 = r1111354 / r1111359;
        double r1111361 = r1111352 - r1111353;
        double r1111362 = r1111360 * r1111361;
        double r1111363 = 2.0;
        double r1111364 = r1111352 + r1111357;
        double r1111365 = r1111353 + r1111364;
        double r1111366 = 0.0;
        double r1111367 = r1111366 * r1111355;
        double r1111368 = r1111365 + r1111367;
        double r1111369 = r1111363 + r1111368;
        double r1111370 = r1111362 / r1111369;
        double r1111371 = 1.0;
        double r1111372 = r1111370 + r1111371;
        double r1111373 = r1111372 / r1111363;
        return r1111373;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 0.9

    \[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  2. Using strategy rm

  3. Applied p16-*-un-lft-identity0.9

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2.0\right)\right)}}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  4. Applied p16-*-un-lft-identity0.9

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}}{\left(\left(1.0\right) \cdot \left(2.0\right)\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  5. Applied distribute-lft-out0.9

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)\right)}}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  6. Applied *p16-rgt-identity-expand0.9

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(1.0\right)\right)}}\right)}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  7. Applied p16-times-frac0.6

    \[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)\right)}}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  8. Applied p16-times-frac0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  9. Simplified0.6

    \[\leadsto \frac{\left(\frac{\left(\color{blue}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)} \cdot \left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  10. Simplified0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right) \cdot \color{blue}{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(2.0\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  11. Using strategy rm

  12. Applied +p16-rgt-identity-expand0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(2.0\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \color{blue}{\left(\frac{\left(2\right)}{\left(0.0\right)}\right)}\right)}\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  13. Applied distribute-rgt-in0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(2.0\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\color{blue}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(\left(0.0\right) \cdot i\right)}\right)}}\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  14. Applied associate-+r+0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(2.0\right)}{\color{blue}{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(0.0\right) \cdot i\right)}\right)}}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  15. Simplified0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(2.0\right)}{\left(\frac{\color{blue}{\left(\frac{\alpha}{\left(\frac{\beta}{\left(i \cdot \left(2\right)\right)}\right)}\right)}}{\left(\left(0.0\right) \cdot i\right)}\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  16. Using strategy rm

  17. Applied associate-*r/0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(2.0\right)}{\left(\frac{\left(\frac{\alpha}{\left(\frac{\beta}{\left(i \cdot \left(2\right)\right)}\right)}\right)}{\left(\left(0.0\right) \cdot i\right)}\right)}\right)}\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  18. Using strategy rm

  19. Applied associate-+l+0.6

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\color{blue}{\left(\frac{\beta}{\left(\frac{\alpha}{\left(i \cdot \left(2\right)\right)}\right)}\right)}}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(2.0\right)}{\left(\frac{\left(\frac{\alpha}{\left(\frac{\beta}{\left(i \cdot \left(2\right)\right)}\right)}\right)}{\left(\left(0.0\right) \cdot i\right)}\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  20. Final simplification0.6

    \[\leadsto \frac{\frac{\frac{\beta + \alpha}{\beta + \left(\alpha + i \cdot 2\right)} \cdot \left(\beta - \alpha\right)}{2.0 + \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) + 0.0 \cdot i\right)} + 1.0}{2.0}\]

Reproduce

herbie shell --seed 2019154 
(FPCore (alpha beta i)
  :name "Octave 3.8, jcobi/2"
  :pre (and (>.p16 alpha (real->posit16 -1)) (>.p16 beta (real->posit16 -1)) (>.p16 i (real->posit16 0)))
  (/.p16 (+.p16 (/.p16 (/.p16 (*.p16 (+.p16 alpha beta) (-.p16 beta alpha)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)))