Average Error: 0.0 → 0.0
Time: 25.7s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[\tan^{-1} \left(\sqrt{\left(1 \cdot 1 + \left(x \cdot x - x \cdot 1\right)\right) \cdot \frac{1 - x}{\mathsf{fma}\left(x \cdot x, x, \left(1 \cdot 1\right) \cdot 1\right)}}\right) \cdot 2\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
\tan^{-1} \left(\sqrt{\left(1 \cdot 1 + \left(x \cdot x - x \cdot 1\right)\right) \cdot \frac{1 - x}{\mathsf{fma}\left(x \cdot x, x, \left(1 \cdot 1\right) \cdot 1\right)}}\right) \cdot 2
double f(double x) {
        double r870138 = 2.0;
        double r870139 = 1.0;
        double r870140 = x;
        double r870141 = r870139 - r870140;
        double r870142 = r870139 + r870140;
        double r870143 = r870141 / r870142;
        double r870144 = sqrt(r870143);
        double r870145 = atan(r870144);
        double r870146 = r870138 * r870145;
        return r870146;
}
↓
double f(double x) {
        double r870147 = 1.0;
        double r870148 = r870147 * r870147;
        double r870149 = x;
        double r870150 = r870149 * r870149;
        double r870151 = r870149 * r870147;
        double r870152 = r870150 - r870151;
        double r870153 = r870148 + r870152;
        double r870154 = r870147 - r870149;
        double r870155 = r870148 * r870147;
        double r870156 = fma(r870150, r870149, r870155);
        double r870157 = r870154 / r870156;
        double r870158 = r870153 * r870157;
        double r870159 = sqrt(r870158);
        double r870160 = atan(r870159);
        double r870161 = 2.0;
        double r870162 = r870160 * r870161;
        return r870162;
}

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 \cdot x, x, \left(1 \cdot 1\right) \cdot 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(1 \cdot 1 + \left(x \cdot x - x \cdot 1\right)\right) \cdot \frac{1 - x}{\mathsf{fma}\left(x \cdot x, x, \left(1 \cdot 1\right) \cdot 1\right)}}\right) \cdot 2\]

Reproduce

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