Initial program 0.1
\[x - \frac{3}{8} \cdot y
\]
Simplified0
\[\leadsto \color{blue}{\mathsf{fma}\left(y, -0.375, x\right)}
\]
Proof
(fma.f64 y -3/8 x): 0 points increase in error, 0 points decrease in error
(fma.f64 y (Rewrite<= metadata-eval (neg.f64 3/8)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 y (neg.f64 (Rewrite<= metadata-eval (/.f64 3 8))) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 (/.f64 3 8))) x)): 16 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 3 8)))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 3 8) y))) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 x (neg.f64 (*.f64 (/.f64 3 8) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 x (*.f64 (/.f64 3 8) y))): 0 points increase in error, 0 points decrease in error
Final simplification0
\[\leadsto \mathsf{fma}\left(y, -0.375, x\right)
\]