Initial program 0.0
\[\frac{\left|x - y\right|}{\left|y\right|}
\]
Taylor expanded in x around -inf 0.0
\[\leadsto \color{blue}{\frac{\left|-\left(y + -1 \cdot x\right)\right|}{\left|y\right|}}
\]
Simplified0.0
\[\leadsto \color{blue}{\left|1 - \frac{x}{y}\right|}
\]
Proof
(fabs.f64 (-.f64 1 (/.f64 x y))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (-.f64 (Rewrite<= *-inverses_binary64 (/.f64 y y)) (/.f64 x y))): 0 points increase in error, 0 points decrease in error
(fabs.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 y x) y))): 5 points increase in error, 1 points decrease in error
(Rewrite=> fabs-div_binary64 (/.f64 (fabs.f64 (-.f64 y x)) (fabs.f64 y))): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (Rewrite=> sub-neg_binary64 (+.f64 y (neg.f64 x)))) (fabs.f64 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (fabs.f64 (+.f64 y (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x)))) (fabs.f64 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fabs-neg_binary64 (fabs.f64 (neg.f64 (+.f64 y (*.f64 -1 x))))) (fabs.f64 y)): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \left|1 - \frac{x}{y}\right|
\]