Average Error: 0.0 → 0.0
Time: 14.0s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[\tan^{-1} \left(\sqrt{\log \left(e^{\frac{\sqrt{1 - x}}{\sqrt{1 + x}} \cdot \frac{\sqrt{1 - x}}{\sqrt{1 + x}}}\right)}\right) \cdot 2\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
\tan^{-1} \left(\sqrt{\log \left(e^{\frac{\sqrt{1 - x}}{\sqrt{1 + x}} \cdot \frac{\sqrt{1 - x}}{\sqrt{1 + x}}}\right)}\right) \cdot 2
double f(double x) {
        double r562720 = 2.0;
        double r562721 = 1.0;
        double r562722 = x;
        double r562723 = r562721 - r562722;
        double r562724 = r562721 + r562722;
        double r562725 = r562723 / r562724;
        double r562726 = sqrt(r562725);
        double r562727 = atan(r562726);
        double r562728 = r562720 * r562727;
        return r562728;
}
↓
double f(double x) {
        double r562729 = 1.0;
        double r562730 = x;
        double r562731 = r562729 - r562730;
        double r562732 = sqrt(r562731);
        double r562733 = r562729 + r562730;
        double r562734 = sqrt(r562733);
        double r562735 = r562732 / r562734;
        double r562736 = r562735 * r562735;
        double r562737 = exp(r562736);
        double r562738 = log(r562737);
        double r562739 = sqrt(r562738);
        double r562740 = atan(r562739);
        double r562741 = 2.0;
        double r562742 = r562740 * r562741;
        return r562742;
}

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-log-exp0.0

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

  5. Applied add-sqr-sqrt0.0

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

  6. Applied add-sqr-sqrt0.0

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

  7. Applied times-frac0.0

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

  8. Final simplification0.0

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

Reproduce

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