Average Error: 0.0 → 0.0
Time: 18.2s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{\sqrt{1 - x}}{\sqrt{1 + x}} \cdot \frac{\sqrt{1 - x}}{\sqrt{1 + x}}}\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\sqrt{\frac{\sqrt{1 - x}}{\sqrt{1 + x}} \cdot \frac{\sqrt{1 - x}}{\sqrt{1 + x}}}\right)
double f(double x) {
        double r26669 = 2.0;
        double r26670 = 1.0;
        double r26671 = x;
        double r26672 = r26670 - r26671;
        double r26673 = r26670 + r26671;
        double r26674 = r26672 / r26673;
        double r26675 = sqrt(r26674);
        double r26676 = atan(r26675);
        double r26677 = r26669 * r26676;
        return r26677;
}
↓
double f(double x) {
        double r26678 = 2.0;
        double r26679 = 1.0;
        double r26680 = x;
        double r26681 = r26679 - r26680;
        double r26682 = sqrt(r26681);
        double r26683 = r26679 + r26680;
        double r26684 = sqrt(r26683);
        double r26685 = r26682 / r26684;
        double r26686 = r26685 * r26685;
        double r26687 = sqrt(r26686);
        double r26688 = atan(r26687);
        double r26689 = r26678 * r26688;
        return r26689;
}

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 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. Final simplification0.0

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

Reproduce

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