Simplified0.1
\[\leadsto \color{blue}{\mathsf{fma}\left(x, \mathsf{fma}\left(x, 9, -12\right), 3\right)}
\]
Proof
(fma.f64 x (fma.f64 x 9 -12) 3): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 x (Rewrite<= metadata-eval (*.f64 3 3)) -12) 3): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 x (*.f64 3 3) (Rewrite<= metadata-eval (*.f64 -4 3))) 3): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 x (*.f64 3 3) (*.f64 (Rewrite<= metadata-eval (neg.f64 4)) 3)) 3): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 3 3)) (*.f64 (neg.f64 4) 3))) 3): 2 points increase in error, 3 points decrease in error
(fma.f64 x (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 3) 3)) (*.f64 (neg.f64 4) 3)) 3): 15 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= distribute-rgt-in_binary64 (*.f64 3 (+.f64 (*.f64 x 3) (neg.f64 4)))) 3): 1 points increase in error, 0 points decrease in error
(fma.f64 x (*.f64 3 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 x 3) 4))) 3): 0 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 x 3) 4) 3)) 3): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 (-.f64 (*.f64 x 3) 4) 3)) 3)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x (-.f64 (*.f64 x 3) 4)) 3)) 3): 11 points increase in error, 14 points decrease in error
(+.f64 (*.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 x 3) x) (*.f64 4 x))) 3) 3): 0 points increase in error, 1 points decrease in error
(+.f64 (*.f64 (-.f64 (*.f64 (*.f64 x 3) x) (Rewrite<= *-commutative_binary64 (*.f64 x 4))) 3) 3): 0 points increase in error, 0 points decrease in error
(Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (-.f64 (*.f64 (*.f64 x 3) x) (*.f64 x 4)) 1) 3)): 4 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 3 (+.f64 (-.f64 (*.f64 (*.f64 x 3) x) (*.f64 x 4)) 1))): 0 points increase in error, 0 points decrease in error