Simplified14.1
\[\leadsto x \cdot \left(z \cdot \left(y \cdot \color{blue}{\mathsf{fma}\left(0.5, \left(\frac{z}{a} \cdot \frac{z}{t}\right) \cdot \left({a}^{-0.5} \cdot {\left(\frac{-1}{t}\right)}^{0.5}\right), {a}^{-0.5} \cdot {\left(\frac{-1}{t}\right)}^{0.5}\right)}\right)\right)
\]
Proof
(fma.f64 1/2 (*.f64 (*.f64 (/.f64 z a) (/.f64 z t)) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 z z) (*.f64 a t))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 25 points increase in error, 6 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) (*.f64 a t)) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 a) -1/2))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 11 points increase in error, 9 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1/2 (log.f64 a)))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (neg.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 (/.f64 1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite=> mul-1-neg_binary64 (neg.f64 (log.f64 (/.f64 1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (neg.f64 (Rewrite=> log-rec_binary64 (neg.f64 (log.f64 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite=> remove-double-neg_binary64 (log.f64 a)))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (log.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (log.f64 (neg.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (Rewrite=> *-commutative_binary64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2))) (pow.f64 (/.f64 -1 t) 1/2))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 (/.f64 -1 t)) 1/2))))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 10 points increase in error, 10 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (exp.f64 (*.f64 (log.f64 (/.f64 -1 t)) (Rewrite<= metadata-eval (*.f64 -1 -1/2)))))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (exp.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (log.f64 (/.f64 -1 t)) -1) -1/2))))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (exp.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (log.f64 (/.f64 -1 t)))) -1/2)))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (Rewrite<= exp-sum_binary64 (exp.f64 (+.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2) (*.f64 (*.f64 -1 (log.f64 (/.f64 -1 t))) -1/2))))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 5 points increase in error, 7 points decrease in error
(fma.f64 1/2 (*.f64 (/.f64 (pow.f64 z 2) (*.f64 a t)) (exp.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t)))))))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 z 2) (/.f64 (*.f64 a t) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 13 points increase in error, 2 points decrease in error
(fma.f64 1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t))) (*.f64 (pow.f64 a -1/2) (pow.f64 (/.f64 -1 t) 1/2))): 5 points increase in error, 15 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 a) -1/2))) (pow.f64 (/.f64 -1 t) 1/2))): 37 points increase in error, 46 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1/2 (log.f64 a)))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (neg.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 (/.f64 1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite=> mul-1-neg_binary64 (neg.f64 (log.f64 (/.f64 1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (neg.f64 (Rewrite=> log-rec_binary64 (neg.f64 (log.f64 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (Rewrite=> remove-double-neg_binary64 (log.f64 a)))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (log.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 -1/2 (log.f64 (neg.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 a)))))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (Rewrite=> *-commutative_binary64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2))) (pow.f64 (/.f64 -1 t) 1/2))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 (/.f64 -1 t)) 1/2))))): 35 points increase in error, 51 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (exp.f64 (*.f64 (log.f64 (/.f64 -1 t)) (Rewrite<= metadata-eval (*.f64 -1 -1/2)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (exp.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (log.f64 (/.f64 -1 t)) -1) -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (*.f64 (exp.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2)) (exp.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (log.f64 (/.f64 -1 t)))) -1/2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (Rewrite<= exp-sum_binary64 (exp.f64 (+.f64 (*.f64 (log.f64 (neg.f64 (*.f64 -1 a))) -1/2) (*.f64 (*.f64 -1 (log.f64 (/.f64 -1 t))) -1/2))))): 39 points increase in error, 27 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t)) (exp.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t)))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 z 2) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t))))))) (*.f64 a t))) (exp.f64 (*.f64 -1/2 (+.f64 (log.f64 (neg.f64 (*.f64 -1 a))) (*.f64 -1 (log.f64 (/.f64 -1 t)))))))): 0 points increase in error, 0 points decrease in error