Average Error: 0.0 → 0.0
Time: 19.1s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{\frac{\frac{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({1}^{8} - \left(\left(x - 1\right) \cdot x\right) \cdot {\left(x \cdot \left(x - 1\right)\right)}^{3}\right)}{\mathsf{fma}\left(x \cdot x, \left(x - 1\right) \cdot \left(x - 1\right), {1}^{4}\right) \cdot \left(1 + x\right)}}{{1}^{3} + {x}^{3}}}{1 \cdot 1 - \left(x \cdot x - 1 \cdot x\right)}}\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\sqrt{\frac{\frac{\frac{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({1}^{8} - \left(\left(x - 1\right) \cdot x\right) \cdot {\left(x \cdot \left(x - 1\right)\right)}^{3}\right)}{\mathsf{fma}\left(x \cdot x, \left(x - 1\right) \cdot \left(x - 1\right), {1}^{4}\right) \cdot \left(1 + x\right)}}{{1}^{3} + {x}^{3}}}{1 \cdot 1 - \left(x \cdot x - 1 \cdot x\right)}}\right)
double f(double x) {
        double r29264 = 2.0;
        double r29265 = 1.0;
        double r29266 = x;
        double r29267 = r29265 - r29266;
        double r29268 = r29265 + r29266;
        double r29269 = r29267 / r29268;
        double r29270 = sqrt(r29269);
        double r29271 = atan(r29270);
        double r29272 = r29264 * r29271;
        return r29272;
}
↓
double f(double x) {
        double r29273 = 2.0;
        double r29274 = 1.0;
        double r29275 = r29274 * r29274;
        double r29276 = x;
        double r29277 = r29276 * r29276;
        double r29278 = r29275 - r29277;
        double r29279 = 8.0;
        double r29280 = pow(r29274, r29279);
        double r29281 = r29276 - r29274;
        double r29282 = r29281 * r29276;
        double r29283 = r29276 * r29281;
        double r29284 = 3.0;
        double r29285 = pow(r29283, r29284);
        double r29286 = r29282 * r29285;
        double r29287 = r29280 - r29286;
        double r29288 = r29278 * r29287;
        double r29289 = r29281 * r29281;
        double r29290 = 4.0;
        double r29291 = pow(r29274, r29290);
        double r29292 = fma(r29277, r29289, r29291);
        double r29293 = r29274 + r29276;
        double r29294 = r29292 * r29293;
        double r29295 = r29288 / r29294;
        double r29296 = pow(r29274, r29284);
        double r29297 = pow(r29276, r29284);
        double r29298 = r29296 + r29297;
        double r29299 = r29295 / r29298;
        double r29300 = r29274 * r29276;
        double r29301 = r29277 - r29300;
        double r29302 = r29275 - r29301;
        double r29303 = r29299 / r29302;
        double r29304 = sqrt(r29303);
        double r29305 = atan(r29304);
        double r29306 = r29273 * r29305;
        return r29306;
}

Error

Bits error versus x

Derivation

  1. Initial program 0.0

    \[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
  2. Using strategy rm

  3. Applied flip3-+0.0

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

  4. Applied associate-/r/0.0

    \[\leadsto 2 \cdot \tan^{-1} \left(\sqrt{\color{blue}{\frac{1 - x}{{1}^{3} + {x}^{3}} \cdot \left(1 \cdot 1 + \left(x \cdot x - 1 \cdot x\right)\right)}}\right)\]
  5. Using strategy rm

  6. Applied flip-+0.0

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

  7. Applied associate-*r/0.0

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

  8. Simplified0.0

    \[\leadsto 2 \cdot \tan^{-1} \left(\sqrt{\frac{\color{blue}{\frac{\left(1 - x\right) \cdot \left({1}^{4} - \left(x \cdot \left(x - 1\right)\right) \cdot \left(x \cdot \left(x - 1\right)\right)\right)}{{1}^{3} + {x}^{3}}}}{1 \cdot 1 - \left(x \cdot x - 1 \cdot x\right)}}\right)\]
  9. Using strategy rm

  10. Applied flip--0.0

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

  11. Applied flip--0.0

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

  12. Applied frac-times0.0

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

  13. Simplified0.0

    \[\leadsto 2 \cdot \tan^{-1} \left(\sqrt{\frac{\frac{\frac{\color{blue}{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({1}^{8} - \left(\left(x - 1\right) \cdot x\right) \cdot {\left(x \cdot \left(x - 1\right)\right)}^{3}\right)}}{\left(1 + x\right) \cdot \left({1}^{4} + \left(x \cdot \left(x - 1\right)\right) \cdot \left(x \cdot \left(x - 1\right)\right)\right)}}{{1}^{3} + {x}^{3}}}{1 \cdot 1 - \left(x \cdot x - 1 \cdot x\right)}}\right)\]

  14. Simplified0.0

    \[\leadsto 2 \cdot \tan^{-1} \left(\sqrt{\frac{\frac{\frac{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({1}^{8} - \left(\left(x - 1\right) \cdot x\right) \cdot {\left(x \cdot \left(x - 1\right)\right)}^{3}\right)}{\color{blue}{\mathsf{fma}\left(x \cdot x, \left(x - 1\right) \cdot \left(x - 1\right), {1}^{4}\right) \cdot \left(1 + x\right)}}}{{1}^{3} + {x}^{3}}}{1 \cdot 1 - \left(x \cdot x - 1 \cdot x\right)}}\right)\]

  15. Final simplification0.0

    \[\leadsto 2 \cdot \tan^{-1} \left(\sqrt{\frac{\frac{\frac{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({1}^{8} - \left(\left(x - 1\right) \cdot x\right) \cdot {\left(x \cdot \left(x - 1\right)\right)}^{3}\right)}{\mathsf{fma}\left(x \cdot x, \left(x - 1\right) \cdot \left(x - 1\right), {1}^{4}\right) \cdot \left(1 + x\right)}}{{1}^{3} + {x}^{3}}}{1 \cdot 1 - \left(x \cdot x - 1 \cdot x\right)}}\right)\]

Reproduce

herbie shell --seed 2019199 +o rules:numerics
(FPCore (x)
  :name "arccos"
  (* 2.0 (atan (sqrt (/ (- 1.0 x) (+ 1.0 x))))))