Initial program 0.1
\[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z
\]
Simplified0.1
\[\leadsto \color{blue}{x + \mathsf{fma}\left(\log y, -0.5 - y, y - z\right)}
\]
Proof
(+.f64 x (fma.f64 (log.f64 y) (-.f64 -1/2 y) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (log.f64 y) (-.f64 (Rewrite<= metadata-eval (-.f64 0 1/2)) y) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (log.f64 y) (Rewrite<= associate--r+_binary64 (-.f64 0 (+.f64 1/2 y))) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (log.f64 y) (-.f64 0 (Rewrite<= +-commutative_binary64 (+.f64 y 1/2))) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 (log.f64 y) (Rewrite<= neg-sub0_binary64 (neg.f64 (+.f64 y 1/2))) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (log.f64 y) (neg.f64 (+.f64 y 1/2))) (-.f64 y z)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (+.f64 y 1/2)) (log.f64 y))) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x (*.f64 (neg.f64 (+.f64 y 1/2)) (log.f64 y))) (-.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 x (*.f64 (+.f64 y 1/2) (log.f64 y)))) (-.f64 y z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (-.f64 x (*.f64 (+.f64 y 1/2) (log.f64 y))) y) z)): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto x + \mathsf{fma}\left(\log y, -0.5 - y, y - z\right)
\]