Simplified0.5
\[\leadsto \sqrt[3]{{\color{blue}{\left(-ux \cdot \mathsf{fma}\left(ux, {\left(maxCos + -1\right)}^{2}, \mathsf{fma}\left(2, maxCos, -2\right)\right)\right)}}^{1.5} \cdot {\sin \left(uy \cdot \left(2 \cdot \pi\right)\right)}^{3}}
\]
Proof
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 maxCos -1) 2) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 maxCos (Rewrite<= metadata-eval (neg.f32 1))) 2) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (Rewrite<= sub-neg_binary32 (-.f32 maxCos 1)) 2) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (Rewrite=> unpow2_binary32 (*.f32 (-.f32 maxCos 1) (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (Rewrite<= sqr-neg_binary32 (*.f32 (neg.f32 (-.f32 maxCos 1)) (neg.f32 (-.f32 maxCos 1)))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (-.f32 maxCos 1))) (neg.f32 (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (*.f32 -1 (-.f32 maxCos 1)) (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (-.f32 maxCos 1)))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (*.f32 -1 (Rewrite=> sub-neg_binary32 (+.f32 maxCos (neg.f32 1)))) (*.f32 -1 (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (*.f32 -1 (+.f32 maxCos (Rewrite=> metadata-eval -1))) (*.f32 -1 (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (*.f32 -1 (Rewrite=> +-commutative_binary32 (+.f32 -1 maxCos))) (*.f32 -1 (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (Rewrite=> distribute-lft-in_binary32 (+.f32 (*.f32 -1 -1) (*.f32 -1 maxCos))) (*.f32 -1 (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (+.f32 (Rewrite=> metadata-eval 1) (*.f32 -1 maxCos)) (*.f32 -1 (-.f32 maxCos 1))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (+.f32 1 (*.f32 -1 maxCos)) (*.f32 -1 (Rewrite=> sub-neg_binary32 (+.f32 maxCos (neg.f32 1))))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (+.f32 1 (*.f32 -1 maxCos)) (*.f32 -1 (+.f32 maxCos (Rewrite=> metadata-eval -1)))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (+.f32 1 (*.f32 -1 maxCos)) (*.f32 -1 (Rewrite=> +-commutative_binary32 (+.f32 -1 maxCos)))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (+.f32 1 (*.f32 -1 maxCos)) (Rewrite=> distribute-lft-in_binary32 (+.f32 (*.f32 -1 -1) (*.f32 -1 maxCos)))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (*.f32 (+.f32 1 (*.f32 -1 maxCos)) (+.f32 (Rewrite=> metadata-eval 1) (*.f32 -1 maxCos))) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (Rewrite<= unpow2_binary32 (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (fma.f32 2 maxCos -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (Rewrite=> fma-udef_binary32 (+.f32 (*.f32 2 maxCos) -2))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (+.f32 (*.f32 (Rewrite<= metadata-eval (*.f32 -1 -2)) maxCos) -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (+.f32 (Rewrite<= associate-*r*_binary32 (*.f32 -1 (*.f32 -2 maxCos))) -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (+.f32 (Rewrite=> *-commutative_binary32 (*.f32 (*.f32 -2 maxCos) -1)) -2)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (+.f32 (*.f32 (*.f32 -2 maxCos) -1) (Rewrite<= metadata-eval (*.f32 2 -1)))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (Rewrite<= distribute-rgt-in_binary32 (*.f32 -1 (+.f32 (*.f32 -2 maxCos) 2)))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (*.f32 -1 (Rewrite=> +-commutative_binary32 (+.f32 2 (*.f32 -2 maxCos))))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (*.f32 -1 (+.f32 2 (*.f32 (Rewrite<= metadata-eval (neg.f32 2)) maxCos)))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (*.f32 -1 (Rewrite<= cancel-sign-sub-inv_binary32 (-.f32 2 (*.f32 2 maxCos))))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (fma.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (Rewrite=> mul-1-neg_binary32 (neg.f32 (-.f32 2 (*.f32 2 maxCos))))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (*.f32 ux (Rewrite<= fma-neg_binary32 (-.f32 (*.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (-.f32 2 (*.f32 2 maxCos)))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (Rewrite<= distribute-lft-out--_binary32 (-.f32 (*.f32 ux (*.f32 ux (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2))) (*.f32 ux (-.f32 2 (*.f32 2 maxCos)))))): 19 points increase in error, 18 points decrease in error
(neg.f32 (-.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 ux ux) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2))) (*.f32 ux (-.f32 2 (*.f32 2 maxCos))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (-.f32 (*.f32 (Rewrite<= unpow2_binary32 (pow.f32 ux 2)) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (*.f32 ux (-.f32 2 (*.f32 2 maxCos))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (-.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (*.f32 ux (Rewrite=> cancel-sign-sub-inv_binary32 (+.f32 2 (*.f32 (neg.f32 2) maxCos)))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (-.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (*.f32 ux (+.f32 2 (*.f32 (Rewrite=> metadata-eval -2) maxCos))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (-.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (*.f32 ux (Rewrite<= +-commutative_binary32 (+.f32 (*.f32 -2 maxCos) 2))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (-.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (Rewrite<= *-commutative_binary32 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)))): 0 points increase in error, 0 points decrease in error
(neg.f32 (Rewrite<= unsub-neg_binary32 (+.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (neg.f32 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (+.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux))))): 0 points increase in error, 0 points decrease in error
(neg.f32 (Rewrite<= +-commutative_binary32 (+.f32 (*.f32 -1 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)) (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub0-neg_binary32 (-.f32 0 (+.f32 (*.f32 -1 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)) (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2))))): 0 points increase in error, 0 points decrease in error
(-.f32 0 (Rewrite=> +-commutative_binary32 (+.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (*.f32 -1 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux))))): 0 points increase in error, 0 points decrease in error
(-.f32 0 (+.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (Rewrite=> mul-1-neg_binary32 (neg.f32 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux))))): 0 points increase in error, 0 points decrease in error
(-.f32 0 (Rewrite=> unsub-neg_binary32 (-.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l-_binary32 (+.f32 (-.f32 0 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux))): 0 points increase in error, 0 points decrease in error
(+.f32 (Rewrite<= neg-sub0_binary32 (neg.f32 (*.f32 (pow.f32 ux 2) (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2)))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (neg.f32 (Rewrite=> *-commutative_binary32 (*.f32 (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (pow.f32 ux 2)))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (Rewrite=> distribute-rgt-neg-in_binary32 (*.f32 (pow.f32 (+.f32 1 (*.f32 -1 maxCos)) 2) (neg.f32 (pow.f32 ux 2)))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (Rewrite=> unpow2_binary32 (*.f32 (+.f32 1 (*.f32 -1 maxCos)) (+.f32 1 (*.f32 -1 maxCos)))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (Rewrite=> +-commutative_binary32 (+.f32 (*.f32 -1 maxCos) 1)) (+.f32 1 (*.f32 -1 maxCos))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (+.f32 (Rewrite=> mul-1-neg_binary32 (neg.f32 maxCos)) 1) (+.f32 1 (*.f32 -1 maxCos))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (+.f32 (Rewrite=> neg-sub0_binary32 (-.f32 0 maxCos)) 1) (+.f32 1 (*.f32 -1 maxCos))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (Rewrite=> associate-+l-_binary32 (-.f32 0 (-.f32 maxCos 1))) (+.f32 1 (*.f32 -1 maxCos))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (Rewrite<= neg-sub0_binary32 (neg.f32 (-.f32 maxCos 1))) (+.f32 1 (*.f32 -1 maxCos))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (neg.f32 (-.f32 maxCos 1)) (Rewrite=> +-commutative_binary32 (+.f32 (*.f32 -1 maxCos) 1))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (neg.f32 (-.f32 maxCos 1)) (+.f32 (Rewrite=> mul-1-neg_binary32 (neg.f32 maxCos)) 1)) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (neg.f32 (-.f32 maxCos 1)) (+.f32 (Rewrite=> neg-sub0_binary32 (-.f32 0 maxCos)) 1)) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (neg.f32 (-.f32 maxCos 1)) (Rewrite=> associate-+l-_binary32 (-.f32 0 (-.f32 maxCos 1)))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 (neg.f32 (-.f32 maxCos 1)) (Rewrite<= neg-sub0_binary32 (neg.f32 (-.f32 maxCos 1)))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (Rewrite=> sqr-neg_binary32 (*.f32 (-.f32 maxCos 1) (-.f32 maxCos 1))) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (Rewrite<= unpow2_binary32 (pow.f32 (-.f32 maxCos 1) 2)) (neg.f32 (pow.f32 ux 2))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (Rewrite<= distribute-rgt-neg-in_binary32 (neg.f32 (*.f32 (pow.f32 (-.f32 maxCos 1) 2) (pow.f32 ux 2)))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(+.f32 (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (*.f32 (pow.f32 (-.f32 maxCos 1) 2) (pow.f32 ux 2)))) (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux)): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary32 (+.f32 (*.f32 (+.f32 (*.f32 -2 maxCos) 2) ux) (*.f32 -1 (*.f32 (pow.f32 (-.f32 maxCos 1) 2) (pow.f32 ux 2))))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (Rewrite=> +-commutative_binary32 (+.f32 2 (*.f32 -2 maxCos))) ux) (*.f32 -1 (*.f32 (pow.f32 (-.f32 maxCos 1) 2) (pow.f32 ux 2)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (+.f32 2 (*.f32 (Rewrite<= metadata-eval (neg.f32 2)) maxCos)) ux) (*.f32 -1 (*.f32 (pow.f32 (-.f32 maxCos 1) 2) (pow.f32 ux 2)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (Rewrite<= cancel-sign-sub-inv_binary32 (-.f32 2 (*.f32 2 maxCos))) ux) (*.f32 -1 (*.f32 (pow.f32 (-.f32 maxCos 1) 2) (pow.f32 ux 2)))): 0 points increase in error, 0 points decrease in error