\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
Test:
arccos
Bits:
128 bits
Bits error versus x
Time: 39.7 s
Input Error: 0.1
Output Error: 0.1
Log: ⚲
Profile: 🕒
\(2 \cdot \tan^{-1} \left(\sqrt{\frac{{1}^{3} - {x}^{3}}{(\left((x * x + x)_*\right) * \left(1 + x\right) + \left(1 + x\right))_*}}\right)\)
  1. Started with
    \[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)\]
    0.1
  2. Using strategy rm
    0.1
  3. Applied flip3-- to get
    \[2 \cdot \tan^{-1} \left(\sqrt{\frac{\color{red}{1 - x}}{1 + x}}\right) \leadsto 2 \cdot \tan^{-1} \left(\sqrt{\frac{\color{blue}{\frac{{1}^{3} - {x}^{3}}{{1}^2 + \left({x}^2 + 1 \cdot x\right)}}}{1 + x}}\right)\]
    0.1
  4. Applied associate-/l/ to get
    \[2 \cdot \tan^{-1} \left(\sqrt{\color{red}{\frac{\frac{{1}^{3} - {x}^{3}}{{1}^2 + \left({x}^2 + 1 \cdot x\right)}}{1 + x}}}\right) \leadsto 2 \cdot \tan^{-1} \left(\sqrt{\color{blue}{\frac{{1}^{3} - {x}^{3}}{\left(1 + x\right) \cdot \left({1}^2 + \left({x}^2 + 1 \cdot x\right)\right)}}}\right)\]
    0.1
  5. Applied simplify to get
    \[2 \cdot \tan^{-1} \left(\sqrt{\frac{{1}^{3} - {x}^{3}}{\color{red}{\left(1 + x\right) \cdot \left({1}^2 + \left({x}^2 + 1 \cdot x\right)\right)}}}\right) \leadsto 2 \cdot \tan^{-1} \left(\sqrt{\frac{{1}^{3} - {x}^{3}}{\color{blue}{(\left((x * x + x)_*\right) * \left(1 + x\right) + \left(1 + x\right))_*}}}\right)\]
    0.1

Original test:


(lambda ((x default))
  #:name "arccos"
  (* 2 (atan (sqrt (/ (- 1 x) (+ 1 x))))))