Average Error: 0.9 → 0.6
Time: 51.2s
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{\alpha + \beta}{1.0}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 2.0} \cdot \left(\frac{1.0}{\alpha + \left(\beta + 2 \cdot i\right)} \cdot \left(\beta - \alpha\right)\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{\alpha + \beta}{1.0}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 2.0} \cdot \left(\frac{1.0}{\alpha + \left(\beta + 2 \cdot i\right)} \cdot \left(\beta - \alpha\right)\right) + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r4104572 = alpha;
        double r4104573 = beta;
        double r4104574 = r4104572 + r4104573;
        double r4104575 = r4104573 - r4104572;
        double r4104576 = r4104574 * r4104575;
        double r4104577 = 2.0;
        double r4104578 = /* ERROR: no posit support in C */;
        double r4104579 = i;
        double r4104580 = r4104578 * r4104579;
        double r4104581 = r4104574 + r4104580;
        double r4104582 = r4104576 / r4104581;
        double r4104583 = 2.0;
        double r4104584 = /* ERROR: no posit support in C */;
        double r4104585 = r4104581 + r4104584;
        double r4104586 = r4104582 / r4104585;
        double r4104587 = 1.0;
        double r4104588 = /* ERROR: no posit support in C */;
        double r4104589 = r4104586 + r4104588;
        double r4104590 = r4104589 / r4104584;
        return r4104590;
}
↓
double f(double alpha, double beta, double i) {
        double r4104591 = alpha;
        double r4104592 = beta;
        double r4104593 = r4104591 + r4104592;
        double r4104594 = 1.0;
        double r4104595 = r4104593 / r4104594;
        double r4104596 = 2.0;
        double r4104597 = i;
        double r4104598 = r4104596 * r4104597;
        double r4104599 = r4104593 + r4104598;
        double r4104600 = 2.0;
        double r4104601 = r4104599 + r4104600;
        double r4104602 = r4104595 / r4104601;
        double r4104603 = r4104592 + r4104598;
        double r4104604 = r4104591 + r4104603;
        double r4104605 = r4104594 / r4104604;
        double r4104606 = r4104592 - r4104591;
        double r4104607 = r4104605 * r4104606;
        double r4104608 = r4104602 * r4104607;
        double r4104609 = r4104608 + r4104594;
        double r4104610 = r4104609 / r4104600;
        return r4104610;
}

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-rgt-identity-expand0.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(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right) \cdot \left(1.0\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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}}\right)}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right) \cdot \left(1.0\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  5. Applied p16-times-frac0.6

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

  6. Applied p16-times-frac0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(1.0\right)}\right)\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  7. Simplified0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \color{blue}{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\left(i \cdot \left(2\right)\right)}\right)}{\beta}\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  8. Using strategy rm

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

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \left(\frac{\left(\beta - \alpha\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\left(i \cdot \left(2\right)\right)}\right)}{\beta}\right) \cdot \left(1.0\right)\right)}}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  10. Applied p16-*-un-lft-identity0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\beta - \alpha\right)\right)}}{\left(\left(\frac{\left(\frac{\alpha}{\left(i \cdot \left(2\right)\right)}\right)}{\beta}\right) \cdot \left(1.0\right)\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  11. Applied p16-times-frac0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \color{blue}{\left(\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\alpha}{\left(i \cdot \left(2\right)\right)}\right)}{\beta}\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  12. Simplified0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \left(\color{blue}{\left(\frac{\left(1.0\right)}{\left(\frac{\alpha}{\left(\frac{\beta}{\left(\left(2\right) \cdot i\right)}\right)}\right)}\right)} \cdot \left(\frac{\left(\beta - \alpha\right)}{\left(1.0\right)}\right)\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  13. Simplified0.6

    \[\leadsto \frac{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\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) \cdot \left(\left(\frac{\left(1.0\right)}{\left(\frac{\alpha}{\left(\frac{\beta}{\left(\left(2\right) \cdot i\right)}\right)}\right)}\right) \cdot \color{blue}{\left(\beta - \alpha\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  14. Final simplification0.6

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

Reproduce

herbie shell --seed 2019165 
(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)))