Initial program 13.5
\[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Simplified0.3
\[\leadsto \color{blue}{\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \cos \left(2 \cdot \left(\pi \cdot u2\right)\right)}
\]
Proof
(*.f32 (sqrt.f32 (neg.f32 (log1p.f32 (neg.f32 u1)))) (cos.f32 (*.f32 2 (*.f32 (PI.f32) u2)))): 0 points increase in error, 0 points decrease in error
(*.f32 (sqrt.f32 (neg.f32 (Rewrite<= log1p-def_binary32 (log.f32 (+.f32 1 (neg.f32 u1)))))) (cos.f32 (*.f32 2 (*.f32 (PI.f32) u2)))): 227 points increase in error, 6 points decrease in error
(*.f32 (sqrt.f32 (neg.f32 (log.f32 (Rewrite<= sub-neg_binary32 (-.f32 1 u1))))) (cos.f32 (*.f32 2 (*.f32 (PI.f32) u2)))): 0 points increase in error, 0 points decrease in error
(*.f32 (sqrt.f32 (neg.f32 (log.f32 (-.f32 1 u1)))) (cos.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 2 (PI.f32)) u2)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.4
\[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left({\cos \left(\pi \cdot u2\right)}^{2} - {\sin \left(\pi \cdot u2\right)}^{2}\right)}
\]
Applied egg-rr0.3
\[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\color{blue}{\left(0.5 + 0.5 \cdot \cos \left(2 \cdot \left(\pi \cdot u2\right)\right)\right)} - {\sin \left(\pi \cdot u2\right)}^{2}\right)
\]
Applied egg-rr0.3
\[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(\left(0.5 \cdot \cos \left(2 \cdot \left(\pi \cdot u2\right)\right) - {\sin \left(\pi \cdot u2\right)}^{2}\right) + 0.5\right)}
\]
Final simplification0.3
\[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(0.5 + \left(0.5 \cdot \cos \left(2 \cdot \left(\pi \cdot u2\right)\right) - {\sin \left(\pi \cdot u2\right)}^{2}\right)\right)
\]