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