Simplified0.0
\[\leadsto \color{blue}{y + \frac{x}{z} \cdot \left(1 - y\right)}
\]
Proof
(+.f64 y (*.f64 (/.f64 x z) (-.f64 1 y))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 (/.f64 x z) (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 y))))): 14 points increase in error, 9 points decrease in error
(+.f64 y (*.f64 (/.f64 x z) (+.f64 1 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 y))))): 9 points increase in error, 14 points decrease in error
(+.f64 y (Rewrite<= associate-/r/_binary64 (/.f64 x (/.f64 z (+.f64 1 (*.f64 -1 y)))))): 1 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x (+.f64 1 (*.f64 -1 y))) z))): 0 points increase in error, 13 points decrease in error
(+.f64 y (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 1 (*.f64 -1 y)) x)) z)): 0 points increase in error, 1 points decrease in error
(+.f64 y (Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 1 (*.f64 -1 y)) (/.f64 z x)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 y) 1)) (/.f64 z x))): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (+.f64 (*.f64 -1 y) (Rewrite<= metadata-eval (*.f64 -1 -1))) (/.f64 z x))): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 -1 (+.f64 y -1))) (/.f64 z x))): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 -1 (+.f64 y (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 z x))): 0 points increase in error, 0 points decrease in error
(+.f64 y (/.f64 (*.f64 -1 (Rewrite<= sub-neg_binary64 (-.f64 y 1))) (/.f64 z x))): 18 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 y 1) (/.f64 z x))))): 0 points increase in error, 18 points decrease in error
(+.f64 y (*.f64 -1 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 y 1) x) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite=> mul-1-neg_binary64 (neg.f64 (/.f64 (*.f64 (-.f64 y 1) x) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 (*.f64 (-.f64 y 1) x) z)))): 31 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 0 (Rewrite=> associate-/l*_binary64 (/.f64 (-.f64 y 1) (/.f64 z x))))): 0 points increase in error, 31 points decrease in error
(+.f64 y (-.f64 0 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y (/.f64 z x)) (/.f64 1 (/.f64 z x)))))): 13 points increase in error, 0 points decrease in error
(+.f64 y (-.f64 0 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y x) z)) (/.f64 1 (/.f64 z x))))): 0 points increase in error, 13 points decrease in error
(+.f64 y (Rewrite=> associate--r-_binary64 (+.f64 (-.f64 0 (/.f64 (*.f64 y x) z)) (/.f64 1 (/.f64 z x))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (/.f64 (*.f64 y x) z))) (/.f64 1 (/.f64 z x)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 y x) z))) (/.f64 1 (/.f64 z x)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 z) x)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 x) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (/.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) x) z))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (/.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 -1 x))) z))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (/.f64 (neg.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 x))) z))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (/.f64 (Rewrite=> remove-double-neg_binary64 x) z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (/.f64 x z)) y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (+.f64 (/.f64 x z) y))): 1 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (*.f64 y x) z)) (Rewrite<= +-commutative_binary64 (+.f64 y (/.f64 x z)))): 0 points increase in error, 1 points decrease in error