Average Error: 0.0 → 0.0
Time: 12.9s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 \cdot 1 - x \cdot x}{\left(1 \cdot 1 - x \cdot x\right) \cdot \left(1 \cdot 1 - x \cdot x\right)}} \cdot \left|1 - x\right|\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 \cdot 1 - x \cdot x}{\left(1 \cdot 1 - x \cdot x\right) \cdot \left(1 \cdot 1 - x \cdot x\right)}} \cdot \left|1 - x\right|\right)
double f(double x) {
        double r19317 = 2.0;
        double r19318 = 1.0;
        double r19319 = x;
        double r19320 = r19318 - r19319;
        double r19321 = r19318 + r19319;
        double r19322 = r19320 / r19321;
        double r19323 = sqrt(r19322);
        double r19324 = atan(r19323);
        double r19325 = r19317 * r19324;
        return r19325;
}
↓
double f(double x) {
        double r19326 = 2.0;
        double r19327 = 1.0;
        double r19328 = r19327 * r19327;
        double r19329 = x;
        double r19330 = r19329 * r19329;
        double r19331 = r19328 - r19330;
        double r19332 = r19331 * r19331;
        double r19333 = r19331 / r19332;
        double r19334 = sqrt(r19333);
        double r19335 = r19327 - r19329;
        double r19336 = fabs(r19335);
        double r19337 = r19334 * r19336;
        double r19338 = atan(r19337);
        double r19339 = r19326 * r19338;
        return r19339;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.0

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

  3. Applied flip--0.0

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

  4. Applied associate-/l/0.0

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

  6. Applied flip-+0.0

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

  7. Applied flip-+0.0

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

  8. Applied frac-times0.0

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

  9. Applied associate-/r/0.0

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

  10. Applied sqrt-prod0.0

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

  11. Simplified0.0

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

  12. Final simplification0.0

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

Reproduce

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