Simplified0.6
\[\leadsto \color{blue}{\mathsf{fma}\left(wj, wj \cdot \mathsf{fma}\left(x, 2.5, 1\right), \mathsf{fma}\left(x \cdot -2.6666666666666665 + -1, {wj}^{3}, \mathsf{fma}\left(wj, x \cdot -2, x\right)\right)\right)}
\]
Proof
(fma.f64 wj (*.f64 wj (fma.f64 x 5/2 1)) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (fma.f64 x (Rewrite<= metadata-eval (neg.f64 -5/2)) 1)) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (fma.f64 x (neg.f64 (Rewrite<= metadata-eval (+.f64 -1/2 -2))) 1)) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (neg.f64 (+.f64 -1/2 -2))) 1))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x (+.f64 -1/2 -2)))) 1)) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 (neg.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1/2 x) (*.f64 -2 x)))) 1)) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 (+.f64 (*.f64 -1/2 x) (*.f64 -2 x)))))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (neg.f64 (Rewrite=> distribute-rgt-out_binary64 (*.f64 x (+.f64 -1/2 -2)))))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 x (neg.f64 (+.f64 -1/2 -2)))))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (*.f64 x (neg.f64 (Rewrite=> metadata-eval -5/2))))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (*.f64 x (Rewrite=> metadata-eval 5/2)))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (*.f64 x (Rewrite<= metadata-eval (-.f64 3/2 -1))))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (*.f64 x (-.f64 (Rewrite<= metadata-eval (/.f64 3 2)) -1)))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (/.f64 3 2) x) (*.f64 -1 x))))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (-.f64 (*.f64 (Rewrite=> metadata-eval 3/2) x) (*.f64 -1 x)))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (-.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 1/2 1)) x) (*.f64 -1 x)))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (+.f64 1 (-.f64 (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x)))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x)))) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (*.f64 x (Rewrite<= metadata-eval (-.f64 -7/6 3/2))) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 3 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (*.f64 x (-.f64 (Rewrite<= metadata-eval (+.f64 -1 -1/6)) 3/2)) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (*.f64 x (-.f64 (+.f64 -1 -1/6) (Rewrite<= metadata-eval (/.f64 3 2)))) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (+.f64 -1 -1/6) x) (*.f64 (/.f64 3 2) x))) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 2 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 x (+.f64 -1 -1/6))) (*.f64 (/.f64 3 2) x)) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (-.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x))) (*.f64 (/.f64 3 2) x)) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 1 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (*.f64 (Rewrite=> metadata-eval 3/2) x)) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (*.f64 (Rewrite<= metadata-eval (+.f64 1/2 1)) x)) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 1/2 x) x))) -1) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (+.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 (*.f64 1/2 x) x)) (Rewrite<= metadata-eval (neg.f64 1))) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (Rewrite<= sub-neg_binary64 (-.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 (*.f64 1/2 x) x)) 1)) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 (+.f64 (*.f64 1/2 x) x) 1))) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (Rewrite<= +-commutative_binary64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)))) (pow.f64 wj 3) (fma.f64 wj (*.f64 x -2) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3) (fma.f64 wj (*.f64 x (Rewrite<= metadata-eval (-.f64 -1 1))) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3) (fma.f64 wj (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 x) (*.f64 1 x))) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3) (fma.f64 wj (-.f64 (*.f64 -1 x) (Rewrite=> *-lft-identity_binary64 x)) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 wj (-.f64 (*.f64 -1 x) x)) x)))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (fma.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 -1 x) x) wj)) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)) (+.f64 (*.f64 (-.f64 (*.f64 -1 x) x) wj) x)))): 2 points increase in error, 1 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 wj (*.f64 wj (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x)))) (+.f64 (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)) (+.f64 (*.f64 (-.f64 (*.f64 -1 x) x) wj) x)))): 2 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 wj wj) (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x)))) (+.f64 (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)) (+.f64 (*.f64 (-.f64 (*.f64 -1 x) x) wj) x))): 0 points increase in error, 1 points decrease in error
(+.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 wj 2)) (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x))) (+.f64 (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)) (+.f64 (*.f64 (-.f64 (*.f64 -1 x) x) wj) x))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x)) (pow.f64 wj 2))) (+.f64 (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)) (+.f64 (*.f64 (-.f64 (*.f64 -1 x) x) wj) x))): 0 points increase in error, 0 points decrease in error