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

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. Using strategy rm

  12. Applied sqrt-div0.0

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

  13. Applied sqrt-div0.0

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

  14. Applied frac-times0.0

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

  15. Simplified0.0

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

  16. Final simplification0.0

    \[\leadsto 2 \cdot \tan^{-1} \left(\frac{\sqrt{{1}^{3} - {x}^{3}}}{\sqrt{\sqrt{1 + x}} \cdot \sqrt{\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))))))