Simplified26.5
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(t, a \cdot -4, \frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z}\right)}{c}}
\]
Proof
(/.f64 (fma.f64 t (*.f64 a -4) (/.f64 (fma.f64 x (*.f64 9 y) b) z)) c): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 t (*.f64 a (Rewrite<= metadata-eval (neg.f64 4))) (/.f64 (fma.f64 x (*.f64 9 y) b) z)) c): 0 points increase in error, 1 points decrease in error
(/.f64 (fma.f64 t (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) (/.f64 (fma.f64 x (*.f64 9 y) b) z)) c): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 t (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 a) 4)) (/.f64 (fma.f64 x (*.f64 9 y) b) z)) c): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 t (Rewrite<= *-commutative_binary64 (*.f64 4 (neg.f64 a))) (/.f64 (fma.f64 x (*.f64 9 y) b) z)) c): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 t (*.f64 4 (neg.f64 a)) (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 9 y)) b)) z)) c): 8 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 t (*.f64 4 (neg.f64 a)) (/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 9) y)) b) z)) c): 18 points increase in error, 1 points decrease in error
(/.f64 (fma.f64 t (*.f64 4 (neg.f64 a)) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 b (*.f64 (*.f64 x 9) y))) z)) c): 1 points increase in error, 21 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (*.f64 4 (neg.f64 a))) (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z))) c): 0 points increase in error, 5 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 t 4) (neg.f64 a))) (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z)) c): 26 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 t)) (neg.f64 a)) (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z)) c): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (*.f64 (*.f64 4 t) (neg.f64 a)))) c): 0 points increase in error, 26 points decrease in error
(/.f64 (+.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (Rewrite=> *-commutative_binary64 (*.f64 (neg.f64 a) (*.f64 4 t)))) c): 5 points increase in error, 21 points decrease in error
(/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (*.f64 a (*.f64 4 t)))) c): 21 points increase in error, 5 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 4 t) a))) c): 1 points increase in error, 25 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (Rewrite<= associate-*r*_binary64 (*.f64 4 (*.f64 t a)))) c): 0 points increase in error, 21 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (Rewrite<= /-rgt-identity_binary64 (/.f64 (*.f64 4 (*.f64 t a)) 1))) c): 21 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (/.f64 (*.f64 4 (*.f64 t a)) (Rewrite<= *-inverses_binary64 (/.f64 z z)))) c): 25 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 4 (*.f64 t a)) z) z))) c): 1 points increase in error, 25 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 z (*.f64 4 (*.f64 t a)))) z)) c): 25 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z 4) (*.f64 t a))) z)) c): 1 points increase in error, 21 points decrease in error
(/.f64 (-.f64 (/.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) z) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 z 4) t) a)) z)) c): 21 points increase in error, 5 points decrease in error
(/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (+.f64 b (*.f64 (*.f64 x 9) y)) (*.f64 (*.f64 (*.f64 z 4) t) a)) z)) c): 26 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= associate-+r-_binary64 (+.f64 b (-.f64 (*.f64 (*.f64 x 9) y) (*.f64 (*.f64 (*.f64 z 4) t) a)))) z) c): 0 points increase in error, 1 points decrease in error
(/.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (-.f64 (*.f64 (*.f64 x 9) y) (*.f64 (*.f64 (*.f64 z 4) t) a)) b)) z) c): 0 points increase in error, 25 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (+.f64 (-.f64 (*.f64 (*.f64 x 9) y) (*.f64 (*.f64 (*.f64 z 4) t) a)) b) (*.f64 z c))): 21 points increase in error, 0 points decrease in error