Simplified0.6
\[\leadsto \color{blue}{\mathsf{fma}\left(-wj, \mathsf{expm1}\left(wj - \left(wj + \mathsf{log1p}\left(wj\right)\right)\right), x \cdot e^{\left(-wj\right) - \mathsf{log1p}\left(wj\right)}\right)}
\]
Proof
(fma.f64 (neg.f64 wj) (expm1.f64 (-.f64 wj (+.f64 wj (log1p.f64 wj)))) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 wj)) (expm1.f64 (-.f64 wj (+.f64 wj (log1p.f64 wj)))) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (expm1.f64 (Rewrite<= unsub-neg_binary64 (+.f64 wj (neg.f64 (+.f64 wj (log1p.f64 wj)))))) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (expm1.f64 (+.f64 wj (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 wj) (neg.f64 (log1p.f64 wj)))))) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (expm1.f64 (+.f64 wj (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 wj)) (neg.f64 (log1p.f64 wj))))) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (expm1.f64 (+.f64 wj (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj))))) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (+.f64 wj (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1)) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 38 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (Rewrite<= prod-exp_binary64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj))))) 1) (*.f64 x (exp.f64 (-.f64 (neg.f64 wj) (log1p.f64 wj))))): 5 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (-.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 wj)) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (Rewrite<= associate--r+_binary64 (-.f64 0 (+.f64 wj (log1p.f64 wj))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (+.f64 wj (log1p.f64 wj))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (log1p.f64 wj) wj)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (neg.f64 (+.f64 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 wj))) wj))))): 2 points increase in error, 1 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (+.f64 (log.f64 (+.f64 1 wj)) wj)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (-.f64 0 (+.f64 (Rewrite=> log1p-def_binary64 (log1p.f64 wj)) wj))))): 1 points increase in error, 2 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (-.f64 0 (Rewrite=> +-commutative_binary64 (+.f64 wj (log1p.f64 wj))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (Rewrite=> associate--r+_binary64 (-.f64 (-.f64 0 wj) (log1p.f64 wj)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (-.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 wj)) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (*.f64 x (exp.f64 (-.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 wj)) (log1p.f64 wj))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1) (Rewrite<= *-commutative_binary64 (*.f64 (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj))) x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 -1 wj) (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1)) (*.f64 (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj))) x))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 wj (-.f64 (*.f64 (exp.f64 wj) (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj)))) 1)))) (*.f64 (exp.f64 (-.f64 (*.f64 -1 wj) (log1p.f64 wj))) x)): 0 points increase in error, 0 points decrease in error