Initial program 0.1
\[\left(\left(x \cdot \log y - y\right) - z\right) + \log t
\]
Simplified0.1
\[\leadsto \color{blue}{\left(\mathsf{fma}\left(x, \log y, \log t\right) - y\right) - z}
\]
Proof
(-.f64 (-.f64 (fma.f64 x (log.f64 y) (log.f64 t)) y) z): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (log.f64 y)) (log.f64 t))) y) z): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (log.f64 t) (*.f64 x (log.f64 y)))) y) z): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-+r-_binary64 (+.f64 (log.f64 t) (-.f64 (*.f64 x (log.f64 y)) y))) z): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (+.f64 (log.f64 t) (-.f64 (*.f64 x (log.f64 y)) y)) 0)) z): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r-_binary64 (+.f64 (+.f64 (log.f64 t) (-.f64 (*.f64 x (log.f64 y)) y)) (-.f64 0 z))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (log.f64 t) (-.f64 (*.f64 x (log.f64 y)) y)) (Rewrite<= neg-sub0_binary64 (neg.f64 z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (log.f64 t) (+.f64 (-.f64 (*.f64 x (log.f64 y)) y) (neg.f64 z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (log.f64 t) (Rewrite<= sub-neg_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))): 3 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto \left(\mathsf{fma}\left(x, \log y, \log t\right) - y\right) - z
\]