Initial program 59.6
\[\cos^{-1} \left(1 - x\right)
\]
Applied egg-rr59.6
\[\leadsto \color{blue}{\frac{{\left(\pi \cdot 0.5\right)}^{3} - {\sin^{-1} \left(1 - x\right)}^{3}}{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right) + \left(\sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right) + \left(\pi \cdot 0.5\right) \cdot \sin^{-1} \left(1 - x\right)\right)}}
\]
Simplified59.6
\[\leadsto \color{blue}{\frac{{\left(\pi \cdot 0.5\right)}^{3} - {\sin^{-1} \left(1 - x\right)}^{3}}{\left(\pi \cdot \pi\right) \cdot 0.25 + \sin^{-1} \left(1 - x\right) \cdot \mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)}}
\]
Proof
(/.f64 (-.f64 (pow.f64 (*.f64 (PI.f64) 1/2) 3) (pow.f64 (asin.f64 (-.f64 1 x)) 3)) (+.f64 (*.f64 (*.f64 (PI.f64) (PI.f64)) 1/4) (*.f64 (asin.f64 (-.f64 1 x)) (fma.f64 (PI.f64) 1/2 (asin.f64 (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (*.f64 (PI.f64) 1/2) 3) (pow.f64 (asin.f64 (-.f64 1 x)) 3)) (+.f64 (*.f64 (*.f64 (PI.f64) (PI.f64)) (Rewrite<= metadata-eval (*.f64 1/2 1/2))) (*.f64 (asin.f64 (-.f64 1 x)) (fma.f64 (PI.f64) 1/2 (asin.f64 (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (*.f64 (PI.f64) 1/2) 3) (pow.f64 (asin.f64 (-.f64 1 x)) 3)) (+.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (PI.f64) 1/2) (*.f64 (PI.f64) 1/2))) (*.f64 (asin.f64 (-.f64 1 x)) (fma.f64 (PI.f64) 1/2 (asin.f64 (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (*.f64 (PI.f64) 1/2) 3) (pow.f64 (asin.f64 (-.f64 1 x)) 3)) (+.f64 (*.f64 (*.f64 (PI.f64) 1/2) (*.f64 (PI.f64) 1/2)) (*.f64 (asin.f64 (-.f64 1 x)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (PI.f64) 1/2) (asin.f64 (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (*.f64 (PI.f64) 1/2) 3) (pow.f64 (asin.f64 (-.f64 1 x)) 3)) (+.f64 (*.f64 (*.f64 (PI.f64) 1/2) (*.f64 (PI.f64) 1/2)) (*.f64 (asin.f64 (-.f64 1 x)) (Rewrite=> +-commutative_binary64 (+.f64 (asin.f64 (-.f64 1 x)) (*.f64 (PI.f64) 1/2)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (*.f64 (PI.f64) 1/2) 3) (pow.f64 (asin.f64 (-.f64 1 x)) 3)) (+.f64 (*.f64 (*.f64 (PI.f64) 1/2) (*.f64 (PI.f64) 1/2)) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (asin.f64 (-.f64 1 x)) (asin.f64 (-.f64 1 x))) (*.f64 (*.f64 (PI.f64) 1/2) (asin.f64 (-.f64 1 x))))))): 1 points increase in error, 0 points decrease in error
Applied egg-rr57.3
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left({\left(\pi \cdot 0.5\right)}^{1.5}, {\left(\pi \cdot 0.5\right)}^{1.5}, -{\sin^{-1} \left(1 - x\right)}^{3}\right)}}{\left(\pi \cdot \pi\right) \cdot 0.25 + \sin^{-1} \left(1 - x\right) \cdot \mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)}
\]
Applied egg-rr57.4
\[\leadsto \frac{\mathsf{fma}\left({\left(\pi \cdot 0.5\right)}^{1.5}, {\left(\pi \cdot 0.5\right)}^{1.5}, -{\color{blue}{\left({\left({\left(\sqrt[3]{\sqrt[3]{\sin^{-1} \left(1 - x\right)}}\right)}^{2}\right)}^{3} \cdot \sqrt[3]{\sin^{-1} \left(1 - x\right)}\right)}}^{3}\right)}{\left(\pi \cdot \pi\right) \cdot 0.25 + \sin^{-1} \left(1 - x\right) \cdot \mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)}
\]
Applied egg-rr57.3
\[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\left(\pi \cdot 0.5\right) \cdot \sqrt{\pi \cdot 0.5}, \left(\pi \cdot 0.5\right) \cdot \sqrt{\pi \cdot 0.5}, -\left(\sqrt{\sin^{-1} \left(1 - x\right)} \cdot {\sin^{-1} \left(1 - x\right)}^{2}\right) \cdot \sqrt{\sin^{-1} \left(1 - x\right)}\right) + \mathsf{fma}\left(-\sqrt{\sin^{-1} \left(1 - x\right)} \cdot {\sin^{-1} \left(1 - x\right)}^{2}, \sqrt{\sin^{-1} \left(1 - x\right)}, \left(\sqrt{\sin^{-1} \left(1 - x\right)} \cdot {\sin^{-1} \left(1 - x\right)}^{2}\right) \cdot \sqrt{\sin^{-1} \left(1 - x\right)}\right)}}{\left(\pi \cdot \pi\right) \cdot 0.25 + \sin^{-1} \left(1 - x\right) \cdot \mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)}
\]
Final simplification57.3
\[\leadsto \frac{\mathsf{fma}\left(\left(\pi \cdot 0.5\right) \cdot \sqrt{\pi \cdot 0.5}, \left(\pi \cdot 0.5\right) \cdot \sqrt{\pi \cdot 0.5}, \left(\sqrt{\sin^{-1} \left(1 - x\right)} \cdot {\sin^{-1} \left(1 - x\right)}^{2}\right) \cdot \left(-\sqrt{\sin^{-1} \left(1 - x\right)}\right)\right) + \mathsf{fma}\left(\sqrt{\sin^{-1} \left(1 - x\right)} \cdot \left(-{\sin^{-1} \left(1 - x\right)}^{2}\right), \sqrt{\sin^{-1} \left(1 - x\right)}, \sqrt{\sin^{-1} \left(1 - x\right)} \cdot \left(\sqrt{\sin^{-1} \left(1 - x\right)} \cdot {\sin^{-1} \left(1 - x\right)}^{2}\right)\right)}{\left(\pi \cdot \pi\right) \cdot 0.25 + \sin^{-1} \left(1 - x\right) \cdot \mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)}
\]