Simplified20.9
\[\leadsto \color{blue}{\mathsf{fma}\left(2, \sqrt{x} \cdot \cos \left(\mathsf{fma}\left(z, t \cdot -0.3333333333333333, y\right)\right), \frac{\frac{a}{-3}}{b}\right)}
\]
Proof
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (fma.f64 z (*.f64 t -1/3) y))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (fma.f64 z (*.f64 t (Rewrite<= metadata-eval (/.f64 -1 3))) y))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (fma.f64 z (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 -1 3) t)) y))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (fma.f64 z (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 3 t))) y))) (/.f64 (/.f64 a -3) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (fma.f64 z (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 t) 3)) y))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (fma.f64 z (/.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 t)) 3) y))) (/.f64 (/.f64 a -3) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (/.f64 (neg.f64 t) 3)) y)))) (/.f64 (/.f64 a -3) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 z (neg.f64 t)) 3)) y))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (+.f64 (/.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 z t))) 3) y))) (/.f64 (/.f64 a -3) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (+.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (*.f64 z t) 3))) y))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 (/.f64 (*.f64 z t) 3)))))) (/.f64 (/.f64 a -3) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (Rewrite<= sub-neg_binary64 (-.f64 y (/.f64 (*.f64 z t) 3))))) (/.f64 (/.f64 a -3) b)): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3)))) (/.f64 (/.f64 a (Rewrite<= metadata-eval (/.f64 3 -1))) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3)))) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a -1) 3)) b)): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3)))) (/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 a)) 3) b)): 20 points increase in error, 0 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3)))) (/.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 a)) 3) b)): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3)))) (Rewrite=> associate-/l/_binary64 (/.f64 (neg.f64 a) (*.f64 b 3)))): 0 points increase in error, 20 points decrease in error
(fma.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3)))) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 a (*.f64 b 3))))): 20 points increase in error, 0 points decrease in error
(Rewrite<= fma-neg_binary64 (-.f64 (*.f64 2 (*.f64 (sqrt.f64 x) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3))))) (/.f64 a (*.f64 b 3)))): 0 points increase in error, 20 points decrease in error
(-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (sqrt.f64 x)) (cos.f64 (-.f64 y (/.f64 (*.f64 z t) 3))))) (/.f64 a (*.f64 b 3))): 20 points increase in error, 0 points decrease in error