Average Error: 3.3 → 1.4
Time: 1.2m
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right) \land i \gt \left(1\right)\]
\[\frac{\left(\frac{\left(\left(i \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)\right) \cdot \left(\frac{\left(\beta \cdot \alpha\right)}{\left(i \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)\right)}\right)\right)}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}\right)}{\left(\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right) - \left(1.0\right)\right)}\]
↓
\[\left(\frac{i}{\left(1.0 + \left(\alpha + \beta\right)\right) + 2 \cdot i} \cdot \frac{1.0}{\frac{\left(2 \cdot i + \alpha\right) + \beta}{\alpha + \left(\beta + i\right)}}\right) \cdot \left(\frac{1.0}{i \cdot 2 + \left(\left(\alpha + \beta\right) - 1.0\right)} \cdot \frac{\alpha \cdot \beta + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{i \cdot 2 + \left(\alpha + \beta\right)}\right)\]
\frac{\left(\frac{\left(\left(i \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)\right) \cdot \left(\frac{\left(\beta \cdot \alpha\right)}{\left(i \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)\right)}\right)\right)}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}\right)}{\left(\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right) - \left(1.0\right)\right)}
↓
\left(\frac{i}{\left(1.0 + \left(\alpha + \beta\right)\right) + 2 \cdot i} \cdot \frac{1.0}{\frac{\left(2 \cdot i + \alpha\right) + \beta}{\alpha + \left(\beta + i\right)}}\right) \cdot \left(\frac{1.0}{i \cdot 2 + \left(\left(\alpha + \beta\right) - 1.0\right)} \cdot \frac{\alpha \cdot \beta + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{i \cdot 2 + \left(\alpha + \beta\right)}\right)
double f(double alpha, double beta, double i) {
        double r1128789 = i;
        double r1128790 = alpha;
        double r1128791 = beta;
        double r1128792 = r1128790 + r1128791;
        double r1128793 = r1128792 + r1128789;
        double r1128794 = r1128789 * r1128793;
        double r1128795 = r1128791 * r1128790;
        double r1128796 = r1128795 + r1128794;
        double r1128797 = r1128794 * r1128796;
        double r1128798 = 2.0;
        double r1128799 = /* ERROR: no posit support in C */;
        double r1128800 = r1128799 * r1128789;
        double r1128801 = r1128792 + r1128800;
        double r1128802 = r1128801 * r1128801;
        double r1128803 = r1128797 / r1128802;
        double r1128804 = 1.0;
        double r1128805 = /* ERROR: no posit support in C */;
        double r1128806 = r1128802 - r1128805;
        double r1128807 = r1128803 / r1128806;
        return r1128807;
}
↓
double f(double alpha, double beta, double i) {
        double r1128808 = i;
        double r1128809 = 1.0;
        double r1128810 = alpha;
        double r1128811 = beta;
        double r1128812 = r1128810 + r1128811;
        double r1128813 = r1128809 + r1128812;
        double r1128814 = 2.0;
        double r1128815 = r1128814 * r1128808;
        double r1128816 = r1128813 + r1128815;
        double r1128817 = r1128808 / r1128816;
        double r1128818 = r1128815 + r1128810;
        double r1128819 = r1128818 + r1128811;
        double r1128820 = r1128811 + r1128808;
        double r1128821 = r1128810 + r1128820;
        double r1128822 = r1128819 / r1128821;
        double r1128823 = r1128809 / r1128822;
        double r1128824 = r1128817 * r1128823;
        double r1128825 = r1128808 * r1128814;
        double r1128826 = r1128812 - r1128809;
        double r1128827 = r1128825 + r1128826;
        double r1128828 = r1128809 / r1128827;
        double r1128829 = r1128810 * r1128811;
        double r1128830 = r1128812 + r1128808;
        double r1128831 = r1128808 * r1128830;
        double r1128832 = r1128829 + r1128831;
        double r1128833 = r1128825 + r1128812;
        double r1128834 = r1128832 / r1128833;
        double r1128835 = r1128828 * r1128834;
        double r1128836 = r1128824 * r1128835;
        return r1128836;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 3.3

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

  3. Applied p16-*-un-lft-identity3.3

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

  4. Applied difference-of-squares3.3

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

  5. Applied p16-times-frac1.7

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

  6. Applied p16-times-frac1.6

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

  8. Applied *p16-rgt-identity-expand1.6

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

  9. Applied distribute-lft1-in1.6

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

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

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

  11. Applied p16-times-frac1.5

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

  12. Applied p16-times-frac1.5

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

  13. Simplified1.5

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

  14. Simplified1.4

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

  16. Applied p16-*-un-lft-identity1.4

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

  17. Applied associate-/l*1.4

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

  19. Applied *p16-rgt-identity-expand1.4

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

  20. Applied p16-*-un-lft-identity1.4

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

  21. Applied p16-*-un-lft-identity1.4

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

  22. Applied p16-times-frac1.4

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

  23. Applied p16-times-frac1.4

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

  24. Simplified1.4

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

  25. Simplified1.4

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

  26. Final simplification1.4

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

Reproduce

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