Simplified0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(y, x + -0.5, 0.918938533204673 - x\right)}
\]
Proof
(fma.f64 y (+.f64 x -1/2) (-.f64 918938533204673/1000000000000000 x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 x (Rewrite<= metadata-eval (neg.f64 1/2))) (-.f64 918938533204673/1000000000000000 x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 1/2) x)) (-.f64 918938533204673/1000000000000000 x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (neg.f64 1/2) x) (-.f64 918938533204673/1000000000000000 (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (neg.f64 1/2) x) (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 918938533204673/1000000000000000 (*.f64 (neg.f64 1) x)))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (neg.f64 1/2) x) (+.f64 918938533204673/1000000000000000 (Rewrite<= *-commutative_binary64 (*.f64 x (neg.f64 1))))): 0 points increase in error, 0 points decrease in error
(fma.f64 y (+.f64 (neg.f64 1/2) x) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x (neg.f64 1)) 918938533204673/1000000000000000))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (+.f64 (neg.f64 1/2) x)) (+.f64 (*.f64 x (neg.f64 1)) 918938533204673/1000000000000000))): 0 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 y (neg.f64 1/2)) (*.f64 y x))) (+.f64 (*.f64 x (neg.f64 1)) 918938533204673/1000000000000000)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y 1/2))) (*.f64 y x)) (+.f64 (*.f64 x (neg.f64 1)) 918938533204673/1000000000000000)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 y) 1/2)) (*.f64 y x)) (+.f64 (*.f64 x (neg.f64 1)) 918938533204673/1000000000000000)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (neg.f64 y) 1/2) (Rewrite<= *-commutative_binary64 (*.f64 x y))) (+.f64 (*.f64 x (neg.f64 1)) 918938533204673/1000000000000000)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (*.f64 (neg.f64 y) 1/2) (*.f64 x y)) (*.f64 x (neg.f64 1))) 918938533204673/1000000000000000)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (neg.f64 y) 1/2) (+.f64 (*.f64 x y) (*.f64 x (neg.f64 1))))) 918938533204673/1000000000000000): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (neg.f64 y) 1/2) (Rewrite<= distribute-lft-in_binary64 (*.f64 x (+.f64 y (neg.f64 1))))) 918938533204673/1000000000000000): 4 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (neg.f64 y) 1/2) (*.f64 x (Rewrite<= sub-neg_binary64 (-.f64 y 1)))) 918938533204673/1000000000000000): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x (-.f64 y 1)) (*.f64 (neg.f64 y) 1/2))) 918938533204673/1000000000000000): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 x (-.f64 y 1)) (*.f64 y 1/2))) 918938533204673/1000000000000000): 0 points increase in error, 0 points decrease in error