Simplified0.4
\[\leadsto \color{blue}{\mathsf{fma}\left(ux, \left(zi \cdot maxCos\right) \cdot \left(1 - ux\right), \sqrt{1 - \left(1 - ux\right) \cdot \left(\left(ux \cdot \left(\left(1 - ux\right) \cdot maxCos\right)\right) \cdot \left(ux \cdot maxCos\right)\right)} \cdot \left(\cos \left(uy \cdot \left(2 \cdot \pi\right)\right) \cdot xi + \sin \left(uy \cdot \left(2 \cdot \pi\right)\right) \cdot yi\right)\right)}
\]
Proof
(fma.f32 ux (*.f32 (*.f32 zi maxCos) (-.f32 1 ux)) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (*.f32 (*.f32 ux (*.f32 (-.f32 1 ux) maxCos)) (*.f32 ux maxCos))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (Rewrite<= associate-*r*_binary32 (*.f32 zi (*.f32 maxCos (-.f32 1 ux)))) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (*.f32 (*.f32 ux (*.f32 (-.f32 1 ux) maxCos)) (*.f32 ux maxCos))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 3 points increase in error, 2 points decrease in error
(fma.f32 ux (*.f32 zi (Rewrite<= *-commutative_binary32 (*.f32 (-.f32 1 ux) maxCos))) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (*.f32 (*.f32 ux (*.f32 (-.f32 1 ux) maxCos)) (*.f32 ux maxCos))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (Rewrite=> *-commutative_binary32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi)) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (*.f32 (*.f32 ux (*.f32 (-.f32 1 ux) maxCos)) (*.f32 ux maxCos))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (*.f32 (Rewrite<= *-commutative_binary32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)) (*.f32 ux maxCos))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (Rewrite<= *-commutative_binary32 (*.f32 maxCos ux)))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (-.f32 1 ux) (Rewrite<= *-commutative_binary32 (*.f32 (*.f32 maxCos ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (-.f32 1 ux) (*.f32 maxCos ux)) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (Rewrite=> swap-sqr_binary32 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) (*.f32 (-.f32 1 ux) maxCos)) (*.f32 ux ux))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (Rewrite=> associate-*l*_binary32 (*.f32 (-.f32 1 ux) (*.f32 maxCos (*.f32 (-.f32 1 ux) maxCos)))) (*.f32 ux ux)))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (Rewrite=> associate-*l*_binary32 (*.f32 (-.f32 1 ux) (*.f32 (*.f32 maxCos (*.f32 (-.f32 1 ux) maxCos)) (*.f32 ux ux)))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (-.f32 1 ux) (*.f32 maxCos (*.f32 (-.f32 1 ux) maxCos))) (*.f32 ux ux))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) (*.f32 (-.f32 1 ux) maxCos))) (*.f32 ux ux)))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (Rewrite<= swap-sqr_binary32 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) (+.f32 (*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))) (+.f32 (*.f32 (cos.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 uy 2) (PI.f32)))) xi) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))) (+.f32 (Rewrite<= *-commutative_binary32 (*.f32 xi (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))))) (*.f32 (sin.f32 (*.f32 uy (*.f32 2 (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))) (+.f32 (*.f32 xi (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32)))) (*.f32 (sin.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 uy 2) (PI.f32)))) yi)))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (*.f32 (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))) (+.f32 (*.f32 xi (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32)))) (Rewrite=> *-commutative_binary32 (*.f32 yi (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32)))))))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (Rewrite<= distribute-rgt-out_binary32 (+.f32 (*.f32 (*.f32 xi (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32)))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) (*.f32 (*.f32 yi (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32)))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)))))))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (+.f32 (Rewrite<= associate-*r*_binary32 (*.f32 xi (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))))) (*.f32 (*.f32 yi (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32)))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (+.f32 (Rewrite<= *-commutative_binary32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi)) (*.f32 (*.f32 yi (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32)))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi) (Rewrite<= associate-*r*_binary32 (*.f32 yi (*.f32 (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))))))): 0 points increase in error, 0 points decrease in error
(fma.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi) (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi) (Rewrite<= *-commutative_binary32 (*.f32 (*.f32 (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) yi)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary32 (+.f32 (*.f32 ux (*.f32 (*.f32 (-.f32 1 ux) maxCos) zi)) (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi) (*.f32 (*.f32 (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) yi)))): 2 points increase in error, 0 points decrease in error
(+.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 ux (*.f32 (-.f32 1 ux) maxCos)) zi)) (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi) (*.f32 (*.f32 (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) yi))): 2 points increase in error, 3 points decrease in error
(+.f32 (*.f32 (Rewrite<= *-commutative_binary32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux)) zi) (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi) (*.f32 (*.f32 (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) yi))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary32 (+.f32 (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) xi) (*.f32 (*.f32 (sin.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (-.f32 1 (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux))))) yi)) (*.f32 (*.f32 (*.f32 (-.f32 1 ux) maxCos) ux) zi))): 0 points increase in error, 0 points decrease in error