Average Error: 0.0 → 0.0
Time: 14.8s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
\[\tan^{-1} \left(\sqrt{\left(\left(x \cdot x - x\right) + 1\right) \cdot \frac{1 - x}{\mathsf{fma}\left(x, x \cdot x, 1\right)}}\right) \cdot 2\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
\tan^{-1} \left(\sqrt{\left(\left(x \cdot x - x\right) + 1\right) \cdot \frac{1 - x}{\mathsf{fma}\left(x, x \cdot x, 1\right)}}\right) \cdot 2
double f(double x) {
        double r270107 = 2.0;
        double r270108 = 1.0;
        double r270109 = x;
        double r270110 = r270108 - r270109;
        double r270111 = r270108 + r270109;
        double r270112 = r270110 / r270111;
        double r270113 = sqrt(r270112);
        double r270114 = atan(r270113);
        double r270115 = r270107 * r270114;
        return r270115;
}

double f(double x) {
        double r270116 = x;
        double r270117 = r270116 * r270116;
        double r270118 = r270117 - r270116;
        double r270119 = 1.0;
        double r270120 = r270118 + r270119;
        double r270121 = r270119 - r270116;
        double r270122 = fma(r270116, r270117, r270119);
        double r270123 = r270121 / r270122;
        double r270124 = r270120 * r270123;
        double r270125 = sqrt(r270124);
        double r270126 = atan(r270125);
        double r270127 = 2.0;
        double r270128 = r270126 * r270127;
        return r270128;
}

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. Simplified0.0

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

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

Reproduce

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