Average Error: 0.0 → 0.0
Time: 4.9s
Precision: 64
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
↓
\[2 \cdot \tan^{-1} \left(\frac{\sqrt{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({\left(1 \cdot 1\right)}^{3} + {\left(x \cdot x - 1 \cdot x\right)}^{3}\right)}}{\sqrt{\left({1}^{3} + {x}^{3}\right) \cdot \left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) + \left(\left(x \cdot x - 1 \cdot x\right) \cdot \left(x \cdot x - 1 \cdot x\right) - \left(1 \cdot 1\right) \cdot \left(x \cdot x - 1 \cdot x\right)\right)\right)} \cdot \sqrt{1 + x}}\right)\]
2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
↓
2 \cdot \tan^{-1} \left(\frac{\sqrt{\left(1 \cdot 1 - x \cdot x\right) \cdot \left({\left(1 \cdot 1\right)}^{3} + {\left(x \cdot x - 1 \cdot x\right)}^{3}\right)}}{\sqrt{\left({1}^{3} + {x}^{3}\right) \cdot \left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) + \left(\left(x \cdot x - 1 \cdot x\right) \cdot \left(x \cdot x - 1 \cdot x\right) - \left(1 \cdot 1\right) \cdot \left(x \cdot x - 1 \cdot x\right)\right)\right)} \cdot \sqrt{1 + x}}\right)
double f(double x) {
        double r20119 = 2.0;
        double r20120 = 1.0;
        double r20121 = x;
        double r20122 = r20120 - r20121;
        double r20123 = r20120 + r20121;
        double r20124 = r20122 / r20123;
        double r20125 = sqrt(r20124);
        double r20126 = atan(r20125);
        double r20127 = r20119 * r20126;
        return r20127;
}
↓
double f(double x) {
        double r20128 = 2.0;
        double r20129 = 1.0;
        double r20130 = r20129 * r20129;
        double r20131 = x;
        double r20132 = r20131 * r20131;
        double r20133 = r20130 - r20132;
        double r20134 = 3.0;
        double r20135 = pow(r20130, r20134);
        double r20136 = r20129 * r20131;
        double r20137 = r20132 - r20136;
        double r20138 = pow(r20137, r20134);
        double r20139 = r20135 + r20138;
        double r20140 = r20133 * r20139;
        double r20141 = sqrt(r20140);
        double r20142 = pow(r20129, r20134);
        double r20143 = pow(r20131, r20134);
        double r20144 = r20142 + r20143;
        double r20145 = r20130 * r20130;
        double r20146 = r20137 * r20137;
        double r20147 = r20130 * r20137;
        double r20148 = r20146 - r20147;
        double r20149 = r20145 + r20148;
        double r20150 = r20144 * r20149;
        double r20151 = sqrt(r20150);
        double r20152 = r20129 + r20131;
        double r20153 = sqrt(r20152);
        double r20154 = r20151 * r20153;
        double r20155 = r20141 / r20154;
        double r20156 = atan(r20155);
        double r20157 = r20128 * r20156;
        return r20157;
}

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 flip3-+0.0

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

  4. Applied associate-/r/0.0

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

  6. Applied flip3-+0.0

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

  7. Applied frac-times0.0

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

  8. Applied sqrt-div0.0

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

  10. Applied flip--0.0

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

  11. Applied associate-*l/0.0

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

  12. Applied sqrt-div0.0

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

  13. Applied associate-/l/0.0

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

  14. Final simplification0.0

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

Reproduce

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