Average Error: 0.0 → 0.0
Time: 20.0s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\left|\frac{\frac{\sqrt{{1}^{3} - {x}^{3}}}{\sqrt{\mathsf{fma}\left(1, 1, x \cdot \left(x + 1\right)\right)}}}{\sqrt{1 + x}}\right|\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\left|\frac{\frac{\sqrt{{1}^{3} - {x}^{3}}}{\sqrt{\mathsf{fma}\left(1, 1, x \cdot \left(x + 1\right)\right)}}}{\sqrt{1 + x}}\right|\right)
double f(double x) {
        double r31800 = 2.0;
        double r31801 = 1.0;
        double r31802 = x;
        double r31803 = r31801 - r31802;
        double r31804 = r31801 + r31802;
        double r31805 = r31803 / r31804;
        double r31806 = sqrt(r31805);
        double r31807 = atan(r31806);
        double r31808 = r31800 * r31807;
        return r31808;
}
↓
double f(double x) {
        double r31809 = 2.0;
        double r31810 = 1.0;
        double r31811 = 3.0;
        double r31812 = pow(r31810, r31811);
        double r31813 = x;
        double r31814 = pow(r31813, r31811);
        double r31815 = r31812 - r31814;
        double r31816 = sqrt(r31815);
        double r31817 = r31813 + r31810;
        double r31818 = r31813 * r31817;
        double r31819 = fma(r31810, r31810, r31818);
        double r31820 = sqrt(r31819);
        double r31821 = r31816 / r31820;
        double r31822 = r31810 + r31813;
        double r31823 = sqrt(r31822);
        double r31824 = r31821 / r31823;
        double r31825 = fabs(r31824);
        double r31826 = atan(r31825);
        double r31827 = r31809 * r31826;
        return r31827;
}

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

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

  5. Applied times-frac0.0

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

  6. Applied rem-sqrt-square0.0

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

  8. Applied flip3--0.0

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

  9. Applied sqrt-div0.0

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

  10. Simplified0.0

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

  11. Final simplification0.0

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

Reproduce

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