Simplified0.2
\[\leadsto \color{blue}{\frac{4}{z} \cdot \left(\left(x - y\right) + z \cdot -0.5\right)}
\]
Proof
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (*.f64 z -1/2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (*.f64 z (Rewrite<= metadata-eval (neg.f64 1/2))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 z 1/2))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (neg.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (*.f64 z 1/2) 1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (neg.f64 (/.f64 (*.f64 z 1/2) (Rewrite<= metadata-eval (neg.f64 -1)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 (*.f64 z 1/2)) (neg.f64 -1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 z 1/2))) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 z 1/2) -1)) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (Rewrite=> associate-/l*_binary64 (/.f64 (*.f64 z 1/2) (/.f64 (neg.f64 -1) -1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (/.f64 (*.f64 z 1/2) (/.f64 (Rewrite=> metadata-eval 1) -1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (/.f64 (*.f64 z 1/2) (Rewrite=> metadata-eval -1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (*.f64 z 1/2) -1)))): 1 points increase in error, 4 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (*.f64 z 1/2) (Rewrite<= metadata-eval (/.f64 1 -1))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (*.f64 z 1/2) (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 z 1/2) -1) (neg.f64 -1))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (*.f64 z 1/2))) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 z 1/2))) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 z) 1/2)) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (/.f64 (*.f64 (neg.f64 z) 1/2) (Rewrite=> metadata-eval 1)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 4 z) (-.f64 x y)) (*.f64 (/.f64 4 z) (Rewrite=> /-rgt-identity_binary64 (*.f64 (neg.f64 z) 1/2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-in_binary64 (*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (*.f64 (neg.f64 z) 1/2)))): 4 points increase in error, 1 points decrease in error
(*.f64 (/.f64 4 z) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (-.f64 x y) (*.f64 z 1/2)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 4 (-.f64 (-.f64 x y) (*.f64 z 1/2))) z)): 1 points increase in error, 57 points decrease in error