Simplified0.2
\[\leadsto \color{blue}{-0.5 \cdot \left(\left(x + z\right) \cdot \frac{z - x}{y} - y\right)}
\]
Proof
(*.f64 -1/2 (-.f64 (*.f64 (+.f64 x z) (/.f64 (-.f64 z x) y)) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) (-.f64 (*.f64 (+.f64 x z) (/.f64 (-.f64 z x) y)) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 x z) (-.f64 z x)) y)) y)): 63 points increase in error, 12 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 z x)) (-.f64 z x)) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 -1 2) (-.f64 (/.f64 (Rewrite<= difference-of-squares_binary64 (-.f64 (*.f64 z z) (*.f64 x x))) y) y)): 0 points increase in error, 1 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)))): 67 points increase in error, 2 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))): 0 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