Original	13.5
Target	12.9
Herbie	0.3

Derivation

Split input into 2 regimes
if wj < -8.379297298080333e-09 or 4.7290331869132735e-09 < wj
1. Initial program 15.2
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Using strategy rm
3. Applied distribute-rgt1-in15.3
  \[\leadsto wj - \frac{wj \cdot e^{wj} - x}{\color{blue}{\left(wj + 1\right) \cdot e^{wj}}}\]
4. Applied *-un-lft-identity15.3
  \[\leadsto wj - \frac{\color{blue}{1 \cdot \left(wj \cdot e^{wj} - x\right)}}{\left(wj + 1\right) \cdot e^{wj}}\]
5. Applied times-frac15.3
  \[\leadsto wj - \color{blue}{\frac{1}{wj + 1} \cdot \frac{wj \cdot e^{wj} - x}{e^{wj}}}\]
6. Simplified3.2
  \[\leadsto wj - \frac{1}{wj + 1} \cdot \color{blue}{\left(wj - \frac{x}{e^{wj}}\right)}\]
7. Using strategy rm
8. Applied flip-+3.4
  \[\leadsto wj - \frac{1}{\color{blue}{\frac{wj \cdot wj - 1 \cdot 1}{wj - 1}}} \cdot \left(wj - \frac{x}{e^{wj}}\right)\]
9. Applied associate-/r/3.3
  \[\leadsto wj - \color{blue}{\left(\frac{1}{wj \cdot wj - 1 \cdot 1} \cdot \left(wj - 1\right)\right)} \cdot \left(wj - \frac{x}{e^{wj}}\right)\]
10. Applied associate-*l*3.3
  \[\leadsto wj - \color{blue}{\frac{1}{wj \cdot wj - 1 \cdot 1} \cdot \left(\left(wj - 1\right) \cdot \left(wj - \frac{x}{e^{wj}}\right)\right)}\]
11. Simplified3.3
  \[\leadsto wj - \color{blue}{\frac{1}{(wj \cdot wj + -1)_*}} \cdot \left(\left(wj - 1\right) \cdot \left(wj - \frac{x}{e^{wj}}\right)\right)\]
12. Using strategy rm
13. Applied sub-neg3.3
  \[\leadsto wj - \frac{1}{(wj \cdot wj + -1)_*} \cdot \left(\left(wj - 1\right) \cdot \color{blue}{\left(wj + \left(-\frac{x}{e^{wj}}\right)\right)}\right)\]
14. Applied distribute-rgt-in3.3
  \[\leadsto wj - \frac{1}{(wj \cdot wj + -1)_*} \cdot \color{blue}{\left(wj \cdot \left(wj - 1\right) + \left(-\frac{x}{e^{wj}}\right) \cdot \left(wj - 1\right)\right)}\]
15. Applied distribute-rgt-in3.3
  \[\leadsto wj - \color{blue}{\left(\left(wj \cdot \left(wj - 1\right)\right) \cdot \frac{1}{(wj \cdot wj + -1)_*} + \left(\left(-\frac{x}{e^{wj}}\right) \cdot \left(wj - 1\right)\right) \cdot \frac{1}{(wj \cdot wj + -1)_*}\right)}\]
16. Applied associate--r+3.3
  \[\leadsto \color{blue}{\left(wj - \left(wj \cdot \left(wj - 1\right)\right) \cdot \frac{1}{(wj \cdot wj + -1)_*}\right) - \left(\left(-\frac{x}{e^{wj}}\right) \cdot \left(wj - 1\right)\right) \cdot \frac{1}{(wj \cdot wj + -1)_*}}\]
17. Simplified3.3
  \[\leadsto \left(wj - \left(wj \cdot \left(wj - 1\right)\right) \cdot \frac{1}{(wj \cdot wj + -1)_*}\right) - \color{blue}{\frac{\frac{wj + -1}{(wj \cdot wj + -1)_*}}{\frac{e^{wj}}{-x}}}\]
if -8.379297298080333e-09 < wj < 4.7290331869132735e-09
1. Initial program 13.4
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Taylor expanded around 0 0.1
  \[\leadsto \color{blue}{\left({wj}^{2} + x\right) - 2 \cdot \left(x \cdot wj\right)}\]
3. Simplified0.2
  \[\leadsto \color{blue}{(wj \cdot \left((x \cdot -2 + wj)_*\right) + x)_*}\]
Recombined 2 regimes into one program.
Final simplification0.3
\[\leadsto \begin{array}{l} \mathbf{if}\;wj \le -8.379297298080333 \cdot 10^{-09} \lor \neg \left(wj \le 4.7290331869132735 \cdot 10^{-09}\right):\\ \;\;\;\;\left(wj - \frac{1}{(wj \cdot wj + -1)_*} \cdot \left(\left(wj - 1\right) \cdot wj\right)\right) - \frac{\frac{wj + -1}{(wj \cdot wj + -1)_*}}{\frac{e^{wj}}{-x}}\\ \mathbf{else}:\\ \;\;\;\;(wj \cdot \left((x \cdot -2 + wj)_*\right) + x)_*\\ \end{array}\]

Error

Target

Derivation

`if wj < -8.379297298080333e-09 or 4.7290331869132735e-09 < wj`

`if -8.379297298080333e-09 < wj < 4.7290331869132735e-09`

Runtime