Initial program 12.7
\[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\]
Simplified0.5
\[\leadsto \color{blue}{\frac{-\mathsf{log1p}\left(-u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}}
\]
Proof
(/.f32 (neg.f32 (log1p.f32 (neg.f32 u0))) (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay)))): 0 points increase in error, 0 points decrease in error
(/.f32 (neg.f32 (Rewrite<= log1p-def_binary32 (log.f32 (+.f32 1 (neg.f32 u0))))) (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay)))): 222 points increase in error, 1 points decrease in error
(/.f32 (neg.f32 (log.f32 (Rewrite<= sub-neg_binary32 (-.f32 1 u0)))) (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay)))): 0 points increase in error, 0 points decrease in error
(/.f32 (Rewrite<= *-rgt-identity_binary32 (*.f32 (neg.f32 (log.f32 (-.f32 1 u0))) 1)) (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/l*_binary32 (/.f32 (neg.f32 (log.f32 (-.f32 1 u0))) (/.f32 (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay))) 1))): 0 points increase in error, 0 points decrease in error
(/.f32 (neg.f32 (log.f32 (-.f32 1 u0))) (Rewrite=> /-rgt-identity_binary32 (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay))))): 0 points increase in error, 0 points decrease in error
Final simplification0.5
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\]