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