Initial program 0.0
\[2 \cdot \tan^{-1} \left(\sqrt{\frac{1 - x}{1 + x}}\right)
\]
Applied egg-rr0.0
\[\leadsto 2 \cdot \tan^{-1} \color{blue}{\left(\frac{1}{\sqrt{\frac{-1 - x}{-1 + x}}}\right)}
\]
Simplified0.0
\[\leadsto 2 \cdot \tan^{-1} \color{blue}{\left(\frac{1}{\sqrt{\frac{-1 - x}{x + -1}}}\right)}
\]
Proof
(*.f64 2 (atan.f64 (/.f64 1 (sqrt.f64 (/.f64 (-.f64 -1 x) (+.f64 x -1)))))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (atan.f64 (/.f64 1 (sqrt.f64 (/.f64 (-.f64 -1 x) (Rewrite<= +-commutative_binary64 (+.f64 -1 x))))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto 2 \cdot \tan^{-1} \left(\frac{1}{\sqrt{\color{blue}{\left(-1 - x\right) \cdot \frac{-1}{1 - x}}}}\right)
\]
Simplified0.0
\[\leadsto 2 \cdot \tan^{-1} \left(\frac{1}{\sqrt{\color{blue}{\frac{-1}{1 - x} \cdot \left(-1 - x\right)}}}\right)
\]
Proof
(*.f64 2 (atan.f64 (/.f64 1 (sqrt.f64 (*.f64 (/.f64 -1 (-.f64 1 x)) (-.f64 -1 x)))))): 0 points increase in error, 0 points decrease in error
(*.f64 2 (atan.f64 (/.f64 1 (sqrt.f64 (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 -1 x) (/.f64 -1 (-.f64 1 x)))))))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto 2 \cdot \tan^{-1} \left(\frac{1}{\sqrt{\frac{-1}{1 - x} \cdot \left(-1 - x\right)}}\right)
\]