Simplified0.0
\[\leadsto \left|\color{blue}{\frac{\left(x - -4\right) - z \cdot x}{y}}\right|
\]
Proof
(/.f64 (-.f64 (-.f64 x -4) (*.f64 z x)) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite=> sub-neg_binary64 (+.f64 x (neg.f64 -4))) (*.f64 z x)) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 x (Rewrite=> metadata-eval 4)) (*.f64 z x)) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (+.f64 x 4) 0)) (*.f64 z x)) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 (+.f64 x 4) 0) (Rewrite<= *-commutative_binary64 (*.f64 x z))) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite=> +-rgt-identity_binary64 (+.f64 x 4)) (*.f64 x z)) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite=> +-commutative_binary64 (+.f64 4 x)) (*.f64 x z)) y): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 4 x) (Rewrite=> *-commutative_binary64 (*.f64 z x))) y): 0 points increase in error, 0 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 (+.f64 4 x) y) (/.f64 (*.f64 z x) y))): 5 points increase in error, 2 points decrease in error
(-.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x 4)) y) (/.f64 (*.f64 z x) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (+.f64 x 4) y) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 x z)) y)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (+.f64 x 4) y) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 x y) z))): 14 points increase in error, 29 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (+.f64 x 4) y) (neg.f64 (*.f64 (/.f64 x y) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (+.f64 x 4) y) (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 (/.f64 x y) (neg.f64 z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (/.f64 x y) (neg.f64 z)) (/.f64 (+.f64 x 4) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 x y) (neg.f64 z)) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 x 4))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 x y) (neg.f64 z)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 y) (+.f64 x 4)))): 22 points increase in error, 5 points decrease in error
(+.f64 (*.f64 (/.f64 x y) (neg.f64 z)) (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 x (/.f64 1 y)) (*.f64 4 (/.f64 1 y))))): 0 points increase in error, 2 points decrease in error
(+.f64 (*.f64 (/.f64 x y) (neg.f64 z)) (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 (/.f64 x y) (neg.f64 z)) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (neg.f64 z) (/.f64 x y))) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (neg.f64 z) x) y)) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 29 points increase in error, 14 points decrease in error
(+.f64 (+.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (neg.f64 z) (/.f64 y x))) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 8 points increase in error, 29 points decrease in error
(+.f64 (+.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 z (/.f64 y x)))) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (neg.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 z y) x))) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 26 points increase in error, 12 points decrease in error
(+.f64 (+.f64 (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 (/.f64 z y)) x)) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 z y))) x) (*.f64 (/.f64 1 y) x)) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 x (+.f64 (*.f64 -1 (/.f64 z y)) (/.f64 1 y)))) (*.f64 4 (/.f64 1 y))): 1 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 1 y) (*.f64 -1 (/.f64 z y))))) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x (+.f64 (/.f64 1 y) (Rewrite=> mul-1-neg_binary64 (neg.f64 (/.f64 z y))))) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 x (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 1 y) (/.f64 z y)))) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (/.f64 1 y) (/.f64 z y)) x)) (*.f64 4 (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 4 (/.f64 1 y)) (*.f64 (-.f64 (/.f64 1 y) (/.f64 z y)) x))): 0 points increase in error, 0 points decrease in error