Initial program 0.0
\[\frac{x \cdot y}{2} - \frac{z}{8}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{y}{2}, \frac{z}{-8}\right)}
\]
Proof
(fma.f64 x (/.f64 y 2) (/.f64 z -8)): 0 points increase in error, 0 points decrease in error
(fma.f64 x (/.f64 y 2) (/.f64 z (Rewrite<= metadata-eval (/.f64 8 -1)))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (/.f64 y 2) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 z -1) 8))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (/.f64 y 2) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 z)) 8)): 0 points increase in error, 0 points decrease in error
(fma.f64 x (/.f64 y 2) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 z 8)))): 0 points increase in error, 0 points decrease in error
(fma.f64 x (/.f64 y 2) (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 z 8)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x (/.f64 y 2)) (/.f64 z 8))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 y 2) x)) (/.f64 z 8)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 y x) 2)) (/.f64 z 8)): 8 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 x y)) 2) (/.f64 z 8)): 0 points increase in error, 8 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{fma}\left(x, \frac{y}{2}, \frac{z}{-8}\right)
\]