Average Error: 0.0 → 0.0
Time: 12.3s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\frac{\sqrt{1 \cdot 1 - x \cdot x}}{1 + x}\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\frac{\sqrt{1 \cdot 1 - x \cdot x}}{1 + x}\right)
double f(double x) {
        double r26428 = 2.0;
        double r26429 = 1.0;
        double r26430 = x;
        double r26431 = r26429 - r26430;
        double r26432 = r26429 + r26430;
        double r26433 = r26431 / r26432;
        double r26434 = sqrt(r26433);
        double r26435 = atan(r26434);
        double r26436 = r26428 * r26435;
        return r26436;
}
↓
double f(double x) {
        double r26437 = 2.0;
        double r26438 = 1.0;
        double r26439 = r26438 * r26438;
        double r26440 = x;
        double r26441 = r26440 * r26440;
        double r26442 = r26439 - r26441;
        double r26443 = sqrt(r26442);
        double r26444 = r26438 + r26440;
        double r26445 = r26443 / r26444;
        double r26446 = atan(r26445);
        double r26447 = r26437 * r26446;
        return r26447;
}

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

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

  4. Applied sqrt-div0.0

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

  5. Simplified0.0

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

  7. Applied flip--0.0

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

  8. Applied sqrt-div0.0

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

  9. Applied associate-/l/0.0

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

  10. Simplified0.0

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

  11. Final simplification0.0

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

Reproduce

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