Initial program 0.0
\[\frac{x - y}{z - y}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{y - x}{y - z}}
\]
Proof
(/.f64 (-.f64 y x) (-.f64 y z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 y x) (-.f64 y z)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 (-.f64 y x) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 y x)) (*.f64 -1 (-.f64 y z)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 y x))) (*.f64 -1 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 y x))) (*.f64 -1 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 y) x)) (*.f64 -1 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 y)) x) (*.f64 -1 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (neg.f64 y))) (*.f64 -1 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 x y)) (*.f64 -1 (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x y) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 y z)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x y) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 y z)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x y) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 y) z))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x y) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 y)) z)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x y) (Rewrite<= +-commutative_binary64 (+.f64 z (neg.f64 y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x y) (Rewrite<= sub-neg_binary64 (-.f64 z y))): 0 points increase in error, 0 points decrease in error
Taylor expanded in x around 0 0.0
\[\leadsto \color{blue}{\frac{y}{y - z} + -1 \cdot \frac{x}{y - z}}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{y}{y - z} - \frac{x}{y - z}}
\]
Proof
(-.f64 (/.f64 y (-.f64 y z)) (/.f64 x (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 y (-.f64 y z)) (neg.f64 (/.f64 x (-.f64 y z))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 y (-.f64 y z)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 x (-.f64 y z))))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \frac{y}{y - z} - \frac{x}{y - z}
\]