Simplified29.0
\[\leadsto \color{blue}{1 - \frac{y}{\frac{1 + y}{1 - x}}}
\]
Proof
(-.f64 1 (/.f64 y (/.f64 (+.f64 1 y) (-.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 y 1)) (-.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 (+.f64 y 1) (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (+.f64 y 1) (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 1 -1)) (/.f64 (+.f64 y 1) (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 1 (+.f64 y 1)) (*.f64 -1 (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (/.f64 (*.f64 1 (+.f64 y 1)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 y 1) 1)) (neg.f64 (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 y 1) (/.f64 (neg.f64 (-.f64 1 x)) 1)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (neg.f64 (/.f64 (+.f64 y 1) (Rewrite=> /-rgt-identity_binary64 (neg.f64 (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 y (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 y -1) (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 (/.f64 y (Rewrite<= metadata-eval (/.f64 1 -1))) (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y -1) 1)) (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 -1 y)) 1) (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 y)) 1) (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (/.f64 (Rewrite=> /-rgt-identity_binary64 (neg.f64 y)) (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 y (/.f64 (+.f64 y 1) (neg.f64 (-.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (neg.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y (neg.f64 (-.f64 1 x))) (+.f64 y 1))))): 44 points increase in error, 13 points decrease in error
(-.f64 1 (neg.f64 (/.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (-.f64 1 x)))) (+.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (neg.f64 (/.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 1 x) y))) (+.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (neg.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (*.f64 (-.f64 1 x) y) (+.f64 y 1)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite=> remove-double-neg_binary64 (/.f64 (*.f64 (-.f64 1 x) y) (+.f64 y 1)))): 0 points increase in error, 0 points decrease in error
Simplified0.1
\[\leadsto \color{blue}{\frac{1}{y} + \left(\left(x + -1\right) \cdot \frac{\frac{1}{y}}{y} + \left(x - \frac{x}{y}\right)\right)}
\]
Proof
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (+.f64 x -1) (/.f64 (/.f64 1 y) y)) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 -1 x)) (/.f64 (/.f64 1 y) y)) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) x) (/.f64 (/.f64 1 y) y)) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 x))) (/.f64 (/.f64 1 y) y)) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 x))) (/.f64 (/.f64 1 y) y)) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (neg.f64 (-.f64 1 x)) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 y))) y)) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (neg.f64 (-.f64 1 x)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 y) (/.f64 1 y)))) (-.f64 x (/.f64 x y)))): 6 points increase in error, 8 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (*.f64 (neg.f64 (-.f64 1 x)) (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 1 y) 2))) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 (-.f64 1 x) (pow.f64 (/.f64 1 y) 2)))) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (neg.f64 (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 1 (neg.f64 x))) (pow.f64 (/.f64 1 y) 2))) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (neg.f64 (*.f64 (+.f64 1 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x))) (pow.f64 (/.f64 1 y) 2))) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (/.f64 1 y) 2) (+.f64 1 (*.f64 -1 x))))) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (pow.f64 (/.f64 1 y) 2) (+.f64 1 (*.f64 -1 x))))) (-.f64 x (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 1 y) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 -1 (*.f64 (pow.f64 (/.f64 1 y) 2) (+.f64 1 (*.f64 -1 x)))) x) (/.f64 x y)))): 1 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 1 y) (+.f64 (*.f64 -1 (*.f64 (pow.f64 (/.f64 1 y) 2) (+.f64 1 (*.f64 -1 x)))) x)) (/.f64 x y))): 0 points increase in error, 0 points decrease in error