Initial program 0.1
\[x \cdot \left(1 - x \cdot y\right)
\]
Taylor expanded in x around 0 7.9
\[\leadsto \color{blue}{-1 \cdot \left(y \cdot {x}^{2}\right) + x}
\]
Simplified0.1
\[\leadsto \color{blue}{x - x \cdot \left(x \cdot y\right)}
\]
Proof
(-.f64 x (*.f64 x (*.f64 x y))): 0 points increase in error, 0 points decrease in error
(-.f64 x (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x x) y))): 37 points increase in error, 12 points decrease in error
(-.f64 x (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) y)): 0 points increase in error, 0 points decrease in error
(-.f64 x (Rewrite<= *-commutative_binary64 (*.f64 y (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 x (neg.f64 (*.f64 y (pow.f64 x 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 y (pow.f64 x 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 y (pow.f64 x 2))) x)): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto x - x \cdot \left(x \cdot y\right)
\]