Error

Derivation

1. Initial program 0.0

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

3. Applied clear-num0.0

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

4. Applied sqrt-div0.0

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

5. Simplified0.0

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

7. Applied add-exp-log0.0

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

8. Applied add-exp-log0.0

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

9. Applied div-exp0.0

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

10. Simplified0.0

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

11. Final simplification0.0

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

Reproduce

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