Initial program 0.1
\[x \cdot \left(y + z\right) + z \cdot 5
\]
Simplified0.1
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y, z \cdot \left(x + 5\right)\right)}
\]
Proof
(fma.f64 x y (*.f64 z (+.f64 x 5))): 0 points increase in error, 0 points decrease in error
(fma.f64 x y (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 z x) (*.f64 z 5)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 x y) (+.f64 (*.f64 z x) (*.f64 z 5)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 y x)) (+.f64 (*.f64 z x) (*.f64 z 5))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 y x) (*.f64 z x)) (*.f64 z 5))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 x (+.f64 y z))) (*.f64 z 5)): 0 points increase in error, 0 points decrease in error
Taylor expanded in x around 0 0.1
\[\leadsto \color{blue}{\left(y + z\right) \cdot x + 5 \cdot z}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(z, 5, x \cdot \left(z + y\right)\right)}
\]
Proof
(fma.f64 z 5 (*.f64 x (+.f64 z y))): 0 points increase in error, 0 points decrease in error
(fma.f64 z 5 (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 z 5) (*.f64 x (+.f64 y z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 5 z)) (*.f64 x (+.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 5 z) (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 y z) x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (+.f64 y z) x) (*.f64 5 z))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{fma}\left(z, 5, x \cdot \left(z + y\right)\right)
\]