Jmat.Real.lambertw, newton loop step

Average Error: 13.2 → 1.6

Time: 17.0s

Precision: binary64

Cost: 33152

Math

\[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}} \]

↓

\[\mathsf{fma}\left(wj, wj \cdot \mathsf{fma}\left(x, 2.5, 1\right), \mathsf{fma}\left(wj, x \cdot -2, \mathsf{fma}\left(x \cdot -2.6666666666666665 + -1, {wj}^{3}, x\right)\right)\right) \]

FPCore

(FPCore (wj x)
 :precision binary64
 (- wj (/ (- (* wj (exp wj)) x) (+ (exp wj) (* wj (exp wj))))))

↓

(FPCore (wj x)
 :precision binary64
 (fma
  wj
  (* wj (fma x 2.5 1.0))
  (fma wj (* x -2.0) (fma (+ (* x -2.6666666666666665) -1.0) (pow wj 3.0) x))))

C

double code(double wj, double x) {
	return wj - (((wj * exp(wj)) - x) / (exp(wj) + (wj * exp(wj))));
}

↓

double code(double wj, double x) {
	return fma(wj, (wj * fma(x, 2.5, 1.0)), fma(wj, (x * -2.0), fma(((x * -2.6666666666666665) + -1.0), pow(wj, 3.0), x)));
}

Julia

function code(wj, x)
	return Float64(wj - Float64(Float64(Float64(wj * exp(wj)) - x) / Float64(exp(wj) + Float64(wj * exp(wj)))))
end

↓

function code(wj, x)
	return fma(wj, Float64(wj * fma(x, 2.5, 1.0)), fma(wj, Float64(x * -2.0), fma(Float64(Float64(x * -2.6666666666666665) + -1.0), (wj ^ 3.0), x)))
end

Wolfram

code[wj_, x_] := N[(wj - N[(N[(N[(wj * N[Exp[wj], $MachinePrecision]), $MachinePrecision] - x), $MachinePrecision] / N[(N[Exp[wj], $MachinePrecision] + N[(wj * N[Exp[wj], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[wj_, x_] := N[(wj * N[(wj * N[(x * 2.5 + 1.0), $MachinePrecision]), $MachinePrecision] + N[(wj * N[(x * -2.0), $MachinePrecision] + N[(N[(N[(x * -2.6666666666666665), $MachinePrecision] + -1.0), $MachinePrecision] * N[Power[wj, 3.0], $MachinePrecision] + x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Target

Original	13.2
Target	12.7
Herbie	1.6

\[wj - \left(\frac{wj}{wj + 1} - \frac{x}{e^{wj} + wj \cdot e^{wj}}\right) \]

Derivation

1. Initial program 13.2

   \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}} \]

2. Simplified 12.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)))): 1 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)))): 4 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, 0 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)))))): 1 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))))))): 1 points increase in error, 1 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

3. Applied egg-rr 12.7

   \[\leadsto wj - \frac{wj - \color{blue}{e^{-wj} \cdot x}}{wj + 1} \]

4. Taylor expanded in wj around 0 1.6

   \[\leadsto \color{blue}{\left(\left(1 + \left(0.5 \cdot x + x\right)\right) - -1 \cdot x\right) \cdot {wj}^{2} + \left(\left(\left(-1 \cdot x + -0.16666666666666666 \cdot x\right) - \left(1 + \left(0.5 \cdot x + x\right)\right)\right) \cdot {wj}^{3} + \left(\left(-1 \cdot x - x\right) \cdot wj + x\right)\right)} \]

5. Simplified 1.6

   \[\leadsto \color{blue}{\mathsf{fma}\left(wj, wj \cdot \mathsf{fma}\left(x, 2.5, 1\right), \mathsf{fma}\left(wj, x \cdot -2, \mathsf{fma}\left(x \cdot -2.6666666666666665 + -1, {wj}^{3}, x\right)\right)\right)} \]
   Proof
   (fma.f64 wj (*.f64 wj (fma.f64 x 5/2 1)) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) x))): 0 points increase in error, 0 points decrease in error
   (fma.f64 wj (*.f64 wj (+.f64 1 (+.f64 (*.f64 (/.f64 3 2) x) (Rewrite=> *-lft-identity_binary64 x)))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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) x))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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) x))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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)) x))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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)) x))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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)) (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 (Rewrite<= metadata-eval (neg.f64 -1)) x))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) x))): 0 points increase in error, 0 points decrease in error
   (fma.f64 wj (*.f64 wj (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (+.f64 1 (+.f64 (*.f64 1/2 x) x)) (*.f64 -1 x)))) (fma.f64 wj (*.f64 x -2) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (Rewrite<= *-commutative_binary64 (*.f64 -2 x)) (fma.f64 (+.f64 (*.f64 x -8/3) -1) (pow.f64 wj 3) 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 wj (*.f64 -2 x) (fma.f64 (+.f64 (*.f64 x (Rewrite<= metadata-eval (-.f64 -7/6 3/2))) -1) (pow.f64 wj 3) x))): 2 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 wj (*.f64 -2 x) (fma.f64 (+.f64 (*.f64 x (-.f64 (Rewrite<= metadata-eval (+.f64 -1 -1/6)) 3/2)) -1) (pow.f64 wj 3) 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 wj (*.f64 -2 x) (fma.f64 (+.f64 (*.f64 x (-.f64 (+.f64 -1 -1/6) (Rewrite<= metadata-eval (/.f64 3 2)))) -1) (pow.f64 wj 3) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 x) (fma.f64 (+.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 x (+.f64 -1 -1/6))) (*.f64 (/.f64 3 2) x)) -1) (pow.f64 wj 3) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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) 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 wj (*.f64 -2 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)) 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 wj (*.f64 -2 x) (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)))))): 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 wj (*.f64 -2 x)) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3)))))): 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))) (+.f64 (*.f64 wj (Rewrite=> *-commutative_binary64 (*.f64 x -2))) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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))) (+.f64 (*.f64 wj (*.f64 x (Rewrite<= metadata-eval (+.f64 -1 -1)))) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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))) (+.f64 (*.f64 wj (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 -1 x) (*.f64 -1 x)))) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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))) (+.f64 (*.f64 wj (+.f64 (*.f64 -1 x) (Rewrite=> mul-1-neg_binary64 (neg.f64 x)))) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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))) (+.f64 (*.f64 wj (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 -1 x) x))) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 -1 x) x) wj)) (+.f64 x (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 (-.f64 (*.f64 -1 x) x) wj) x) (*.f64 (-.f64 (+.f64 (*.f64 -1 x) (*.f64 -1/6 x)) (+.f64 1 (+.f64 (*.f64 1/2 x) x))) (pow.f64 wj 3))))): 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<= +-commutative_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)))): 0 points increase in error, 0 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, 0 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

6. Final simplification 1.6

   \[\leadsto \mathsf{fma}\left(wj, wj \cdot \mathsf{fma}\left(x, 2.5, 1\right), \mathsf{fma}\left(wj, x \cdot -2, \mathsf{fma}\left(x \cdot -2.6666666666666665 + -1, {wj}^{3}, x\right)\right)\right) \]

Alternatives

Alternative 1
Error	1.6
Cost	15552

\[{wj}^{3} \cdot \left(x \cdot -0.6666666666666666 - \left(x \cdot -3 + \left(1 + -2 \cdot \left(x \cdot -4 + x \cdot 1.5\right)\right)\right)\right) + \left(\left(1 + \left(x \cdot 4 - x \cdot 1.5\right)\right) \cdot {wj}^{2} + \left(x + -2 \cdot \left(wj \cdot x\right)\right)\right) \]

Alternative 2
Error	1.7
Cost	7424

\[\left(wj \cdot wj - {wj}^{3}\right) + \frac{x - wj \cdot x}{wj + 1} \]

Alternative 3
Error	2.0
Cost	704

\[\left(x + -2 \cdot \left(wj \cdot x\right)\right) + wj \cdot wj \]

Alternative 4
Error	9.7
Cost	580

\[\begin{array}{l} \mathbf{if}\;wj \leq 2.7226500308852283 \cdot 10^{-47}:\\ \;\;\;\;x + -2 \cdot \left(wj \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;wj \cdot \left(wj \cdot \left(1 - wj\right)\right)\\ \end{array} \]

Alternative 5
Error	8.9
Cost	448

\[x + -2 \cdot \left(wj \cdot x\right) \]

Alternative 6
Error	9.2
Cost	64

\[x \]

Reproduce

herbie shell --seed 2022317 
(FPCore (wj x)
  :name "Jmat.Real.lambertw, newton loop step"
  :precision binary64

  :herbie-target
  (- wj (- (/ wj (+ wj 1.0)) (/ x (+ (exp wj) (* wj (exp wj))))))

  (- wj (/ (- (* wj (exp wj)) x) (+ (exp wj) (* wj (exp wj))))))