Simplified0.0
\[\leadsto \color{blue}{x + \frac{-1 + x}{y} \cdot \left(\frac{1}{y} + \left(-1 + \frac{\frac{-1}{y}}{y}\right)\right)}
\]
Proof
(+.f64 x (*.f64 (/.f64 (+.f64 -1 x) y) (+.f64 (/.f64 1 y) (+.f64 -1 (/.f64 (/.f64 -1 y) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x -1)) y) (+.f64 (/.f64 1 y) (+.f64 -1 (/.f64 (/.f64 -1 y) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (+.f64 x (Rewrite<= metadata-eval (neg.f64 1))) y) (+.f64 (/.f64 1 y) (+.f64 -1 (/.f64 (/.f64 -1 y) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 x 1)) y) (+.f64 (/.f64 1 y) (+.f64 -1 (/.f64 (/.f64 -1 y) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 -1 (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 y y))))))): 5 points increase in error, 6 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 -1 (/.f64 -1 (Rewrite<= unpow2_binary64 (pow.f64 y 2))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 -1 (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) (pow.f64 y 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 -1 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 (pow.f64 y 2)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 -1 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 1 (pow.f64 y 2)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 -1 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 1 (pow.f64 y 2)) -1)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (Rewrite=> distribute-rgt1-in_binary64 (*.f64 (+.f64 (/.f64 1 (pow.f64 y 2)) 1) -1))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 (/.f64 1 (pow.f64 y 2)) -1) -1))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 1 (pow.f64 y 2)))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (/.f64 1 y) (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 1 (pow.f64 y 2)))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 (-.f64 x 1) y) (/.f64 1 y)) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1))))): 2 points increase in error, 2 points decrease in error
(+.f64 x (+.f64 (*.f64 (/.f64 (-.f64 x 1) y) (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) y)) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 (/.f64 (-.f64 x 1) y) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 -1 y)))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 (-.f64 x 1) y) (/.f64 -1 y)))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 x 1) -1) (*.f64 y y)))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 x 1))) (*.f64 y y))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (*.f64 -1 (-.f64 x 1)) (Rewrite<= unpow2_binary64 (pow.f64 y 2)))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (-.f64 x 1))) (pow.f64 y 2))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (-.f64 x 1))) (pow.f64 y 2))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 x) 1)) (pow.f64 y 2))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 x)) 1) (pow.f64 y 2))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 x))) (pow.f64 y 2))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 x)) (pow.f64 y 2))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))) (*.f64 (/.f64 (-.f64 x 1) y) (+.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) -1)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (neg.f64 (/.f64 1 (pow.f64 y 2))) (/.f64 (-.f64 x 1) y)) (*.f64 -1 (/.f64 (-.f64 x 1) y)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (+.f64 (*.f64 (Rewrite=> distribute-neg-frac_binary64 (/.f64 (neg.f64 1) (pow.f64 y 2))) (/.f64 (-.f64 x 1) y)) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (+.f64 (*.f64 (/.f64 (Rewrite=> metadata-eval -1) (pow.f64 y 2)) (/.f64 (-.f64 x 1) y)) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 x 1)) (*.f64 (pow.f64 y 2) y))) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 10 points increase in error, 12 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (+.f64 (/.f64 (*.f64 -1 (-.f64 x 1)) (*.f64 (Rewrite=> unpow2_binary64 (*.f64 y y)) y)) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (+.f64 (/.f64 (*.f64 -1 (-.f64 x 1)) (Rewrite<= unpow3_binary64 (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 7 points increase in error, 3 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3)))) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))) (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3)))) (*.f64 -1 (/.f64 (-.f64 x 1) y))))): 0 points increase in error, 1 points decrease in error
(+.f64 x (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))))) (*.f64 -1 (/.f64 (-.f64 x 1) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-lft-identity_binary64 (+.f64 0 x)) (+.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))) (*.f64 -1 (/.f64 (-.f64 x 1) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 1 1)) x) (+.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))) (*.f64 -1 (/.f64 (-.f64 x 1) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate--r-_binary64 (-.f64 1 (-.f64 1 x))) (+.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))) (*.f64 -1 (/.f64 (-.f64 x 1) y)))): 33 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (-.f64 1 x)))) (+.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))) (*.f64 -1 (/.f64 (-.f64 x 1) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 1 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (-.f64 1 x)))) (+.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))) (*.f64 -1 (/.f64 (-.f64 x 1) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 1 (*.f64 -1 (-.f64 1 x))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) y)) (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 (*.f64 -1 (-.f64 1 x)) (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) y)) (+.f64 (*.f64 -1 (/.f64 (-.f64 x 1) (pow.f64 y 3))) (*.f64 -1 (/.f64 (-.f64 1 x) (pow.f64 y 2)))))))): 48 points increase in error, 15 points decrease in error