Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y, 1\right) - y}
\]
Proof
(-.f64 (fma.f64 x y 1) y): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x y) 1)) y): 13 points increase in error, 28 points decrease in error
(-.f64 (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 y x)) 1) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 (*.f64 y (Rewrite<= *-lft-identity_binary64 (*.f64 1 x))) 1) y): 13 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 y (*.f64 (Rewrite<= metadata-eval (*.f64 -1 -1)) x)) 1) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 (*.f64 y (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 -1 x)))) 1) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 (*.f64 y (*.f64 -1 (*.f64 (Rewrite<= metadata-eval (*.f64 1 -1)) x))) 1) y): 38 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 y (*.f64 -1 (Rewrite<= associate-*r*_binary64 (*.f64 1 (*.f64 -1 x))))) 1) y): 0 points increase in error, 38 points decrease in error
(-.f64 (+.f64 (*.f64 y (*.f64 -1 (*.f64 1 (Rewrite<= neg-mul-1_binary64 (neg.f64 x))))) 1) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y -1) (*.f64 1 (neg.f64 x)))) 1) y): 7 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 y)) (*.f64 1 (neg.f64 x))) 1) y): 0 points increase in error, 7 points decrease in error
(-.f64 (+.f64 (*.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 y)) (*.f64 1 (neg.f64 x))) 1) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 (neg.f64 y) (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 1 x)))) 1) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 (neg.f64 y) (neg.f64 (Rewrite=> *-lft-identity_binary64 x))) 1) y): 13 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 (Rewrite<= metadata-eval (+.f64 1 0)) (*.f64 (neg.f64 y) (neg.f64 x))) y): 13 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 0 (*.f64 (neg.f64 y) (neg.f64 x))))) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 1 (+.f64 (Rewrite<= mul0-lft_binary64 (*.f64 0 (*.f64 1 (neg.f64 x)))) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (*.f64 0 (*.f64 1 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x)))) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (*.f64 0 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 1 -1) x))) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (*.f64 0 (*.f64 (Rewrite=> metadata-eval -1) x)) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 0 -1) x)) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (*.f64 (Rewrite=> metadata-eval 0) x) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) x) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 13 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 x (*.f64 -1 x))) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 1 (+.f64 (+.f64 x (*.f64 (Rewrite<= metadata-eval (*.f64 1 -1)) x)) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 13 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 (+.f64 x (Rewrite<= associate-*r*_binary64 (*.f64 1 (*.f64 -1 x)))) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 1 (+.f64 (+.f64 x (*.f64 1 (Rewrite<= neg-mul-1_binary64 (neg.f64 x)))) (*.f64 (neg.f64 y) (neg.f64 x)))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (Rewrite<= associate-+r+_binary64 (+.f64 x (+.f64 (*.f64 1 (neg.f64 x)) (*.f64 (neg.f64 y) (neg.f64 x)))))) y): 7 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 x (Rewrite<= distribute-rgt-in_binary64 (*.f64 (neg.f64 x) (+.f64 1 (neg.f64 y)))))) y): 13 points increase in error, 0 points decrease in error
(-.f64 (+.f64 1 (+.f64 x (*.f64 (neg.f64 x) (Rewrite<= sub-neg_binary64 (-.f64 1 y))))) y): 0 points increase in error, 13 points decrease in error
(-.f64 (+.f64 1 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (neg.f64 x) (-.f64 1 y)) x))) y): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 (neg.f64 x) (-.f64 1 y)) x) 1)) y): 13 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r-_binary64 (+.f64 (+.f64 (*.f64 (neg.f64 x) (-.f64 1 y)) x) (-.f64 1 y))): 0 points increase in error, 13 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (neg.f64 x) (-.f64 1 y)) (+.f64 x (-.f64 1 y)))): 13 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (neg.f64 x) (-.f64 1 y)) (+.f64 x (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 1 y))))): 0 points increase in error, 13 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 x (*.f64 1 (-.f64 1 y))) (*.f64 (neg.f64 x) (-.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 x (+.f64 (*.f64 1 (-.f64 1 y)) (*.f64 (neg.f64 x) (-.f64 1 y))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= distribute-rgt-in_binary64 (*.f64 (-.f64 1 y) (+.f64 1 (neg.f64 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 (-.f64 1 y) (Rewrite<= sub-neg_binary64 (-.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 1 x) (-.f64 1 y)))): 0 points increase in error, 0 points decrease in error