Average Error: 0.0 → 0.0
Time: 30.1s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\frac{\sqrt{1 - x \cdot \left(x \cdot x\right)}}{\sqrt{1 + \left(x \cdot x + x\right)} \cdot \sqrt{1 + x}}\right)\]
double f(double x) {
        double r974758 = 2.0;
        double r974759 = 1.0;
        double r974760 = x;
        double r974761 = r974759 - r974760;
        double r974762 = r974759 + r974760;
        double r974763 = r974761 / r974762;
        double r974764 = sqrt(r974763);
        double r974765 = atan(r974764);
        double r974766 = r974758 * r974765;
        return r974766;
}
↓
double f(double x) {
        double r974767 = 2.0;
        double r974768 = 1.0;
        double r974769 = x;
        double r974770 = r974769 * r974769;
        double r974771 = r974769 * r974770;
        double r974772 = r974768 - r974771;
        double r974773 = sqrt(r974772);
        double r974774 = r974770 + r974769;
        double r974775 = r974768 + r974774;
        double r974776 = sqrt(r974775);
        double r974777 = r974768 + r974769;
        double r974778 = sqrt(r974777);
        double r974779 = r974776 * r974778;
        double r974780 = r974773 / r974779;
        double r974781 = atan(r974780);
        double r974782 = r974767 * r974781;
        return r974782;
}


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

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 sqrt-div0.0

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

  5. Applied flip3--0.0

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

  6. Applied sqrt-div0.0

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

  7. Applied associate-/l/0.0

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

  8. Simplified0.0

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

  9. Final simplification0.0

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

Reproduce

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