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