Simplified0.3
\[\leadsto x \cdot x - \color{blue}{z \cdot \left(y \cdot \left(4 \cdot z\right)\right)}
\]
Proof
(*.f64 z (*.f64 y (*.f64 4 z))): 0 points increase in error, 0 points decrease in error
(*.f64 z (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y 4) z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (*.f64 y 4) z) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 y 4) (*.f64 z z))): 71 points increase in error, 30 points decrease in error
(*.f64 (Rewrite=> *-commutative_binary64 (*.f64 4 y)) (*.f64 z z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 4 (*.f64 y (*.f64 z z)))): 0 points increase in error, 0 points decrease in error
(*.f64 4 (*.f64 y (Rewrite<= unpow2_binary64 (pow.f64 z 2)))): 0 points increase in error, 0 points decrease in error
Simplified0.3
\[\leadsto \color{blue}{\mathsf{fma}\left(x, x, \left(y \cdot z\right) \cdot \left(-4 \cdot z\right)\right)}
\]
Proof
(fma.f64 x x (*.f64 (*.f64 y z) (*.f64 -4 z))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 z y)) (*.f64 -4 z))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (*.f64 (*.f64 z y) (*.f64 (Rewrite<= metadata-eval (neg.f64 4)) z))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (*.f64 (*.f64 z y) (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 4 z))))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 z y) (*.f64 4 z))))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 z y) 4) z)))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (neg.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 z y))) z))): 0 points increase in error, 0 points decrease in error
(fma.f64 x x (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 z (*.f64 4 (*.f64 z y)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 x x) (neg.f64 (*.f64 z (*.f64 4 (*.f64 z y)))))): 3 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 z (*.f64 4 (*.f64 z y)))) (*.f64 x x))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 4 (*.f64 z y)) z))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite=> associate-*l*_binary64 (*.f64 4 (*.f64 (*.f64 z y) z)))) (*.f64 x x)): 1 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 4 (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 y z)) z))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 4 (Rewrite<= associate-*r*_binary64 (*.f64 y (*.f64 z z))))) (*.f64 x x)): 50 points increase in error, 23 points decrease in error
(+.f64 (neg.f64 (*.f64 4 (*.f64 y (Rewrite<= unpow2_binary64 (pow.f64 z 2))))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 4 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 y (pow.f64 z 2)) 1)))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 4 (Rewrite<= *-commutative_binary64 (*.f64 1 (*.f64 y (pow.f64 z 2)))))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (*.f64 4 (*.f64 (Rewrite<= pow-base-1_binary64 (pow.f64 1 1/3)) (*.f64 y (pow.f64 z 2))))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 4) (*.f64 (pow.f64 1 1/3) (*.f64 y (pow.f64 z 2))))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite=> metadata-eval -4) (*.f64 (pow.f64 1 1/3) (*.f64 y (pow.f64 z 2)))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -4 (*.f64 (pow.f64 1 1/3) (*.f64 y (pow.f64 z 2)))) (Rewrite<= unpow2_binary64 (pow.f64 x 2))): 0 points increase in error, 0 points decrease in error