Sample trimmed logistic on [-pi, pi]

Percentage Accurate: 98.9% → 98.9%
Time: 22.9s
Alternatives: 13
Speedup: 1.0×

Specification

?
\[\left(2.328306437 \cdot 10^{-10} \leq u \land u \leq 1\right) \land \left(0 \leq s \land s \leq 1.0651631\right)\]
\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\ \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - t\_0\right) + t\_0} - 1\right) \end{array} \end{array} \]
(FPCore (u s)
 :precision binary32
 (let* ((t_0 (/ 1.0 (+ 1.0 (exp (/ (PI) s))))))
   (*
    (- s)
    (log
     (-
      (/ 1.0 (+ (* u (- (/ 1.0 (+ 1.0 (exp (/ (- (PI)) s)))) t_0)) t_0))
      1.0)))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\
\left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - t\_0\right) + t\_0} - 1\right)
\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 13 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: 98.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\ \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - t\_0\right) + t\_0} - 1\right) \end{array} \end{array} \]
(FPCore (u s)
 :precision binary32
 (let* ((t_0 (/ 1.0 (+ 1.0 (exp (/ (PI) s))))))
   (*
    (- s)
    (log
     (-
      (/ 1.0 (+ (* u (- (/ 1.0 (+ 1.0 (exp (/ (- (PI)) s)))) t_0)) t_0))
      1.0)))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\
\left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - t\_0\right) + t\_0} - 1\right)
\end{array}
\end{array}

Alternative 1: 98.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \log \left(\frac{1}{\frac{1}{e^{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}} + 1} + \left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right) \end{array} \]
(FPCore (u s)
 :precision binary32
 (*
  (log
   (-
    (/
     1.0
     (+
      (/ 1.0 (+ (exp (/ 1.0 (/ s (PI)))) 1.0))
      (*
       (-
        (/ -1.0 (- (exp (/ (PI) s)) -1.0))
        (/ -1.0 (- (exp (/ (- (PI)) s)) -1.0)))
       u)))
    1.0))
  (- s)))
\begin{array}{l}

\\
\log \left(\frac{1}{\frac{1}{e^{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}} + 1} + \left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right)
\end{array}
Derivation
  1. Initial program 99.1%

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

      \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{\mathsf{PI}\left(\right)}{s}}}}} - 1\right) \]
    2. clear-numN/A

      \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
    3. lower-/.f32N/A

      \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
    4. lower-/.f3299.1

      \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\frac{1}{\color{blue}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
  4. Applied rewrites99.1%

    \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
  5. Final simplification99.1%

    \[\leadsto \log \left(\frac{1}{\frac{1}{e^{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}} + 1} + \left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right) \]
  6. Add Preprocessing

Alternative 2: 16.9% accurate, 0.8× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\mathsf{PI}\left(\right)}{s}\\ t_1 := \frac{-1}{e^{t\_0} - -1}\\ \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -9.999999682655225 \cdot 10^{-20}:\\ \;\;\;\;\log \left(\left(t\_0 + 1\right) - \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s} \cdot \frac{-0.5}{s}\right) \cdot \left(-s\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \end{array} \]
(FPCore (u s)
 :precision binary32
 (let* ((t_0 (/ (PI) s)) (t_1 (/ -1.0 (- (exp t_0) -1.0))))
   (if (<=
        (*
         (log
          (-
           -1.0
           (/
            -1.0
            (- (* (- t_1 (/ -1.0 (- (exp (/ (- (PI)) s)) -1.0))) u) t_1))))
         (- s))
        -9.999999682655225e-20)
     (* (log (- (+ t_0 1.0) (* (/ (* (PI) (PI)) s) (/ -0.5 s)))) (- s))
     (* (log (fma (/ (fma -0.5 (* (PI) u) (* 0.25 (PI))) s) 4.0 1.0)) (- s)))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{\mathsf{PI}\left(\right)}{s}\\
t_1 := \frac{-1}{e^{t\_0} - -1}\\
\mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -9.999999682655225 \cdot 10^{-20}:\\
\;\;\;\;\log \left(\left(t\_0 + 1\right) - \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s} \cdot \frac{-0.5}{s}\right) \cdot \left(-s\right)\\

\mathbf{else}:\\
\;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -9.99999968e-20

    1. Initial program 99.3%

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

      \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
    4. Step-by-step derivation
      1. cancel-sign-sub-invN/A

        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
      2. metadata-evalN/A

        \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
      3. +-commutativeN/A

        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
    5. Applied rewrites6.3%

      \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
    6. Taylor expanded in u around 0

      \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + \frac{\mathsf{PI}\left(\right)}{s}\right) - \color{blue}{\frac{-1}{2} \cdot \frac{{\mathsf{PI}\left(\right)}^{2}}{{s}^{2}}}\right) \]
    7. Step-by-step derivation
      1. Applied rewrites25.4%

        \[\leadsto \left(-s\right) \cdot \log \left(\left(\frac{\mathsf{PI}\left(\right)}{s} + 1\right) - \color{blue}{\frac{-0.5}{s} \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s}}\right) \]

      if -9.99999968e-20 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32))))

      1. Initial program 99.0%

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

        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
      4. Step-by-step derivation
        1. cancel-sign-sub-invN/A

          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
        2. metadata-evalN/A

          \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
        3. +-commutativeN/A

          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
      5. Applied rewrites10.1%

        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
      6. Taylor expanded in u around inf

        \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{-2 \cdot \left({u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{s \cdot s}\right)\right) \]
      7. Step-by-step derivation
        1. Applied rewrites4.5%

          \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\left(\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u\right) \cdot u\right) \cdot -2}{s \cdot s}\right)\right) \]
        2. Taylor expanded in s around -inf

          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 + 4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
        3. Step-by-step derivation
          1. associate-*r/N/A

            \[\leadsto \left(-s\right) \cdot \log \left(1 + \color{blue}{\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}}\right) \]
          2. +-commutativeN/A

            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s} + 1\right)} \]
          3. associate-*r/N/A

            \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}} + 1\right) \]
          4. *-commutativeN/A

            \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s} \cdot 4} + 1\right) \]
          5. lower-fma.f32N/A

            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}, 4, 1\right)\right)} \]
        4. Applied rewrites9.5%

          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right)} \]
      8. Recombined 2 regimes into one program.
      9. Final simplification16.5%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}}\right) \cdot \left(-s\right) \leq -9.999999682655225 \cdot 10^{-20}:\\ \;\;\;\;\log \left(\left(\frac{\mathsf{PI}\left(\right)}{s} + 1\right) - \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s} \cdot \frac{-0.5}{s}\right) \cdot \left(-s\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \]
      10. Add Preprocessing

      Alternative 3: 15.4% accurate, 0.8× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\ \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_0 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_0}\right) \cdot \left(-s\right) \leq -9.999999682655225 \cdot 10^{-21}:\\ \;\;\;\;\log \left(\left(\frac{u \cdot u}{s} \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s}\right) \cdot 2\right) \cdot \left(-s\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \end{array} \]
      (FPCore (u s)
       :precision binary32
       (let* ((t_0 (/ -1.0 (- (exp (/ (PI) s)) -1.0))))
         (if (<=
              (*
               (log
                (-
                 -1.0
                 (/
                  -1.0
                  (- (* (- t_0 (/ -1.0 (- (exp (/ (- (PI)) s)) -1.0))) u) t_0))))
               (- s))
              -9.999999682655225e-21)
           (* (log (* (* (/ (* u u) s) (/ (* (PI) (PI)) s)) 2.0)) (- s))
           (* (log (fma (/ (fma -0.5 (* (PI) u) (* 0.25 (PI))) s) 4.0 1.0)) (- s)))))
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\
      \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_0 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_0}\right) \cdot \left(-s\right) \leq -9.999999682655225 \cdot 10^{-21}:\\
      \;\;\;\;\log \left(\left(\frac{u \cdot u}{s} \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s}\right) \cdot 2\right) \cdot \left(-s\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -9.99999968e-21

        1. Initial program 99.3%

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

          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
        4. Step-by-step derivation
          1. cancel-sign-sub-invN/A

            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
          2. metadata-evalN/A

            \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
          3. +-commutativeN/A

            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
        5. Applied rewrites5.9%

          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
        6. Taylor expanded in u around inf

          \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, {u}^{2} \cdot \left(\frac{1}{{u}^{2}} - \left(-2 \cdot \frac{{\mathsf{PI}\left(\right)}^{2}}{{s}^{2}} + \left(\frac{-1}{2} \cdot \frac{{\mathsf{PI}\left(\right)}^{2}}{{s}^{2} \cdot {u}^{2}} + 2 \cdot \frac{{\mathsf{PI}\left(\right)}^{2}}{{s}^{2} \cdot u}\right)\right)\right)\right)\right) \]
        7. Step-by-step derivation
          1. Applied rewrites9.6%

            \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, \left(\frac{1}{u \cdot u} - \mathsf{fma}\left(\frac{-0.5}{u \cdot u}, \frac{\mathsf{PI}\left(\right)}{s} \cdot \frac{\mathsf{PI}\left(\right)}{s}, \mathsf{fma}\left(\frac{2}{s \cdot s}, \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{u}, \frac{-2}{s} \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s}\right)\right)\right) \cdot \left(u \cdot u\right)\right)\right) \]
          2. Taylor expanded in s around 0

            \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, \left(\frac{1}{u \cdot u} - \mathsf{fma}\left(\frac{\frac{-1}{2}}{u \cdot u}, \frac{\mathsf{PI}\left(\right)}{s} \cdot \frac{\mathsf{PI}\left(\right)}{s}, \frac{-2 \cdot {\mathsf{PI}\left(\right)}^{2} + 2 \cdot \frac{{\mathsf{PI}\left(\right)}^{2}}{u}}{{s}^{2}}\right)\right) \cdot \left(u \cdot u\right)\right)\right) \]
          3. Step-by-step derivation
            1. Applied rewrites10.1%

              \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, \left(\frac{1}{u \cdot u} - \mathsf{fma}\left(\frac{-0.5}{u \cdot u}, \frac{\mathsf{PI}\left(\right)}{s} \cdot \frac{\mathsf{PI}\left(\right)}{s}, \frac{\frac{\mathsf{fma}\left(\frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{u}, 2, \left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -2\right)}{s}}{s}\right)\right) \cdot \left(u \cdot u\right)\right)\right) \]
            2. Taylor expanded in u around inf

              \[\leadsto \left(-s\right) \cdot \log \left(2 \cdot \color{blue}{\frac{{u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}}{{s}^{2}}}\right) \]
            3. Step-by-step derivation
              1. Applied rewrites20.6%

                \[\leadsto \left(-s\right) \cdot \log \left(\left(\frac{u \cdot u}{s} \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s}\right) \cdot \color{blue}{2}\right) \]

              if -9.99999968e-21 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32))))

              1. Initial program 98.9%

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

                \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
              4. Step-by-step derivation
                1. cancel-sign-sub-invN/A

                  \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                2. metadata-evalN/A

                  \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
                3. +-commutativeN/A

                  \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
              5. Applied rewrites9.1%

                \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
              6. Taylor expanded in u around inf

                \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{-2 \cdot \left({u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{s \cdot s}\right)\right) \]
              7. Step-by-step derivation
                1. Applied rewrites4.3%

                  \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\left(\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u\right) \cdot u\right) \cdot -2}{s \cdot s}\right)\right) \]
                2. Taylor expanded in s around -inf

                  \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 + 4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                3. Step-by-step derivation
                  1. associate-*r/N/A

                    \[\leadsto \left(-s\right) \cdot \log \left(1 + \color{blue}{\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}}\right) \]
                  2. +-commutativeN/A

                    \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s} + 1\right)} \]
                  3. associate-*r/N/A

                    \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}} + 1\right) \]
                  4. *-commutativeN/A

                    \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s} \cdot 4} + 1\right) \]
                  5. lower-fma.f32N/A

                    \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}, 4, 1\right)\right)} \]
                4. Applied rewrites13.4%

                  \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right)} \]
              8. Recombined 2 regimes into one program.
              9. Final simplification14.8%

                \[\leadsto \begin{array}{l} \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}}\right) \cdot \left(-s\right) \leq -9.999999682655225 \cdot 10^{-21}:\\ \;\;\;\;\log \left(\left(\frac{u \cdot u}{s} \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}{s}\right) \cdot 2\right) \cdot \left(-s\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \]
              10. Add Preprocessing

              Alternative 4: 14.4% accurate, 0.8× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\mathsf{PI}\left(\right)}{s}\\ t_1 := \frac{-1}{e^{t\_0} - -1}\\ \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -2.1999999560335437 \cdot 10^{-18}:\\ \;\;\;\;\log \left(\left(t\_0 \cdot t\_0\right) \cdot \left(\left(u \cdot u\right) \cdot 2\right)\right) \cdot \left(-s\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \end{array} \]
              (FPCore (u s)
               :precision binary32
               (let* ((t_0 (/ (PI) s)) (t_1 (/ -1.0 (- (exp t_0) -1.0))))
                 (if (<=
                      (*
                       (log
                        (-
                         -1.0
                         (/
                          -1.0
                          (- (* (- t_1 (/ -1.0 (- (exp (/ (- (PI)) s)) -1.0))) u) t_1))))
                       (- s))
                      -2.1999999560335437e-18)
                   (* (log (* (* t_0 t_0) (* (* u u) 2.0))) (- s))
                   (* (log (fma (/ (fma -0.5 (* (PI) u) (* 0.25 (PI))) s) 4.0 1.0)) (- s)))))
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              t_0 := \frac{\mathsf{PI}\left(\right)}{s}\\
              t_1 := \frac{-1}{e^{t\_0} - -1}\\
              \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -2.1999999560335437 \cdot 10^{-18}:\\
              \;\;\;\;\log \left(\left(t\_0 \cdot t\_0\right) \cdot \left(\left(u \cdot u\right) \cdot 2\right)\right) \cdot \left(-s\right)\\
              
              \mathbf{else}:\\
              \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -2.19999996e-18

                1. Initial program 99.3%

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

                  \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                4. Step-by-step derivation
                  1. cancel-sign-sub-invN/A

                    \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                  2. metadata-evalN/A

                    \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
                  3. +-commutativeN/A

                    \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
                5. Applied rewrites6.3%

                  \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
                6. Taylor expanded in u around inf

                  \[\leadsto \left(-s\right) \cdot \log \left(2 \cdot \color{blue}{\frac{{u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}}{{s}^{2}}}\right) \]
                7. Step-by-step derivation
                  1. Applied rewrites20.2%

                    \[\leadsto \left(-s\right) \cdot \log \left(\left(2 \cdot \left(u \cdot u\right)\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{s} \cdot \frac{\mathsf{PI}\left(\right)}{s}\right)}\right) \]

                  if -2.19999996e-18 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32))))

                  1. Initial program 99.0%

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

                    \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                  4. Step-by-step derivation
                    1. cancel-sign-sub-invN/A

                      \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                    2. metadata-evalN/A

                      \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
                    3. +-commutativeN/A

                      \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
                  5. Applied rewrites9.5%

                    \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
                  6. Taylor expanded in u around inf

                    \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{-2 \cdot \left({u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{s \cdot s}\right)\right) \]
                  7. Step-by-step derivation
                    1. Applied rewrites6.3%

                      \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\left(\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u\right) \cdot u\right) \cdot -2}{s \cdot s}\right)\right) \]
                    2. Taylor expanded in s around -inf

                      \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 + 4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                    3. Step-by-step derivation
                      1. associate-*r/N/A

                        \[\leadsto \left(-s\right) \cdot \log \left(1 + \color{blue}{\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}}\right) \]
                      2. +-commutativeN/A

                        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s} + 1\right)} \]
                      3. associate-*r/N/A

                        \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}} + 1\right) \]
                      4. *-commutativeN/A

                        \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s} \cdot 4} + 1\right) \]
                      5. lower-fma.f32N/A

                        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}, 4, 1\right)\right)} \]
                    4. Applied rewrites13.1%

                      \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right)} \]
                  8. Recombined 2 regimes into one program.
                  9. Final simplification13.8%

                    \[\leadsto \begin{array}{l} \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}}\right) \cdot \left(-s\right) \leq -2.1999999560335437 \cdot 10^{-18}:\\ \;\;\;\;\log \left(\left(\frac{\mathsf{PI}\left(\right)}{s} \cdot \frac{\mathsf{PI}\left(\right)}{s}\right) \cdot \left(\left(u \cdot u\right) \cdot 2\right)\right) \cdot \left(-s\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \]
                  10. Add Preprocessing

                  Alternative 5: 12.1% accurate, 0.8× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} t_0 := -\mathsf{PI}\left(\right)\\ t_1 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\ \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{t\_0}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -1.7999999428779406 \cdot 10^{-21}:\\ \;\;\;\;\log \mathsf{E}\left(\right) \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \end{array} \]
                  (FPCore (u s)
                   :precision binary32
                   (let* ((t_0 (- (PI))) (t_1 (/ -1.0 (- (exp (/ (PI) s)) -1.0))))
                     (if (<=
                          (*
                           (log
                            (-
                             -1.0
                             (/ -1.0 (- (* (- t_1 (/ -1.0 (- (exp (/ t_0 s)) -1.0))) u) t_1))))
                           (- s))
                          -1.7999999428779406e-21)
                       (* (log (E)) t_0)
                       (* (log (fma (/ (fma -0.5 (* (PI) u) (* 0.25 (PI))) s) 4.0 1.0)) (- s)))))
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  t_0 := -\mathsf{PI}\left(\right)\\
                  t_1 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\
                  \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{t\_0}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -1.7999999428779406 \cdot 10^{-21}:\\
                  \;\;\;\;\log \mathsf{E}\left(\right) \cdot t\_0\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 2 regimes
                  2. if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -1.7999999e-21

                    1. Initial program 99.3%

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

                      \[\leadsto \color{blue}{-1 \cdot \mathsf{PI}\left(\right)} \]
                    4. Step-by-step derivation
                      1. mul-1-negN/A

                        \[\leadsto \color{blue}{\mathsf{neg}\left(\mathsf{PI}\left(\right)\right)} \]
                      2. lower-neg.f32N/A

                        \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                      3. lower-PI.f3215.2

                        \[\leadsto -\color{blue}{\mathsf{PI}\left(\right)} \]
                    5. Applied rewrites15.2%

                      \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                    6. Step-by-step derivation
                      1. Applied rewrites15.2%

                        \[\leadsto -\mathsf{PI}\left(\right) \cdot \log \mathsf{E}\left(\right) \]

                      if -1.7999999e-21 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32))))

                      1. Initial program 98.9%

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

                        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                      4. Step-by-step derivation
                        1. cancel-sign-sub-invN/A

                          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                        2. metadata-evalN/A

                          \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
                        3. +-commutativeN/A

                          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
                      5. Applied rewrites7.1%

                        \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
                      6. Taylor expanded in u around inf

                        \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{-2 \cdot \left({u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{s \cdot s}\right)\right) \]
                      7. Step-by-step derivation
                        1. Applied rewrites5.2%

                          \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\left(\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u\right) \cdot u\right) \cdot -2}{s \cdot s}\right)\right) \]
                        2. Taylor expanded in s around -inf

                          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 + 4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                        3. Step-by-step derivation
                          1. associate-*r/N/A

                            \[\leadsto \left(-s\right) \cdot \log \left(1 + \color{blue}{\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}}\right) \]
                          2. +-commutativeN/A

                            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\frac{4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s} + 1\right)} \]
                          3. associate-*r/N/A

                            \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{4 \cdot \frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}} + 1\right) \]
                          4. *-commutativeN/A

                            \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s} \cdot 4} + 1\right) \]
                          5. lower-fma.f32N/A

                            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)}{s}, 4, 1\right)\right)} \]
                        4. Applied rewrites13.4%

                          \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right)} \]
                      8. Recombined 2 regimes into one program.
                      9. Final simplification7.2%

                        \[\leadsto \begin{array}{l} \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}}\right) \cdot \left(-s\right) \leq -1.7999999428779406 \cdot 10^{-21}:\\ \;\;\;\;\log \mathsf{E}\left(\right) \cdot \left(-\mathsf{PI}\left(\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, 4, 1\right)\right) \cdot \left(-s\right)\\ \end{array} \]
                      10. Add Preprocessing

                      Alternative 6: 14.2% accurate, 1.0× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} t_0 := -\mathsf{PI}\left(\right)\\ t_1 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\ \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{t\_0}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -1.5000000170217692 \cdot 10^{-19}:\\ \;\;\;\;t\_0\\ \mathbf{else}:\\ \;\;\;\;0 \cdot s\\ \end{array} \end{array} \]
                      (FPCore (u s)
                       :precision binary32
                       (let* ((t_0 (- (PI))) (t_1 (/ -1.0 (- (exp (/ (PI) s)) -1.0))))
                         (if (<=
                              (*
                               (log
                                (-
                                 -1.0
                                 (/ -1.0 (- (* (- t_1 (/ -1.0 (- (exp (/ t_0 s)) -1.0))) u) t_1))))
                               (- s))
                              -1.5000000170217692e-19)
                           t_0
                           (* 0.0 s))))
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      t_0 := -\mathsf{PI}\left(\right)\\
                      t_1 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\
                      \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(t\_1 - \frac{-1}{e^{\frac{t\_0}{s}} - -1}\right) \cdot u - t\_1}\right) \cdot \left(-s\right) \leq -1.5000000170217692 \cdot 10^{-19}:\\
                      \;\;\;\;t\_0\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;0 \cdot s\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -1.50000002e-19

                        1. Initial program 99.3%

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

                          \[\leadsto \color{blue}{-1 \cdot \mathsf{PI}\left(\right)} \]
                        4. Step-by-step derivation
                          1. mul-1-negN/A

                            \[\leadsto \color{blue}{\mathsf{neg}\left(\mathsf{PI}\left(\right)\right)} \]
                          2. lower-neg.f32N/A

                            \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                          3. lower-PI.f3215.6

                            \[\leadsto -\color{blue}{\mathsf{PI}\left(\right)} \]
                        5. Applied rewrites15.6%

                          \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]

                        if -1.50000002e-19 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32))))

                        1. Initial program 99.0%

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

                            \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{\mathsf{PI}\left(\right)}{s}}}}} - 1\right) \]
                          2. clear-numN/A

                            \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                          3. lower-/.f32N/A

                            \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                          4. lower-/.f3299.0

                            \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\frac{1}{\color{blue}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                        4. Applied rewrites99.0%

                          \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                        5. Applied rewrites99.0%

                          \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\frac{{\left(e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1\right)}^{-2} - {\left(\left(e^{-\mathsf{log1p}\left(e^{\frac{-\mathsf{PI}\left(\right)}{s}}\right)} - e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)}\right) \cdot u\right)}^{2}}{e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)} - \left(e^{-\mathsf{log1p}\left(e^{\frac{-\mathsf{PI}\left(\right)}{s}}\right)} - e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)}\right) \cdot u}}} - 1\right) \]
                        6. Taylor expanded in s around inf

                          \[\leadsto \color{blue}{-1 \cdot \left(s \cdot \log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right)\right)} \]
                        7. Step-by-step derivation
                          1. mul-1-negN/A

                            \[\leadsto \color{blue}{\mathsf{neg}\left(s \cdot \log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right)\right)} \]
                          2. *-commutativeN/A

                            \[\leadsto \mathsf{neg}\left(\color{blue}{\log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right) \cdot s}\right) \]
                          3. distribute-lft-neg-inN/A

                            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right)\right)\right) \cdot s} \]
                          4. exp-negN/A

                            \[\leadsto \left(\mathsf{neg}\left(\log \left(4 \cdot \color{blue}{\frac{1}{e^{\log 2}}} - 1\right)\right)\right) \cdot s \]
                          5. rem-exp-logN/A

                            \[\leadsto \left(\mathsf{neg}\left(\log \left(4 \cdot \frac{1}{\color{blue}{2}} - 1\right)\right)\right) \cdot s \]
                          6. metadata-evalN/A

                            \[\leadsto \left(\mathsf{neg}\left(\log \left(4 \cdot \color{blue}{\frac{1}{2}} - 1\right)\right)\right) \cdot s \]
                          7. metadata-evalN/A

                            \[\leadsto \left(\mathsf{neg}\left(\log \left(\color{blue}{2} - 1\right)\right)\right) \cdot s \]
                          8. metadata-evalN/A

                            \[\leadsto \left(\mathsf{neg}\left(\log \color{blue}{1}\right)\right) \cdot s \]
                          9. metadata-evalN/A

                            \[\leadsto \left(\mathsf{neg}\left(\color{blue}{0}\right)\right) \cdot s \]
                          10. metadata-evalN/A

                            \[\leadsto \color{blue}{0} \cdot s \]
                          11. lower-*.f3213.2

                            \[\leadsto \color{blue}{0 \cdot s} \]
                        8. Applied rewrites13.2%

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

                        \[\leadsto \begin{array}{l} \mathbf{if}\;\log \left(-1 - \frac{-1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}}\right) \cdot \left(-s\right) \leq -1.5000000170217692 \cdot 10^{-19}:\\ \;\;\;\;-\mathsf{PI}\left(\right)\\ \mathbf{else}:\\ \;\;\;\;0 \cdot s\\ \end{array} \]
                      5. Add Preprocessing

                      Alternative 7: 98.9% accurate, 1.0× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\ \log \left(-1 - \frac{-1}{\left(t\_0 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_0}\right) \cdot \left(-s\right) \end{array} \end{array} \]
                      (FPCore (u s)
                       :precision binary32
                       (let* ((t_0 (/ -1.0 (- (exp (/ (PI) s)) -1.0))))
                         (*
                          (log
                           (-
                            -1.0
                            (/ -1.0 (- (* (- t_0 (/ -1.0 (- (exp (/ (- (PI)) s)) -1.0))) u) t_0))))
                          (- s))))
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      t_0 := \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}\\
                      \log \left(-1 - \frac{-1}{\left(t\_0 - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - t\_0}\right) \cdot \left(-s\right)
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Initial program 99.1%

                        \[\left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}} - 1\right) \]
                      2. Add Preprocessing
                      3. Final simplification99.1%

                        \[\leadsto \log \left(-1 - \frac{-1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u - \frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1}}\right) \cdot \left(-s\right) \]
                      4. Add Preprocessing

                      Alternative 8: 54.9% accurate, 1.2× speedup?

                      \[\begin{array}{l} \\ \log \left(\frac{1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{\frac{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{PI}\left(\right), \mathsf{PI}\left(\right), 0 \cdot \mathsf{PI}\left(\right)\right)}}{-s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right) \end{array} \]
                      (FPCore (u s)
                       :precision binary32
                       (*
                        (log
                         (-
                          (/
                           1.0
                           (*
                            (-
                             (/ -1.0 (- (exp (/ (PI) s)) -1.0))
                             (/
                              -1.0
                              (-
                               (exp
                                (/ (/ (* (* (PI) (PI)) (PI)) (fma (PI) (PI) (* 0.0 (PI)))) (- s)))
                               -1.0)))
                            u))
                          1.0))
                        (- s)))
                      \begin{array}{l}
                      
                      \\
                      \log \left(\frac{1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{\frac{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{PI}\left(\right), \mathsf{PI}\left(\right), 0 \cdot \mathsf{PI}\left(\right)\right)}}{-s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right)
                      \end{array}
                      
                      Derivation
                      1. Initial program 99.1%

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

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

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

                          \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\left(\frac{1}{1 + e^{-1 \cdot \frac{\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) \cdot u}} - 1\right) \]
                      5. Applied rewrites97.9%

                        \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\left(\frac{1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} + 1} - \frac{1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1}\right) \cdot u}} - 1\right) \]
                      6. Step-by-step derivation
                        1. Applied rewrites97.9%

                          \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\left(\frac{1}{e^{\frac{\frac{0 - {\mathsf{PI}\left(\right)}^{3}}{0 + \mathsf{fma}\left(\mathsf{PI}\left(\right), \mathsf{PI}\left(\right), 0 \cdot \mathsf{PI}\left(\right)\right)}}{s}} + 1} - \frac{1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1}\right) \cdot u} - 1\right) \]
                        2. Step-by-step derivation
                          1. Applied rewrites64.7%

                            \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\left(\frac{1}{e^{\frac{\frac{0 - \left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \mathsf{PI}\left(\right)}{0 + \mathsf{fma}\left(\mathsf{PI}\left(\right), \mathsf{PI}\left(\right), 0 \cdot \mathsf{PI}\left(\right)\right)}}{s}} + 1} - \frac{1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1}\right) \cdot u} - 1\right) \]
                          2. Final simplification96.9%

                            \[\leadsto \log \left(\frac{1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{\frac{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{PI}\left(\right), \mathsf{PI}\left(\right), 0 \cdot \mathsf{PI}\left(\right)\right)}}{-s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right) \]
                          3. Add Preprocessing

                          Alternative 9: 97.7% accurate, 1.3× speedup?

                          \[\begin{array}{l} \\ \log \left(\frac{1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right) \end{array} \]
                          (FPCore (u s)
                           :precision binary32
                           (*
                            (log
                             (-
                              (/
                               1.0
                               (*
                                (-
                                 (/ -1.0 (- (exp (/ (PI) s)) -1.0))
                                 (/ -1.0 (- (exp (/ (- (PI)) s)) -1.0)))
                                u))
                              1.0))
                            (- s)))
                          \begin{array}{l}
                          
                          \\
                          \log \left(\frac{1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right)
                          \end{array}
                          
                          Derivation
                          1. Initial program 99.1%

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

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

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

                              \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\left(\frac{1}{1 + e^{-1 \cdot \frac{\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) \cdot u}} - 1\right) \]
                          5. Applied rewrites97.9%

                            \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\left(\frac{1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} + 1} - \frac{1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1}\right) \cdot u}} - 1\right) \]
                          6. Final simplification97.9%

                            \[\leadsto \log \left(\frac{1}{\left(\frac{-1}{e^{\frac{\mathsf{PI}\left(\right)}{s}} - -1} - \frac{-1}{e^{\frac{-\mathsf{PI}\left(\right)}{s}} - -1}\right) \cdot u} - 1\right) \cdot \left(-s\right) \]
                          7. Add Preprocessing

                          Alternative 10: 8.2% accurate, 1.8× speedup?

                          \[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)\\ \log \left(1 - \frac{\mathsf{fma}\left(\frac{{t\_0}^{2}}{s}, -8, \frac{0}{s}\right) - 4 \cdot t\_0}{s}\right) \cdot \left(-s\right) \end{array} \end{array} \]
                          (FPCore (u s)
                           :precision binary32
                           (let* ((t_0 (fma -0.5 (* (PI) u) (* 0.25 (PI)))))
                             (*
                              (log
                               (- 1.0 (/ (- (fma (/ (pow t_0 2.0) s) -8.0 (/ 0.0 s)) (* 4.0 t_0)) s)))
                              (- s))))
                          \begin{array}{l}
                          
                          \\
                          \begin{array}{l}
                          t_0 := \mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)\\
                          \log \left(1 - \frac{\mathsf{fma}\left(\frac{{t\_0}^{2}}{s}, -8, \frac{0}{s}\right) - 4 \cdot t\_0}{s}\right) \cdot \left(-s\right)
                          \end{array}
                          \end{array}
                          
                          Derivation
                          1. Initial program 99.1%

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

                            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) - 4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                          4. Step-by-step derivation
                            1. cancel-sign-sub-invN/A

                              \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \left(\mathsf{neg}\left(4\right)\right) \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right)} \]
                            2. metadata-evalN/A

                              \[\leadsto \left(-s\right) \cdot \log \left(\left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right) + \color{blue}{-4} \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s}\right) \]
                            3. +-commutativeN/A

                              \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(-4 \cdot \frac{u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)}{s} + \left(1 + -1 \cdot \frac{-8 \cdot {\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2} + -4 \cdot \left(\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{{s}^{2}}\right)\right)} \]
                          5. Applied rewrites8.0%

                            \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\mathsf{fma}\left(-8, {\left(\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}, 0\right)}{s \cdot s}\right)\right)} \]
                          6. Taylor expanded in u around inf

                            \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), \frac{1}{2}, \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{-2 \cdot \left({u}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}{s \cdot s}\right)\right) \]
                          7. Step-by-step derivation
                            1. Applied rewrites9.2%

                              \[\leadsto \left(-s\right) \cdot \log \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(u \cdot \mathsf{PI}\left(\right), 0.5, -0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}, -4, 1 - \frac{\left(\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u\right) \cdot u\right) \cdot -2}{s \cdot s}\right)\right) \]
                            2. Taylor expanded in s around -inf

                              \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 + -1 \cdot \frac{\left(-8 \cdot \frac{{\left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2}}{s} + -4 \cdot \frac{\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}}{s}\right) - 4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}\right)} \]
                            3. Step-by-step derivation
                              1. mul-1-negN/A

                                \[\leadsto \left(-s\right) \cdot \log \left(1 + \color{blue}{\left(\mathsf{neg}\left(\frac{\left(-8 \cdot \frac{{\left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2}}{s} + -4 \cdot \frac{\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}}{s}\right) - 4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}\right)\right)}\right) \]
                              2. unsub-negN/A

                                \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 - \frac{\left(-8 \cdot \frac{{\left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2}}{s} + -4 \cdot \frac{\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}}{s}\right) - 4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}\right)} \]
                              3. lower--.f32N/A

                                \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 - \frac{\left(-8 \cdot \frac{{\left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}^{2}}{s} + -4 \cdot \frac{\frac{-1}{8} \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{1}{8} \cdot {\mathsf{PI}\left(\right)}^{2}}{s}\right) - 4 \cdot \left(u \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)}{s}\right)} \]
                            4. Applied rewrites13.8%

                              \[\leadsto \left(-s\right) \cdot \log \color{blue}{\left(1 - \frac{\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}}{s}, -8, \frac{0}{s}\right) - \mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right) \cdot 4}{s}\right)} \]
                            5. Final simplification12.9%

                              \[\leadsto \log \left(1 - \frac{\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)\right)}^{2}}{s}, -8, \frac{0}{s}\right) - 4 \cdot \mathsf{fma}\left(-0.5, \mathsf{PI}\left(\right) \cdot u, 0.25 \cdot \mathsf{PI}\left(\right)\right)}{s}\right) \cdot \left(-s\right) \]
                            6. Add Preprocessing

                            Alternative 11: 25.0% accurate, 3.2× speedup?

                            \[\begin{array}{l} \\ \begin{array}{l} t_0 := 0.5 \cdot \mathsf{PI}\left(\right)\\ \log \left(\left(2 - \frac{\left(\left(t\_0 \cdot u + t\_0 \cdot 0.5\right) - t\_0\right) \cdot 4}{s}\right) - 1\right) \cdot \left(-s\right) \end{array} \end{array} \]
                            (FPCore (u s)
                             :precision binary32
                             (let* ((t_0 (* 0.5 (PI))))
                               (*
                                (log (- (- 2.0 (/ (* (- (+ (* t_0 u) (* t_0 0.5)) t_0) 4.0) s)) 1.0))
                                (- s))))
                            \begin{array}{l}
                            
                            \\
                            \begin{array}{l}
                            t_0 := 0.5 \cdot \mathsf{PI}\left(\right)\\
                            \log \left(\left(2 - \frac{\left(\left(t\_0 \cdot u + t\_0 \cdot 0.5\right) - t\_0\right) \cdot 4}{s}\right) - 1\right) \cdot \left(-s\right)
                            \end{array}
                            \end{array}
                            
                            Derivation
                            1. Initial program 99.1%

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

                                \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{\mathsf{PI}\left(\right)}{s}}}}} - 1\right) \]
                              2. clear-numN/A

                                \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                              3. lower-/.f32N/A

                                \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                              4. lower-/.f3299.1

                                \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\frac{1}{\color{blue}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                            4. Applied rewrites99.1%

                              \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                            5. Applied rewrites97.3%

                              \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\frac{{\left(e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1\right)}^{-2} - {\left(\left(e^{-\mathsf{log1p}\left(e^{\frac{-\mathsf{PI}\left(\right)}{s}}\right)} - e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)}\right) \cdot u\right)}^{2}}{e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)} - \left(e^{-\mathsf{log1p}\left(e^{\frac{-\mathsf{PI}\left(\right)}{s}}\right)} - e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)}\right) \cdot u}}} - 1\right) \]
                            6. Taylor expanded in s around -inf

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

                                \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} + -1 \cdot \frac{4 \cdot \left(\frac{1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right) - u \cdot \left(\frac{-1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right) - \frac{1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right)\right)\right) - 4 \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right)}{s}\right)} - 1\right) \]
                              2. mul-1-negN/A

                                \[\leadsto \left(-s\right) \cdot \log \left(\left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} + \color{blue}{\left(\mathsf{neg}\left(\frac{4 \cdot \left(\frac{1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right) - u \cdot \left(\frac{-1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right) - \frac{1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right)\right)\right) - 4 \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right)}{s}\right)\right)}\right) - 1\right) \]
                              3. unsub-negN/A

                                \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - \frac{4 \cdot \left(\frac{1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right) - u \cdot \left(\frac{-1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right) - \frac{1}{2} \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right)\right)\right) - 4 \cdot \left(\mathsf{PI}\left(\right) \cdot e^{\mathsf{neg}\left(\log 2\right)}\right)}{s}\right)} - 1\right) \]
                            8. Applied rewrites24.8%

                              \[\leadsto \left(-s\right) \cdot \log \left(\color{blue}{\left(2 - \frac{4 \cdot \left(\left(\left(0.5 \cdot \mathsf{PI}\left(\right)\right) \cdot 0.5 - \left(\left(0.5 \cdot \mathsf{PI}\left(\right)\right) \cdot -1\right) \cdot u\right) - 0.5 \cdot \mathsf{PI}\left(\right)\right)}{s}\right)} - 1\right) \]
                            9. Final simplification24.8%

                              \[\leadsto \log \left(\left(2 - \frac{\left(\left(\left(0.5 \cdot \mathsf{PI}\left(\right)\right) \cdot u + \left(0.5 \cdot \mathsf{PI}\left(\right)\right) \cdot 0.5\right) - 0.5 \cdot \mathsf{PI}\left(\right)\right) \cdot 4}{s}\right) - 1\right) \cdot \left(-s\right) \]
                            10. Add Preprocessing

                            Alternative 12: 14.3% accurate, 25.5× speedup?

                            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;s \leq 1.199999961918627 \cdot 10^{-20}:\\ \;\;\;\;0 \cdot s\\ \mathbf{else}:\\ \;\;\;\;\left(\mathsf{PI}\left(\right) \cdot u\right) \cdot 2 - \mathsf{PI}\left(\right)\\ \end{array} \end{array} \]
                            (FPCore (u s)
                             :precision binary32
                             (if (<= s 1.199999961918627e-20) (* 0.0 s) (- (* (* (PI) u) 2.0) (PI))))
                            \begin{array}{l}
                            
                            \\
                            \begin{array}{l}
                            \mathbf{if}\;s \leq 1.199999961918627 \cdot 10^{-20}:\\
                            \;\;\;\;0 \cdot s\\
                            
                            \mathbf{else}:\\
                            \;\;\;\;\left(\mathsf{PI}\left(\right) \cdot u\right) \cdot 2 - \mathsf{PI}\left(\right)\\
                            
                            
                            \end{array}
                            \end{array}
                            
                            Derivation
                            1. Split input into 2 regimes
                            2. if s < 1.2e-20

                              1. Initial program 99.1%

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

                                  \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{\mathsf{PI}\left(\right)}{s}}}}} - 1\right) \]
                                2. clear-numN/A

                                  \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                                3. lower-/.f32N/A

                                  \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                                4. lower-/.f3299.1

                                  \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\frac{1}{\color{blue}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                              4. Applied rewrites99.1%

                                \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\right) + \frac{1}{1 + e^{\color{blue}{\frac{1}{\frac{s}{\mathsf{PI}\left(\right)}}}}}} - 1\right) \]
                              5. Applied rewrites99.1%

                                \[\leadsto \left(-s\right) \cdot \log \left(\frac{1}{\color{blue}{\frac{{\left(e^{\frac{\mathsf{PI}\left(\right)}{s}} + 1\right)}^{-2} - {\left(\left(e^{-\mathsf{log1p}\left(e^{\frac{-\mathsf{PI}\left(\right)}{s}}\right)} - e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)}\right) \cdot u\right)}^{2}}{e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)} - \left(e^{-\mathsf{log1p}\left(e^{\frac{-\mathsf{PI}\left(\right)}{s}}\right)} - e^{-\mathsf{log1p}\left(e^{\frac{\mathsf{PI}\left(\right)}{s}}\right)}\right) \cdot u}}} - 1\right) \]
                              6. Taylor expanded in s around inf

                                \[\leadsto \color{blue}{-1 \cdot \left(s \cdot \log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right)\right)} \]
                              7. Step-by-step derivation
                                1. mul-1-negN/A

                                  \[\leadsto \color{blue}{\mathsf{neg}\left(s \cdot \log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right)\right)} \]
                                2. *-commutativeN/A

                                  \[\leadsto \mathsf{neg}\left(\color{blue}{\log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right) \cdot s}\right) \]
                                3. distribute-lft-neg-inN/A

                                  \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\log \left(4 \cdot e^{\mathsf{neg}\left(\log 2\right)} - 1\right)\right)\right) \cdot s} \]
                                4. exp-negN/A

                                  \[\leadsto \left(\mathsf{neg}\left(\log \left(4 \cdot \color{blue}{\frac{1}{e^{\log 2}}} - 1\right)\right)\right) \cdot s \]
                                5. rem-exp-logN/A

                                  \[\leadsto \left(\mathsf{neg}\left(\log \left(4 \cdot \frac{1}{\color{blue}{2}} - 1\right)\right)\right) \cdot s \]
                                6. metadata-evalN/A

                                  \[\leadsto \left(\mathsf{neg}\left(\log \left(4 \cdot \color{blue}{\frac{1}{2}} - 1\right)\right)\right) \cdot s \]
                                7. metadata-evalN/A

                                  \[\leadsto \left(\mathsf{neg}\left(\log \left(\color{blue}{2} - 1\right)\right)\right) \cdot s \]
                                8. metadata-evalN/A

                                  \[\leadsto \left(\mathsf{neg}\left(\log \color{blue}{1}\right)\right) \cdot s \]
                                9. metadata-evalN/A

                                  \[\leadsto \left(\mathsf{neg}\left(\color{blue}{0}\right)\right) \cdot s \]
                                10. metadata-evalN/A

                                  \[\leadsto \color{blue}{0} \cdot s \]
                                11. lower-*.f3213.5

                                  \[\leadsto \color{blue}{0 \cdot s} \]
                              8. Applied rewrites13.5%

                                \[\leadsto \color{blue}{0 \cdot s} \]

                              if 1.2e-20 < s

                              1. Initial program 99.1%

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

                                \[\leadsto \color{blue}{-1 \cdot \mathsf{PI}\left(\right)} \]
                              4. Step-by-step derivation
                                1. mul-1-negN/A

                                  \[\leadsto \color{blue}{\mathsf{neg}\left(\mathsf{PI}\left(\right)\right)} \]
                                2. lower-neg.f32N/A

                                  \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                                3. lower-PI.f3215.0

                                  \[\leadsto -\color{blue}{\mathsf{PI}\left(\right)} \]
                              5. Applied rewrites15.0%

                                \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                              6. Taylor expanded in s around inf

                                \[\leadsto \color{blue}{4 \cdot \left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) - \frac{1}{4} \cdot \mathsf{PI}\left(\right)\right)} \]
                              7. Step-by-step derivation
                                1. cancel-sign-sub-invN/A

                                  \[\leadsto 4 \cdot \color{blue}{\left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) + \left(\mathsf{neg}\left(\frac{1}{4}\right)\right) \cdot \mathsf{PI}\left(\right)\right)} \]
                                2. metadata-evalN/A

                                  \[\leadsto 4 \cdot \left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) + \color{blue}{\frac{-1}{4}} \cdot \mathsf{PI}\left(\right)\right) \]
                                3. distribute-lft-inN/A

                                  \[\leadsto \color{blue}{4 \cdot \left(u \cdot \left(\frac{1}{4} \cdot \mathsf{PI}\left(\right) - \frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)\right) + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right)} \]
                                4. distribute-rgt-out--N/A

                                  \[\leadsto 4 \cdot \left(u \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \left(\frac{1}{4} - \frac{-1}{4}\right)\right)}\right) + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) \]
                                5. metadata-evalN/A

                                  \[\leadsto 4 \cdot \left(u \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{1}{2}}\right)\right) + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) \]
                                6. associate-*r*N/A

                                  \[\leadsto 4 \cdot \color{blue}{\left(\left(u \cdot \mathsf{PI}\left(\right)\right) \cdot \frac{1}{2}\right)} + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) \]
                                7. *-commutativeN/A

                                  \[\leadsto 4 \cdot \color{blue}{\left(\frac{1}{2} \cdot \left(u \cdot \mathsf{PI}\left(\right)\right)\right)} + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) \]
                                8. associate-*r*N/A

                                  \[\leadsto \color{blue}{\left(4 \cdot \frac{1}{2}\right) \cdot \left(u \cdot \mathsf{PI}\left(\right)\right)} + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) \]
                                9. metadata-evalN/A

                                  \[\leadsto \color{blue}{2} \cdot \left(u \cdot \mathsf{PI}\left(\right)\right) + 4 \cdot \left(\frac{-1}{4} \cdot \mathsf{PI}\left(\right)\right) \]
                                10. associate-*r*N/A

                                  \[\leadsto 2 \cdot \left(u \cdot \mathsf{PI}\left(\right)\right) + \color{blue}{\left(4 \cdot \frac{-1}{4}\right) \cdot \mathsf{PI}\left(\right)} \]
                                11. metadata-evalN/A

                                  \[\leadsto 2 \cdot \left(u \cdot \mathsf{PI}\left(\right)\right) + \color{blue}{-1} \cdot \mathsf{PI}\left(\right) \]
                                12. lower-fma.f32N/A

                                  \[\leadsto \color{blue}{\mathsf{fma}\left(2, u \cdot \mathsf{PI}\left(\right), -1 \cdot \mathsf{PI}\left(\right)\right)} \]
                                13. *-commutativeN/A

                                  \[\leadsto \mathsf{fma}\left(2, \color{blue}{\mathsf{PI}\left(\right) \cdot u}, -1 \cdot \mathsf{PI}\left(\right)\right) \]
                                14. lower-*.f32N/A

                                  \[\leadsto \mathsf{fma}\left(2, \color{blue}{\mathsf{PI}\left(\right) \cdot u}, -1 \cdot \mathsf{PI}\left(\right)\right) \]
                                15. lower-PI.f32N/A

                                  \[\leadsto \mathsf{fma}\left(2, \color{blue}{\mathsf{PI}\left(\right)} \cdot u, -1 \cdot \mathsf{PI}\left(\right)\right) \]
                                16. mul-1-negN/A

                                  \[\leadsto \mathsf{fma}\left(2, \mathsf{PI}\left(\right) \cdot u, \color{blue}{\mathsf{neg}\left(\mathsf{PI}\left(\right)\right)}\right) \]
                                17. lower-neg.f32N/A

                                  \[\leadsto \mathsf{fma}\left(2, \mathsf{PI}\left(\right) \cdot u, \color{blue}{-\mathsf{PI}\left(\right)}\right) \]
                                18. lower-PI.f3215.0

                                  \[\leadsto \mathsf{fma}\left(2, \mathsf{PI}\left(\right) \cdot u, -\color{blue}{\mathsf{PI}\left(\right)}\right) \]
                              8. Applied rewrites15.0%

                                \[\leadsto \color{blue}{\mathsf{fma}\left(2, \mathsf{PI}\left(\right) \cdot u, -\mathsf{PI}\left(\right)\right)} \]
                              9. Step-by-step derivation
                                1. Applied rewrites15.4%

                                  \[\leadsto \left(u \cdot \mathsf{PI}\left(\right)\right) \cdot 2 - \color{blue}{\mathsf{PI}\left(\right)} \]
                              10. Recombined 2 regimes into one program.
                              11. Final simplification14.4%

                                \[\leadsto \begin{array}{l} \mathbf{if}\;s \leq 1.199999961918627 \cdot 10^{-20}:\\ \;\;\;\;0 \cdot s\\ \mathbf{else}:\\ \;\;\;\;\left(\mathsf{PI}\left(\right) \cdot u\right) \cdot 2 - \mathsf{PI}\left(\right)\\ \end{array} \]
                              12. Add Preprocessing

                              Alternative 13: 11.4% accurate, 170.0× speedup?

                              \[\begin{array}{l} \\ -\mathsf{PI}\left(\right) \end{array} \]
                              (FPCore (u s) :precision binary32 (- (PI)))
                              \begin{array}{l}
                              
                              \\
                              -\mathsf{PI}\left(\right)
                              \end{array}
                              
                              Derivation
                              1. Initial program 99.1%

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

                                \[\leadsto \color{blue}{-1 \cdot \mathsf{PI}\left(\right)} \]
                              4. Step-by-step derivation
                                1. mul-1-negN/A

                                  \[\leadsto \color{blue}{\mathsf{neg}\left(\mathsf{PI}\left(\right)\right)} \]
                                2. lower-neg.f32N/A

                                  \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                                3. lower-PI.f3211.0

                                  \[\leadsto -\color{blue}{\mathsf{PI}\left(\right)} \]
                              5. Applied rewrites11.0%

                                \[\leadsto \color{blue}{-\mathsf{PI}\left(\right)} \]
                              6. Add Preprocessing

                              Reproduce

                              ?
                              herbie shell --seed 2024267 
                              (FPCore (u s)
                                :name "Sample trimmed logistic on [-pi, pi]"
                                :precision binary32
                                :pre (and (and (<= 2.328306437e-10 u) (<= u 1.0)) (and (<= 0.0 s) (<= s 1.0651631)))
                                (* (- s) (log (- (/ 1.0 (+ (* u (- (/ 1.0 (+ 1.0 (exp (/ (- (PI)) s)))) (/ 1.0 (+ 1.0 (exp (/ (PI) s)))))) (/ 1.0 (+ 1.0 (exp (/ (PI) s)))))) 1.0))))