Simplified0.1
\[\leadsto \color{blue}{t + \left(\mathsf{fma}\left(b + -0.5, \log c, a\right) + \mathsf{fma}\left(x, \log y, \mathsf{fma}\left(y, i, z\right)\right)\right)}
\]
Proof
(+.f64 t (+.f64 (fma.f64 (+.f64 b -1/2) (log.f64 c) a) (fma.f64 x (log.f64 y) (fma.f64 y i z)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (fma.f64 (+.f64 b (Rewrite<= metadata-eval (neg.f64 1/2))) (log.f64 c) a) (fma.f64 x (log.f64 y) (fma.f64 y i z)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (fma.f64 (Rewrite<= sub-neg_binary64 (-.f64 b 1/2)) (log.f64 c) a) (fma.f64 x (log.f64 y) (fma.f64 y i z)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 b 1/2) (log.f64 c)) a)) (fma.f64 x (log.f64 y) (fma.f64 y i z)))): 1 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c)))) (fma.f64 x (log.f64 y) (fma.f64 y i z)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))) (fma.f64 x (log.f64 y) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y i) z))))): 1 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (log.f64 y)) (+.f64 (*.f64 y i) z))))): 2 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))) (+.f64 (*.f64 x (log.f64 y)) (Rewrite=> +-commutative_binary64 (+.f64 z (*.f64 y i)))))): 0 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 x (log.f64 y)) z) (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 t (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))) (+.f64 (*.f64 x (log.f64 y)) z)) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 x (log.f64 y)) z) (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))))) (*.f64 y i))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 t (+.f64 (+.f64 (*.f64 x (log.f64 y)) z) (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))))) (*.f64 y i))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 t (+.f64 (*.f64 x (log.f64 y)) z)) (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c))))) (*.f64 y i)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 x (log.f64 y)) z) t)) (+.f64 a (*.f64 (-.f64 b 1/2) (log.f64 c)))) (*.f64 y i)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (+.f64 (*.f64 x (log.f64 y)) z) t) a) (*.f64 (-.f64 b 1/2) (log.f64 c)))) (*.f64 y i)): 0 points increase in error, 0 points decrease in error