Logistic distribution

Percentage Accurate: 99.5% → 99.5%
Time: 8.1s
Alternatives: 14
Speedup: 1.1×

Specification

?
\[0 \leq s \land s \leq 1.0651631\]
\[\begin{array}{l} \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\right|}{s}}\\ t_1 := 1 + t\_0\\ \frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \end{array} \end{array} \]
(FPCore (x s)
 :precision binary32
 (let* ((t_0 (exp (/ (- (fabs x)) s))) (t_1 (+ 1.0 t_0)))
   (/ t_0 (* (* s t_1) t_1))))
float code(float x, float s) {
	float t_0 = expf((-fabsf(x) / s));
	float t_1 = 1.0f + t_0;
	return t_0 / ((s * t_1) * t_1);
}
real(4) function code(x, s)
    real(4), intent (in) :: x
    real(4), intent (in) :: s
    real(4) :: t_0
    real(4) :: t_1
    t_0 = exp((-abs(x) / s))
    t_1 = 1.0e0 + t_0
    code = t_0 / ((s * t_1) * t_1)
end function
function code(x, s)
	t_0 = exp(Float32(Float32(-abs(x)) / s))
	t_1 = Float32(Float32(1.0) + t_0)
	return Float32(t_0 / Float32(Float32(s * t_1) * t_1))
end
function tmp = code(x, s)
	t_0 = exp((-abs(x) / s));
	t_1 = single(1.0) + t_0;
	tmp = t_0 / ((s * t_1) * t_1);
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := e^{\frac{-\left|x\right|}{s}}\\
t_1 := 1 + t\_0\\
\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1}
\end{array}
\end{array}

Sampling outcomes in binary32 precision:

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 14 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.

Initial Program: 99.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\right|}{s}}\\ t_1 := 1 + t\_0\\ \frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \end{array} \end{array} \]
(FPCore (x s)
 :precision binary32
 (let* ((t_0 (exp (/ (- (fabs x)) s))) (t_1 (+ 1.0 t_0)))
   (/ t_0 (* (* s t_1) t_1))))
float code(float x, float s) {
	float t_0 = expf((-fabsf(x) / s));
	float t_1 = 1.0f + t_0;
	return t_0 / ((s * t_1) * t_1);
}
real(4) function code(x, s)
    real(4), intent (in) :: x
    real(4), intent (in) :: s
    real(4) :: t_0
    real(4) :: t_1
    t_0 = exp((-abs(x) / s))
    t_1 = 1.0e0 + t_0
    code = t_0 / ((s * t_1) * t_1)
end function
function code(x, s)
	t_0 = exp(Float32(Float32(-abs(x)) / s))
	t_1 = Float32(Float32(1.0) + t_0)
	return Float32(t_0 / Float32(Float32(s * t_1) * t_1))
end
function tmp = code(x, s)
	t_0 = exp((-abs(x) / s));
	t_1 = single(1.0) + t_0;
	tmp = t_0 / ((s * t_1) * t_1);
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := e^{\frac{-\left|x\right|}{s}}\\
t_1 := 1 + t\_0\\
\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1}
\end{array}
\end{array}

Alternative 1: 99.5% accurate, 1.0× speedup?

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-x\_m}{s}}\\ \frac{t\_0}{\left(1 + t\_0\right) \cdot \left(\frac{s}{e^{\frac{x\_m}{s}}} + s\right)} \end{array} \end{array} \]
x_m = (fabs.f32 x)
(FPCore (x_m s)
 :precision binary32
 (let* ((t_0 (exp (/ (- x_m) s))))
   (/ t_0 (* (+ 1.0 t_0) (+ (/ s (exp (/ x_m s))) s)))))
x_m = fabs(x);
float code(float x_m, float s) {
	float t_0 = expf((-x_m / s));
	return t_0 / ((1.0f + t_0) * ((s / expf((x_m / s))) + s));
}
x_m = abs(x)
real(4) function code(x_m, s)
    real(4), intent (in) :: x_m
    real(4), intent (in) :: s
    real(4) :: t_0
    t_0 = exp((-x_m / s))
    code = t_0 / ((1.0e0 + t_0) * ((s / exp((x_m / s))) + s))
end function
x_m = abs(x)
function code(x_m, s)
	t_0 = exp(Float32(Float32(-x_m) / s))
	return Float32(t_0 / Float32(Float32(Float32(1.0) + t_0) * Float32(Float32(s / exp(Float32(x_m / s))) + s)))
end
x_m = abs(x);
function tmp = code(x_m, s)
	t_0 = exp((-x_m / s));
	tmp = t_0 / ((single(1.0) + t_0) * ((s / exp((x_m / s))) + s));
end
\begin{array}{l}
x_m = \left|x\right|

\\
\begin{array}{l}
t_0 := e^{\frac{-x\_m}{s}}\\
\frac{t\_0}{\left(1 + t\_0\right) \cdot \left(\frac{s}{e^{\frac{x\_m}{s}}} + s\right)}
\end{array}
\end{array}
Derivation
  1. Initial program 99.8%

    \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f32N/A

      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    2. lift-+.f32N/A

      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    3. +-commutativeN/A

      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(e^{\frac{-\left|x\right|}{s}} + 1\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    4. distribute-lft-inN/A

      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s \cdot 1\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    5. *-rgt-identityN/A

      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + \color{blue}{s}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    6. lower-+.f32N/A

      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
  4. Applied rewrites97.0%

    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
  5. Step-by-step derivation
    1. lift-/.f32N/A

      \[\leadsto \frac{e^{\color{blue}{\frac{-\left|x\right|}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    2. frac-2negN/A

      \[\leadsto \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(\left(-\left|x\right|\right)\right)}{\mathsf{neg}\left(s\right)}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    3. lift-neg.f32N/A

      \[\leadsto \frac{e^{\frac{\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\left|x\right|\right)\right)}\right)}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    4. remove-double-negN/A

      \[\leadsto \frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    5. lift-fabs.f32N/A

      \[\leadsto \frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    6. rem-sqrt-square-revN/A

      \[\leadsto \frac{e^{\frac{\color{blue}{\sqrt{x \cdot x}}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    7. sqrt-prodN/A

      \[\leadsto \frac{e^{\frac{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    8. rem-square-sqrtN/A

      \[\leadsto \frac{e^{\frac{\color{blue}{x}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    9. distribute-neg-frac2N/A

      \[\leadsto \frac{e^{\color{blue}{\mathsf{neg}\left(\frac{x}{s}\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    10. distribute-frac-negN/A

      \[\leadsto \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(x\right)}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    11. lift-neg.f32N/A

      \[\leadsto \frac{e^{\frac{\color{blue}{-x}}{s}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    12. lift-/.f3259.5

      \[\leadsto \frac{e^{\color{blue}{\frac{-x}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    13. lift-*.f32N/A

      \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
    14. *-commutativeN/A

      \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
    15. lower-*.f3259.5

      \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
  6. Applied rewrites62.3%

    \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
  7. Add Preprocessing

Alternative 2: 29.5% accurate, 0.9× speedup?

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ t_1 := 1 + t\_0\\ \mathbf{if}\;\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \leq 0:\\ \;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x\_m \cdot x\_m}{s}}{s}\\ \mathbf{else}:\\ \;\;\;\;\frac{0.25 + \frac{-0.25}{s} \cdot \left(\left(\frac{x\_m}{s} \cdot x\_m\right) \cdot 0.25\right)}{s}\\ \end{array} \end{array} \]
x_m = (fabs.f32 x)
(FPCore (x_m s)
 :precision binary32
 (let* ((t_0 (exp (/ (- (fabs x_m)) s))) (t_1 (+ 1.0 t_0)))
   (if (<= (/ t_0 (* (* s t_1) t_1)) 0.0)
     (/ (* (/ -0.0625 s) (/ (* x_m x_m) s)) s)
     (/ (+ 0.25 (* (/ -0.25 s) (* (* (/ x_m s) x_m) 0.25))) s))))
x_m = fabs(x);
float code(float x_m, float s) {
	float t_0 = expf((-fabsf(x_m) / s));
	float t_1 = 1.0f + t_0;
	float tmp;
	if ((t_0 / ((s * t_1) * t_1)) <= 0.0f) {
		tmp = ((-0.0625f / s) * ((x_m * x_m) / s)) / s;
	} else {
		tmp = (0.25f + ((-0.25f / s) * (((x_m / s) * x_m) * 0.25f))) / s;
	}
	return tmp;
}
x_m = abs(x)
real(4) function code(x_m, s)
    real(4), intent (in) :: x_m
    real(4), intent (in) :: s
    real(4) :: t_0
    real(4) :: t_1
    real(4) :: tmp
    t_0 = exp((-abs(x_m) / s))
    t_1 = 1.0e0 + t_0
    if ((t_0 / ((s * t_1) * t_1)) <= 0.0e0) then
        tmp = (((-0.0625e0) / s) * ((x_m * x_m) / s)) / s
    else
        tmp = (0.25e0 + (((-0.25e0) / s) * (((x_m / s) * x_m) * 0.25e0))) / s
    end if
    code = tmp
end function
x_m = abs(x)
function code(x_m, s)
	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
	t_1 = Float32(Float32(1.0) + t_0)
	tmp = Float32(0.0)
	if (Float32(t_0 / Float32(Float32(s * t_1) * t_1)) <= Float32(0.0))
		tmp = Float32(Float32(Float32(Float32(-0.0625) / s) * Float32(Float32(x_m * x_m) / s)) / s);
	else
		tmp = Float32(Float32(Float32(0.25) + Float32(Float32(Float32(-0.25) / s) * Float32(Float32(Float32(x_m / s) * x_m) * Float32(0.25)))) / s);
	end
	return tmp
end
x_m = abs(x);
function tmp_2 = code(x_m, s)
	t_0 = exp((-abs(x_m) / s));
	t_1 = single(1.0) + t_0;
	tmp = single(0.0);
	if ((t_0 / ((s * t_1) * t_1)) <= single(0.0))
		tmp = ((single(-0.0625) / s) * ((x_m * x_m) / s)) / s;
	else
		tmp = (single(0.25) + ((single(-0.25) / s) * (((x_m / s) * x_m) * single(0.25)))) / s;
	end
	tmp_2 = tmp;
end
\begin{array}{l}
x_m = \left|x\right|

\\
\begin{array}{l}
t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
t_1 := 1 + t\_0\\
\mathbf{if}\;\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \leq 0:\\
\;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x\_m \cdot x\_m}{s}}{s}\\

\mathbf{else}:\\
\;\;\;\;\frac{0.25 + \frac{-0.25}{s} \cdot \left(\left(\frac{x\_m}{s} \cdot x\_m\right) \cdot 0.25\right)}{s}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f32 (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)) (*.f32 (*.f32 s (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s))))) < 0.0

    1. Initial program 100.0%

      \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f32N/A

        \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
      2. lift-*.f32N/A

        \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
      3. lift-*.f32N/A

        \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
      4. associate-*l*N/A

        \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
      5. *-commutativeN/A

        \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
      6. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
      7. lower-/.f32N/A

        \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
    4. Applied rewrites76.5%

      \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
    5. Taylor expanded in x around 0

      \[\leadsto \frac{\color{blue}{e^{\mathsf{neg}\left(2 \cdot \log 2\right)} + \frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}}}}{s} \]
    6. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \frac{\color{blue}{\frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}} + e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}}{s} \]
    7. Applied rewrites4.5%

      \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{-0.25}{s}, \frac{\left(x \cdot x\right) \cdot 0.25}{s}, 0.25\right)}}{s} \]
    8. Taylor expanded in x around inf

      \[\leadsto \frac{\frac{-1}{16} \cdot \color{blue}{\frac{{x}^{2}}{{s}^{2}}}}{s} \]
    9. Step-by-step derivation
      1. Applied rewrites10.0%

        \[\leadsto \frac{\frac{-0.0625}{s} \cdot \color{blue}{\frac{x \cdot x}{s}}}{s} \]

      if 0.0 < (/.f32 (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)) (*.f32 (*.f32 s (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))))

      1. Initial program 99.1%

        \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-/.f32N/A

          \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
        2. lift-*.f32N/A

          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
        4. associate-*l*N/A

          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
        5. *-commutativeN/A

          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
        6. associate-/r*N/A

          \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
        7. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
      4. Applied rewrites24.8%

        \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
      5. Taylor expanded in x around 0

        \[\leadsto \frac{\color{blue}{e^{\mathsf{neg}\left(2 \cdot \log 2\right)} + \frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}}}}{s} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}} + e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}}{s} \]
      7. Applied rewrites87.1%

        \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{-0.25}{s}, \frac{\left(x \cdot x\right) \cdot 0.25}{s}, 0.25\right)}}{s} \]
      8. Step-by-step derivation
        1. Applied rewrites87.1%

          \[\leadsto \frac{\mathsf{fma}\left(\frac{-0.25}{s}, \color{blue}{\frac{0.25 \cdot \left(x \cdot x\right)}{s}}, 0.25\right)}{s} \]
        2. Step-by-step derivation
          1. Applied rewrites90.9%

            \[\leadsto \frac{0.25 - \color{blue}{\left(-\frac{-0.25}{s}\right) \cdot \left(\left(\frac{x}{s} \cdot x\right) \cdot 0.25\right)}}{s} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification31.8%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \leq 0:\\ \;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x \cdot x}{s}}{s}\\ \mathbf{else}:\\ \;\;\;\;\frac{0.25 + \frac{-0.25}{s} \cdot \left(\left(\frac{x}{s} \cdot x\right) \cdot 0.25\right)}{s}\\ \end{array} \]
        5. Add Preprocessing

        Alternative 3: 29.3% accurate, 0.9× speedup?

        \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ t_1 := 1 + t\_0\\ \mathbf{if}\;\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \leq 0:\\ \;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x\_m \cdot x\_m}{s}}{s}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\frac{-0.0625 \cdot \left(x\_m \cdot x\_m\right)}{s}}{s} + 0.25}{s}\\ \end{array} \end{array} \]
        x_m = (fabs.f32 x)
        (FPCore (x_m s)
         :precision binary32
         (let* ((t_0 (exp (/ (- (fabs x_m)) s))) (t_1 (+ 1.0 t_0)))
           (if (<= (/ t_0 (* (* s t_1) t_1)) 0.0)
             (/ (* (/ -0.0625 s) (/ (* x_m x_m) s)) s)
             (/ (+ (/ (/ (* -0.0625 (* x_m x_m)) s) s) 0.25) s))))
        x_m = fabs(x);
        float code(float x_m, float s) {
        	float t_0 = expf((-fabsf(x_m) / s));
        	float t_1 = 1.0f + t_0;
        	float tmp;
        	if ((t_0 / ((s * t_1) * t_1)) <= 0.0f) {
        		tmp = ((-0.0625f / s) * ((x_m * x_m) / s)) / s;
        	} else {
        		tmp = ((((-0.0625f * (x_m * x_m)) / s) / s) + 0.25f) / s;
        	}
        	return tmp;
        }
        
        x_m = abs(x)
        real(4) function code(x_m, s)
            real(4), intent (in) :: x_m
            real(4), intent (in) :: s
            real(4) :: t_0
            real(4) :: t_1
            real(4) :: tmp
            t_0 = exp((-abs(x_m) / s))
            t_1 = 1.0e0 + t_0
            if ((t_0 / ((s * t_1) * t_1)) <= 0.0e0) then
                tmp = (((-0.0625e0) / s) * ((x_m * x_m) / s)) / s
            else
                tmp = (((((-0.0625e0) * (x_m * x_m)) / s) / s) + 0.25e0) / s
            end if
            code = tmp
        end function
        
        x_m = abs(x)
        function code(x_m, s)
        	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
        	t_1 = Float32(Float32(1.0) + t_0)
        	tmp = Float32(0.0)
        	if (Float32(t_0 / Float32(Float32(s * t_1) * t_1)) <= Float32(0.0))
        		tmp = Float32(Float32(Float32(Float32(-0.0625) / s) * Float32(Float32(x_m * x_m) / s)) / s);
        	else
        		tmp = Float32(Float32(Float32(Float32(Float32(Float32(-0.0625) * Float32(x_m * x_m)) / s) / s) + Float32(0.25)) / s);
        	end
        	return tmp
        end
        
        x_m = abs(x);
        function tmp_2 = code(x_m, s)
        	t_0 = exp((-abs(x_m) / s));
        	t_1 = single(1.0) + t_0;
        	tmp = single(0.0);
        	if ((t_0 / ((s * t_1) * t_1)) <= single(0.0))
        		tmp = ((single(-0.0625) / s) * ((x_m * x_m) / s)) / s;
        	else
        		tmp = ((((single(-0.0625) * (x_m * x_m)) / s) / s) + single(0.25)) / s;
        	end
        	tmp_2 = tmp;
        end
        
        \begin{array}{l}
        x_m = \left|x\right|
        
        \\
        \begin{array}{l}
        t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
        t_1 := 1 + t\_0\\
        \mathbf{if}\;\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \leq 0:\\
        \;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x\_m \cdot x\_m}{s}}{s}\\
        
        \mathbf{else}:\\
        \;\;\;\;\frac{\frac{\frac{-0.0625 \cdot \left(x\_m \cdot x\_m\right)}{s}}{s} + 0.25}{s}\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (/.f32 (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)) (*.f32 (*.f32 s (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s))))) < 0.0

          1. Initial program 100.0%

            \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-/.f32N/A

              \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
            2. lift-*.f32N/A

              \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
            3. lift-*.f32N/A

              \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
            4. associate-*l*N/A

              \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
            5. *-commutativeN/A

              \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
            6. associate-/r*N/A

              \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
            7. lower-/.f32N/A

              \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
          4. Applied rewrites76.5%

            \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
          5. Taylor expanded in x around 0

            \[\leadsto \frac{\color{blue}{e^{\mathsf{neg}\left(2 \cdot \log 2\right)} + \frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}}}}{s} \]
          6. Step-by-step derivation
            1. +-commutativeN/A

              \[\leadsto \frac{\color{blue}{\frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}} + e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}}{s} \]
          7. Applied rewrites4.5%

            \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{-0.25}{s}, \frac{\left(x \cdot x\right) \cdot 0.25}{s}, 0.25\right)}}{s} \]
          8. Taylor expanded in x around inf

            \[\leadsto \frac{\frac{-1}{16} \cdot \color{blue}{\frac{{x}^{2}}{{s}^{2}}}}{s} \]
          9. Step-by-step derivation
            1. Applied rewrites10.0%

              \[\leadsto \frac{\frac{-0.0625}{s} \cdot \color{blue}{\frac{x \cdot x}{s}}}{s} \]

            if 0.0 < (/.f32 (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)) (*.f32 (*.f32 s (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))))

            1. Initial program 99.1%

              \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-/.f32N/A

                \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
              2. lift-*.f32N/A

                \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
              3. lift-*.f32N/A

                \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
              4. associate-*l*N/A

                \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
              5. *-commutativeN/A

                \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
              6. associate-/r*N/A

                \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
              7. lower-/.f32N/A

                \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
            4. Applied rewrites24.8%

              \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
            5. Taylor expanded in x around 0

              \[\leadsto \frac{\color{blue}{e^{\mathsf{neg}\left(2 \cdot \log 2\right)} + \frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}}}}{s} \]
            6. Step-by-step derivation
              1. +-commutativeN/A

                \[\leadsto \frac{\color{blue}{\frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}} + e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}}{s} \]
            7. Applied rewrites88.6%

              \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{-0.25}{s}, \frac{\left(x \cdot x\right) \cdot 0.25}{s}, 0.25\right)}}{s} \]
            8. Step-by-step derivation
              1. Applied rewrites90.1%

                \[\leadsto \frac{\frac{\frac{-0.0625 \cdot \left(x \cdot x\right)}{s}}{s} + \color{blue}{0.25}}{s} \]
            9. Recombined 2 regimes into one program.
            10. Add Preprocessing

            Alternative 4: 29.0% accurate, 0.9× speedup?

            \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ t_1 := 1 + t\_0\\ \mathbf{if}\;\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \leq 0:\\ \;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x\_m \cdot x\_m}{s}}{s}\\ \mathbf{else}:\\ \;\;\;\;\frac{0.25}{s}\\ \end{array} \end{array} \]
            x_m = (fabs.f32 x)
            (FPCore (x_m s)
             :precision binary32
             (let* ((t_0 (exp (/ (- (fabs x_m)) s))) (t_1 (+ 1.0 t_0)))
               (if (<= (/ t_0 (* (* s t_1) t_1)) 0.0)
                 (/ (* (/ -0.0625 s) (/ (* x_m x_m) s)) s)
                 (/ 0.25 s))))
            x_m = fabs(x);
            float code(float x_m, float s) {
            	float t_0 = expf((-fabsf(x_m) / s));
            	float t_1 = 1.0f + t_0;
            	float tmp;
            	if ((t_0 / ((s * t_1) * t_1)) <= 0.0f) {
            		tmp = ((-0.0625f / s) * ((x_m * x_m) / s)) / s;
            	} else {
            		tmp = 0.25f / s;
            	}
            	return tmp;
            }
            
            x_m = abs(x)
            real(4) function code(x_m, s)
                real(4), intent (in) :: x_m
                real(4), intent (in) :: s
                real(4) :: t_0
                real(4) :: t_1
                real(4) :: tmp
                t_0 = exp((-abs(x_m) / s))
                t_1 = 1.0e0 + t_0
                if ((t_0 / ((s * t_1) * t_1)) <= 0.0e0) then
                    tmp = (((-0.0625e0) / s) * ((x_m * x_m) / s)) / s
                else
                    tmp = 0.25e0 / s
                end if
                code = tmp
            end function
            
            x_m = abs(x)
            function code(x_m, s)
            	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
            	t_1 = Float32(Float32(1.0) + t_0)
            	tmp = Float32(0.0)
            	if (Float32(t_0 / Float32(Float32(s * t_1) * t_1)) <= Float32(0.0))
            		tmp = Float32(Float32(Float32(Float32(-0.0625) / s) * Float32(Float32(x_m * x_m) / s)) / s);
            	else
            		tmp = Float32(Float32(0.25) / s);
            	end
            	return tmp
            end
            
            x_m = abs(x);
            function tmp_2 = code(x_m, s)
            	t_0 = exp((-abs(x_m) / s));
            	t_1 = single(1.0) + t_0;
            	tmp = single(0.0);
            	if ((t_0 / ((s * t_1) * t_1)) <= single(0.0))
            		tmp = ((single(-0.0625) / s) * ((x_m * x_m) / s)) / s;
            	else
            		tmp = single(0.25) / s;
            	end
            	tmp_2 = tmp;
            end
            
            \begin{array}{l}
            x_m = \left|x\right|
            
            \\
            \begin{array}{l}
            t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
            t_1 := 1 + t\_0\\
            \mathbf{if}\;\frac{t\_0}{\left(s \cdot t\_1\right) \cdot t\_1} \leq 0:\\
            \;\;\;\;\frac{\frac{-0.0625}{s} \cdot \frac{x\_m \cdot x\_m}{s}}{s}\\
            
            \mathbf{else}:\\
            \;\;\;\;\frac{0.25}{s}\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if (/.f32 (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)) (*.f32 (*.f32 s (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s))))) < 0.0

              1. Initial program 100.0%

                \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
              2. Add Preprocessing
              3. Step-by-step derivation
                1. lift-/.f32N/A

                  \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                2. lift-*.f32N/A

                  \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                3. lift-*.f32N/A

                  \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                4. associate-*l*N/A

                  \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
                5. *-commutativeN/A

                  \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
                6. associate-/r*N/A

                  \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
                7. lower-/.f32N/A

                  \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
              4. Applied rewrites76.5%

                \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
              5. Taylor expanded in x around 0

                \[\leadsto \frac{\color{blue}{e^{\mathsf{neg}\left(2 \cdot \log 2\right)} + \frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}}}}{s} \]
              6. Step-by-step derivation
                1. +-commutativeN/A

                  \[\leadsto \frac{\color{blue}{\frac{-1}{4} \cdot \frac{{x}^{2} \cdot e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}{{s}^{2}} + e^{\mathsf{neg}\left(2 \cdot \log 2\right)}}}{s} \]
              7. Applied rewrites4.5%

                \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{-0.25}{s}, \frac{\left(x \cdot x\right) \cdot 0.25}{s}, 0.25\right)}}{s} \]
              8. Taylor expanded in x around inf

                \[\leadsto \frac{\frac{-1}{16} \cdot \color{blue}{\frac{{x}^{2}}{{s}^{2}}}}{s} \]
              9. Step-by-step derivation
                1. Applied rewrites10.0%

                  \[\leadsto \frac{\frac{-0.0625}{s} \cdot \color{blue}{\frac{x \cdot x}{s}}}{s} \]

                if 0.0 < (/.f32 (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)) (*.f32 (*.f32 s (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (fabs.f32 x)) s)))))

                1. Initial program 99.1%

                  \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                2. Add Preprocessing
                3. Taylor expanded in s around inf

                  \[\leadsto \color{blue}{\frac{\frac{1}{4}}{s}} \]
                4. Step-by-step derivation
                  1. lower-/.f3288.6

                    \[\leadsto \color{blue}{\frac{0.25}{s}} \]
                5. Applied rewrites88.6%

                  \[\leadsto \color{blue}{\frac{0.25}{s}} \]
              10. Recombined 2 regimes into one program.
              11. Add Preprocessing

              Alternative 5: 99.5% accurate, 1.1× speedup?

              \[\begin{array}{l} x_m = \left|x\right| \\ \frac{\frac{e^{\frac{-x\_m}{s}}}{s}}{{\left(1 + e^{\frac{-\left|x\_m\right|}{s}}\right)}^{2}} \end{array} \]
              x_m = (fabs.f32 x)
              (FPCore (x_m s)
               :precision binary32
               (/ (/ (exp (/ (- x_m) s)) s) (pow (+ 1.0 (exp (/ (- (fabs x_m)) s))) 2.0)))
              x_m = fabs(x);
              float code(float x_m, float s) {
              	return (expf((-x_m / s)) / s) / powf((1.0f + expf((-fabsf(x_m) / s))), 2.0f);
              }
              
              x_m = abs(x)
              real(4) function code(x_m, s)
                  real(4), intent (in) :: x_m
                  real(4), intent (in) :: s
                  code = (exp((-x_m / s)) / s) / ((1.0e0 + exp((-abs(x_m) / s))) ** 2.0e0)
              end function
              
              x_m = abs(x)
              function code(x_m, s)
              	return Float32(Float32(exp(Float32(Float32(-x_m) / s)) / s) / (Float32(Float32(1.0) + exp(Float32(Float32(-abs(x_m)) / s))) ^ Float32(2.0)))
              end
              
              x_m = abs(x);
              function tmp = code(x_m, s)
              	tmp = (exp((-x_m / s)) / s) / ((single(1.0) + exp((-abs(x_m) / s))) ^ single(2.0));
              end
              
              \begin{array}{l}
              x_m = \left|x\right|
              
              \\
              \frac{\frac{e^{\frac{-x\_m}{s}}}{s}}{{\left(1 + e^{\frac{-\left|x\_m\right|}{s}}\right)}^{2}}
              \end{array}
              
              Derivation
              1. Initial program 99.8%

                \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
              2. Add Preprocessing
              3. Taylor expanded in x around 0

                \[\leadsto \color{blue}{\frac{e^{-1 \cdot \frac{\left|x\right|}{s}}}{s \cdot {\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}}} \]
              4. Step-by-step derivation
                1. associate-/r*N/A

                  \[\leadsto \color{blue}{\frac{\frac{e^{-1 \cdot \frac{\left|x\right|}{s}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}}} \]
                2. lower-/.f32N/A

                  \[\leadsto \color{blue}{\frac{\frac{e^{-1 \cdot \frac{\left|x\right|}{s}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}}} \]
                3. lower-/.f32N/A

                  \[\leadsto \frac{\color{blue}{\frac{e^{-1 \cdot \frac{\left|x\right|}{s}}}{s}}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                4. lower-exp.f32N/A

                  \[\leadsto \frac{\frac{\color{blue}{e^{-1 \cdot \frac{\left|x\right|}{s}}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                5. mul-1-negN/A

                  \[\leadsto \frac{\frac{e^{\color{blue}{\mathsf{neg}\left(\frac{\left|x\right|}{s}\right)}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                6. distribute-neg-frac2N/A

                  \[\leadsto \frac{\frac{e^{\color{blue}{\frac{\left|x\right|}{\mathsf{neg}\left(s\right)}}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                7. lower-/.f32N/A

                  \[\leadsto \frac{\frac{e^{\color{blue}{\frac{\left|x\right|}{\mathsf{neg}\left(s\right)}}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                8. lower-fabs.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                9. lower-neg.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{\color{blue}{-s}}}}{s}}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}} \]
                10. lower-pow.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{\color{blue}{{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}^{2}}} \]
                11. lower-+.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\color{blue}{\left(1 + e^{-1 \cdot \frac{\left|x\right|}{s}}\right)}}^{2}} \]
                12. lower-exp.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + \color{blue}{e^{-1 \cdot \frac{\left|x\right|}{s}}}\right)}^{2}} \]
                13. mul-1-negN/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + e^{\color{blue}{\mathsf{neg}\left(\frac{\left|x\right|}{s}\right)}}\right)}^{2}} \]
                14. distribute-neg-frac2N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + e^{\color{blue}{\frac{\left|x\right|}{\mathsf{neg}\left(s\right)}}}\right)}^{2}} \]
                15. lower-/.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + e^{\color{blue}{\frac{\left|x\right|}{\mathsf{neg}\left(s\right)}}}\right)}^{2}} \]
                16. lower-fabs.f32N/A

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}\right)}^{2}} \]
                17. lower-neg.f3299.8

                  \[\leadsto \frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + e^{\frac{\left|x\right|}{\color{blue}{-s}}}\right)}^{2}} \]
              5. Applied rewrites99.8%

                \[\leadsto \color{blue}{\frac{\frac{e^{\frac{\left|x\right|}{-s}}}{s}}{{\left(1 + e^{\frac{\left|x\right|}{-s}}\right)}^{2}}} \]
              6. Step-by-step derivation
                1. Applied rewrites60.4%

                  \[\leadsto \frac{\frac{e^{\frac{-x}{s}}}{s}}{{\color{blue}{\left(1 + e^{\frac{\left|x\right|}{-s}}\right)}}^{2}} \]
                2. Final simplification60.4%

                  \[\leadsto \frac{\frac{e^{\frac{-x}{s}}}{s}}{{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)}^{2}} \]
                3. Add Preprocessing

                Alternative 6: 99.5% accurate, 1.1× speedup?

                \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := \frac{-x\_m}{s}\\ \frac{e^{t\_0 - \log \left(1 + e^{t\_0}\right) \cdot 2}}{s} \end{array} \end{array} \]
                x_m = (fabs.f32 x)
                (FPCore (x_m s)
                 :precision binary32
                 (let* ((t_0 (/ (- x_m) s)))
                   (/ (exp (- t_0 (* (log (+ 1.0 (exp t_0))) 2.0))) s)))
                x_m = fabs(x);
                float code(float x_m, float s) {
                	float t_0 = -x_m / s;
                	return expf((t_0 - (logf((1.0f + expf(t_0))) * 2.0f))) / s;
                }
                
                x_m = abs(x)
                real(4) function code(x_m, s)
                    real(4), intent (in) :: x_m
                    real(4), intent (in) :: s
                    real(4) :: t_0
                    t_0 = -x_m / s
                    code = exp((t_0 - (log((1.0e0 + exp(t_0))) * 2.0e0))) / s
                end function
                
                x_m = abs(x)
                function code(x_m, s)
                	t_0 = Float32(Float32(-x_m) / s)
                	return Float32(exp(Float32(t_0 - Float32(log(Float32(Float32(1.0) + exp(t_0))) * Float32(2.0)))) / s)
                end
                
                x_m = abs(x);
                function tmp = code(x_m, s)
                	t_0 = -x_m / s;
                	tmp = exp((t_0 - (log((single(1.0) + exp(t_0))) * single(2.0)))) / s;
                end
                
                \begin{array}{l}
                x_m = \left|x\right|
                
                \\
                \begin{array}{l}
                t_0 := \frac{-x\_m}{s}\\
                \frac{e^{t\_0 - \log \left(1 + e^{t\_0}\right) \cdot 2}}{s}
                \end{array}
                \end{array}
                
                Derivation
                1. Initial program 99.8%

                  \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-/.f32N/A

                    \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                  2. lift-*.f32N/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                  3. lift-*.f32N/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  4. associate-*l*N/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
                  5. *-commutativeN/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
                  6. associate-/r*N/A

                    \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
                  7. lower-/.f32N/A

                    \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
                4. Applied rewrites62.8%

                  \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
                5. Step-by-step derivation
                  1. lift-/.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\color{blue}{\frac{-x}{s}}}\right) \cdot 2}}{s} \]
                  2. frac-2negN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\color{blue}{\frac{\mathsf{neg}\left(\left(-x\right)\right)}{\mathsf{neg}\left(s\right)}}}\right) \cdot 2}}{s} \]
                  3. lift-neg.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(x\right)\right)}\right)}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  4. remove-double-negN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\color{blue}{x}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  5. rem-square-sqrtN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  6. sqrt-prodN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\color{blue}{\sqrt{x \cdot x}}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  7. rem-sqrt-square-revN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  8. lift-fabs.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  9. distribute-frac-neg2N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\color{blue}{\mathsf{neg}\left(\frac{\left|x\right|}{s}\right)}}\right) \cdot 2}}{s} \]
                  10. distribute-frac-negN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\color{blue}{\frac{\mathsf{neg}\left(\left|x\right|\right)}{s}}}\right) \cdot 2}}{s} \]
                  11. lift-neg.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{\color{blue}{-\left|x\right|}}{s}}\right) \cdot 2}}{s} \]
                  12. lift-/.f3243.4

                    \[\leadsto \frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\color{blue}{\frac{-\left|x\right|}{s}}}\right) \cdot 2}}{s} \]
                  13. lower-log1p.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \color{blue}{\log \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \cdot 2}}{s} \]
                  14. lift-+.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \cdot 2}}{s} \]
                  15. lower-log.f3260.5

                    \[\leadsto \frac{e^{\frac{-x}{s} - \color{blue}{\log \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \cdot 2}}{s} \]
                  16. lift-/.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\color{blue}{\frac{-\left|x\right|}{s}}}\right) \cdot 2}}{s} \]
                  17. frac-2negN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\color{blue}{\frac{\mathsf{neg}\left(\left(-\left|x\right|\right)\right)}{\mathsf{neg}\left(s\right)}}}\right) \cdot 2}}{s} \]
                  18. lift-neg.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\frac{\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\left|x\right|\right)\right)}\right)}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  19. remove-double-negN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  20. lift-fabs.f32N/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  21. rem-sqrt-square-revN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\frac{\color{blue}{\sqrt{x \cdot x}}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  22. sqrt-prodN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\frac{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                  23. rem-square-sqrtN/A

                    \[\leadsto \frac{e^{\frac{-x}{s} - \log \left(1 + e^{\frac{\color{blue}{x}}{\mathsf{neg}\left(s\right)}}\right) \cdot 2}}{s} \]
                6. Applied rewrites82.5%

                  \[\leadsto \frac{e^{\frac{-x}{s} - \color{blue}{\log \left(1 + e^{\frac{-x}{s}}\right)} \cdot 2}}{s} \]
                7. Add Preprocessing

                Alternative 7: 97.1% accurate, 1.3× speedup?

                \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ \frac{t\_0}{\left(\left(\frac{\left(\frac{x\_m}{s} \cdot x\_m\right) \cdot 0.5 - x\_m}{s} - -1\right) \cdot s + s\right) \cdot \left(1 + t\_0\right)} \end{array} \end{array} \]
                x_m = (fabs.f32 x)
                (FPCore (x_m s)
                 :precision binary32
                 (let* ((t_0 (exp (/ (- (fabs x_m)) s))))
                   (/
                    t_0
                    (*
                     (+ (* (- (/ (- (* (* (/ x_m s) x_m) 0.5) x_m) s) -1.0) s) s)
                     (+ 1.0 t_0)))))
                x_m = fabs(x);
                float code(float x_m, float s) {
                	float t_0 = expf((-fabsf(x_m) / s));
                	return t_0 / (((((((((x_m / s) * x_m) * 0.5f) - x_m) / s) - -1.0f) * s) + s) * (1.0f + t_0));
                }
                
                x_m = abs(x)
                real(4) function code(x_m, s)
                    real(4), intent (in) :: x_m
                    real(4), intent (in) :: s
                    real(4) :: t_0
                    t_0 = exp((-abs(x_m) / s))
                    code = t_0 / (((((((((x_m / s) * x_m) * 0.5e0) - x_m) / s) - (-1.0e0)) * s) + s) * (1.0e0 + t_0))
                end function
                
                x_m = abs(x)
                function code(x_m, s)
                	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
                	return Float32(t_0 / Float32(Float32(Float32(Float32(Float32(Float32(Float32(Float32(Float32(x_m / s) * x_m) * Float32(0.5)) - x_m) / s) - Float32(-1.0)) * s) + s) * Float32(Float32(1.0) + t_0)))
                end
                
                x_m = abs(x);
                function tmp = code(x_m, s)
                	t_0 = exp((-abs(x_m) / s));
                	tmp = t_0 / (((((((((x_m / s) * x_m) * single(0.5)) - x_m) / s) - single(-1.0)) * s) + s) * (single(1.0) + t_0));
                end
                
                \begin{array}{l}
                x_m = \left|x\right|
                
                \\
                \begin{array}{l}
                t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
                \frac{t\_0}{\left(\left(\frac{\left(\frac{x\_m}{s} \cdot x\_m\right) \cdot 0.5 - x\_m}{s} - -1\right) \cdot s + s\right) \cdot \left(1 + t\_0\right)}
                \end{array}
                \end{array}
                
                Derivation
                1. Initial program 99.8%

                  \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. lift-*.f32N/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  2. lift-+.f32N/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  3. +-commutativeN/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(e^{\frac{-\left|x\right|}{s}} + 1\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  4. distribute-lft-inN/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s \cdot 1\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  5. *-rgt-identityN/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + \color{blue}{s}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  6. lower-+.f32N/A

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                4. Applied rewrites97.0%

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

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

                  \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\color{blue}{\left(\frac{\frac{x \cdot x}{s} \cdot 0.5 - x}{-s} - 1\right) \cdot \left(-s\right)} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                7. Step-by-step derivation
                  1. Applied rewrites96.1%

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\left(\frac{\left(\frac{x}{s} \cdot x\right) \cdot 0.5 - x}{-s} - 1\right) \cdot \left(-s\right) + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  2. Final simplification96.1%

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\left(\frac{\left(\frac{x}{s} \cdot x\right) \cdot 0.5 - x}{s} - -1\right) \cdot s + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  3. Add Preprocessing

                  Alternative 8: 97.0% accurate, 1.4× speedup?

                  \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-x\_m}{s}}\\ \frac{t\_0}{\left(1 + t\_0\right) \cdot \left(\frac{s}{\frac{x\_m}{s} + 1} + s\right)} \end{array} \end{array} \]
                  x_m = (fabs.f32 x)
                  (FPCore (x_m s)
                   :precision binary32
                   (let* ((t_0 (exp (/ (- x_m) s))))
                     (/ t_0 (* (+ 1.0 t_0) (+ (/ s (+ (/ x_m s) 1.0)) s)))))
                  x_m = fabs(x);
                  float code(float x_m, float s) {
                  	float t_0 = expf((-x_m / s));
                  	return t_0 / ((1.0f + t_0) * ((s / ((x_m / s) + 1.0f)) + s));
                  }
                  
                  x_m = abs(x)
                  real(4) function code(x_m, s)
                      real(4), intent (in) :: x_m
                      real(4), intent (in) :: s
                      real(4) :: t_0
                      t_0 = exp((-x_m / s))
                      code = t_0 / ((1.0e0 + t_0) * ((s / ((x_m / s) + 1.0e0)) + s))
                  end function
                  
                  x_m = abs(x)
                  function code(x_m, s)
                  	t_0 = exp(Float32(Float32(-x_m) / s))
                  	return Float32(t_0 / Float32(Float32(Float32(1.0) + t_0) * Float32(Float32(s / Float32(Float32(x_m / s) + Float32(1.0))) + s)))
                  end
                  
                  x_m = abs(x);
                  function tmp = code(x_m, s)
                  	t_0 = exp((-x_m / s));
                  	tmp = t_0 / ((single(1.0) + t_0) * ((s / ((x_m / s) + single(1.0))) + s));
                  end
                  
                  \begin{array}{l}
                  x_m = \left|x\right|
                  
                  \\
                  \begin{array}{l}
                  t_0 := e^{\frac{-x\_m}{s}}\\
                  \frac{t\_0}{\left(1 + t\_0\right) \cdot \left(\frac{s}{\frac{x\_m}{s} + 1} + s\right)}
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Initial program 99.8%

                    \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-*.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    2. lift-+.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    3. +-commutativeN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(e^{\frac{-\left|x\right|}{s}} + 1\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    4. distribute-lft-inN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s \cdot 1\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    5. *-rgt-identityN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + \color{blue}{s}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    6. lower-+.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  4. Applied rewrites97.0%

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  5. Step-by-step derivation
                    1. lift-/.f32N/A

                      \[\leadsto \frac{e^{\color{blue}{\frac{-\left|x\right|}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    2. frac-2negN/A

                      \[\leadsto \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(\left(-\left|x\right|\right)\right)}{\mathsf{neg}\left(s\right)}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    3. lift-neg.f32N/A

                      \[\leadsto \frac{e^{\frac{\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\left|x\right|\right)\right)}\right)}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    4. remove-double-negN/A

                      \[\leadsto \frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    5. lift-fabs.f32N/A

                      \[\leadsto \frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    6. rem-sqrt-square-revN/A

                      \[\leadsto \frac{e^{\frac{\color{blue}{\sqrt{x \cdot x}}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    7. sqrt-prodN/A

                      \[\leadsto \frac{e^{\frac{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    8. rem-square-sqrtN/A

                      \[\leadsto \frac{e^{\frac{\color{blue}{x}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    9. distribute-neg-frac2N/A

                      \[\leadsto \frac{e^{\color{blue}{\mathsf{neg}\left(\frac{x}{s}\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    10. distribute-frac-negN/A

                      \[\leadsto \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(x\right)}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    11. lift-neg.f32N/A

                      \[\leadsto \frac{e^{\frac{\color{blue}{-x}}{s}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    12. lift-/.f3259.5

                      \[\leadsto \frac{e^{\color{blue}{\frac{-x}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    13. lift-*.f32N/A

                      \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                    14. *-commutativeN/A

                      \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
                    15. lower-*.f3259.5

                      \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
                  6. Applied rewrites62.3%

                    \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
                  7. Taylor expanded in x around 0

                    \[\leadsto \frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{\color{blue}{1 + \frac{x}{s}}} + s\right)} \]
                  8. Step-by-step derivation
                    1. +-commutativeN/A

                      \[\leadsto \frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{\color{blue}{\frac{x}{s} + 1}} + s\right)} \]
                    2. lower-+.f32N/A

                      \[\leadsto \frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{\color{blue}{\frac{x}{s} + 1}} + s\right)} \]
                    3. lower-/.f3259.4

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

                    \[\leadsto \frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{\color{blue}{\frac{x}{s} + 1}} + s\right)} \]
                  10. Add Preprocessing

                  Alternative 9: 96.2% accurate, 1.4× speedup?

                  \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ \frac{t\_0}{\left(s \cdot \left(1 + t\_0\right)\right) \cdot \left(2 - \frac{\left|x\_m\right|}{s}\right)} \end{array} \end{array} \]
                  x_m = (fabs.f32 x)
                  (FPCore (x_m s)
                   :precision binary32
                   (let* ((t_0 (exp (/ (- (fabs x_m)) s))))
                     (/ t_0 (* (* s (+ 1.0 t_0)) (- 2.0 (/ (fabs x_m) s))))))
                  x_m = fabs(x);
                  float code(float x_m, float s) {
                  	float t_0 = expf((-fabsf(x_m) / s));
                  	return t_0 / ((s * (1.0f + t_0)) * (2.0f - (fabsf(x_m) / s)));
                  }
                  
                  x_m = abs(x)
                  real(4) function code(x_m, s)
                      real(4), intent (in) :: x_m
                      real(4), intent (in) :: s
                      real(4) :: t_0
                      t_0 = exp((-abs(x_m) / s))
                      code = t_0 / ((s * (1.0e0 + t_0)) * (2.0e0 - (abs(x_m) / s)))
                  end function
                  
                  x_m = abs(x)
                  function code(x_m, s)
                  	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
                  	return Float32(t_0 / Float32(Float32(s * Float32(Float32(1.0) + t_0)) * Float32(Float32(2.0) - Float32(abs(x_m) / s))))
                  end
                  
                  x_m = abs(x);
                  function tmp = code(x_m, s)
                  	t_0 = exp((-abs(x_m) / s));
                  	tmp = t_0 / ((s * (single(1.0) + t_0)) * (single(2.0) - (abs(x_m) / s)));
                  end
                  
                  \begin{array}{l}
                  x_m = \left|x\right|
                  
                  \\
                  \begin{array}{l}
                  t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
                  \frac{t\_0}{\left(s \cdot \left(1 + t\_0\right)\right) \cdot \left(2 - \frac{\left|x\_m\right|}{s}\right)}
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Initial program 99.8%

                    \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  2. Add Preprocessing
                  3. Taylor expanded in s around inf

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \color{blue}{\left(2 + -1 \cdot \frac{\left|x\right|}{s}\right)}} \]
                  4. Step-by-step derivation
                    1. fp-cancel-sign-sub-invN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \color{blue}{\left(2 - \left(\mathsf{neg}\left(-1\right)\right) \cdot \frac{\left|x\right|}{s}\right)}} \]
                    2. metadata-evalN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(2 - \color{blue}{1} \cdot \frac{\left|x\right|}{s}\right)} \]
                    3. *-lft-identityN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(2 - \color{blue}{\frac{\left|x\right|}{s}}\right)} \]
                    4. lower--.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \color{blue}{\left(2 - \frac{\left|x\right|}{s}\right)}} \]
                    5. lower-/.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(2 - \color{blue}{\frac{\left|x\right|}{s}}\right)} \]
                    6. lower-fabs.f3296.6

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(2 - \frac{\color{blue}{\left|x\right|}}{s}\right)} \]
                  5. Applied rewrites96.6%

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \color{blue}{\left(2 - \frac{\left|x\right|}{s}\right)}} \]
                  6. Add Preprocessing

                  Alternative 10: 96.2% accurate, 1.5× speedup?

                  \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ \frac{t\_0}{\left(\left(s - x\_m\right) + s\right) \cdot \left(1 + t\_0\right)} \end{array} \end{array} \]
                  x_m = (fabs.f32 x)
                  (FPCore (x_m s)
                   :precision binary32
                   (let* ((t_0 (exp (/ (- (fabs x_m)) s))))
                     (/ t_0 (* (+ (- s x_m) s) (+ 1.0 t_0)))))
                  x_m = fabs(x);
                  float code(float x_m, float s) {
                  	float t_0 = expf((-fabsf(x_m) / s));
                  	return t_0 / (((s - x_m) + s) * (1.0f + t_0));
                  }
                  
                  x_m = abs(x)
                  real(4) function code(x_m, s)
                      real(4), intent (in) :: x_m
                      real(4), intent (in) :: s
                      real(4) :: t_0
                      t_0 = exp((-abs(x_m) / s))
                      code = t_0 / (((s - x_m) + s) * (1.0e0 + t_0))
                  end function
                  
                  x_m = abs(x)
                  function code(x_m, s)
                  	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
                  	return Float32(t_0 / Float32(Float32(Float32(s - x_m) + s) * Float32(Float32(1.0) + t_0)))
                  end
                  
                  x_m = abs(x);
                  function tmp = code(x_m, s)
                  	t_0 = exp((-abs(x_m) / s));
                  	tmp = t_0 / (((s - x_m) + s) * (single(1.0) + t_0));
                  end
                  
                  \begin{array}{l}
                  x_m = \left|x\right|
                  
                  \\
                  \begin{array}{l}
                  t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
                  \frac{t\_0}{\left(\left(s - x\_m\right) + s\right) \cdot \left(1 + t\_0\right)}
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Initial program 99.8%

                    \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-*.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    2. lift-+.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    3. +-commutativeN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(e^{\frac{-\left|x\right|}{s}} + 1\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    4. distribute-lft-inN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s \cdot 1\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    5. *-rgt-identityN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + \color{blue}{s}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    6. lower-+.f32N/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  4. Applied rewrites97.0%

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

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\color{blue}{\left(s + -1 \cdot x\right)} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  6. Step-by-step derivation
                    1. mul-1-negN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\left(s + \color{blue}{\left(\mathsf{neg}\left(x\right)\right)}\right) + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    2. +-commutativeN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + s\right)} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    3. mul-1-negN/A

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\left(\color{blue}{-1 \cdot x} + s\right) + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    4. lower-fma.f3275.6

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\color{blue}{\mathsf{fma}\left(-1, x, s\right)} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  7. Applied rewrites75.9%

                    \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(\color{blue}{\mathsf{fma}\left(-1, x, s\right)} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                  8. Step-by-step derivation
                    1. Applied rewrites95.8%

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

                    Alternative 11: 95.3% accurate, 1.5× speedup?

                    \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\ \frac{t\_0}{\left(s \cdot \left(1 + t\_0\right)\right) \cdot 2} \end{array} \end{array} \]
                    x_m = (fabs.f32 x)
                    (FPCore (x_m s)
                     :precision binary32
                     (let* ((t_0 (exp (/ (- (fabs x_m)) s)))) (/ t_0 (* (* s (+ 1.0 t_0)) 2.0))))
                    x_m = fabs(x);
                    float code(float x_m, float s) {
                    	float t_0 = expf((-fabsf(x_m) / s));
                    	return t_0 / ((s * (1.0f + t_0)) * 2.0f);
                    }
                    
                    x_m = abs(x)
                    real(4) function code(x_m, s)
                        real(4), intent (in) :: x_m
                        real(4), intent (in) :: s
                        real(4) :: t_0
                        t_0 = exp((-abs(x_m) / s))
                        code = t_0 / ((s * (1.0e0 + t_0)) * 2.0e0)
                    end function
                    
                    x_m = abs(x)
                    function code(x_m, s)
                    	t_0 = exp(Float32(Float32(-abs(x_m)) / s))
                    	return Float32(t_0 / Float32(Float32(s * Float32(Float32(1.0) + t_0)) * Float32(2.0)))
                    end
                    
                    x_m = abs(x);
                    function tmp = code(x_m, s)
                    	t_0 = exp((-abs(x_m) / s));
                    	tmp = t_0 / ((s * (single(1.0) + t_0)) * single(2.0));
                    end
                    
                    \begin{array}{l}
                    x_m = \left|x\right|
                    
                    \\
                    \begin{array}{l}
                    t_0 := e^{\frac{-\left|x\_m\right|}{s}}\\
                    \frac{t\_0}{\left(s \cdot \left(1 + t\_0\right)\right) \cdot 2}
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Initial program 99.8%

                      \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                    2. Add Preprocessing
                    3. Taylor expanded in s around inf

                      \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \color{blue}{2}} \]
                    4. Step-by-step derivation
                      1. Applied rewrites95.4%

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

                      Alternative 12: 95.0% accurate, 1.6× speedup?

                      \[\begin{array}{l} x_m = \left|x\right| \\ \frac{e^{\frac{-x\_m}{s} - \log 2 \cdot 2}}{s} \end{array} \]
                      x_m = (fabs.f32 x)
                      (FPCore (x_m s)
                       :precision binary32
                       (/ (exp (- (/ (- x_m) s) (* (log 2.0) 2.0))) s))
                      x_m = fabs(x);
                      float code(float x_m, float s) {
                      	return expf(((-x_m / s) - (logf(2.0f) * 2.0f))) / s;
                      }
                      
                      x_m = abs(x)
                      real(4) function code(x_m, s)
                          real(4), intent (in) :: x_m
                          real(4), intent (in) :: s
                          code = exp(((-x_m / s) - (log(2.0e0) * 2.0e0))) / s
                      end function
                      
                      x_m = abs(x)
                      function code(x_m, s)
                      	return Float32(exp(Float32(Float32(Float32(-x_m) / s) - Float32(log(Float32(2.0)) * Float32(2.0)))) / s)
                      end
                      
                      x_m = abs(x);
                      function tmp = code(x_m, s)
                      	tmp = exp(((-x_m / s) - (log(single(2.0)) * single(2.0)))) / s;
                      end
                      
                      \begin{array}{l}
                      x_m = \left|x\right|
                      
                      \\
                      \frac{e^{\frac{-x\_m}{s} - \log 2 \cdot 2}}{s}
                      \end{array}
                      
                      Derivation
                      1. Initial program 99.8%

                        \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. lift-/.f32N/A

                          \[\leadsto \color{blue}{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                        2. lift-*.f32N/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                        3. lift-*.f32N/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        4. associate-*l*N/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{s \cdot \left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)}} \]
                        5. *-commutativeN/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot s}} \]
                        6. associate-/r*N/A

                          \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
                        7. lower-/.f32N/A

                          \[\leadsto \color{blue}{\frac{\frac{e^{\frac{-\left|x\right|}{s}}}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}}{s}} \]
                      4. Applied rewrites62.8%

                        \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s} - \mathsf{log1p}\left(e^{\frac{-x}{s}}\right) \cdot 2}}{s}} \]
                      5. Taylor expanded in x around 0

                        \[\leadsto \frac{e^{\frac{-x}{s} - \color{blue}{\log 2} \cdot 2}}{s} \]
                      6. Step-by-step derivation
                        1. lower-log.f3258.7

                          \[\leadsto \frac{e^{\frac{-x}{s} - \color{blue}{\log 2} \cdot 2}}{s} \]
                      7. Applied rewrites58.7%

                        \[\leadsto \frac{e^{\frac{-x}{s} - \color{blue}{\log 2} \cdot 2}}{s} \]
                      8. Add Preprocessing

                      Alternative 13: 95.0% accurate, 2.9× speedup?

                      \[\begin{array}{l} x_m = \left|x\right| \\ \frac{e^{\frac{-x\_m}{s}}}{4 \cdot s} \end{array} \]
                      x_m = (fabs.f32 x)
                      (FPCore (x_m s) :precision binary32 (/ (exp (/ (- x_m) s)) (* 4.0 s)))
                      x_m = fabs(x);
                      float code(float x_m, float s) {
                      	return expf((-x_m / s)) / (4.0f * s);
                      }
                      
                      x_m = abs(x)
                      real(4) function code(x_m, s)
                          real(4), intent (in) :: x_m
                          real(4), intent (in) :: s
                          code = exp((-x_m / s)) / (4.0e0 * s)
                      end function
                      
                      x_m = abs(x)
                      function code(x_m, s)
                      	return Float32(exp(Float32(Float32(-x_m) / s)) / Float32(Float32(4.0) * s))
                      end
                      
                      x_m = abs(x);
                      function tmp = code(x_m, s)
                      	tmp = exp((-x_m / s)) / (single(4.0) * s);
                      end
                      
                      \begin{array}{l}
                      x_m = \left|x\right|
                      
                      \\
                      \frac{e^{\frac{-x\_m}{s}}}{4 \cdot s}
                      \end{array}
                      
                      Derivation
                      1. Initial program 99.8%

                        \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. lift-*.f32N/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        2. lift-+.f32N/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        3. +-commutativeN/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \color{blue}{\left(e^{\frac{-\left|x\right|}{s}} + 1\right)}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        4. distribute-lft-inN/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s \cdot 1\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        5. *-rgt-identityN/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + \color{blue}{s}\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        6. lower-+.f32N/A

                          \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(s \cdot e^{\frac{-\left|x\right|}{s}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                      4. Applied rewrites97.0%

                        \[\leadsto \frac{e^{\frac{-\left|x\right|}{s}}}{\color{blue}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right)} \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                      5. Step-by-step derivation
                        1. lift-/.f32N/A

                          \[\leadsto \frac{e^{\color{blue}{\frac{-\left|x\right|}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        2. frac-2negN/A

                          \[\leadsto \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(\left(-\left|x\right|\right)\right)}{\mathsf{neg}\left(s\right)}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        3. lift-neg.f32N/A

                          \[\leadsto \frac{e^{\frac{\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\left|x\right|\right)\right)}\right)}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        4. remove-double-negN/A

                          \[\leadsto \frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        5. lift-fabs.f32N/A

                          \[\leadsto \frac{e^{\frac{\color{blue}{\left|x\right|}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        6. rem-sqrt-square-revN/A

                          \[\leadsto \frac{e^{\frac{\color{blue}{\sqrt{x \cdot x}}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        7. sqrt-prodN/A

                          \[\leadsto \frac{e^{\frac{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        8. rem-square-sqrtN/A

                          \[\leadsto \frac{e^{\frac{\color{blue}{x}}{\mathsf{neg}\left(s\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        9. distribute-neg-frac2N/A

                          \[\leadsto \frac{e^{\color{blue}{\mathsf{neg}\left(\frac{x}{s}\right)}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        10. distribute-frac-negN/A

                          \[\leadsto \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(x\right)}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        11. lift-neg.f32N/A

                          \[\leadsto \frac{e^{\frac{\color{blue}{-x}}{s}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        12. lift-/.f3259.5

                          \[\leadsto \frac{e^{\color{blue}{\frac{-x}{s}}}}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                        13. lift-*.f32N/A

                          \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(\frac{s}{e^{\frac{x}{s}}} + s\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)}} \]
                        14. *-commutativeN/A

                          \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
                        15. lower-*.f3259.5

                          \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{\left(1 + e^{\frac{-\left|x\right|}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
                      6. Applied rewrites62.3%

                        \[\leadsto \color{blue}{\frac{e^{\frac{-x}{s}}}{\left(1 + e^{\frac{-x}{s}}\right) \cdot \left(\frac{s}{e^{\frac{x}{s}}} + s\right)}} \]
                      7. Taylor expanded in x around 0

                        \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{4 \cdot s}} \]
                      8. Step-by-step derivation
                        1. lower-*.f3258.7

                          \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{4 \cdot s}} \]
                      9. Applied rewrites58.7%

                        \[\leadsto \frac{e^{\frac{-x}{s}}}{\color{blue}{4 \cdot s}} \]
                      10. Add Preprocessing

                      Alternative 14: 27.3% accurate, 31.1× speedup?

                      \[\begin{array}{l} x_m = \left|x\right| \\ \frac{0.25}{s} \end{array} \]
                      x_m = (fabs.f32 x)
                      (FPCore (x_m s) :precision binary32 (/ 0.25 s))
                      x_m = fabs(x);
                      float code(float x_m, float s) {
                      	return 0.25f / s;
                      }
                      
                      x_m = abs(x)
                      real(4) function code(x_m, s)
                          real(4), intent (in) :: x_m
                          real(4), intent (in) :: s
                          code = 0.25e0 / s
                      end function
                      
                      x_m = abs(x)
                      function code(x_m, s)
                      	return Float32(Float32(0.25) / s)
                      end
                      
                      x_m = abs(x);
                      function tmp = code(x_m, s)
                      	tmp = single(0.25) / s;
                      end
                      
                      \begin{array}{l}
                      x_m = \left|x\right|
                      
                      \\
                      \frac{0.25}{s}
                      \end{array}
                      
                      Derivation
                      1. Initial program 99.8%

                        \[\frac{e^{\frac{-\left|x\right|}{s}}}{\left(s \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)\right) \cdot \left(1 + e^{\frac{-\left|x\right|}{s}}\right)} \]
                      2. Add Preprocessing
                      3. Taylor expanded in s around inf

                        \[\leadsto \color{blue}{\frac{\frac{1}{4}}{s}} \]
                      4. Step-by-step derivation
                        1. lower-/.f3227.1

                          \[\leadsto \color{blue}{\frac{0.25}{s}} \]
                      5. Applied rewrites27.1%

                        \[\leadsto \color{blue}{\frac{0.25}{s}} \]
                      6. Add Preprocessing

                      Reproduce

                      ?
                      herbie shell --seed 2024339 
                      (FPCore (x s)
                        :name "Logistic distribution"
                        :precision binary32
                        :pre (and (<= 0.0 s) (<= s 1.0651631))
                        (/ (exp (/ (- (fabs x)) s)) (* (* s (+ 1.0 (exp (/ (- (fabs x)) s)))) (+ 1.0 (exp (/ (- (fabs x)) s))))))