Initial program 17.8
\[\left(\left(x \cdot y + y \cdot y\right) - y \cdot z\right) - y \cdot y
\]
Simplified0.0
\[\leadsto \color{blue}{y \cdot \left(x - z\right)}
\]
Proof
(*.f64 y (-.f64 x z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y x) (*.f64 y z))): 3 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= *-commutative_binary64 (*.f64 x y)) (*.f64 y z)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (*.f64 x y) 0)) (*.f64 y z)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 x y) (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 y y) (*.f64 y y)))) (*.f64 y z)): 29 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (*.f64 y y))) (*.f64 y z)): 22 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (+.f64 (*.f64 y y) (*.f64 y z)))): 33 points increase in error, 8 points decrease in error
(-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y z) (*.f64 y y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l-_binary64 (-.f64 (-.f64 (+.f64 (*.f64 x y) (*.f64 y y)) (*.f64 y z)) (*.f64 y y))): 0 points increase in error, 0 points decrease in error
Applied egg-rr29.7
\[\leadsto \color{blue}{\frac{\left(x \cdot x - z \cdot z\right) \cdot y}{x + z}}
\]
Taylor expanded in x around 0 0.0
\[\leadsto \color{blue}{y \cdot x + -1 \cdot \left(y \cdot z\right)}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y, x, \left(-y\right) \cdot z\right)}
\]
Proof
(fma.f64 y x (*.f64 (neg.f64 y) z)): 0 points increase in error, 0 points decrease in error
(fma.f64 y x (*.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 y)) z)): 0 points increase in error, 0 points decrease in error
(fma.f64 y x (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 y z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y x) (*.f64 -1 (*.f64 y z)))): 3 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{fma}\left(y, x, -y \cdot z\right)
\]