Initial program 28.3
\[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}
\]
Simplified12.4
\[\leadsto \color{blue}{-0.5 \cdot \left(\frac{\mathsf{fma}\left(z, z, x \cdot \left(-x\right)\right)}{y} - y\right)}
\]
Proof
(*.f64 -1/2 (-.f64 (/.f64 (fma.f64 z z (*.f64 x (neg.f64 x))) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) (-.f64 (/.f64 (fma.f64 z z (*.f64 x (neg.f64 x))) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (fma.f64 z z (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x x)))) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z z) (*.f64 x x))) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (-.f64 (*.f64 z z) (*.f64 x x)) y) (Rewrite<= /-rgt-identity_binary64 (/.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (-.f64 (*.f64 z z) (*.f64 x x)) y) (/.f64 y (Rewrite<= *-inverses_binary64 (/.f64 y y))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (-.f64 (*.f64 z z) (*.f64 x x)) y) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y y) y)))): 65 points increase in error, 1 points decrease in error
(*.f64 (/.f64 -1 2) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (-.f64 (*.f64 z z) (*.f64 x x)) (*.f64 y y)) y))): 2 points increase in error, 1 points decrease in error
(*.f64 (/.f64 -1 2) (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y)))) y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y)))) (*.f64 2 y))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y))))) (*.f64 2 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y))))) (*.f64 2 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 z z)) (+.f64 (*.f64 x x) (*.f64 y y)))) (*.f64 2 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 z z))) (+.f64 (*.f64 x x) (*.f64 y y))) (*.f64 2 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (neg.f64 (*.f64 z z)))) (*.f64 2 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z))) (*.f64 2 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (Rewrite<= *-commutative_binary64 (*.f64 y 2))): 0 points increase in error, 0 points decrease in error
Taylor expanded in z around 0 12.4
\[\leadsto -0.5 \cdot \color{blue}{\left(\left(-1 \cdot \frac{{x}^{2}}{y} + \frac{{z}^{2}}{y}\right) - y\right)}
\]
Simplified0.1
\[\leadsto -0.5 \cdot \color{blue}{\left(\frac{z - x}{y} \cdot \left(x + z\right) - y\right)}
\]
Proof
(-.f64 (*.f64 (/.f64 (-.f64 z x) y) (+.f64 x z)) y): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 (-.f64 z x) y) (Rewrite<= +-commutative_binary64 (+.f64 z x))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 z x) (/.f64 y (+.f64 z x)))) y): 25 points increase in error, 21 points decrease in error
(-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 z x) (+.f64 z x)) y)) y): 67 points increase in error, 20 points decrease in error
(-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 z x) (-.f64 z x))) y) y): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= difference-of-squares_binary64 (-.f64 (*.f64 z z) (*.f64 x x))) y) y): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) (*.f64 x x)) y) y): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (-.f64 (pow.f64 z 2) (Rewrite<= unpow2_binary64 (pow.f64 x 2))) y) y): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (pow.f64 z 2) y) (/.f64 (pow.f64 x 2) y))) y): 0 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (pow.f64 z 2) y) (neg.f64 (/.f64 (pow.f64 x 2) y)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (pow.f64 z 2) y) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (pow.f64 x 2) y)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (pow.f64 x 2) y)) (/.f64 (pow.f64 z 2) y))) y): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto -0.5 \cdot \left(\color{blue}{\frac{z - x}{\frac{y}{z + x}}} - y\right)
\]
Final simplification0.1
\[\leadsto -0.5 \cdot \left(\frac{z - x}{\frac{y}{z + x}} - y\right)
\]