Average Error: 13.4 → 0.3
Time: 18.5s
Precision: 64
\[\left(x = 0.0 \lor 0.588414199999999998 \le x \le 505.590899999999976\right) \land \left(-1.79665800000000009 \cdot 10^{308} \le y \le -9.425585000000013 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \le y \le 1.7512240000000001 \cdot 10^{308}\right) \land \left(-1.7767070000000002 \cdot 10^{308} \le z \le -8.59979600000002 \cdot 10^{-310} \lor 3.29314499999998 \cdot 10^{-311} \le z \le 1.72515400000000009 \cdot 10^{308}\right) \land \left(-1.79665800000000009 \cdot 10^{308} \le a \le -9.425585000000013 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \le a \le 1.7512240000000001 \cdot 10^{308}\right)\]
\[x + \left(\tan \left(y + z\right) - \tan a\right)\]
↓
\[\frac{\left(\left(\tan z + \tan y\right) \cdot \frac{\frac{\tan z + \tan y}{1 - {\left(\tan y \cdot \tan z\right)}^{3}}}{\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}}\right) \cdot \frac{\left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + \tan y \cdot \tan z\right) + 1}{\sqrt[3]{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a} + x\]
x + \left(\tan \left(y + z\right) - \tan a\right)
↓
\frac{\left(\left(\tan z + \tan y\right) \cdot \frac{\frac{\tan z + \tan y}{1 - {\left(\tan y \cdot \tan z\right)}^{3}}}{\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}}\right) \cdot \frac{\left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + \tan y \cdot \tan z\right) + 1}{\sqrt[3]{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a} + x
double f(double x, double y, double z, double a) {
        double r156463 = x;
        double r156464 = y;
        double r156465 = z;
        double r156466 = r156464 + r156465;
        double r156467 = tan(r156466);
        double r156468 = a;
        double r156469 = tan(r156468);
        double r156470 = r156467 - r156469;
        double r156471 = r156463 + r156470;
        return r156471;
}
↓
double f(double x, double y, double z, double a) {
        double r156472 = z;
        double r156473 = tan(r156472);
        double r156474 = y;
        double r156475 = tan(r156474);
        double r156476 = r156473 + r156475;
        double r156477 = 1.0;
        double r156478 = r156475 * r156473;
        double r156479 = 3.0;
        double r156480 = pow(r156478, r156479);
        double r156481 = r156477 - r156480;
        double r156482 = r156476 / r156481;
        double r156483 = r156477 - r156478;
        double r156484 = cbrt(r156483);
        double r156485 = r156484 * r156484;
        double r156486 = r156482 / r156485;
        double r156487 = r156476 * r156486;
        double r156488 = r156478 * r156478;
        double r156489 = r156488 + r156478;
        double r156490 = r156489 + r156477;
        double r156491 = r156490 / r156484;
        double r156492 = r156487 * r156491;
        double r156493 = a;
        double r156494 = tan(r156493);
        double r156495 = r156494 * r156494;
        double r156496 = r156492 - r156495;
        double r156497 = r156475 + r156473;
        double r156498 = r156497 / r156483;
        double r156499 = r156498 + r156494;
        double r156500 = r156496 / r156499;
        double r156501 = x;
        double r156502 = r156500 + r156501;
        return r156502;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus a

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 13.4

    \[x + \left(\tan \left(y + z\right) - \tan a\right)\]
  2. Using strategy rm

  3. Applied tan-sum0.2

    \[\leadsto x + \left(\color{blue}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}} - \tan a\right)\]
  4. Using strategy rm

  5. Applied flip--0.2

    \[\leadsto x + \color{blue}{\frac{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} \cdot \frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}}\]
  6. Using strategy rm

  7. Applied *-un-lft-identity0.2

    \[\leadsto x + \frac{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} \cdot \frac{\tan y + \tan z}{\color{blue}{1 \cdot \left(1 - \tan y \cdot \tan z\right)}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  8. Applied add-sqr-sqrt31.9

    \[\leadsto x + \frac{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} \cdot \frac{\color{blue}{\sqrt{\tan y + \tan z} \cdot \sqrt{\tan y + \tan z}}}{1 \cdot \left(1 - \tan y \cdot \tan z\right)} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  9. Applied times-frac31.9

    \[\leadsto x + \frac{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} \cdot \color{blue}{\left(\frac{\sqrt{\tan y + \tan z}}{1} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right)} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  10. Applied *-un-lft-identity31.9

    \[\leadsto x + \frac{\frac{\tan y + \tan z}{\color{blue}{1 \cdot \left(1 - \tan y \cdot \tan z\right)}} \cdot \left(\frac{\sqrt{\tan y + \tan z}}{1} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right) - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  11. Applied add-sqr-sqrt32.0

    \[\leadsto x + \frac{\frac{\color{blue}{\sqrt{\tan y + \tan z} \cdot \sqrt{\tan y + \tan z}}}{1 \cdot \left(1 - \tan y \cdot \tan z\right)} \cdot \left(\frac{\sqrt{\tan y + \tan z}}{1} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right) - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  12. Applied times-frac32.0

    \[\leadsto x + \frac{\color{blue}{\left(\frac{\sqrt{\tan y + \tan z}}{1} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right)} \cdot \left(\frac{\sqrt{\tan y + \tan z}}{1} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right) - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  13. Applied swap-sqr32.0

    \[\leadsto x + \frac{\color{blue}{\left(\frac{\sqrt{\tan y + \tan z}}{1} \cdot \frac{\sqrt{\tan y + \tan z}}{1}\right) \cdot \left(\frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right)} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  14. Simplified31.9

    \[\leadsto x + \frac{\color{blue}{\left(\tan y + \tan z\right)} \cdot \left(\frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z} \cdot \frac{\sqrt{\tan y + \tan z}}{1 - \tan y \cdot \tan z}\right) - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  15. Simplified0.2

    \[\leadsto x + \frac{\left(\tan y + \tan z\right) \cdot \color{blue}{\frac{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}}{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]
  16. Using strategy rm

  17. Applied add-cube-cbrt0.3

    \[\leadsto x + \frac{\left(\tan y + \tan z\right) \cdot \frac{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}}{\color{blue}{\left(\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}\right) \cdot \sqrt[3]{1 - \tan y \cdot \tan z}}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  18. Applied flip3--0.3

    \[\leadsto x + \frac{\left(\tan y + \tan z\right) \cdot \frac{\frac{\tan y + \tan z}{\color{blue}{\frac{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}}{1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)}}}}{\left(\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}\right) \cdot \sqrt[3]{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  19. Applied associate-/r/0.3

    \[\leadsto x + \frac{\left(\tan y + \tan z\right) \cdot \frac{\color{blue}{\frac{\tan y + \tan z}{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)\right)}}{\left(\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}\right) \cdot \sqrt[3]{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  20. Applied times-frac0.3

    \[\leadsto x + \frac{\left(\tan y + \tan z\right) \cdot \color{blue}{\left(\frac{\frac{\tan y + \tan z}{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}}}{\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}} \cdot \frac{1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)}{\sqrt[3]{1 - \tan y \cdot \tan z}}\right)} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  21. Applied associate-*r*0.3

    \[\leadsto x + \frac{\color{blue}{\left(\left(\tan y + \tan z\right) \cdot \frac{\frac{\tan y + \tan z}{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}}}{\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}}\right) \cdot \frac{1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)}{\sqrt[3]{1 - \tan y \cdot \tan z}}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  22. Simplified0.3

    \[\leadsto x + \frac{\color{blue}{\left(\left(\tan z + \tan y\right) \cdot \frac{\frac{\tan z + \tan y}{1 - {\left(\tan y \cdot \tan z\right)}^{3}}}{\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}}\right)} \cdot \frac{1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)}{\sqrt[3]{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a}\]

  23. Final simplification0.3

    \[\leadsto \frac{\left(\left(\tan z + \tan y\right) \cdot \frac{\frac{\tan z + \tan y}{1 - {\left(\tan y \cdot \tan z\right)}^{3}}}{\sqrt[3]{1 - \tan y \cdot \tan z} \cdot \sqrt[3]{1 - \tan y \cdot \tan z}}\right) \cdot \frac{\left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + \tan y \cdot \tan z\right) + 1}{\sqrt[3]{1 - \tan y \cdot \tan z}} - \tan a \cdot \tan a}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} + \tan a} + x\]

Reproduce

herbie shell --seed 2020047 
(FPCore (x y z a)
  :name "(+ x (- (tan (+ y z)) (tan a)))"
  :precision binary64
  :pre (and (or (== x 0.0) (<= 0.5884142 x 505.5909)) (or (<= -1.796658e+308 y -9.425585e-310) (<= 1.284938e-309 y 1.7512240000000001e+308)) (or (<= -1.7767070000000002e+308 z -8.599796e-310) (<= 3.293145e-311 z 1.725154e+308)) (or (<= -1.796658e+308 a -9.425585e-310) (<= 1.284938e-309 a 1.7512240000000001e+308)))
  (+ x (- (tan (+ y z)) (tan a))))