Average Error: 0.9 → 0.6
Time: 58.6s
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{\left(\frac{\left(\left(\frac{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\alpha}\right)}{\beta}\right)}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\beta}{\alpha}\right)}\right) \cdot \left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\left(\frac{\alpha}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(2.0\right)}\right)}\right) - \left(\left(0.0\right) - \beta\right)\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.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{\left(\frac{\left(\left(\frac{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\left(i \cdot \left(2\right)\right)}{\alpha}\right)}{\beta}\right)}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\beta}{\alpha}\right)}\right) \cdot \left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\left(\frac{\alpha}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(2.0\right)}\right)}\right) - \left(\left(0.0\right) - \beta\right)\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
double f(double alpha, double beta, double i) {
        double r3092066 = alpha;
        double r3092067 = beta;
        double r3092068 = r3092066 + r3092067;
        double r3092069 = r3092067 - r3092066;
        double r3092070 = r3092068 * r3092069;
        double r3092071 = 2.0;
        double r3092072 = /* ERROR: no posit support in C */;
        double r3092073 = i;
        double r3092074 = r3092072 * r3092073;
        double r3092075 = r3092068 + r3092074;
        double r3092076 = r3092070 / r3092075;
        double r3092077 = 2.0;
        double r3092078 = /* ERROR: no posit support in C */;
        double r3092079 = r3092075 + r3092078;
        double r3092080 = r3092076 / r3092079;
        double r3092081 = 1.0;
        double r3092082 = /* ERROR: no posit support in C */;
        double r3092083 = r3092080 + r3092082;
        double r3092084 = r3092083 / r3092078;
        return r3092084;
}
↓
double f(double alpha, double beta, double i) {
        double r3092085 = alpha;
        double r3092086 = beta;
        double r3092087 = r3092085 + r3092086;
        double r3092088 = i;
        double r3092089 = 2.0;
        double r3092090 = /* ERROR: no posit support in C */;
        double r3092091 = r3092088 * r3092090;
        double r3092092 = r3092091 + r3092085;
        double r3092093 = r3092092 + r3092086;
        double r3092094 = r3092087 / r3092093;
        double r3092095 = r3092086 - r3092085;
        double r3092096 = r3092094 * r3092095;
        double r3092097 = r3092086 + r3092085;
        double r3092098 = r3092096 / r3092097;
        double r3092099 = r3092090 * r3092088;
        double r3092100 = 2.0;
        double r3092101 = /* ERROR: no posit support in C */;
        double r3092102 = r3092099 + r3092101;
        double r3092103 = r3092085 + r3092102;
        double r3092104 = 0.0;
        double r3092105 = /* ERROR: no posit support in C */;
        double r3092106 = r3092105 - r3092086;
        double r3092107 = r3092103 - r3092106;
        double r3092108 = r3092097 / r3092107;
        double r3092109 = r3092098 * r3092108;
        double r3092110 = 1.0;
        double r3092111 = /* ERROR: no posit support in C */;
        double r3092112 = r3092109 + r3092111;
        double r3092113 = r3092112 / r3092101;
        return r3092113;
}

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. Simplified1.0

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

  4. Applied p16-times-frac0.6

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

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

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

  7. Applied associate-+l-0.6

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

  8. Applied associate-+r-0.6

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

  9. Applied associate-+r-0.6

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

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

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

  12. Applied associate-/l*0.6

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

  14. Applied p16-flip--1.0

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

  15. Applied associate-/r/1.0

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

  16. Applied associate-/r*1.0

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

  17. Simplified0.6

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

  18. Final simplification0.6

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

Reproduce

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