Simplified18.7
\[\leadsto \color{blue}{wj - \frac{wj - \frac{x}{e^{wj}}}{wj + 1}}
\]
Proof
(-.f64 wj (/.f64 (-.f64 wj (/.f64 x (exp.f64 wj))) (+.f64 wj 1))): 0 points increase in error, 0 points decrease in error
(-.f64 wj (Rewrite=> div-sub_binary64 (-.f64 (/.f64 wj (+.f64 wj 1)) (/.f64 (/.f64 x (exp.f64 wj)) (+.f64 wj 1))))): 0 points increase in error, 0 points decrease in error
(-.f64 wj (-.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 wj (+.f64 wj 1)) 1)) (/.f64 (/.f64 x (exp.f64 wj)) (+.f64 wj 1)))): 0 points increase in error, 0 points decrease in error
(-.f64 wj (-.f64 (*.f64 (/.f64 wj (+.f64 wj 1)) (Rewrite<= *-inverses_binary64 (/.f64 (exp.f64 wj) (exp.f64 wj)))) (/.f64 (/.f64 x (exp.f64 wj)) (+.f64 wj 1)))): 3 points increase in error, 0 points decrease in error
(-.f64 wj (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 wj (exp.f64 wj)) (*.f64 (+.f64 wj 1) (exp.f64 wj)))) (/.f64 (/.f64 x (exp.f64 wj)) (+.f64 wj 1)))): 3 points increase in error, 1 points decrease in error
(-.f64 wj (-.f64 (/.f64 (*.f64 wj (exp.f64 wj)) (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (exp.f64 wj) (*.f64 wj (exp.f64 wj))))) (/.f64 (/.f64 x (exp.f64 wj)) (+.f64 wj 1)))): 0 points increase in error, 1 points decrease in error
(-.f64 wj (-.f64 (/.f64 (*.f64 wj (exp.f64 wj)) (+.f64 (exp.f64 wj) (*.f64 wj (exp.f64 wj)))) (Rewrite=> associate-/l/_binary64 (/.f64 x (*.f64 (+.f64 wj 1) (exp.f64 wj)))))): 0 points increase in error, 1 points decrease in error
(-.f64 wj (-.f64 (/.f64 (*.f64 wj (exp.f64 wj)) (+.f64 (exp.f64 wj) (*.f64 wj (exp.f64 wj)))) (/.f64 x (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (exp.f64 wj) (*.f64 wj (exp.f64 wj))))))): 0 points increase in error, 0 points decrease in error
(-.f64 wj (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 wj (exp.f64 wj)) x) (+.f64 (exp.f64 wj) (*.f64 wj (exp.f64 wj)))))): 0 points increase in error, 0 points decrease in error
Simplified0.5
\[\leadsto \color{blue}{\mathsf{fma}\left(wj, wj + x \cdot \mathsf{fma}\left(wj, 2, -2\right), x\right)}
\]
Proof
(fma.f64 wj (+.f64 wj (*.f64 x (fma.f64 wj 2 -2))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 wj (*.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 wj 2) -2)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 wj (*.f64 x (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 wj)) -2))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 wj (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 -2 (*.f64 2 wj))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 wj (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -2 x) (*.f64 (*.f64 2 wj) x)))) x): 1 points increase in error, 0 points decrease in error
(fma.f64 wj (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 -2 x) (*.f64 (*.f64 2 wj) x)) wj)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -2 x) (+.f64 (*.f64 (*.f64 2 wj) x) wj))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (+.f64 (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 wj 2)) x) wj)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (+.f64 (Rewrite=> associate-*l*_binary64 (*.f64 wj (*.f64 2 x))) wj)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (+.f64 (*.f64 wj (*.f64 2 x)) (Rewrite<= *-rgt-identity_binary64 (*.f64 wj 1)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (Rewrite<= distribute-lft-in_binary64 (*.f64 wj (+.f64 (*.f64 2 x) 1)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (+.f64 (Rewrite<= count-2_binary64 (+.f64 x x)) 1))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (Rewrite=> associate-+l+_binary64 (+.f64 x (+.f64 x 1))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 1 x))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 1 x) x)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (+.f64 (+.f64 1 x) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 x)))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (+.f64 (+.f64 1 x) (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x)))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (+.f64 (*.f64 -2 x) (*.f64 wj (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 1 x) (*.f64 -1 x))))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 wj (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 wj (-.f64 (+.f64 1 x) (*.f64 -1 x))) (*.f64 -2 x))) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 wj (+.f64 (*.f64 wj (-.f64 (+.f64 1 x) (*.f64 -1 x))) (*.f64 -2 x))) x)): 1 points increase in error, 2 points decrease in error
(+.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 wj (*.f64 wj (-.f64 (+.f64 1 x) (*.f64 -1 x)))) (*.f64 wj (*.f64 -2 x)))) x): 2 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 wj wj) (-.f64 (+.f64 1 x) (*.f64 -1 x)))) (*.f64 wj (*.f64 -2 x))) x): 0 points increase in error, 1 points decrease in error
(+.f64 (+.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 wj 2)) (-.f64 (+.f64 1 x) (*.f64 -1 x))) (*.f64 wj (*.f64 -2 x))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (pow.f64 wj 2) (-.f64 (+.f64 1 x) (*.f64 -1 x))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 wj -2) x))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (pow.f64 wj 2) (-.f64 (+.f64 1 x) (*.f64 -1 x))) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -2 wj)) x)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (pow.f64 wj 2) (-.f64 (+.f64 1 x) (*.f64 -1 x))) (Rewrite<= associate-*r*_binary64 (*.f64 -2 (*.f64 wj x)))) x): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-+l+_binary64 (+.f64 (*.f64 (pow.f64 wj 2) (-.f64 (+.f64 1 x) (*.f64 -1 x))) (+.f64 (*.f64 -2 (*.f64 wj x)) x))): 3 points increase in error, 2 points decrease in error
(+.f64 (*.f64 (pow.f64 wj 2) (Rewrite=> associate--l+_binary64 (+.f64 1 (-.f64 x (*.f64 -1 x))))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (*.f64 (-.f64 x (*.f64 -1 x)) (pow.f64 wj 2)))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (*.f64 (-.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)) (*.f64 -1 x)) (pow.f64 wj 2))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (*.f64 (Rewrite=> distribute-rgt-out--_binary64 (*.f64 x (-.f64 1 -1))) (pow.f64 wj 2))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (*.f64 (*.f64 x (Rewrite=> metadata-eval 2)) (pow.f64 wj 2))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 x)) (pow.f64 wj 2))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 x (pow.f64 wj 2))))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1 (pow.f64 wj 2)) (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 wj 2) x)))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (Rewrite=> *-lft-identity_binary64 (pow.f64 wj 2)) (*.f64 2 (*.f64 (pow.f64 wj 2) x))) (+.f64 (*.f64 -2 (*.f64 wj x)) x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (pow.f64 wj 2) (+.f64 (*.f64 2 (*.f64 (pow.f64 wj 2) x)) (+.f64 (*.f64 -2 (*.f64 wj x)) x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 wj 2) (+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 2 (pow.f64 wj 2)) x)) (+.f64 (*.f64 -2 (*.f64 wj x)) x))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 wj 2) (+.f64 (*.f64 (*.f64 2 (pow.f64 wj 2)) x) (+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 -2 wj) x)) x))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 wj 2) (+.f64 (*.f64 (*.f64 2 (pow.f64 wj 2)) x) (Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (*.f64 -2 wj) 1) x)))): 1 points increase in error, 1 points decrease in error
(+.f64 (pow.f64 wj 2) (Rewrite<= distribute-rgt-in_binary64 (*.f64 x (+.f64 (*.f64 2 (pow.f64 wj 2)) (+.f64 (*.f64 -2 wj) 1))))): 0 points increase in error, 2 points decrease in error
(+.f64 (pow.f64 wj 2) (*.f64 x (+.f64 (*.f64 2 (pow.f64 wj 2)) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 -2 wj)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 wj 2) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 2 (pow.f64 wj 2)) (+.f64 1 (*.f64 -2 wj))) x))): 0 points increase in error, 0 points decrease in error