NMSE Section 6.1 mentioned, A

Percentage Accurate: 73.0% → 99.8%
Time: 19.1s
Alternatives: 18
Speedup: 227.0×

Specification

?
\[\begin{array}{l} t_0 := \frac{1}{\varepsilon}\\ \frac{\left(1 + t_0\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(t_0 - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \end{array} \]

Your Program's Arguments

Results

Enter valid numbers for all inputs

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 18 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Alternative 1: 99.8% accurate, 1.0× speedup?

\[\begin{array}{l} t_0 := \left(1 + x\right) \cdot e^{-x}\\ t_1 := e^{\varepsilon \cdot \left(-x\right)}\\ \mathbf{if}\;\varepsilon \leq -1:\\ \;\;\;\;\frac{t_1 + e^{\varepsilon \cdot x}}{2}\\ \mathbf{elif}\;\varepsilon \leq 5 \cdot 10^{-29}:\\ \;\;\;\;\frac{t_0 + t_0}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + t_1}{2}\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if eps < -1

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv100.0%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg100.0%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative100.0%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative100.0%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative100.0%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in100.0%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified100.0%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\varepsilon \cdot x}}}{2} \]

    if -1 < eps < 4.99999999999999986e-29

    1. Initial program 38.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub38.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity38.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub38.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified38.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around 0 98.9%

      \[\leadsto \frac{\color{blue}{\left(e^{-1 \cdot x} \cdot x + e^{-1 \cdot x}\right) - \left(-1 \cdot \left(e^{-1 \cdot x} \cdot x\right) + -1 \cdot e^{-1 \cdot x}\right)}}{2} \]
    5. Step-by-step derivation
      1. *-commutative98.9%

        \[\leadsto \frac{\left(\color{blue}{x \cdot e^{-1 \cdot x}} + e^{-1 \cdot x}\right) - \left(-1 \cdot \left(e^{-1 \cdot x} \cdot x\right) + -1 \cdot e^{-1 \cdot x}\right)}{2} \]
      2. distribute-lft1-in98.9%

        \[\leadsto \frac{\color{blue}{\left(x + 1\right) \cdot e^{-1 \cdot x}} - \left(-1 \cdot \left(e^{-1 \cdot x} \cdot x\right) + -1 \cdot e^{-1 \cdot x}\right)}{2} \]
      3. neg-mul-198.9%

        \[\leadsto \frac{\left(x + 1\right) \cdot e^{\color{blue}{-x}} - \left(-1 \cdot \left(e^{-1 \cdot x} \cdot x\right) + -1 \cdot e^{-1 \cdot x}\right)}{2} \]
      4. distribute-lft-out98.9%

        \[\leadsto \frac{\left(x + 1\right) \cdot e^{-x} - \color{blue}{-1 \cdot \left(e^{-1 \cdot x} \cdot x + e^{-1 \cdot x}\right)}}{2} \]
      5. mul-1-neg98.9%

        \[\leadsto \frac{\left(x + 1\right) \cdot e^{-x} - \color{blue}{\left(-\left(e^{-1 \cdot x} \cdot x + e^{-1 \cdot x}\right)\right)}}{2} \]
      6. *-commutative98.9%

        \[\leadsto \frac{\left(x + 1\right) \cdot e^{-x} - \left(-\left(\color{blue}{x \cdot e^{-1 \cdot x}} + e^{-1 \cdot x}\right)\right)}{2} \]
      7. distribute-lft1-in100.0%

        \[\leadsto \frac{\left(x + 1\right) \cdot e^{-x} - \left(-\color{blue}{\left(x + 1\right) \cdot e^{-1 \cdot x}}\right)}{2} \]
      8. neg-mul-1100.0%

        \[\leadsto \frac{\left(x + 1\right) \cdot e^{-x} - \left(-\left(x + 1\right) \cdot e^{\color{blue}{-x}}\right)}{2} \]
    6. Simplified100.0%

      \[\leadsto \frac{\color{blue}{\left(x + 1\right) \cdot e^{-x} - \left(-\left(x + 1\right) \cdot e^{-x}\right)}}{2} \]

    if 4.99999999999999986e-29 < eps

    1. Initial program 97.5%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub97.5%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity97.5%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub97.5%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified97.5%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv100.0%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg100.0%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative100.0%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative100.0%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative100.0%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in100.0%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified100.0%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification100.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -1:\\ \;\;\;\;\frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\varepsilon \cdot x}}{2}\\ \mathbf{elif}\;\varepsilon \leq 5 \cdot 10^{-29}:\\ \;\;\;\;\frac{\left(1 + x\right) \cdot e^{-x} + \left(1 + x\right) \cdot e^{-x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + e^{\varepsilon \cdot \left(-x\right)}}{2}\\ \end{array} \]

Alternative 2: 98.8% accurate, 1.1× speedup?

\[\begin{array}{l} t_0 := e^{x \cdot \left(-1 + \varepsilon\right)}\\ t_1 := e^{\varepsilon \cdot \left(-x\right)}\\ \mathbf{if}\;\varepsilon \leq -1:\\ \;\;\;\;\frac{t_1 + e^{\varepsilon \cdot x}}{2}\\ \mathbf{elif}\;\varepsilon \leq 5 \cdot 10^{-29}:\\ \;\;\;\;\frac{t_0 + e^{-x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0 + t_1}{2}\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if eps < -1

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv100.0%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg100.0%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative100.0%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative100.0%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative100.0%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in100.0%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified100.0%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\varepsilon \cdot x}}}{2} \]

    if -1 < eps < 4.99999999999999986e-29

    1. Initial program 38.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub38.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity38.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub38.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified38.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 95.7%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around 0 95.7%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{x}}}{2} \]

    if 4.99999999999999986e-29 < eps

    1. Initial program 97.5%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub97.5%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity97.5%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub97.5%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified97.5%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv100.0%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg100.0%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative100.0%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity100.0%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative100.0%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative100.0%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in100.0%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified100.0%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification98.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -1:\\ \;\;\;\;\frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\varepsilon \cdot x}}{2}\\ \mathbf{elif}\;\varepsilon \leq 5 \cdot 10^{-29}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + e^{-x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + e^{\varepsilon \cdot \left(-x\right)}}{2}\\ \end{array} \]

Alternative 3: 98.8% accurate, 1.1× speedup?

\[\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + e^{x \cdot \left(-1 - \varepsilon\right)}}{2} \]
Derivation
  1. Initial program 76.5%

    \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
  2. Step-by-step derivation
    1. div-sub76.5%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    2. +-rgt-identity76.5%

      \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    3. div-sub76.5%

      \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
  3. Simplified76.5%

    \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
  4. Taylor expanded in eps around inf 98.4%

    \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
  5. Final simplification98.4%

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

Alternative 4: 92.1% accurate, 1.1× speedup?

\[\begin{array}{l} \mathbf{if}\;x \leq 135:\\ \;\;\;\;\frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\varepsilon \cdot x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if x < 135

    1. Initial program 67.1%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub67.1%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity67.1%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub67.1%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified67.1%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 98.2%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 98.2%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative98.2%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified98.2%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 98.2%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv98.2%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg98.2%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative98.2%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval98.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg98.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative98.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out98.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity98.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative98.2%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative98.2%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in98.2%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified98.2%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around inf 98.4%

      \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\varepsilon \cdot x}}}{2} \]

    if 135 < x

    1. Initial program 98.7%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub98.7%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity98.7%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub98.7%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified98.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 34.1%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around 0 31.2%

      \[\leadsto \frac{\color{blue}{\frac{1 + -1 \cdot x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. mul-1-neg31.2%

        \[\leadsto \frac{\frac{1 + \color{blue}{\left(-x\right)}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. unsub-neg31.2%

        \[\leadsto \frac{\frac{\color{blue}{1 - x}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified31.2%

      \[\leadsto \frac{\color{blue}{\frac{1 - x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    8. Taylor expanded in eps around inf 75.6%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. exp-prod75.6%

        \[\leadsto \frac{\color{blue}{{\left(e^{-1}\right)}^{\left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      2. +-commutative75.6%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 + \varepsilon\right)} \cdot x\right)}}{2} \]
      3. *-lft-identity75.6%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{1 \cdot \varepsilon}\right) \cdot x\right)}}{2} \]
      4. metadata-eval75.6%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{\left(--1\right)} \cdot \varepsilon\right) \cdot x\right)}}{2} \]
      5. cancel-sign-sub-inv75.6%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 - -1 \cdot \varepsilon\right)} \cdot x\right)}}{2} \]
      6. exp-prod75.6%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      7. mul-1-neg75.6%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - -1 \cdot \varepsilon\right) \cdot x}}}{2} \]
      8. *-commutative75.6%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - -1 \cdot \varepsilon\right)}}}{2} \]
      9. sub-neg75.6%

        \[\leadsto \frac{e^{-x \cdot \color{blue}{\left(1 + \left(--1 \cdot \varepsilon\right)\right)}}}{2} \]
      10. mul-1-neg75.6%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \left(-\color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      11. remove-double-neg75.6%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \color{blue}{\varepsilon}\right)}}{2} \]
    10. Simplified75.6%

      \[\leadsto \frac{\color{blue}{e^{-x \cdot \left(1 + \varepsilon\right)}}}{2} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification91.6%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 135:\\ \;\;\;\;\frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\varepsilon \cdot x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]

Alternative 5: 82.1% accurate, 1.7× speedup?

\[\begin{array}{l} t_0 := e^{x \cdot \left(-1 - \varepsilon\right)}\\ t_1 := \frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 6.5 \cdot 10^{-99}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;x \leq 3.3 \cdot 10^{-57}:\\ \;\;\;\;\frac{\left(1 - \left(1 - \varepsilon\right) \cdot x\right) \cdot \left(1 + \frac{1}{\varepsilon}\right) + t_0 \cdot \left(1 + \frac{-1}{\varepsilon}\right)}{2}\\ \mathbf{elif}\;x \leq 1.3 \cdot 10^{-12}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{2}\\ \end{array} \]
Derivation
  1. Split input into 4 regimes
  2. if x < -4900

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around 0 100.0%

      \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
    9. Step-by-step derivation
      1. neg-mul-1100.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
    10. Simplified100.0%

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

    if -4900 < x < 6.50000000000000033e-99 or 3.2999999999999998e-57 < x < 1.29999999999999991e-12

    1. Initial program 51.5%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub51.5%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity51.5%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub51.5%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified51.5%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative97.4%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified97.4%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv97.4%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg97.4%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative97.4%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative97.4%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative97.4%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in97.4%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified97.4%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around 0 82.2%

      \[\leadsto \frac{\color{blue}{\left(-1 \cdot \left(\varepsilon \cdot x\right) + 1\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    12. Step-by-step derivation
      1. +-commutative82.2%

        \[\leadsto \frac{\color{blue}{\left(1 + -1 \cdot \left(\varepsilon \cdot x\right)\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      2. mul-1-neg82.2%

        \[\leadsto \frac{\left(1 + \color{blue}{\left(-\varepsilon \cdot x\right)}\right) + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      3. unsub-neg82.2%

        \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    13. Simplified82.2%

      \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]

    if 6.50000000000000033e-99 < x < 3.2999999999999998e-57

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified78.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 92.6%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]

    if 1.29999999999999991e-12 < x

    1. Initial program 98.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub98.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity98.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub98.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified98.9%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 35.4%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around 0 32.6%

      \[\leadsto \frac{\color{blue}{\frac{1 + -1 \cdot x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. mul-1-neg32.6%

        \[\leadsto \frac{\frac{1 + \color{blue}{\left(-x\right)}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. unsub-neg32.6%

        \[\leadsto \frac{\frac{\color{blue}{1 - x}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified32.6%

      \[\leadsto \frac{\color{blue}{\frac{1 - x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    8. Taylor expanded in eps around inf 75.2%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. exp-prod75.2%

        \[\leadsto \frac{\color{blue}{{\left(e^{-1}\right)}^{\left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      2. +-commutative75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 + \varepsilon\right)} \cdot x\right)}}{2} \]
      3. *-lft-identity75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{1 \cdot \varepsilon}\right) \cdot x\right)}}{2} \]
      4. metadata-eval75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{\left(--1\right)} \cdot \varepsilon\right) \cdot x\right)}}{2} \]
      5. cancel-sign-sub-inv75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 - -1 \cdot \varepsilon\right)} \cdot x\right)}}{2} \]
      6. exp-prod75.2%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      7. mul-1-neg75.2%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - -1 \cdot \varepsilon\right) \cdot x}}}{2} \]
      8. *-commutative75.2%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - -1 \cdot \varepsilon\right)}}}{2} \]
      9. sub-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \color{blue}{\left(1 + \left(--1 \cdot \varepsilon\right)\right)}}}{2} \]
      10. mul-1-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \left(-\color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      11. remove-double-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \color{blue}{\varepsilon}\right)}}{2} \]
    10. Simplified75.2%

      \[\leadsto \frac{\color{blue}{e^{-x \cdot \left(1 + \varepsilon\right)}}}{2} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification83.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 6.5 \cdot 10^{-99}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{elif}\;x \leq 3.3 \cdot 10^{-57}:\\ \;\;\;\;\frac{\left(1 - \left(1 - \varepsilon\right) \cdot x\right) \cdot \left(1 + \frac{1}{\varepsilon}\right) + e^{x \cdot \left(-1 - \varepsilon\right)} \cdot \left(1 + \frac{-1}{\varepsilon}\right)}{2}\\ \mathbf{elif}\;x \leq 1.3 \cdot 10^{-12}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]

Alternative 6: 82.0% accurate, 1.8× speedup?

\[\begin{array}{l} t_0 := \frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ t_1 := e^{x \cdot \left(-1 - \varepsilon\right)}\\ \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 6.5 \cdot 10^{-99}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x \leq 3.7 \cdot 10^{-57}:\\ \;\;\;\;\frac{\left(1 + \varepsilon \cdot x\right) + t_1 \cdot \left(1 + \frac{-1}{\varepsilon}\right)}{2}\\ \mathbf{elif}\;x \leq 1.3 \cdot 10^{-12}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{t_1}{2}\\ \end{array} \]
Derivation
  1. Split input into 4 regimes
  2. if x < -4900

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around 0 100.0%

      \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
    9. Step-by-step derivation
      1. neg-mul-1100.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
    10. Simplified100.0%

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

    if -4900 < x < 6.50000000000000033e-99 or 3.7e-57 < x < 1.29999999999999991e-12

    1. Initial program 51.5%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub51.5%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity51.5%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub51.5%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified51.5%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative97.4%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified97.4%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv97.4%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg97.4%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative97.4%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative97.4%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative97.4%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in97.4%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified97.4%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around 0 82.2%

      \[\leadsto \frac{\color{blue}{\left(-1 \cdot \left(\varepsilon \cdot x\right) + 1\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    12. Step-by-step derivation
      1. +-commutative82.2%

        \[\leadsto \frac{\color{blue}{\left(1 + -1 \cdot \left(\varepsilon \cdot x\right)\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      2. mul-1-neg82.2%

        \[\leadsto \frac{\left(1 + \color{blue}{\left(-\varepsilon \cdot x\right)}\right) + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      3. unsub-neg82.2%

        \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    13. Simplified82.2%

      \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]

    if 6.50000000000000033e-99 < x < 3.7e-57

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified78.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 92.6%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around inf 89.1%

      \[\leadsto \frac{\color{blue}{\left(1 + \left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right)\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. +-commutative89.1%

        \[\leadsto \frac{\color{blue}{\left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. distribute-lft1-in89.1%

        \[\leadsto \frac{\left(\left(\varepsilon \cdot x + \color{blue}{\left(-1 + 1\right) \cdot x}\right) + 1\right) - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      3. metadata-eval89.1%

        \[\leadsto \frac{\left(\left(\varepsilon \cdot x + \color{blue}{0} \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      4. mul0-lft89.1%

        \[\leadsto \frac{\left(\left(\varepsilon \cdot x + \color{blue}{0}\right) + 1\right) - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      5. associate-+l+89.1%

        \[\leadsto \frac{\color{blue}{\left(\varepsilon \cdot x + \left(0 + 1\right)\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      6. metadata-eval89.1%

        \[\leadsto \frac{\left(\varepsilon \cdot x + \color{blue}{1}\right) - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      7. *-commutative89.1%

        \[\leadsto \frac{\left(\color{blue}{x \cdot \varepsilon} + 1\right) - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified89.1%

      \[\leadsto \frac{\color{blue}{\left(x \cdot \varepsilon + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]

    if 1.29999999999999991e-12 < x

    1. Initial program 98.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub98.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity98.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub98.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified98.9%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 35.4%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around 0 32.6%

      \[\leadsto \frac{\color{blue}{\frac{1 + -1 \cdot x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. mul-1-neg32.6%

        \[\leadsto \frac{\frac{1 + \color{blue}{\left(-x\right)}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. unsub-neg32.6%

        \[\leadsto \frac{\frac{\color{blue}{1 - x}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified32.6%

      \[\leadsto \frac{\color{blue}{\frac{1 - x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    8. Taylor expanded in eps around inf 75.2%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. exp-prod75.2%

        \[\leadsto \frac{\color{blue}{{\left(e^{-1}\right)}^{\left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      2. +-commutative75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 + \varepsilon\right)} \cdot x\right)}}{2} \]
      3. *-lft-identity75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{1 \cdot \varepsilon}\right) \cdot x\right)}}{2} \]
      4. metadata-eval75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{\left(--1\right)} \cdot \varepsilon\right) \cdot x\right)}}{2} \]
      5. cancel-sign-sub-inv75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 - -1 \cdot \varepsilon\right)} \cdot x\right)}}{2} \]
      6. exp-prod75.2%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      7. mul-1-neg75.2%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - -1 \cdot \varepsilon\right) \cdot x}}}{2} \]
      8. *-commutative75.2%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - -1 \cdot \varepsilon\right)}}}{2} \]
      9. sub-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \color{blue}{\left(1 + \left(--1 \cdot \varepsilon\right)\right)}}}{2} \]
      10. mul-1-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \left(-\color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      11. remove-double-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \color{blue}{\varepsilon}\right)}}{2} \]
    10. Simplified75.2%

      \[\leadsto \frac{\color{blue}{e^{-x \cdot \left(1 + \varepsilon\right)}}}{2} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification83.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 6.5 \cdot 10^{-99}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{elif}\;x \leq 3.7 \cdot 10^{-57}:\\ \;\;\;\;\frac{\left(1 + \varepsilon \cdot x\right) + e^{x \cdot \left(-1 - \varepsilon\right)} \cdot \left(1 + \frac{-1}{\varepsilon}\right)}{2}\\ \mathbf{elif}\;x \leq 1.3 \cdot 10^{-12}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]

Alternative 7: 82.1% accurate, 1.8× speedup?

\[\begin{array}{l} t_0 := e^{x \cdot \left(-1 - \varepsilon\right)}\\ t_1 := \frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 5.5 \cdot 10^{-99}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;x \leq 3.7 \cdot 10^{-57}:\\ \;\;\;\;\frac{\left(1 + \frac{1}{\varepsilon}\right) - \left(-1 + \frac{1}{\varepsilon}\right) \cdot t_0}{2}\\ \mathbf{elif}\;x \leq 5.8 \cdot 10^{-13}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{2}\\ \end{array} \]
Derivation
  1. Split input into 4 regimes
  2. if x < -4900

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around 0 100.0%

      \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
    9. Step-by-step derivation
      1. neg-mul-1100.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
    10. Simplified100.0%

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

    if -4900 < x < 5.49999999999999991e-99 or 3.7e-57 < x < 5.7999999999999995e-13

    1. Initial program 51.5%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub51.5%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity51.5%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub51.5%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified51.5%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative97.4%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified97.4%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 97.4%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv97.4%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg97.4%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative97.4%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity97.4%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative97.4%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative97.4%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in97.4%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified97.4%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around 0 82.2%

      \[\leadsto \frac{\color{blue}{\left(-1 \cdot \left(\varepsilon \cdot x\right) + 1\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    12. Step-by-step derivation
      1. +-commutative82.2%

        \[\leadsto \frac{\color{blue}{\left(1 + -1 \cdot \left(\varepsilon \cdot x\right)\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      2. mul-1-neg82.2%

        \[\leadsto \frac{\left(1 + \color{blue}{\left(-\varepsilon \cdot x\right)}\right) + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      3. unsub-neg82.2%

        \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    13. Simplified82.2%

      \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]

    if 5.49999999999999991e-99 < x < 3.7e-57

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 92.5%

      \[\leadsto \frac{\color{blue}{\left(\frac{1}{\varepsilon} + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]

    if 5.7999999999999995e-13 < x

    1. Initial program 98.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub98.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity98.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub98.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified98.9%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 35.4%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around 0 32.6%

      \[\leadsto \frac{\color{blue}{\frac{1 + -1 \cdot x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. mul-1-neg32.6%

        \[\leadsto \frac{\frac{1 + \color{blue}{\left(-x\right)}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. unsub-neg32.6%

        \[\leadsto \frac{\frac{\color{blue}{1 - x}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified32.6%

      \[\leadsto \frac{\color{blue}{\frac{1 - x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    8. Taylor expanded in eps around inf 75.2%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. exp-prod75.2%

        \[\leadsto \frac{\color{blue}{{\left(e^{-1}\right)}^{\left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      2. +-commutative75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 + \varepsilon\right)} \cdot x\right)}}{2} \]
      3. *-lft-identity75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{1 \cdot \varepsilon}\right) \cdot x\right)}}{2} \]
      4. metadata-eval75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{\left(--1\right)} \cdot \varepsilon\right) \cdot x\right)}}{2} \]
      5. cancel-sign-sub-inv75.2%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 - -1 \cdot \varepsilon\right)} \cdot x\right)}}{2} \]
      6. exp-prod75.2%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      7. mul-1-neg75.2%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - -1 \cdot \varepsilon\right) \cdot x}}}{2} \]
      8. *-commutative75.2%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - -1 \cdot \varepsilon\right)}}}{2} \]
      9. sub-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \color{blue}{\left(1 + \left(--1 \cdot \varepsilon\right)\right)}}}{2} \]
      10. mul-1-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \left(-\color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      11. remove-double-neg75.2%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \color{blue}{\varepsilon}\right)}}{2} \]
    10. Simplified75.2%

      \[\leadsto \frac{\color{blue}{e^{-x \cdot \left(1 + \varepsilon\right)}}}{2} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification83.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 5.5 \cdot 10^{-99}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{elif}\;x \leq 3.7 \cdot 10^{-57}:\\ \;\;\;\;\frac{\left(1 + \frac{1}{\varepsilon}\right) - \left(-1 + \frac{1}{\varepsilon}\right) \cdot e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \mathbf{elif}\;x \leq 5.8 \cdot 10^{-13}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]

Alternative 8: 83.1% accurate, 1.9× speedup?

\[\begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 1.45 \cdot 10^{-77} \lor \neg \left(x \leq 3.5 \cdot 10^{-57}\right) \land x \leq 6.4 \cdot 10^{-12}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if x < -4900

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around 0 100.0%

      \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
    9. Step-by-step derivation
      1. neg-mul-1100.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
    10. Simplified100.0%

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

    if -4900 < x < 1.4499999999999999e-77 or 3.49999999999999991e-57 < x < 6.4000000000000002e-12

    1. Initial program 53.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub53.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity53.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub53.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified53.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 97.5%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 97.5%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative97.5%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified97.5%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 97.5%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. cancel-sign-sub-inv97.5%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}}{2} \]
      2. mul-1-neg97.5%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - \varepsilon\right) \cdot x}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      3. *-commutative97.5%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - \varepsilon\right)}} + \left(--1\right) \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      4. metadata-eval97.5%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{1} \cdot e^{-1 \cdot \left(\varepsilon \cdot x\right)}}{2} \]
      5. mul-1-neg97.5%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{-\varepsilon \cdot x}}}{2} \]
      6. *-commutative97.5%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{-\color{blue}{x \cdot \varepsilon}}}{2} \]
      7. distribute-lft-neg-out97.5%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + 1 \cdot e^{\color{blue}{\left(-x\right) \cdot \varepsilon}}}{2} \]
      8. *-lft-identity97.5%

        \[\leadsto \frac{e^{-x \cdot \left(1 - \varepsilon\right)} + \color{blue}{e^{\left(-x\right) \cdot \varepsilon}}}{2} \]
      9. +-commutative97.5%

        \[\leadsto \frac{\color{blue}{e^{\left(-x\right) \cdot \varepsilon} + e^{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. *-commutative97.5%

        \[\leadsto \frac{e^{\color{blue}{\varepsilon \cdot \left(-x\right)}} + e^{-x \cdot \left(1 - \varepsilon\right)}}{2} \]
      11. distribute-lft-neg-in97.5%

        \[\leadsto \frac{e^{\varepsilon \cdot \left(-x\right)} + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    10. Simplified97.5%

      \[\leadsto \frac{\color{blue}{e^{\varepsilon \cdot \left(-x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    11. Taylor expanded in eps around 0 81.6%

      \[\leadsto \frac{\color{blue}{\left(-1 \cdot \left(\varepsilon \cdot x\right) + 1\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    12. Step-by-step derivation
      1. +-commutative81.6%

        \[\leadsto \frac{\color{blue}{\left(1 + -1 \cdot \left(\varepsilon \cdot x\right)\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      2. mul-1-neg81.6%

        \[\leadsto \frac{\left(1 + \color{blue}{\left(-\varepsilon \cdot x\right)}\right) + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
      3. unsub-neg81.6%

        \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]
    13. Simplified81.6%

      \[\leadsto \frac{\color{blue}{\left(1 - \varepsilon \cdot x\right)} + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}{2} \]

    if 1.4499999999999999e-77 < x < 3.49999999999999991e-57 or 6.4000000000000002e-12 < x

    1. Initial program 98.9%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub98.9%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity98.9%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub98.9%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified99.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 40.7%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around 0 38.1%

      \[\leadsto \frac{\color{blue}{\frac{1 + -1 \cdot x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. mul-1-neg38.1%

        \[\leadsto \frac{\frac{1 + \color{blue}{\left(-x\right)}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. unsub-neg38.1%

        \[\leadsto \frac{\frac{\color{blue}{1 - x}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified38.1%

      \[\leadsto \frac{\color{blue}{\frac{1 - x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    8. Taylor expanded in eps around inf 77.3%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. exp-prod77.3%

        \[\leadsto \frac{\color{blue}{{\left(e^{-1}\right)}^{\left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      2. +-commutative77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 + \varepsilon\right)} \cdot x\right)}}{2} \]
      3. *-lft-identity77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{1 \cdot \varepsilon}\right) \cdot x\right)}}{2} \]
      4. metadata-eval77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{\left(--1\right)} \cdot \varepsilon\right) \cdot x\right)}}{2} \]
      5. cancel-sign-sub-inv77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 - -1 \cdot \varepsilon\right)} \cdot x\right)}}{2} \]
      6. exp-prod77.3%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      7. mul-1-neg77.3%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - -1 \cdot \varepsilon\right) \cdot x}}}{2} \]
      8. *-commutative77.3%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - -1 \cdot \varepsilon\right)}}}{2} \]
      9. sub-neg77.3%

        \[\leadsto \frac{e^{-x \cdot \color{blue}{\left(1 + \left(--1 \cdot \varepsilon\right)\right)}}}{2} \]
      10. mul-1-neg77.3%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \left(-\color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      11. remove-double-neg77.3%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \color{blue}{\varepsilon}\right)}}{2} \]
    10. Simplified77.3%

      \[\leadsto \frac{\color{blue}{e^{-x \cdot \left(1 + \varepsilon\right)}}}{2} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification83.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 1.45 \cdot 10^{-77} \lor \neg \left(x \leq 3.5 \cdot 10^{-57}\right) \land x \leq 6.4 \cdot 10^{-12}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 + \varepsilon\right)} + \left(1 - \varepsilon \cdot x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]

Alternative 9: 82.9% accurate, 2.0× speedup?

\[\begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 1.45 \cdot 10^{-77} \lor \neg \left(x \leq 2 \cdot 10^{-56}\right) \land x \leq 6.4 \cdot 10^{-12}:\\ \;\;\;\;\frac{1 + e^{\varepsilon \cdot x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if x < -4900

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around 0 100.0%

      \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
    9. Step-by-step derivation
      1. neg-mul-1100.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
    10. Simplified100.0%

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

    if -4900 < x < 1.4499999999999999e-77 or 2.0000000000000001e-56 < x < 6.4000000000000002e-12

    1. Initial program 53.8%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub53.8%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity53.8%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub53.8%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified53.8%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 38.1%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \color{blue}{\left(\frac{1}{\varepsilon} - 1\right)}}{2} \]
    5. Taylor expanded in eps around inf 81.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + 1}}{2} \]
    6. Step-by-step derivation
      1. associate-*r*81.0%

        \[\leadsto \frac{e^{\color{blue}{\left(-1 \cdot \left(1 - \varepsilon\right)\right) \cdot x}} + 1}{2} \]
      2. sub-neg81.0%

        \[\leadsto \frac{e^{\left(-1 \cdot \color{blue}{\left(1 + \left(-\varepsilon\right)\right)}\right) \cdot x} + 1}{2} \]
      3. neg-mul-181.0%

        \[\leadsto \frac{e^{\left(-1 \cdot \left(1 + \color{blue}{-1 \cdot \varepsilon}\right)\right) \cdot x} + 1}{2} \]
      4. associate-*r*81.0%

        \[\leadsto \frac{e^{\color{blue}{-1 \cdot \left(\left(1 + -1 \cdot \varepsilon\right) \cdot x\right)}} + 1}{2} \]
      5. +-commutative81.0%

        \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot \left(\left(1 + -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      6. *-commutative81.0%

        \[\leadsto \frac{1 + e^{-1 \cdot \color{blue}{\left(x \cdot \left(1 + -1 \cdot \varepsilon\right)\right)}}}{2} \]
      7. neg-mul-181.0%

        \[\leadsto \frac{1 + e^{-1 \cdot \left(x \cdot \left(1 + \color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      8. sub-neg81.0%

        \[\leadsto \frac{1 + e^{-1 \cdot \left(x \cdot \color{blue}{\left(1 - \varepsilon\right)}\right)}}{2} \]
      9. neg-mul-181.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. distribute-lft-neg-in81.0%

        \[\leadsto \frac{1 + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    7. Simplified81.0%

      \[\leadsto \frac{\color{blue}{1 + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 81.2%

      \[\leadsto \frac{1 + e^{\color{blue}{\varepsilon \cdot x}}}{2} \]

    if 1.4499999999999999e-77 < x < 2.0000000000000001e-56 or 6.4000000000000002e-12 < x

    1. Initial program 98.9%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub98.9%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity98.9%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub98.9%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified99.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 40.7%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    5. Taylor expanded in eps around 0 38.1%

      \[\leadsto \frac{\color{blue}{\frac{1 + -1 \cdot x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    6. Step-by-step derivation
      1. mul-1-neg38.1%

        \[\leadsto \frac{\frac{1 + \color{blue}{\left(-x\right)}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
      2. unsub-neg38.1%

        \[\leadsto \frac{\frac{\color{blue}{1 - x}}{\varepsilon} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    7. Simplified38.1%

      \[\leadsto \frac{\color{blue}{\frac{1 - x}{\varepsilon}} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
    8. Taylor expanded in eps around inf 77.3%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    9. Step-by-step derivation
      1. exp-prod77.3%

        \[\leadsto \frac{\color{blue}{{\left(e^{-1}\right)}^{\left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      2. +-commutative77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 + \varepsilon\right)} \cdot x\right)}}{2} \]
      3. *-lft-identity77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{1 \cdot \varepsilon}\right) \cdot x\right)}}{2} \]
      4. metadata-eval77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\left(1 + \color{blue}{\left(--1\right)} \cdot \varepsilon\right) \cdot x\right)}}{2} \]
      5. cancel-sign-sub-inv77.3%

        \[\leadsto \frac{{\left(e^{-1}\right)}^{\left(\color{blue}{\left(1 - -1 \cdot \varepsilon\right)} \cdot x\right)}}{2} \]
      6. exp-prod77.3%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      7. mul-1-neg77.3%

        \[\leadsto \frac{e^{\color{blue}{-\left(1 - -1 \cdot \varepsilon\right) \cdot x}}}{2} \]
      8. *-commutative77.3%

        \[\leadsto \frac{e^{-\color{blue}{x \cdot \left(1 - -1 \cdot \varepsilon\right)}}}{2} \]
      9. sub-neg77.3%

        \[\leadsto \frac{e^{-x \cdot \color{blue}{\left(1 + \left(--1 \cdot \varepsilon\right)\right)}}}{2} \]
      10. mul-1-neg77.3%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \left(-\color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      11. remove-double-neg77.3%

        \[\leadsto \frac{e^{-x \cdot \left(1 + \color{blue}{\varepsilon}\right)}}{2} \]
    10. Simplified77.3%

      \[\leadsto \frac{\color{blue}{e^{-x \cdot \left(1 + \varepsilon\right)}}}{2} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification83.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 1.45 \cdot 10^{-77} \lor \neg \left(x \leq 2 \cdot 10^{-56}\right) \land x \leq 6.4 \cdot 10^{-12}:\\ \;\;\;\;\frac{1 + e^{\varepsilon \cdot x}}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{x \cdot \left(-1 - \varepsilon\right)}}{2}\\ \end{array} \]

Alternative 10: 77.1% accurate, 2.0× speedup?

\[\begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 520000000000:\\ \;\;\;\;\frac{1 + e^{\varepsilon \cdot x}}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if x < -4900

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity100.0%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub100.0%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
    5. Taylor expanded in eps around inf 100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
    6. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    7. Simplified100.0%

      \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around 0 100.0%

      \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
    9. Step-by-step derivation
      1. neg-mul-1100.0%

        \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
    10. Simplified100.0%

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

    if -4900 < x < 5.2e11

    1. Initial program 57.1%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. div-sub57.1%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      2. +-rgt-identity57.1%

        \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      3. div-sub57.1%

        \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
    3. Simplified57.1%

      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
    4. Taylor expanded in x around 0 35.8%

      \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \color{blue}{\left(\frac{1}{\varepsilon} - 1\right)}}{2} \]
    5. Taylor expanded in eps around inf 75.1%

      \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + 1}}{2} \]
    6. Step-by-step derivation
      1. associate-*r*75.1%

        \[\leadsto \frac{e^{\color{blue}{\left(-1 \cdot \left(1 - \varepsilon\right)\right) \cdot x}} + 1}{2} \]
      2. sub-neg75.1%

        \[\leadsto \frac{e^{\left(-1 \cdot \color{blue}{\left(1 + \left(-\varepsilon\right)\right)}\right) \cdot x} + 1}{2} \]
      3. neg-mul-175.1%

        \[\leadsto \frac{e^{\left(-1 \cdot \left(1 + \color{blue}{-1 \cdot \varepsilon}\right)\right) \cdot x} + 1}{2} \]
      4. associate-*r*75.1%

        \[\leadsto \frac{e^{\color{blue}{-1 \cdot \left(\left(1 + -1 \cdot \varepsilon\right) \cdot x\right)}} + 1}{2} \]
      5. +-commutative75.1%

        \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot \left(\left(1 + -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
      6. *-commutative75.1%

        \[\leadsto \frac{1 + e^{-1 \cdot \color{blue}{\left(x \cdot \left(1 + -1 \cdot \varepsilon\right)\right)}}}{2} \]
      7. neg-mul-175.1%

        \[\leadsto \frac{1 + e^{-1 \cdot \left(x \cdot \left(1 + \color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
      8. sub-neg75.1%

        \[\leadsto \frac{1 + e^{-1 \cdot \left(x \cdot \color{blue}{\left(1 - \varepsilon\right)}\right)}}{2} \]
      9. neg-mul-175.1%

        \[\leadsto \frac{1 + e^{\color{blue}{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
      10. distribute-lft-neg-in75.1%

        \[\leadsto \frac{1 + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    7. Simplified75.1%

      \[\leadsto \frac{\color{blue}{1 + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
    8. Taylor expanded in eps around inf 75.2%

      \[\leadsto \frac{1 + e^{\color{blue}{\varepsilon \cdot x}}}{2} \]

    if 5.2e11 < x

    1. Initial program 100.0%

      \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
    2. Step-by-step derivation
      1. Simplified100.0%

        \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
      2. Taylor expanded in eps around 0 46.8%

        \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
      3. Step-by-step derivation
        1. div-sub46.8%

          \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
        2. rec-exp46.8%

          \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
        3. neg-mul-146.8%

          \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
        4. +-inverses46.8%

          \[\leadsto \frac{\color{blue}{0}}{2} \]
      4. Simplified46.8%

        \[\leadsto \frac{\color{blue}{0}}{2} \]
    3. Recombined 3 regimes into one program.
    4. Final simplification71.1%

      \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4900:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{elif}\;x \leq 520000000000:\\ \;\;\;\;\frac{1 + e^{\varepsilon \cdot x}}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

    Alternative 11: 70.3% accurate, 2.1× speedup?

    \[\begin{array}{l} \mathbf{if}\;x \leq 13000:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
    Derivation
    1. Split input into 2 regimes
    2. if x < 13000

      1. Initial program 67.0%

        \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      2. Step-by-step derivation
        1. div-sub67.0%

          \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
        2. +-rgt-identity67.0%

          \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
        3. div-sub67.0%

          \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
      3. Simplified67.0%

        \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
      4. Taylor expanded in eps around inf 97.8%

        \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \left(\left(\varepsilon + 1\right) \cdot x\right)}}}{2} \]
      5. Taylor expanded in eps around inf 97.7%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(\varepsilon \cdot x\right)}}}{2} \]
      6. Step-by-step derivation
        1. *-commutative97.7%

          \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
      7. Simplified97.7%

        \[\leadsto \frac{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} - -1 \cdot e^{-1 \cdot \color{blue}{\left(x \cdot \varepsilon\right)}}}{2} \]
      8. Taylor expanded in eps around 0 72.0%

        \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot x}}}{2} \]
      9. Step-by-step derivation
        1. neg-mul-172.0%

          \[\leadsto \frac{1 + e^{\color{blue}{-x}}}{2} \]
      10. Simplified72.0%

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

      if 13000 < x

      1. Initial program 100.0%

        \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
      2. Step-by-step derivation
        1. Simplified100.0%

          \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
        2. Taylor expanded in eps around 0 46.8%

          \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
        3. Step-by-step derivation
          1. div-sub46.8%

            \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
          2. rec-exp46.8%

            \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
          3. neg-mul-146.8%

            \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
          4. +-inverses46.8%

            \[\leadsto \frac{\color{blue}{0}}{2} \]
        4. Simplified46.8%

          \[\leadsto \frac{\color{blue}{0}}{2} \]
      3. Recombined 2 regimes into one program.
      4. Final simplification64.7%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 13000:\\ \;\;\;\;\frac{1 + e^{-x}}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

      Alternative 12: 60.4% accurate, 8.4× speedup?

      \[\begin{array}{l} \mathbf{if}\;x \leq -1.4 \cdot 10^{+69}:\\ \;\;\;\;\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(1 + \left(1 - \varepsilon\right) \cdot x\right) + \left(1 + \left(\left(x - x\right) - \varepsilon \cdot x\right)\right)}{2}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
      Derivation
      1. Split input into 3 regimes
      2. if x < -1.39999999999999991e69

        1. Initial program 100.0%

          \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
        2. Step-by-step derivation
          1. div-sub100.0%

            \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
          2. +-rgt-identity100.0%

            \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
          3. div-sub100.0%

            \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
        3. Simplified100.0%

          \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
        4. Taylor expanded in x around 0 46.3%

          \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
        5. Taylor expanded in x around 0 0.5%

          \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\left(\frac{1}{\varepsilon} + -1 \cdot \left(\left(\frac{1}{\varepsilon} - 1\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right)\right)\right) - 1\right)}}{2} \]
        6. Step-by-step derivation
          1. associate--l+0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\frac{1}{\varepsilon} + \left(-1 \cdot \left(\left(\frac{1}{\varepsilon} - 1\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right)\right) - 1\right)\right)}}{2} \]
          2. associate-*r*0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\color{blue}{\left(-1 \cdot \left(\frac{1}{\varepsilon} - 1\right)\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right)} - 1\right)\right)}{2} \]
          3. neg-mul-10.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\color{blue}{\left(-\left(\frac{1}{\varepsilon} - 1\right)\right)} \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
          4. sub-neg0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\color{blue}{\left(\frac{1}{\varepsilon} + \left(-1\right)\right)}\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
          5. metadata-eval0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\left(\frac{1}{\varepsilon} + \color{blue}{-1}\right)\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
          6. +-commutative0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\color{blue}{\left(-1 + \frac{1}{\varepsilon}\right)}\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
          7. *-commutative0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\left(-1 + \frac{1}{\varepsilon}\right)\right) \cdot \color{blue}{\left(x \cdot \left(1 + \varepsilon\right)\right)} - 1\right)\right)}{2} \]
          8. +-commutative0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\left(-1 + \frac{1}{\varepsilon}\right)\right) \cdot \left(x \cdot \color{blue}{\left(\varepsilon + 1\right)}\right) - 1\right)\right)}{2} \]
        7. Simplified0.5%

          \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\frac{1}{\varepsilon} + \left(\left(-\left(-1 + \frac{1}{\varepsilon}\right)\right) \cdot \left(x \cdot \left(\varepsilon + 1\right)\right) - 1\right)\right)}}{2} \]
        8. Taylor expanded in eps around inf 0.5%

          \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}}{2} \]
        9. Step-by-step derivation
          1. add-sqr-sqrt0.0%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)}\right) + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          2. sqrt-unprod43.7%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot \color{blue}{\sqrt{x \cdot x}}\right) + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          3. sqr-neg43.7%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot \sqrt{\color{blue}{\left(-x\right) \cdot \left(-x\right)}}\right) + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          4. sqrt-unprod40.9%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot \color{blue}{\left(\sqrt{-x} \cdot \sqrt{-x}\right)}\right) + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          5. add-sqr-sqrt40.9%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot \color{blue}{\left(-x\right)}\right) + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          6. distribute-rgt-neg-out40.9%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \color{blue}{\left(-\left(1 - \varepsilon\right) \cdot x\right)} + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          7. *-commutative40.9%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(-\color{blue}{x \cdot \left(1 - \varepsilon\right)}\right) + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
        10. Applied egg-rr40.9%

          \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \color{blue}{\left(-x \cdot \left(1 - \varepsilon\right)\right)} + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]

        if -1.39999999999999991e69 < x < 13000

        1. Initial program 59.7%

          \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
        2. Step-by-step derivation
          1. div-sub59.7%

            \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
          2. +-rgt-identity59.7%

            \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
          3. div-sub59.7%

            \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
        3. Simplified59.7%

          \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
        4. Taylor expanded in x around 0 60.1%

          \[\leadsto \frac{\color{blue}{2}}{2} \]

        if 13000 < x

        1. Initial program 100.0%

          \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
        2. Step-by-step derivation
          1. Simplified100.0%

            \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
          2. Taylor expanded in eps around 0 46.8%

            \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
          3. Step-by-step derivation
            1. div-sub46.8%

              \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
            2. rec-exp46.8%

              \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
            3. neg-mul-146.8%

              \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
            4. +-inverses46.8%

              \[\leadsto \frac{\color{blue}{0}}{2} \]
          4. Simplified46.8%

            \[\leadsto \frac{\color{blue}{0}}{2} \]
        3. Recombined 3 regimes into one program.
        4. Final simplification53.8%

          \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.4 \cdot 10^{+69}:\\ \;\;\;\;\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(1 + \left(1 - \varepsilon\right) \cdot x\right) + \left(1 + \left(\left(x - x\right) - \varepsilon \cdot x\right)\right)}{2}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

        Alternative 13: 60.4% accurate, 11.9× speedup?

        \[\begin{array}{l} \mathbf{if}\;x \leq -1.12 \cdot 10^{+69}:\\ \;\;\;\;\frac{\left(1 + \frac{1}{\varepsilon}\right) + \left(1 + \left(\left(x - x\right) - \varepsilon \cdot x\right)\right)}{2}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
        Derivation
        1. Split input into 3 regimes
        2. if x < -1.12e69

          1. Initial program 100.0%

            \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
          2. Step-by-step derivation
            1. div-sub100.0%

              \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
            2. +-rgt-identity100.0%

              \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
            3. div-sub100.0%

              \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
          3. Simplified100.0%

            \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
          4. Taylor expanded in x around 0 46.3%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
          5. Taylor expanded in x around 0 0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\left(\frac{1}{\varepsilon} + -1 \cdot \left(\left(\frac{1}{\varepsilon} - 1\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right)\right)\right) - 1\right)}}{2} \]
          6. Step-by-step derivation
            1. associate--l+0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\frac{1}{\varepsilon} + \left(-1 \cdot \left(\left(\frac{1}{\varepsilon} - 1\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right)\right) - 1\right)\right)}}{2} \]
            2. associate-*r*0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\color{blue}{\left(-1 \cdot \left(\frac{1}{\varepsilon} - 1\right)\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right)} - 1\right)\right)}{2} \]
            3. neg-mul-10.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\color{blue}{\left(-\left(\frac{1}{\varepsilon} - 1\right)\right)} \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
            4. sub-neg0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\color{blue}{\left(\frac{1}{\varepsilon} + \left(-1\right)\right)}\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
            5. metadata-eval0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\left(\frac{1}{\varepsilon} + \color{blue}{-1}\right)\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
            6. +-commutative0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\color{blue}{\left(-1 + \frac{1}{\varepsilon}\right)}\right) \cdot \left(\left(1 + \varepsilon\right) \cdot x\right) - 1\right)\right)}{2} \]
            7. *-commutative0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\left(-1 + \frac{1}{\varepsilon}\right)\right) \cdot \color{blue}{\left(x \cdot \left(1 + \varepsilon\right)\right)} - 1\right)\right)}{2} \]
            8. +-commutative0.5%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \left(\frac{1}{\varepsilon} + \left(\left(-\left(-1 + \frac{1}{\varepsilon}\right)\right) \cdot \left(x \cdot \color{blue}{\left(\varepsilon + 1\right)}\right) - 1\right)\right)}{2} \]
          7. Simplified0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\frac{1}{\varepsilon} + \left(\left(-\left(-1 + \frac{1}{\varepsilon}\right)\right) \cdot \left(x \cdot \left(\varepsilon + 1\right)\right) - 1\right)\right)}}{2} \]
          8. Taylor expanded in eps around inf 0.5%

            \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right) - \color{blue}{\left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}}{2} \]
          9. Taylor expanded in x around 0 40.9%

            \[\leadsto \frac{\color{blue}{\left(\frac{1}{\varepsilon} + 1\right)} - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          10. Step-by-step derivation
            1. unpow-140.9%

              \[\leadsto \frac{\left(\color{blue}{{\varepsilon}^{-1}} + 1\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
            2. +-commutative40.9%

              \[\leadsto \frac{\color{blue}{\left(1 + {\varepsilon}^{-1}\right)} - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
            3. remove-double-neg40.9%

              \[\leadsto \frac{\left(1 + \color{blue}{\left(-\left(-{\varepsilon}^{-1}\right)\right)}\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
            4. sub-neg40.9%

              \[\leadsto \frac{\color{blue}{\left(1 - \left(-{\varepsilon}^{-1}\right)\right)} - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
            5. unpow-140.9%

              \[\leadsto \frac{\left(1 - \left(-\color{blue}{\frac{1}{\varepsilon}}\right)\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
            6. distribute-neg-frac40.9%

              \[\leadsto \frac{\left(1 - \color{blue}{\frac{-1}{\varepsilon}}\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
            7. metadata-eval40.9%

              \[\leadsto \frac{\left(1 - \frac{\color{blue}{-1}}{\varepsilon}\right) - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]
          11. Simplified40.9%

            \[\leadsto \frac{\color{blue}{\left(1 - \frac{-1}{\varepsilon}\right)} - \left(\left(\varepsilon \cdot x + \left(-1 \cdot x + x\right)\right) - 1\right)}{2} \]

          if -1.12e69 < x < 13000

          1. Initial program 59.7%

            \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
          2. Step-by-step derivation
            1. div-sub59.7%

              \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
            2. +-rgt-identity59.7%

              \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
            3. div-sub59.7%

              \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
          3. Simplified59.7%

            \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
          4. Taylor expanded in x around 0 60.1%

            \[\leadsto \frac{\color{blue}{2}}{2} \]

          if 13000 < x

          1. Initial program 100.0%

            \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
          2. Step-by-step derivation
            1. Simplified100.0%

              \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
            2. Taylor expanded in eps around 0 46.8%

              \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
            3. Step-by-step derivation
              1. div-sub46.8%

                \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
              2. rec-exp46.8%

                \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
              3. neg-mul-146.8%

                \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
              4. +-inverses46.8%

                \[\leadsto \frac{\color{blue}{0}}{2} \]
            4. Simplified46.8%

              \[\leadsto \frac{\color{blue}{0}}{2} \]
          3. Recombined 3 regimes into one program.
          4. Final simplification53.8%

            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.12 \cdot 10^{+69}:\\ \;\;\;\;\frac{\left(1 + \frac{1}{\varepsilon}\right) + \left(1 + \left(\left(x - x\right) - \varepsilon \cdot x\right)\right)}{2}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

          Alternative 14: 59.8% accurate, 20.5× speedup?

          \[\begin{array}{l} \mathbf{if}\;x \leq 6.4 \cdot 10^{-12}:\\ \;\;\;\;\frac{2 - \left(1 - \varepsilon\right) \cdot x}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
          Derivation
          1. Split input into 2 regimes
          2. if x < 6.4000000000000002e-12

            1. Initial program 66.6%

              \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
            2. Step-by-step derivation
              1. div-sub66.6%

                \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
              2. +-rgt-identity66.6%

                \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
              3. div-sub66.6%

                \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
            3. Simplified66.6%

              \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
            4. Taylor expanded in x around 0 39.4%

              \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \color{blue}{\left(\frac{1}{\varepsilon} - 1\right)}}{2} \]
            5. Taylor expanded in eps around inf 70.4%

              \[\leadsto \frac{\color{blue}{e^{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)} + 1}}{2} \]
            6. Step-by-step derivation
              1. associate-*r*70.4%

                \[\leadsto \frac{e^{\color{blue}{\left(-1 \cdot \left(1 - \varepsilon\right)\right) \cdot x}} + 1}{2} \]
              2. sub-neg70.4%

                \[\leadsto \frac{e^{\left(-1 \cdot \color{blue}{\left(1 + \left(-\varepsilon\right)\right)}\right) \cdot x} + 1}{2} \]
              3. neg-mul-170.4%

                \[\leadsto \frac{e^{\left(-1 \cdot \left(1 + \color{blue}{-1 \cdot \varepsilon}\right)\right) \cdot x} + 1}{2} \]
              4. associate-*r*70.4%

                \[\leadsto \frac{e^{\color{blue}{-1 \cdot \left(\left(1 + -1 \cdot \varepsilon\right) \cdot x\right)}} + 1}{2} \]
              5. +-commutative70.4%

                \[\leadsto \frac{\color{blue}{1 + e^{-1 \cdot \left(\left(1 + -1 \cdot \varepsilon\right) \cdot x\right)}}}{2} \]
              6. *-commutative70.4%

                \[\leadsto \frac{1 + e^{-1 \cdot \color{blue}{\left(x \cdot \left(1 + -1 \cdot \varepsilon\right)\right)}}}{2} \]
              7. neg-mul-170.4%

                \[\leadsto \frac{1 + e^{-1 \cdot \left(x \cdot \left(1 + \color{blue}{\left(-\varepsilon\right)}\right)\right)}}{2} \]
              8. sub-neg70.4%

                \[\leadsto \frac{1 + e^{-1 \cdot \left(x \cdot \color{blue}{\left(1 - \varepsilon\right)}\right)}}{2} \]
              9. neg-mul-170.4%

                \[\leadsto \frac{1 + e^{\color{blue}{-x \cdot \left(1 - \varepsilon\right)}}}{2} \]
              10. distribute-lft-neg-in70.4%

                \[\leadsto \frac{1 + e^{\color{blue}{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
            7. Simplified70.4%

              \[\leadsto \frac{\color{blue}{1 + e^{\left(-x\right) \cdot \left(1 - \varepsilon\right)}}}{2} \]
            8. Taylor expanded in x around 0 55.2%

              \[\leadsto \frac{\color{blue}{-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 2}}{2} \]

            if 6.4000000000000002e-12 < x

            1. Initial program 98.8%

              \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
            2. Step-by-step derivation
              1. Simplified98.8%

                \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
              2. Taylor expanded in eps around 0 44.0%

                \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
              3. Step-by-step derivation
                1. div-sub44.0%

                  \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                2. rec-exp44.0%

                  \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
                3. neg-mul-144.0%

                  \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
                4. +-inverses44.0%

                  \[\leadsto \frac{\color{blue}{0}}{2} \]
              4. Simplified44.0%

                \[\leadsto \frac{\color{blue}{0}}{2} \]
            3. Recombined 2 regimes into one program.
            4. Final simplification51.7%

              \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 6.4 \cdot 10^{-12}:\\ \;\;\;\;\frac{2 - \left(1 - \varepsilon\right) \cdot x}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

            Alternative 15: 60.6% accurate, 25.0× speedup?

            \[\begin{array}{l} \mathbf{if}\;x \leq -1.5 \cdot 10^{+160}:\\ \;\;\;\;\frac{-0.25 \cdot \left(x \cdot x\right)}{\varepsilon}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
            Derivation
            1. Split input into 3 regimes
            2. if x < -1.4999999999999999e160

              1. Initial program 100.0%

                \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
              2. Step-by-step derivation
                1. div-sub100.0%

                  \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                2. +-rgt-identity100.0%

                  \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                3. div-sub100.0%

                  \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
              3. Simplified100.0%

                \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
              4. Taylor expanded in x around 0 43.5%

                \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
              5. Taylor expanded in eps around 0 47.6%

                \[\leadsto \frac{\color{blue}{\frac{\left(1 + -1 \cdot x\right) - e^{-1 \cdot x}}{\varepsilon}}}{2} \]
              6. Step-by-step derivation
                1. mul-1-neg47.6%

                  \[\leadsto \frac{\frac{\left(1 + \color{blue}{\left(-x\right)}\right) - e^{-1 \cdot x}}{\varepsilon}}{2} \]
                2. unsub-neg47.6%

                  \[\leadsto \frac{\frac{\color{blue}{\left(1 - x\right)} - e^{-1 \cdot x}}{\varepsilon}}{2} \]
                3. mul-1-neg47.6%

                  \[\leadsto \frac{\frac{\left(1 - x\right) - e^{\color{blue}{-x}}}{\varepsilon}}{2} \]
              7. Simplified47.6%

                \[\leadsto \frac{\color{blue}{\frac{\left(1 - x\right) - e^{-x}}{\varepsilon}}}{2} \]
              8. Taylor expanded in x around 0 47.6%

                \[\leadsto \color{blue}{-0.25 \cdot \frac{{x}^{2}}{\varepsilon}} \]
              9. Step-by-step derivation
                1. associate-*r/47.6%

                  \[\leadsto \color{blue}{\frac{-0.25 \cdot {x}^{2}}{\varepsilon}} \]
                2. unpow247.6%

                  \[\leadsto \frac{-0.25 \cdot \color{blue}{\left(x \cdot x\right)}}{\varepsilon} \]
              10. Simplified47.6%

                \[\leadsto \color{blue}{\frac{-0.25 \cdot \left(x \cdot x\right)}{\varepsilon}} \]

              if -1.4999999999999999e160 < x < 13000

              1. Initial program 62.7%

                \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
              2. Step-by-step derivation
                1. div-sub62.7%

                  \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                2. +-rgt-identity62.7%

                  \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                3. div-sub62.7%

                  \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
              3. Simplified62.7%

                \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
              4. Taylor expanded in x around 0 55.9%

                \[\leadsto \frac{\color{blue}{2}}{2} \]

              if 13000 < x

              1. Initial program 100.0%

                \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
              2. Step-by-step derivation
                1. Simplified100.0%

                  \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
                2. Taylor expanded in eps around 0 46.8%

                  \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                3. Step-by-step derivation
                  1. div-sub46.8%

                    \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                  2. rec-exp46.8%

                    \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
                  3. neg-mul-146.8%

                    \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
                  4. +-inverses46.8%

                    \[\leadsto \frac{\color{blue}{0}}{2} \]
                4. Simplified46.8%

                  \[\leadsto \frac{\color{blue}{0}}{2} \]
              3. Recombined 3 regimes into one program.
              4. Final simplification52.6%

                \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.5 \cdot 10^{+160}:\\ \;\;\;\;\frac{-0.25 \cdot \left(x \cdot x\right)}{\varepsilon}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

              Alternative 16: 60.7% accurate, 32.1× speedup?

              \[\begin{array}{l} \mathbf{if}\;x \leq -1:\\ \;\;\;\;\frac{\varepsilon \cdot x}{2}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
              Derivation
              1. Split input into 3 regimes
              2. if x < -1

                1. Initial program 93.5%

                  \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                2. Step-by-step derivation
                  1. div-sub93.5%

                    \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                  2. +-rgt-identity93.5%

                    \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                  3. div-sub93.5%

                    \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                3. Simplified93.4%

                  \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot {\left(e^{1 - \varepsilon}\right)}^{\left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
                4. Taylor expanded in x around 0 41.6%

                  \[\leadsto \frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot \color{blue}{\left(-1 \cdot \left(\left(1 - \varepsilon\right) \cdot x\right) + 1\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2} \]
                5. Taylor expanded in x around inf 21.9%

                  \[\leadsto \frac{\color{blue}{-1 \cdot \left(\left(\frac{1}{\varepsilon} + 1\right) \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)\right)}}{2} \]
                6. Step-by-step derivation
                  1. mul-1-neg21.9%

                    \[\leadsto \frac{\color{blue}{-\left(\frac{1}{\varepsilon} + 1\right) \cdot \left(\left(1 - \varepsilon\right) \cdot x\right)}}{2} \]
                  2. *-commutative21.9%

                    \[\leadsto \frac{-\left(\frac{1}{\varepsilon} + 1\right) \cdot \color{blue}{\left(x \cdot \left(1 - \varepsilon\right)\right)}}{2} \]
                  3. *-commutative21.9%

                    \[\leadsto \frac{-\color{blue}{\left(x \cdot \left(1 - \varepsilon\right)\right) \cdot \left(\frac{1}{\varepsilon} + 1\right)}}{2} \]
                  4. unpow-121.9%

                    \[\leadsto \frac{-\left(x \cdot \left(1 - \varepsilon\right)\right) \cdot \left(\color{blue}{{\varepsilon}^{-1}} + 1\right)}{2} \]
                  5. +-commutative21.9%

                    \[\leadsto \frac{-\left(x \cdot \left(1 - \varepsilon\right)\right) \cdot \color{blue}{\left(1 + {\varepsilon}^{-1}\right)}}{2} \]
                  6. associate-*l*21.9%

                    \[\leadsto \frac{-\color{blue}{x \cdot \left(\left(1 - \varepsilon\right) \cdot \left(1 + {\varepsilon}^{-1}\right)\right)}}{2} \]
                  7. +-commutative21.9%

                    \[\leadsto \frac{-x \cdot \left(\left(1 - \varepsilon\right) \cdot \color{blue}{\left({\varepsilon}^{-1} + 1\right)}\right)}{2} \]
                  8. unpow-121.9%

                    \[\leadsto \frac{-x \cdot \left(\left(1 - \varepsilon\right) \cdot \left(\color{blue}{\frac{1}{\varepsilon}} + 1\right)\right)}{2} \]
                  9. *-commutative21.9%

                    \[\leadsto \frac{-x \cdot \color{blue}{\left(\left(\frac{1}{\varepsilon} + 1\right) \cdot \left(1 - \varepsilon\right)\right)}}{2} \]
                  10. distribute-rgt-neg-in21.9%

                    \[\leadsto \frac{\color{blue}{x \cdot \left(-\left(\frac{1}{\varepsilon} + 1\right) \cdot \left(1 - \varepsilon\right)\right)}}{2} \]
                  11. unpow-121.9%

                    \[\leadsto \frac{x \cdot \left(-\left(\color{blue}{{\varepsilon}^{-1}} + 1\right) \cdot \left(1 - \varepsilon\right)\right)}{2} \]
                  12. +-commutative21.9%

                    \[\leadsto \frac{x \cdot \left(-\color{blue}{\left(1 + {\varepsilon}^{-1}\right)} \cdot \left(1 - \varepsilon\right)\right)}{2} \]
                  13. distribute-rgt-neg-in21.9%

                    \[\leadsto \frac{x \cdot \color{blue}{\left(\left(1 + {\varepsilon}^{-1}\right) \cdot \left(-\left(1 - \varepsilon\right)\right)\right)}}{2} \]
                7. Simplified21.9%

                  \[\leadsto \frac{\color{blue}{x \cdot \left(\left(1 - \frac{-1}{\varepsilon}\right) \cdot \left(\varepsilon + -1\right)\right)}}{2} \]
                8. Taylor expanded in eps around inf 21.7%

                  \[\leadsto \frac{x \cdot \color{blue}{\varepsilon}}{2} \]

                if -1 < x < 13000

                1. Initial program 58.3%

                  \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                2. Step-by-step derivation
                  1. div-sub58.3%

                    \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                  2. +-rgt-identity58.3%

                    \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                  3. div-sub58.3%

                    \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                3. Simplified58.3%

                  \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
                4. Taylor expanded in x around 0 65.1%

                  \[\leadsto \frac{\color{blue}{2}}{2} \]

                if 13000 < x

                1. Initial program 100.0%

                  \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                2. Step-by-step derivation
                  1. Simplified100.0%

                    \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
                  2. Taylor expanded in eps around 0 46.8%

                    \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                  3. Step-by-step derivation
                    1. div-sub46.8%

                      \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                    2. rec-exp46.8%

                      \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
                    3. neg-mul-146.8%

                      \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
                    4. +-inverses46.8%

                      \[\leadsto \frac{\color{blue}{0}}{2} \]
                  4. Simplified46.8%

                    \[\leadsto \frac{\color{blue}{0}}{2} \]
                3. Recombined 3 regimes into one program.
                4. Final simplification52.2%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1:\\ \;\;\;\;\frac{\varepsilon \cdot x}{2}\\ \mathbf{elif}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

                Alternative 17: 57.3% accurate, 74.1× speedup?

                \[\begin{array}{l} \mathbf{if}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
                Derivation
                1. Split input into 2 regimes
                2. if x < 13000

                  1. Initial program 67.0%

                    \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                  2. Step-by-step derivation
                    1. div-sub67.0%

                      \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                    2. +-rgt-identity67.0%

                      \[\leadsto \frac{\color{blue}{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0}}{2} - \frac{\left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                    3. div-sub67.0%

                      \[\leadsto \color{blue}{\frac{\left(\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} + 0\right) - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}} \]
                  3. Simplified67.0%

                    \[\leadsto \color{blue}{\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{\left(1 - \varepsilon\right) \cdot \left(-x\right)} - \left(\frac{1}{\varepsilon} + -1\right) \cdot e^{\left(1 + \varepsilon\right) \cdot \left(-x\right)}}{2}} \]
                  4. Taylor expanded in x around 0 49.8%

                    \[\leadsto \frac{\color{blue}{2}}{2} \]

                  if 13000 < x

                  1. Initial program 100.0%

                    \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                  2. Step-by-step derivation
                    1. Simplified100.0%

                      \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
                    2. Taylor expanded in eps around 0 46.8%

                      \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                    3. Step-by-step derivation
                      1. div-sub46.8%

                        \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                      2. rec-exp46.8%

                        \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
                      3. neg-mul-146.8%

                        \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
                      4. +-inverses46.8%

                        \[\leadsto \frac{\color{blue}{0}}{2} \]
                    4. Simplified46.8%

                      \[\leadsto \frac{\color{blue}{0}}{2} \]
                  3. Recombined 2 regimes into one program.
                  4. Final simplification48.9%

                    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 13000:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]

                  Alternative 18: 15.9% accurate, 227.0× speedup?

                  \[0 \]
                  Derivation
                  1. Initial program 76.5%

                    \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
                  2. Step-by-step derivation
                    1. Simplified69.8%

                      \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{x}\right)}^{\left(\varepsilon + -1\right)}, \frac{1 + \frac{-1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
                    2. Taylor expanded in eps around 0 15.0%

                      \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x} - \frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                    3. Step-by-step derivation
                      1. div-sub15.0%

                        \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\frac{1}{e^{x}}}{\varepsilon}}}{2} \]
                      2. rec-exp14.9%

                        \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{\color{blue}{e^{-x}}}{\varepsilon}}{2} \]
                      3. neg-mul-114.9%

                        \[\leadsto \frac{\frac{e^{-1 \cdot x}}{\varepsilon} - \frac{e^{\color{blue}{-1 \cdot x}}}{\varepsilon}}{2} \]
                      4. +-inverses15.2%

                        \[\leadsto \frac{\color{blue}{0}}{2} \]
                    4. Simplified15.2%

                      \[\leadsto \frac{\color{blue}{0}}{2} \]
                    5. Final simplification15.2%

                      \[\leadsto 0 \]

                    Reproduce

                    ?
                    herbie shell --seed 2023167 
                    (FPCore (x eps)
                      :name "NMSE Section 6.1 mentioned, A"
                      :precision binary64
                      (/ (- (* (+ 1.0 (/ 1.0 eps)) (exp (- (* (- 1.0 eps) x)))) (* (- (/ 1.0 eps) 1.0) (exp (- (* (+ 1.0 eps) x))))) 2.0))