Initial program 0.2
\[\frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\]
Taylor expanded in alphay around 0 0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\color{blue}{{\cos \tan^{-1} \left(\frac{\tan \left(0.5 \cdot \pi + 2 \cdot \left(u1 \cdot \pi\right)\right) \cdot alphay}{alphax}\right)}^{2}}}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\]
Simplified0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\color{blue}{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\]
Proof
(pow.f32 (cos.f32 (atan.f32 (*.f32 (/.f32 alphay alphax) (tan.f32 (*.f32 (PI.f32) (fma.f32 2 u1 1/2)))))) 2): 0 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (*.f32 (/.f32 alphay alphax) (tan.f32 (*.f32 (PI.f32) (Rewrite<= fma-def_binary32 (+.f32 (*.f32 2 u1) 1/2))))))) 2): 0 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (*.f32 (/.f32 alphay alphax) (tan.f32 (Rewrite<= distribute-rgt-out_binary32 (+.f32 (*.f32 (*.f32 2 u1) (PI.f32)) (*.f32 1/2 (PI.f32)))))))) 2): 26 points increase in error, 26 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (*.f32 (/.f32 alphay alphax) (tan.f32 (+.f32 (Rewrite<= associate-*r*_binary32 (*.f32 2 (*.f32 u1 (PI.f32)))) (*.f32 1/2 (PI.f32))))))) 2): 0 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (*.f32 (/.f32 alphay alphax) (tan.f32 (+.f32 (*.f32 2 (Rewrite=> *-commutative_binary32 (*.f32 (PI.f32) u1))) (*.f32 1/2 (PI.f32))))))) 2): 0 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (Rewrite<= associate-/r/_binary32 (/.f32 alphay (/.f32 alphax (tan.f32 (+.f32 (*.f32 2 (*.f32 (PI.f32) u1)) (*.f32 1/2 (PI.f32))))))))) 2): 1 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (Rewrite<= associate-/l*_binary32 (/.f32 (*.f32 alphay (tan.f32 (+.f32 (*.f32 2 (*.f32 (PI.f32) u1)) (*.f32 1/2 (PI.f32))))) alphax)))) 2): 0 points increase in error, 1 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (/.f32 (*.f32 alphay (tan.f32 (Rewrite=> +-commutative_binary32 (+.f32 (*.f32 1/2 (PI.f32)) (*.f32 2 (*.f32 (PI.f32) u1)))))) alphax))) 2): 0 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (/.f32 (*.f32 alphay (tan.f32 (+.f32 (*.f32 1/2 (PI.f32)) (*.f32 2 (Rewrite<= *-commutative_binary32 (*.f32 u1 (PI.f32))))))) alphax))) 2): 0 points increase in error, 0 points decrease in error
(pow.f32 (cos.f32 (atan.f32 (/.f32 (Rewrite<= *-commutative_binary32 (*.f32 (tan.f32 (+.f32 (*.f32 1/2 (PI.f32)) (*.f32 2 (*.f32 u1 (PI.f32))))) alphay)) alphax))) 2): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\color{blue}{\frac{1}{1 + {\left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}}}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\]
Final simplification0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\frac{1}{1 + {\left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(u1 \cdot \left(\pi \cdot 2\right) + \pi \cdot 0.5\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(u1 \cdot \left(\pi \cdot 2\right) + \pi \cdot 0.5\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\]