Simplified0.9
\[\leadsto \color{blue}{\left|\frac{\mathsf{fma}\left(x, z, -4 - x\right)}{y}\right|}
\]
Proof
(fabs.f64 (/.f64 (fma.f64 x z (-.f64 -4 x)) y)): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (fma.f64 x z (-.f64 (Rewrite<= metadata-eval (neg.f64 4)) x)) y)): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (fma.f64 x z (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 4) (neg.f64 x)))) y)): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (fma.f64 x z (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 4 x)))) y)): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (fma.f64 x z (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 4)))) y)): 0 points increase in error, 0 points decrease in error
(fabs.f64 (/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x z) (+.f64 x 4))) y)): 1 points increase in error, 0 points decrease in error
(fabs.f64 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 x z) y) (/.f64 (+.f64 x 4) y)))): 3 points increase in error, 6 points decrease in error
(fabs.f64 (-.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 x y) z)) (/.f64 (+.f64 x 4) y))): 23 points increase in error, 20 points decrease in error
(fabs.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 (*.f64 (/.f64 x y) z) (/.f64 (+.f64 x 4) y)) 1))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (*.f64 (-.f64 (*.f64 (/.f64 x y) z) (/.f64 (+.f64 x 4) y)) (Rewrite<= metadata-eval (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> fabs-mul_binary64 (*.f64 (fabs.f64 (-.f64 (*.f64 (/.f64 x y) z) (/.f64 (+.f64 x 4) y))) (fabs.f64 (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= fabs-sub_binary64 (fabs.f64 (-.f64 (/.f64 (+.f64 x 4) y) (*.f64 (/.f64 x y) z)))) (fabs.f64 (neg.f64 -1))): 0 points increase in error, 0 points decrease in error
(*.f64 (fabs.f64 (-.f64 (/.f64 (+.f64 x 4) y) (*.f64 (/.f64 x y) z))) (fabs.f64 (Rewrite=> metadata-eval 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (fabs.f64 (-.f64 (/.f64 (+.f64 x 4) y) (*.f64 (/.f64 x y) z))) (Rewrite=> metadata-eval 1)): 0 points increase in error, 0 points decrease in error
(Rewrite=> *-rgt-identity_binary64 (fabs.f64 (-.f64 (/.f64 (+.f64 x 4) y) (*.f64 (/.f64 x y) z)))): 0 points increase in error, 0 points decrease in error