Initial program 0.0
\[2 \cdot \left(x \cdot x - x \cdot y\right)
\]
Taylor expanded in x around 0 0.0
\[\leadsto 2 \cdot \color{blue}{\left({x}^{2} + -1 \cdot \left(y \cdot x\right)\right)}
\]
Simplified0.0
\[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(y, -x, x \cdot x\right)}
\]
Proof
(fma.f64 y (neg.f64 x) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 x)) (*.f64 x x))): 1 points increase in error, 1 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x x) (*.f64 y (neg.f64 x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (*.f64 y (neg.f64 x))): 0 points increase in error, 1 points decrease in error
(+.f64 (pow.f64 x 2) (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 x 2) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto 2 \cdot \mathsf{fma}\left(y, -x, x \cdot x\right)
\]