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