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