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 3 -4))) 3): 0 points increase in error, 0 points decrease in error
(fma.f64 x (fma.f64 x (*.f64 3 3) (*.f64 3 (Rewrite<= metadata-eval (neg.f64 4)))) 3): 7 points increase in error, 0 points decrease in error
(fma.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (*.f64 3 3)) (*.f64 3 (neg.f64 4)))) 3): 11 points increase in error, 1 points decrease in error
(fma.f64 x (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 3) 3)) (*.f64 3 (neg.f64 4))) 3): 0 points increase in error, 10 points decrease in error
(fma.f64 x (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 3 (*.f64 x 3))) (*.f64 3 (neg.f64 4))) 3): 0 points increase in error, 1 points decrease in error
(fma.f64 x (Rewrite<= distribute-lft-in_binary64 (*.f64 3 (+.f64 (*.f64 x 3) (neg.f64 4)))) 3): 0 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, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 x (*.f64 x 3)) (*.f64 x 4))) 3) 3): 0 points increase in error, 6 points decrease in error
(+.f64 (*.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 x 3) x)) (*.f64 x 4)) 3) 3): 0 points increase in error, 5 points decrease in error
(+.f64 (*.f64 (-.f64 (*.f64 (*.f64 x 3) x) (*.f64 x 4)) 3) (Rewrite<= metadata-eval (*.f64 1 3))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-in_binary64 (*.f64 3 (+.f64 (-.f64 (*.f64 (*.f64 x 3) x) (*.f64 x 4)) 1))): 6 points increase in error, 0 points decrease in error