Average Error: 0.0 → 0.0
Time: 17.1s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1}{\sqrt{1 + x}}} \cdot \sqrt{\frac{{1}^{3} - {x}^{3}}{\sqrt{x + 1} \cdot \mathsf{fma}\left(1, 1, x \cdot \left(1 + x\right)\right)}}\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\sqrt{\frac{1}{\sqrt{1 + x}}} \cdot \sqrt{\frac{{1}^{3} - {x}^{3}}{\sqrt{x + 1} \cdot \mathsf{fma}\left(1, 1, x \cdot \left(1 + x\right)\right)}}\right)
double f(double x) {
        double r31453 = 2.0;
        double r31454 = 1.0;
        double r31455 = x;
        double r31456 = r31454 - r31455;
        double r31457 = r31454 + r31455;
        double r31458 = r31456 / r31457;
        double r31459 = sqrt(r31458);
        double r31460 = atan(r31459);
        double r31461 = r31453 * r31460;
        return r31461;
}
↓
double f(double x) {
        double r31462 = 2.0;
        double r31463 = 1.0;
        double r31464 = 1.0;
        double r31465 = x;
        double r31466 = r31464 + r31465;
        double r31467 = sqrt(r31466);
        double r31468 = r31463 / r31467;
        double r31469 = sqrt(r31468);
        double r31470 = 3.0;
        double r31471 = pow(r31464, r31470);
        double r31472 = pow(r31465, r31470);
        double r31473 = r31471 - r31472;
        double r31474 = r31465 + r31464;
        double r31475 = sqrt(r31474);
        double r31476 = r31465 * r31466;
        double r31477 = fma(r31464, r31464, r31476);
        double r31478 = r31475 * r31477;
        double r31479 = r31473 / r31478;
        double r31480 = sqrt(r31479);
        double r31481 = r31469 * r31480;
        double r31482 = atan(r31481);
        double r31483 = r31462 * r31482;
        return r31483;
}

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 add-sqr-sqrt0.0

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

  4. Applied *-un-lft-identity0.0

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

  5. Applied times-frac0.0

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

  6. Applied sqrt-prod0.0

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

  8. Applied flip3--0.0

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

  9. Applied associate-/l/0.0

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

  10. Simplified0.0

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

  11. Final simplification0.0

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

Reproduce

herbie shell --seed 2019323 +o rules:numerics
(FPCore (x)
  :name "arccos"
  :precision binary64
  (* 2 (atan (sqrt (/ (- 1 x) (+ 1 x))))))