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