Simplified3.1
\[\leadsto \color{blue}{z \cdot \left(-1 - \frac{x}{y}\right)}
\]
Proof
(*.f64 z (-.f64 -1 (/.f64 x y))): 0 points increase in error, 0 points decrease in error
(*.f64 z (-.f64 -1 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)) y))): 0 points increase in error, 0 points decrease in error
(*.f64 z (-.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 y) x)))): 12 points increase in error, 7 points decrease in error
(Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 z) (*.f64 (*.f64 (/.f64 1 y) x) z))): 2 points increase in error, 2 points decrease in error
(-.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) z) (*.f64 (*.f64 (/.f64 1 y) x) z)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 1 z))) (*.f64 (*.f64 (/.f64 1 y) x) z)): 0 points increase in error, 0 points decrease in error
(-.f64 (neg.f64 (*.f64 (Rewrite<= lft-mult-inverse_binary64 (*.f64 (/.f64 1 y) y)) z)) (*.f64 (*.f64 (/.f64 1 y) x) z)): 14 points increase in error, 3 points decrease in error
(-.f64 (neg.f64 (Rewrite=> associate-*l*_binary64 (*.f64 (/.f64 1 y) (*.f64 y z)))) (*.f64 (*.f64 (/.f64 1 y) x) z)): 40 points increase in error, 12 points decrease in error
(-.f64 (neg.f64 (*.f64 (/.f64 1 y) (*.f64 y z))) (Rewrite<= *-commutative_binary64 (*.f64 z (*.f64 (/.f64 1 y) x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 (/.f64 1 y) (neg.f64 (*.f64 y z)))) (*.f64 z (*.f64 (/.f64 1 y) x))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 1 y) (neg.f64 (*.f64 y z))) (*.f64 z (Rewrite=> *-commutative_binary64 (*.f64 x (/.f64 1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 1 y) (neg.f64 (*.f64 y z))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z x) (/.f64 1 y)))): 23 points increase in error, 26 points decrease in error
(-.f64 (*.f64 (/.f64 1 y) (neg.f64 (*.f64 y z))) (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 x z)) (/.f64 1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 1 y) (neg.f64 (*.f64 y z))) (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 1 y) (*.f64 x z)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> distribute-lft-out--_binary64 (*.f64 (/.f64 1 y) (-.f64 (neg.f64 (*.f64 y z)) (*.f64 x z)))): 0 points increase in error, 4 points decrease in error
(*.f64 (/.f64 1 y) (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 (*.f64 y z)) (neg.f64 (*.f64 x z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 1 y) (Rewrite=> distribute-neg-out_binary64 (neg.f64 (+.f64 (*.f64 y z) (*.f64 x z))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 1 y) (neg.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 z (+.f64 y x))))): 2 points increase in error, 2 points decrease in error
(Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 1 y) (*.f64 z (+.f64 y x))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 y (*.f64 z (+.f64 y x)))))): 26 points increase in error, 21 points decrease in error
(Rewrite=> distribute-neg-frac_binary64 (/.f64 (neg.f64 1) (/.f64 y (*.f64 z (+.f64 y x))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> metadata-eval -1) (/.f64 y (*.f64 z (+.f64 y x)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 z (+.f64 y x))) y)): 13 points increase in error, 24 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 z (+.f64 y x)) y))): 0 points increase in error, 0 points decrease in error
(*.f64 -1 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 y x) z)) y)): 0 points increase in error, 0 points decrease in error