Initial program 0.1
\[\left(x \cdot y\right) \cdot \left(1 - y\right)
\]
Applied egg-rr0.1
\[\leadsto \color{blue}{x \cdot y + \left(x \cdot y\right) \cdot \left(-y\right)}
\]
Taylor expanded in x around 0 5.3
\[\leadsto \color{blue}{\left(-1 \cdot {y}^{2} + y\right) \cdot x}
\]
Simplified0.1
\[\leadsto \color{blue}{y \cdot \left(x - y \cdot x\right)}
\]
Proof
(*.f64 y (-.f64 x (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y x) (*.f64 y (*.f64 y x)))): 5 points increase in error, 2 points decrease in error
(-.f64 (*.f64 y x) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y y) x))): 40 points increase in error, 8 points decrease in error
(-.f64 (*.f64 y x) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) x)): 0 points increase in error, 0 points decrease in error
(Rewrite=> distribute-rgt-out--_binary64 (*.f64 x (-.f64 y (pow.f64 y 2)))): 2 points increase in error, 4 points decrease in error
(*.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 y (neg.f64 (pow.f64 y 2))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 y (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (pow.f64 y 2))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (pow.f64 y 2)) y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 -1 (pow.f64 y 2)) y) x)): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto y \cdot \left(x - y \cdot x\right)
\]