Simplified0.2
\[\leadsto \color{blue}{\left(\frac{z - x}{\frac{y}{x + z}} - y\right) \cdot -0.5}
\]
Proof
(*.f64 (-.f64 (/.f64 (-.f64 z x) (/.f64 y (+.f64 x z))) y) -1/2): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 z x) (+.f64 x z)) y)) y) -1/2): 7 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 x z) (-.f64 z x))) y) y) -1/2): 0 points increase in error, 19 points decrease in error
(*.f64 (-.f64 (/.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 z x)) (-.f64 z x)) y) y) -1/2): 18 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (/.f64 (Rewrite<= difference-of-squares_binary64 (-.f64 (*.f64 z z) (*.f64 x x))) y) y) -1/2): 0 points increase in error, 18 points decrease in error
(*.f64 (-.f64 (/.f64 (-.f64 (*.f64 z z) (*.f64 x x)) y) (Rewrite<= /-rgt-identity_binary64 (/.f64 y 1))) -1/2): 12 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (/.f64 (-.f64 (*.f64 z z) (*.f64 x x)) y) (/.f64 y (Rewrite<= *-inverses_binary64 (/.f64 y y)))) -1/2): 19 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (/.f64 (-.f64 (*.f64 z z) (*.f64 x x)) y) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y y) y))) -1/2): 0 points increase in error, 19 points decrease in error
(*.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (-.f64 (*.f64 z z) (*.f64 x x)) (*.f64 y y)) y)) -1/2): 12 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y)))) y) -1/2): 1 points increase in error, 12 points decrease in error
(*.f64 (/.f64 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y))) y) (Rewrite<= metadata-eval (/.f64 -1 2))): 12 points increase in error, 1 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y))) -1) (*.f64 y 2))): 1 points increase in error, 12 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y))))) (*.f64 y 2)): 0 points increase in error, 1 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 (*.f64 z z) (+.f64 (*.f64 x x) (*.f64 y y))))) (*.f64 y 2)): 12 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 y 2)): 0 points increase in error, 12 points decrease in error
(/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 z z)) (+.f64 (*.f64 x x) (*.f64 y y)))) (*.f64 y 2)): 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 y 2)): 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 y 2)): 12 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 y 2)): 0 points increase in error, 12 points decrease in error