Average Error: 3.3 → 1.4
Time: 1.3m
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{\alpha \cdot \beta + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{i \cdot 2 + \left(\alpha + \beta\right)} \cdot \frac{1.0}{i \cdot 2 + \left(\left(\alpha + \beta\right) - 1.0\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{\alpha \cdot \beta + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{i \cdot 2 + \left(\alpha + \beta\right)} \cdot \frac{1.0}{i \cdot 2 + \left(\left(\alpha + \beta\right) - 1.0\right)}\right)
double f(double alpha, double beta, double i) {
        double r1087604 = i;
        double r1087605 = alpha;
        double r1087606 = beta;
        double r1087607 = r1087605 + r1087606;
        double r1087608 = r1087607 + r1087604;
        double r1087609 = r1087604 * r1087608;
        double r1087610 = r1087606 * r1087605;
        double r1087611 = r1087610 + r1087609;
        double r1087612 = r1087609 * r1087611;
        double r1087613 = 2.0;
        double r1087614 = /* ERROR: no posit support in C */;
        double r1087615 = r1087614 * r1087604;
        double r1087616 = r1087607 + r1087615;
        double r1087617 = r1087616 * r1087616;
        double r1087618 = r1087612 / r1087617;
        double r1087619 = 1.0;
        double r1087620 = /* ERROR: no posit support in C */;
        double r1087621 = r1087617 - r1087620;
        double r1087622 = r1087618 / r1087621;
        return r1087622;
}
↓
double f(double alpha, double beta, double i) {
        double r1087623 = i;
        double r1087624 = 1.0;
        double r1087625 = alpha;
        double r1087626 = beta;
        double r1087627 = r1087625 + r1087626;
        double r1087628 = r1087624 + r1087627;
        double r1087629 = 2.0;
        double r1087630 = r1087629 * r1087623;
        double r1087631 = r1087628 + r1087630;
        double r1087632 = r1087623 / r1087631;
        double r1087633 = r1087630 + r1087625;
        double r1087634 = r1087633 + r1087626;
        double r1087635 = r1087626 + r1087623;
        double r1087636 = r1087625 + r1087635;
        double r1087637 = r1087634 / r1087636;
        double r1087638 = r1087624 / r1087637;
        double r1087639 = r1087632 * r1087638;
        double r1087640 = r1087625 * r1087626;
        double r1087641 = r1087627 + r1087623;
        double r1087642 = r1087623 * r1087641;
        double r1087643 = r1087640 + r1087642;
        double r1087644 = r1087623 * r1087629;
        double r1087645 = r1087644 + r1087627;
        double r1087646 = r1087643 / r1087645;
        double r1087647 = r1087627 - r1087624;
        double r1087648 = r1087644 + r1087647;
        double r1087649 = r1087624 / r1087648;
        double r1087650 = r1087646 * r1087649;
        double r1087651 = r1087639 * r1087650;
        return r1087651;
}

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

  21. Applied distribute-lft-out--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 \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(1.0\right) \cdot \left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) - \left(1.0\right)\right)\right)}}\right)\]

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

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

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

  25. 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(\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) \cdot \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)\right)}\]

  26. 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(\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)} \cdot \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)\right)\]

  27. 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(\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) \cdot \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)}\right)\]

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

Reproduce

herbie shell --seed 2019154 +o rules:numerics
(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))))