Simplified13.8
\[\leadsto \color{blue}{\cos \left(uy \cdot \left(2 \cdot \pi\right)\right) \cdot \sqrt{\mathsf{fma}\left(\mathsf{fma}\left(ux, maxCos - 1, 1\right), ux - \mathsf{fma}\left(ux, maxCos, 1\right), 1\right)}}
\]
Proof
(*.f32 (cos.f32 (*.f32 uy (*.f32 2 (PI.f32)))) (sqrt.f32 (fma.f32 (fma.f32 ux (-.f32 maxCos 1) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 uy 2) (PI.f32)))) (sqrt.f32 (fma.f32 (fma.f32 ux (-.f32 maxCos 1) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (fma.f32 ux (Rewrite=> sub-neg_binary32 (+.f32 maxCos (neg.f32 1))) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (fma.f32 ux (+.f32 maxCos (Rewrite=> metadata-eval -1)) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (fma.f32 ux (Rewrite<= +-commutative_binary32 (+.f32 -1 maxCos)) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (Rewrite<= fma-def_binary32 (+.f32 (*.f32 ux (+.f32 -1 maxCos)) 1)) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (Rewrite<= distribute-rgt-out_binary32 (+.f32 (*.f32 -1 ux) (*.f32 maxCos ux))) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 1 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (+.f32 (Rewrite<= neg-mul-1_binary32 (neg.f32 ux)) (*.f32 maxCos ux)) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (+.f32 (neg.f32 ux) (Rewrite<= *-commutative_binary32 (*.f32 ux maxCos))) 1) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (Rewrite<= +-commutative_binary32 (+.f32 1 (+.f32 (neg.f32 ux) (*.f32 ux maxCos)))) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (Rewrite<= associate-+l+_binary32 (+.f32 (+.f32 1 (neg.f32 ux)) (*.f32 ux maxCos))) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 6 points increase in error, 2 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (Rewrite<= sub-neg_binary32 (-.f32 1 ux)) (*.f32 ux maxCos)) (-.f32 ux (fma.f32 ux maxCos 1)) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (-.f32 ux (Rewrite<= fma-def_binary32 (+.f32 (*.f32 ux maxCos) 1))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (Rewrite<= unsub-neg_binary32 (+.f32 ux (neg.f32 (+.f32 (*.f32 ux maxCos) 1)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (+.f32 (Rewrite<= remove-double-neg_binary32 (neg.f32 (neg.f32 ux))) (neg.f32 (+.f32 (*.f32 ux maxCos) 1))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (Rewrite<= distribute-neg-in_binary32 (neg.f32 (+.f32 (neg.f32 ux) (+.f32 (*.f32 ux maxCos) 1)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (neg.f32 (Rewrite<= +-commutative_binary32 (+.f32 (+.f32 (*.f32 ux maxCos) 1) (neg.f32 ux)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (neg.f32 (Rewrite<= associate-+r+_binary32 (+.f32 (*.f32 ux maxCos) (+.f32 1 (neg.f32 ux))))) 1))): 4 points increase in error, 5 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (neg.f32 (+.f32 (*.f32 ux maxCos) (Rewrite<= sub-neg_binary32 (-.f32 1 ux)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (fma.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (neg.f32 (Rewrite<= +-commutative_binary32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (Rewrite<= fma-def_binary32 (+.f32 (*.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (neg.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)))) 1)))): 87 points increase in error, 63 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (+.f32 (Rewrite<= *-commutative_binary32 (*.f32 (neg.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos))) (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (Rewrite<= +-commutative_binary32 (+.f32 1 (*.f32 (neg.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos))) (+.f32 (-.f32 1 ux) (*.f32 ux maxCos))))))): 0 points increase in error, 0 points decrease in error
(*.f32 (cos.f32 (*.f32 (*.f32 uy 2) (PI.f32))) (sqrt.f32 (Rewrite<= cancel-sign-sub-inv_binary32 (-.f32 1 (*.f32 (+.f32 (-.f32 1 ux) (*.f32 ux maxCos)) (+.f32 (-.f32 1 ux) (*.f32 ux maxCos))))))): 0 points increase in error, 0 points decrease in error