Simplified0.2
\[\leadsto \color{blue}{\mathsf{fma}\left(x - y, \frac{4}{z}, -2\right)}
\]
Proof
(fma.f64 (-.f64 x y) (/.f64 4 z) -2): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (Rewrite<= metadata-eval (*.f64 1 -2))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (*.f64 (Rewrite<= *-inverses_binary64 (/.f64 (neg.f64 z) (neg.f64 z))) -2)): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (*.f64 (/.f64 (neg.f64 z) (neg.f64 z)) (Rewrite<= metadata-eval (/.f64 2 -1)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (*.f64 (/.f64 (neg.f64 z) (neg.f64 z)) (/.f64 (Rewrite<= metadata-eval (*.f64 1/2 4)) -1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (neg.f64 z) (*.f64 1/2 4)) (*.f64 (neg.f64 z) -1)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (neg.f64 z) 1/2) 4)) (*.f64 (neg.f64 z) -1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (/.f64 (*.f64 (*.f64 (neg.f64 z) 1/2) 4) (Rewrite=> *-commutative_binary64 (*.f64 -1 (neg.f64 z))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (/.f64 (*.f64 (*.f64 (neg.f64 z) 1/2) 4) (Rewrite<= neg-mul-1_binary64 (neg.f64 (neg.f64 z))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (/.f64 (*.f64 (*.f64 (neg.f64 z) 1/2) 4) (Rewrite=> remove-double-neg_binary64 z))): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 x y) (/.f64 4 z) (Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 (neg.f64 z) 1/2) (/.f64 4 z)))): 18 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 x y) (/.f64 4 z)) (*.f64 (*.f64 (neg.f64 z) 1/2) (/.f64 4 z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-in_binary64 (*.f64 (/.f64 4 z) (+.f64 (-.f64 x y) (*.f64 (neg.f64 z) 1/2)))): 4 points increase in error, 3 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)): 0 points increase in error, 52 points decrease in error