Simplified0.2
\[\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))): 16 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, 16 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)))))): 10 points increase in error, 0 points decrease in error
(+.f64 (log.f64 (+.f64 x y)) (Rewrite=> associate--r+_binary64 (-.f64 (-.f64 (log.f64 z) t) (*.f64 (neg.f64 (-.f64 a 1/2)) (log.f64 t))))): 6 points increase in error, 0 points decrease in error
(+.f64 (log.f64 (+.f64 x y)) (Rewrite=> cancel-sign-sub_binary64 (+.f64 (-.f64 (log.f64 z) t) (*.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 (Rewrite=> sub-neg_binary64 (+.f64 (log.f64 z) (neg.f64 t))) (*.f64 (-.f64 a 1/2) (log.f64 t)))): 0 points increase in error, 16 points decrease in error
(+.f64 (log.f64 (+.f64 x y)) (Rewrite=> associate-+l+_binary64 (+.f64 (log.f64 z) (+.f64 (neg.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 (neg.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 (+.f64 (log.f64 (+.f64 x y)) (log.f64 z)) (neg.f64 t)) (*.f64 (-.f64 a 1/2) (log.f64 t)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= sub-neg_binary64 (-.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