Average Error: 3.3 → 1.4
Time: 1.1m
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(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{\left(\alpha + \beta\right) + i}{\left(1.0 + 2 \cdot i\right) + \left(\alpha + \beta\right)}\right) \cdot \left(\frac{1.0}{\frac{\left(\alpha + 2 \cdot i\right) + \beta}{\alpha \cdot \beta + i \cdot \left(\left(\alpha + \beta\right) + i\right)}} \cdot \frac{1.0}{\left(2 \cdot i - 1.0\right) + \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(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{\left(\alpha + \beta\right) + i}{\left(1.0 + 2 \cdot i\right) + \left(\alpha + \beta\right)}\right) \cdot \left(\frac{1.0}{\frac{\left(\alpha + 2 \cdot i\right) + \beta}{\alpha \cdot \beta + i \cdot \left(\left(\alpha + \beta\right) + i\right)}} \cdot \frac{1.0}{\left(2 \cdot i - 1.0\right) + \left(\alpha + \beta\right)}\right)
double f(double alpha, double beta, double i) {
        double r3600481 = i;
        double r3600482 = alpha;
        double r3600483 = beta;
        double r3600484 = r3600482 + r3600483;
        double r3600485 = r3600484 + r3600481;
        double r3600486 = r3600481 * r3600485;
        double r3600487 = r3600483 * r3600482;
        double r3600488 = r3600487 + r3600486;
        double r3600489 = r3600486 * r3600488;
        double r3600490 = 2.0;
        double r3600491 = /* ERROR: no posit support in C */;
        double r3600492 = r3600491 * r3600481;
        double r3600493 = r3600484 + r3600492;
        double r3600494 = r3600493 * r3600493;
        double r3600495 = r3600489 / r3600494;
        double r3600496 = 1.0;
        double r3600497 = /* ERROR: no posit support in C */;
        double r3600498 = r3600494 - r3600497;
        double r3600499 = r3600495 / r3600498;
        return r3600499;
}

double f(double alpha, double beta, double i) {
        double r3600500 = i;
        double r3600501 = alpha;
        double r3600502 = beta;
        double r3600503 = r3600501 + r3600502;
        double r3600504 = 2.0;
        double r3600505 = r3600504 * r3600500;
        double r3600506 = r3600503 + r3600505;
        double r3600507 = r3600500 / r3600506;
        double r3600508 = r3600503 + r3600500;
        double r3600509 = 1.0;
        double r3600510 = r3600509 + r3600505;
        double r3600511 = r3600510 + r3600503;
        double r3600512 = r3600508 / r3600511;
        double r3600513 = r3600507 * r3600512;
        double r3600514 = r3600501 + r3600505;
        double r3600515 = r3600514 + r3600502;
        double r3600516 = r3600501 * r3600502;
        double r3600517 = r3600500 * r3600508;
        double r3600518 = r3600516 + r3600517;
        double r3600519 = r3600515 / r3600518;
        double r3600520 = r3600509 / r3600519;
        double r3600521 = r3600505 - r3600509;
        double r3600522 = r3600521 + r3600503;
        double r3600523 = r3600509 / r3600522;
        double r3600524 = r3600520 * r3600523;
        double r3600525 = r3600513 * r3600524;
        return r3600525;
}

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.2

    \[\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-*-un-lft-identity1.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{\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) \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 p16-*-un-lft-identity1.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(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) \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 distribute-lft-out1.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(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\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(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) - \left(1.0\right)\right)}\right)\]
  11. Applied *p16-rgt-identity-expand1.6

    \[\leadsto \left(\frac{\left(\frac{\left(i \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\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(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(\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 \left(\frac{\color{blue}{\left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\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(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(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right) - \left(1.0\right)\right)}\right)\]
  13. Applied p16-times-frac1.5

    \[\leadsto \color{blue}{\left(\left(\frac{\left(\frac{i}{\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(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\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)\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.5

    \[\leadsto \left(\color{blue}{\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\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(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)\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. Simplified1.4

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \color{blue}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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)\]
  16. Using strategy rm
  17. Applied p16-*-un-lft-identity1.4

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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)\]
  18. Applied p16-*-un-lft-identity1.4

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

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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)\]
  20. Applied *p16-rgt-identity-expand1.4

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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)\]
  21. Applied *p16-rgt-identity-expand1.4

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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)\]
  22. Applied p16-times-frac1.4

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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)\]
  23. Applied p16-times-frac1.4

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

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

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\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(\frac{\alpha}{\left(\left(2\right) \cdot i\right)}\right)}{\beta}\right)}\right) \cdot \color{blue}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}{\left(\frac{\alpha}{\beta}\right)}\right)}\right)}\right)\]
  26. Using strategy rm
  27. Applied p16-*-un-lft-identity1.4

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)}{\left(\frac{\left(\frac{\left(1.0\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\alpha}{\beta}\right)}\right)}\right)\right) \cdot \left(\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\alpha \cdot \beta\right)}{\left(i \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{i}\right)\right)}\right)\right)}}{\left(\frac{\left(\frac{\alpha}{\left(\left(2\right) \cdot i\right)}\right)}{\beta}\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}{\left(\frac{\alpha}{\beta}\right)}\right)}\right)\right)\]
  28. Applied associate-/l*1.4

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

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

Reproduce

herbie shell --seed 2019163 +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))))