Error

Try it out

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 add-cbrt-cube0.0

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

6. Applied add-cbrt-cube0.0

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

7. Applied cbrt-undiv0.0

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

8. Simplified0.0

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

9. Final simplification0.0

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

Reproduce

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

Details

Time bar (total: 4.6m)Debug log