expfmod (used to be hard to sample)

Percentage Accurate: 6.7% → 66.0%
Time: 12.8s
Alternatives: 7
Speedup: 3.8×

Specification

?
\[\begin{array}{l} \\ \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \end{array} \]
(FPCore (x) :precision binary64 (* (fmod (exp x) (sqrt (cos x))) (exp (- x))))
double code(double x) {
	return fmod(exp(x), sqrt(cos(x))) * exp(-x);
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = mod(exp(x), sqrt(cos(x))) * exp(-x)
end function
def code(x):
	return math.fmod(math.exp(x), math.sqrt(math.cos(x))) * math.exp(-x)
function code(x)
	return Float64(rem(exp(x), sqrt(cos(x))) * exp(Float64(-x)))
end
code[x_] := N[(N[With[{TMP1 = N[Exp[x], $MachinePrecision], TMP2 = N[Sqrt[N[Cos[x], $MachinePrecision]], $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[Exp[(-x)], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}
\end{array}

Sampling outcomes in binary64 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 7 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: 6.7% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \end{array} \]
(FPCore (x) :precision binary64 (* (fmod (exp x) (sqrt (cos x))) (exp (- x))))
double code(double x) {
	return fmod(exp(x), sqrt(cos(x))) * exp(-x);
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = mod(exp(x), sqrt(cos(x))) * exp(-x)
end function
def code(x):
	return math.fmod(math.exp(x), math.sqrt(math.cos(x))) * math.exp(-x)
function code(x)
	return Float64(rem(exp(x), sqrt(cos(x))) * exp(Float64(-x)))
end
code[x_] := N[(N[With[{TMP1 = N[Exp[x], $MachinePrecision], TMP2 = N[Sqrt[N[Cos[x], $MachinePrecision]], $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[Exp[(-x)], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}
\end{array}

Alternative 1: 66.0% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -7.5 \cdot 10^{-155}:\\ \;\;\;\;\left(\left(x \cdot \left(0.16666666666666666 \cdot \left(x \cdot x\right) - x \cdot \left(-0.5 + \left(\frac{-1}{x} + \frac{-1}{x \cdot x}\right)\right)\right)\right) \bmod 1\right) \cdot e^{-x}\\ \mathbf{elif}\;x \leq 400:\\ \;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (if (<= x -7.5e-155)
   (*
    (fmod
     (*
      x
      (-
       (* 0.16666666666666666 (* x x))
       (* x (+ -0.5 (+ (/ -1.0 x) (/ -1.0 (* x x)))))))
     1.0)
    (exp (- x)))
   (if (<= x 400.0)
     (/ (fmod (fma x (* x (fma x 0.16666666666666666 0.5)) x) 1.0) (exp x))
     (* (fmod 1.0 1.0) (- 1.0 x)))))
double code(double x) {
	double tmp;
	if (x <= -7.5e-155) {
		tmp = fmod((x * ((0.16666666666666666 * (x * x)) - (x * (-0.5 + ((-1.0 / x) + (-1.0 / (x * x))))))), 1.0) * exp(-x);
	} else if (x <= 400.0) {
		tmp = fmod(fma(x, (x * fma(x, 0.16666666666666666, 0.5)), x), 1.0) / exp(x);
	} else {
		tmp = fmod(1.0, 1.0) * (1.0 - x);
	}
	return tmp;
}
function code(x)
	tmp = 0.0
	if (x <= -7.5e-155)
		tmp = Float64(rem(Float64(x * Float64(Float64(0.16666666666666666 * Float64(x * x)) - Float64(x * Float64(-0.5 + Float64(Float64(-1.0 / x) + Float64(-1.0 / Float64(x * x))))))), 1.0) * exp(Float64(-x)));
	elseif (x <= 400.0)
		tmp = Float64(rem(fma(x, Float64(x * fma(x, 0.16666666666666666, 0.5)), x), 1.0) / exp(x));
	else
		tmp = Float64(rem(1.0, 1.0) * Float64(1.0 - x));
	end
	return tmp
end
code[x_] := If[LessEqual[x, -7.5e-155], N[(N[With[{TMP1 = N[(x * N[(N[(0.16666666666666666 * N[(x * x), $MachinePrecision]), $MachinePrecision] - N[(x * N[(-0.5 + N[(N[(-1.0 / x), $MachinePrecision] + N[(-1.0 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[Exp[(-x)], $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 400.0], N[(N[With[{TMP1 = N[(x * N[(x * N[(x * 0.16666666666666666 + 0.5), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] / N[Exp[x], $MachinePrecision]), $MachinePrecision], N[(N[With[{TMP1 = 1.0, TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;x \leq -7.5 \cdot 10^{-155}:\\
\;\;\;\;\left(\left(x \cdot \left(0.16666666666666666 \cdot \left(x \cdot x\right) - x \cdot \left(-0.5 + \left(\frac{-1}{x} + \frac{-1}{x \cdot x}\right)\right)\right)\right) \bmod 1\right) \cdot e^{-x}\\

\mathbf{elif}\;x \leq 400:\\
\;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\

\mathbf{else}:\\
\;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if x < -7.5000000000000006e-155

    1. Initial program 18.4%

      \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{1}\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
    4. Step-by-step derivation
      1. Applied rewrites18.4%

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

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

          \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right)\right) + 1\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        2. lower-fma.f64N/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, 1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right), 1\right)\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        3. +-commutativeN/A

          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right) + 1}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        4. lower-fma.f64N/A

          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, \frac{1}{2} + \frac{1}{6} \cdot x, 1\right)}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        5. +-commutativeN/A

          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\frac{1}{6} \cdot x + \frac{1}{2}}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        6. *-commutativeN/A

          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{x \cdot \frac{1}{6}} + \frac{1}{2}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        7. lower-fma.f6417.1

          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{-x} \]
      4. Applied rewrites17.1%

        \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), 1\right), 1\right)\right)} \bmod 1\right) \cdot e^{-x} \]
      5. Taylor expanded in x around -inf

        \[\leadsto \left(\left(-1 \cdot \color{blue}{\left({x}^{3} \cdot \left(-1 \cdot \frac{\frac{1}{2} + \left(\frac{1}{x} + \frac{1}{{x}^{2}}\right)}{x} - \frac{1}{6}\right)\right)}\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
      6. Applied rewrites30.6%

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

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

        if -7.5000000000000006e-155 < x < 400

        1. Initial program 6.4%

          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{1}\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
        4. Step-by-step derivation
          1. Applied rewrites6.0%

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

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

              \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right)\right) + 1\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
            2. lower-fma.f64N/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, 1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right), 1\right)\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
            3. +-commutativeN/A

              \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right) + 1}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
            4. lower-fma.f64N/A

              \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, \frac{1}{2} + \frac{1}{6} \cdot x, 1\right)}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
            5. +-commutativeN/A

              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\frac{1}{6} \cdot x + \frac{1}{2}}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
            6. *-commutativeN/A

              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{x \cdot \frac{1}{6}} + \frac{1}{2}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
            7. lower-fma.f646.0

              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{-x} \]
          4. Applied rewrites6.0%

            \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), 1\right), 1\right)\right)} \bmod 1\right) \cdot e^{-x} \]
          5. Taylor expanded in x around inf

            \[\leadsto \left(\left({x}^{3} \cdot \color{blue}{\left(\frac{1}{6} + \left(\frac{1}{2} \cdot \frac{1}{x} + \frac{1}{{x}^{2}}\right)\right)}\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
          6. Step-by-step derivation
            1. Applied rewrites67.4%

              \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, x\right)\right) \bmod 1\right) \cdot e^{-x} \]
            2. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)}} \]
              2. lift-exp.f64N/A

                \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot \color{blue}{e^{\mathsf{neg}\left(x\right)}} \]
              3. lift-neg.f64N/A

                \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
              4. exp-negN/A

                \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
              5. un-div-invN/A

                \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]
              6. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]
              7. lift-exp.f6467.4

                \[\leadsto \frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{\color{blue}{e^{x}}} \]
            3. Applied rewrites67.4%

              \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]

            if 400 < x

            1. Initial program 0.0%

              \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
            2. Add Preprocessing
            3. Taylor expanded in x around 0

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

                \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
              2. neg-mul-1N/A

                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
              3. distribute-lft1-inN/A

                \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
              4. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
              5. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
              6. lower-fmod.f64N/A

                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
              7. lower-exp.f64N/A

                \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
              8. lower-sqrt.f64N/A

                \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
              9. lower-cos.f64N/A

                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
              10. +-commutativeN/A

                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
              11. unsub-negN/A

                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
              12. lower--.f640.0

                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
            5. Applied rewrites0.0%

              \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
            6. Taylor expanded in x around 0

              \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
            7. Step-by-step derivation
              1. Applied rewrites0.0%

                \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
              2. Taylor expanded in x around 0

                \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
              3. Step-by-step derivation
                1. Applied rewrites100.0%

                  \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
              4. Recombined 3 regimes into one program.
              5. Add Preprocessing

              Alternative 2: 64.0% accurate, 1.6× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -5 \cdot 10^{-17}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\ \mathbf{elif}\;x \leq -7.5 \cdot 10^{-155}:\\ \;\;\;\;e^{-x} \cdot \left(\left(x \cdot \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) - \left(x \cdot x\right) \cdot \frac{-1}{x \cdot x}\right) \bmod 1\right)\\ \mathbf{elif}\;x \leq 400:\\ \;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \end{array} \]
              (FPCore (x)
               :precision binary64
               (if (<= x -5e-17)
                 (*
                  (fmod (fma x (fma x 0.5 1.0) 1.0) (fma x (* x -0.25) 1.0))
                  (fma x (fma x 0.5 -1.0) 1.0))
                 (if (<= x -7.5e-155)
                   (*
                    (exp (- x))
                    (fmod
                     (- (* x (* 0.16666666666666666 (* x x))) (* (* x x) (/ -1.0 (* x x))))
                     1.0))
                   (if (<= x 400.0)
                     (/ (fmod (fma x (* x (fma x 0.16666666666666666 0.5)) x) 1.0) (exp x))
                     (* (fmod 1.0 1.0) (- 1.0 x))))))
              double code(double x) {
              	double tmp;
              	if (x <= -5e-17) {
              		tmp = fmod(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, (x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0);
              	} else if (x <= -7.5e-155) {
              		tmp = exp(-x) * fmod(((x * (0.16666666666666666 * (x * x))) - ((x * x) * (-1.0 / (x * x)))), 1.0);
              	} else if (x <= 400.0) {
              		tmp = fmod(fma(x, (x * fma(x, 0.16666666666666666, 0.5)), x), 1.0) / exp(x);
              	} else {
              		tmp = fmod(1.0, 1.0) * (1.0 - x);
              	}
              	return tmp;
              }
              
              function code(x)
              	tmp = 0.0
              	if (x <= -5e-17)
              		tmp = Float64(rem(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, Float64(x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0));
              	elseif (x <= -7.5e-155)
              		tmp = Float64(exp(Float64(-x)) * rem(Float64(Float64(x * Float64(0.16666666666666666 * Float64(x * x))) - Float64(Float64(x * x) * Float64(-1.0 / Float64(x * x)))), 1.0));
              	elseif (x <= 400.0)
              		tmp = Float64(rem(fma(x, Float64(x * fma(x, 0.16666666666666666, 0.5)), x), 1.0) / exp(x));
              	else
              		tmp = Float64(rem(1.0, 1.0) * Float64(1.0 - x));
              	end
              	return tmp
              end
              
              code[x_] := If[LessEqual[x, -5e-17], N[(N[With[{TMP1 = N[(x * N[(x * 0.5 + 1.0), $MachinePrecision] + 1.0), $MachinePrecision], TMP2 = N[(x * N[(x * -0.25), $MachinePrecision] + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(x * N[(x * 0.5 + -1.0), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, -7.5e-155], N[(N[Exp[(-x)], $MachinePrecision] * N[With[{TMP1 = N[(N[(x * N[(0.16666666666666666 * N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[(x * x), $MachinePrecision] * N[(-1.0 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 400.0], N[(N[With[{TMP1 = N[(x * N[(x * N[(x * 0.16666666666666666 + 0.5), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] / N[Exp[x], $MachinePrecision]), $MachinePrecision], N[(N[With[{TMP1 = 1.0, TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]]]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              \mathbf{if}\;x \leq -5 \cdot 10^{-17}:\\
              \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\
              
              \mathbf{elif}\;x \leq -7.5 \cdot 10^{-155}:\\
              \;\;\;\;e^{-x} \cdot \left(\left(x \cdot \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) - \left(x \cdot x\right) \cdot \frac{-1}{x \cdot x}\right) \bmod 1\right)\\
              
              \mathbf{elif}\;x \leq 400:\\
              \;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\
              
              \mathbf{else}:\\
              \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 4 regimes
              2. if x < -4.9999999999999999e-17

                1. Initial program 74.6%

                  \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                2. Add Preprocessing
                3. Taylor expanded in x around 0

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

                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right)} \]
                  2. *-rgt-identityN/A

                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1} + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \]
                  3. *-commutativeN/A

                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \cdot x} \]
                  4. +-commutativeN/A

                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)} \cdot x \]
                  5. associate-*r*N/A

                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \left(\color{blue}{\left(\frac{1}{2} \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) \cdot x \]
                  6. distribute-rgt-outN/A

                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\frac{1}{2} \cdot x + -1\right)\right)} \cdot x \]
                  7. associate-*l*N/A

                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                  8. distribute-lft-outN/A

                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 + \left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                5. Applied rewrites66.7%

                  \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)} \]
                6. Taylor expanded in x around 0

                  \[\leadsto \left(\left(e^{x}\right) \bmod \left(1 + \frac{-1}{4} \cdot {x}^{2}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                7. Step-by-step derivation
                  1. Applied rewrites66.7%

                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]
                  2. Taylor expanded in x around 0

                    \[\leadsto \left(\left(1 + x \cdot \left(1 + \frac{1}{2} \cdot x\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot \frac{-1}{4}, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                  3. Step-by-step derivation
                    1. Applied rewrites70.0%

                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]

                    if -4.9999999999999999e-17 < x < -7.5000000000000006e-155

                    1. Initial program 3.1%

                      \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                    2. Add Preprocessing
                    3. Taylor expanded in x around 0

                      \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{1}\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                    4. Step-by-step derivation
                      1. Applied rewrites3.1%

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

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

                          \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right)\right) + 1\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        2. lower-fma.f64N/A

                          \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, 1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right), 1\right)\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        3. +-commutativeN/A

                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right) + 1}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        4. lower-fma.f64N/A

                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, \frac{1}{2} + \frac{1}{6} \cdot x, 1\right)}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        5. +-commutativeN/A

                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\frac{1}{6} \cdot x + \frac{1}{2}}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        6. *-commutativeN/A

                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{x \cdot \frac{1}{6}} + \frac{1}{2}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        7. lower-fma.f643.1

                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{-x} \]
                      4. Applied rewrites3.1%

                        \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), 1\right), 1\right)\right)} \bmod 1\right) \cdot e^{-x} \]
                      5. Taylor expanded in x around -inf

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

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

                        \[\leadsto \left(\left(x \cdot \left(\frac{1}{6} \cdot \left(x \cdot x\right)\right) - \left(x \cdot x\right) \cdot \frac{-1}{{x}^{\color{blue}{2}}}\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                      8. Step-by-step derivation
                        1. Applied rewrites20.5%

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

                        if -7.5000000000000006e-155 < x < 400

                        1. Initial program 6.4%

                          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                        2. Add Preprocessing
                        3. Taylor expanded in x around 0

                          \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{1}\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                        4. Step-by-step derivation
                          1. Applied rewrites6.0%

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

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

                              \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right)\right) + 1\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                            2. lower-fma.f64N/A

                              \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, 1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right), 1\right)\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                            3. +-commutativeN/A

                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right) + 1}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                            4. lower-fma.f64N/A

                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, \frac{1}{2} + \frac{1}{6} \cdot x, 1\right)}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                            5. +-commutativeN/A

                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\frac{1}{6} \cdot x + \frac{1}{2}}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                            6. *-commutativeN/A

                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{x \cdot \frac{1}{6}} + \frac{1}{2}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                            7. lower-fma.f646.0

                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{-x} \]
                          4. Applied rewrites6.0%

                            \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), 1\right), 1\right)\right)} \bmod 1\right) \cdot e^{-x} \]
                          5. Taylor expanded in x around inf

                            \[\leadsto \left(\left({x}^{3} \cdot \color{blue}{\left(\frac{1}{6} + \left(\frac{1}{2} \cdot \frac{1}{x} + \frac{1}{{x}^{2}}\right)\right)}\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                          6. Step-by-step derivation
                            1. Applied rewrites67.4%

                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, x\right)\right) \bmod 1\right) \cdot e^{-x} \]
                            2. Step-by-step derivation
                              1. lift-*.f64N/A

                                \[\leadsto \color{blue}{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)}} \]
                              2. lift-exp.f64N/A

                                \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot \color{blue}{e^{\mathsf{neg}\left(x\right)}} \]
                              3. lift-neg.f64N/A

                                \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
                              4. exp-negN/A

                                \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
                              5. un-div-invN/A

                                \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]
                              6. lower-/.f64N/A

                                \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]
                              7. lift-exp.f6467.4

                                \[\leadsto \frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{\color{blue}{e^{x}}} \]
                            3. Applied rewrites67.4%

                              \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]

                            if 400 < x

                            1. Initial program 0.0%

                              \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                            2. Add Preprocessing
                            3. Taylor expanded in x around 0

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

                                \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                              2. neg-mul-1N/A

                                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                              3. distribute-lft1-inN/A

                                \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
                              4. *-commutativeN/A

                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                              5. lower-*.f64N/A

                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                              6. lower-fmod.f64N/A

                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                              7. lower-exp.f64N/A

                                \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                              8. lower-sqrt.f64N/A

                                \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                              9. lower-cos.f64N/A

                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                              10. +-commutativeN/A

                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
                              11. unsub-negN/A

                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                              12. lower--.f640.0

                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                            5. Applied rewrites0.0%

                              \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
                            6. Taylor expanded in x around 0

                              \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                            7. Step-by-step derivation
                              1. Applied rewrites0.0%

                                \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                              2. Taylor expanded in x around 0

                                \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                              3. Step-by-step derivation
                                1. Applied rewrites100.0%

                                  \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                              4. Recombined 4 regimes into one program.
                              5. Final simplification65.2%

                                \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -5 \cdot 10^{-17}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\ \mathbf{elif}\;x \leq -7.5 \cdot 10^{-155}:\\ \;\;\;\;e^{-x} \cdot \left(\left(x \cdot \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) - \left(x \cdot x\right) \cdot \frac{-1}{x \cdot x}\right) \bmod 1\right)\\ \mathbf{elif}\;x \leq 400:\\ \;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \]
                              6. Add Preprocessing

                              Alternative 3: 61.8% accurate, 1.7× speedup?

                              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -5 \cdot 10^{-310}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\ \mathbf{elif}\;x \leq 400:\\ \;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \end{array} \]
                              (FPCore (x)
                               :precision binary64
                               (if (<= x -5e-310)
                                 (*
                                  (fmod (fma x (fma x 0.5 1.0) 1.0) (fma x (* x -0.25) 1.0))
                                  (fma x (fma x 0.5 -1.0) 1.0))
                                 (if (<= x 400.0)
                                   (/ (fmod (fma x (* x (fma x 0.16666666666666666 0.5)) x) 1.0) (exp x))
                                   (* (fmod 1.0 1.0) (- 1.0 x)))))
                              double code(double x) {
                              	double tmp;
                              	if (x <= -5e-310) {
                              		tmp = fmod(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, (x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0);
                              	} else if (x <= 400.0) {
                              		tmp = fmod(fma(x, (x * fma(x, 0.16666666666666666, 0.5)), x), 1.0) / exp(x);
                              	} else {
                              		tmp = fmod(1.0, 1.0) * (1.0 - x);
                              	}
                              	return tmp;
                              }
                              
                              function code(x)
                              	tmp = 0.0
                              	if (x <= -5e-310)
                              		tmp = Float64(rem(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, Float64(x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0));
                              	elseif (x <= 400.0)
                              		tmp = Float64(rem(fma(x, Float64(x * fma(x, 0.16666666666666666, 0.5)), x), 1.0) / exp(x));
                              	else
                              		tmp = Float64(rem(1.0, 1.0) * Float64(1.0 - x));
                              	end
                              	return tmp
                              end
                              
                              code[x_] := If[LessEqual[x, -5e-310], N[(N[With[{TMP1 = N[(x * N[(x * 0.5 + 1.0), $MachinePrecision] + 1.0), $MachinePrecision], TMP2 = N[(x * N[(x * -0.25), $MachinePrecision] + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(x * N[(x * 0.5 + -1.0), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 400.0], N[(N[With[{TMP1 = N[(x * N[(x * N[(x * 0.16666666666666666 + 0.5), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] / N[Exp[x], $MachinePrecision]), $MachinePrecision], N[(N[With[{TMP1 = 1.0, TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]]]
                              
                              \begin{array}{l}
                              
                              \\
                              \begin{array}{l}
                              \mathbf{if}\;x \leq -5 \cdot 10^{-310}:\\
                              \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\
                              
                              \mathbf{elif}\;x \leq 400:\\
                              \;\;\;\;\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}\\
                              
                              \mathbf{else}:\\
                              \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\
                              
                              
                              \end{array}
                              \end{array}
                              
                              Derivation
                              1. Split input into 3 regimes
                              2. if x < -4.999999999999985e-310

                                1. Initial program 11.2%

                                  \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                2. Add Preprocessing
                                3. Taylor expanded in x around 0

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

                                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right)} \]
                                  2. *-rgt-identityN/A

                                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1} + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \]
                                  3. *-commutativeN/A

                                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \cdot x} \]
                                  4. +-commutativeN/A

                                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)} \cdot x \]
                                  5. associate-*r*N/A

                                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \left(\color{blue}{\left(\frac{1}{2} \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) \cdot x \]
                                  6. distribute-rgt-outN/A

                                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\frac{1}{2} \cdot x + -1\right)\right)} \cdot x \]
                                  7. associate-*l*N/A

                                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                                  8. distribute-lft-outN/A

                                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 + \left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                                5. Applied rewrites10.3%

                                  \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)} \]
                                6. Taylor expanded in x around 0

                                  \[\leadsto \left(\left(e^{x}\right) \bmod \left(1 + \frac{-1}{4} \cdot {x}^{2}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                                7. Step-by-step derivation
                                  1. Applied rewrites10.3%

                                    \[\leadsto \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]
                                  2. Taylor expanded in x around 0

                                    \[\leadsto \left(\left(1 + x \cdot \left(1 + \frac{1}{2} \cdot x\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot \frac{-1}{4}, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                                  3. Step-by-step derivation
                                    1. Applied rewrites10.7%

                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]

                                    if -4.999999999999985e-310 < x < 400

                                    1. Initial program 8.0%

                                      \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                    2. Add Preprocessing
                                    3. Taylor expanded in x around 0

                                      \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{1}\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                    4. Step-by-step derivation
                                      1. Applied rewrites7.3%

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

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

                                          \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right)\right) + 1\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                        2. lower-fma.f64N/A

                                          \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, 1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right), 1\right)\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                        3. +-commutativeN/A

                                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right) + 1}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                        4. lower-fma.f64N/A

                                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, \frac{1}{2} + \frac{1}{6} \cdot x, 1\right)}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                        5. +-commutativeN/A

                                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\frac{1}{6} \cdot x + \frac{1}{2}}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                        6. *-commutativeN/A

                                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{x \cdot \frac{1}{6}} + \frac{1}{2}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                        7. lower-fma.f647.3

                                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{-x} \]
                                      4. Applied rewrites7.3%

                                        \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), 1\right), 1\right)\right)} \bmod 1\right) \cdot e^{-x} \]
                                      5. Taylor expanded in x around inf

                                        \[\leadsto \left(\left({x}^{3} \cdot \color{blue}{\left(\frac{1}{6} + \left(\frac{1}{2} \cdot \frac{1}{x} + \frac{1}{{x}^{2}}\right)\right)}\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                      6. Step-by-step derivation
                                        1. Applied rewrites98.3%

                                          \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, x\right)\right) \bmod 1\right) \cdot e^{-x} \]
                                        2. Step-by-step derivation
                                          1. lift-*.f64N/A

                                            \[\leadsto \color{blue}{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)}} \]
                                          2. lift-exp.f64N/A

                                            \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot \color{blue}{e^{\mathsf{neg}\left(x\right)}} \]
                                          3. lift-neg.f64N/A

                                            \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
                                          4. exp-negN/A

                                            \[\leadsto \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
                                          5. un-div-invN/A

                                            \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]
                                          6. lower-/.f64N/A

                                            \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, \frac{1}{6}, \frac{1}{2}\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]
                                          7. lift-exp.f6498.3

                                            \[\leadsto \frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{\color{blue}{e^{x}}} \]
                                        3. Applied rewrites98.3%

                                          \[\leadsto \color{blue}{\frac{\left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)}{e^{x}}} \]

                                        if 400 < x

                                        1. Initial program 0.0%

                                          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                        2. Add Preprocessing
                                        3. Taylor expanded in x around 0

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

                                            \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                          2. neg-mul-1N/A

                                            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                          3. distribute-lft1-inN/A

                                            \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
                                          4. *-commutativeN/A

                                            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                          5. lower-*.f64N/A

                                            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                          6. lower-fmod.f64N/A

                                            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                          7. lower-exp.f64N/A

                                            \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                          8. lower-sqrt.f64N/A

                                            \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                          9. lower-cos.f64N/A

                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                          10. +-commutativeN/A

                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
                                          11. unsub-negN/A

                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                          12. lower--.f640.0

                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                        5. Applied rewrites0.0%

                                          \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
                                        6. Taylor expanded in x around 0

                                          \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                        7. Step-by-step derivation
                                          1. Applied rewrites0.0%

                                            \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                          2. Taylor expanded in x around 0

                                            \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                          3. Step-by-step derivation
                                            1. Applied rewrites100.0%

                                              \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                          4. Recombined 3 regimes into one program.
                                          5. Add Preprocessing

                                          Alternative 4: 61.8% accurate, 1.8× speedup?

                                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -5 \cdot 10^{-310}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\ \mathbf{elif}\;x \leq 400:\\ \;\;\;\;e^{-x} \cdot \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \end{array} \]
                                          (FPCore (x)
                                           :precision binary64
                                           (if (<= x -5e-310)
                                             (*
                                              (fmod (fma x (fma x 0.5 1.0) 1.0) (fma x (* x -0.25) 1.0))
                                              (fma x (fma x 0.5 -1.0) 1.0))
                                             (if (<= x 400.0)
                                               (* (exp (- x)) (fmod (fma x (* x (fma x 0.16666666666666666 0.5)) x) 1.0))
                                               (* (fmod 1.0 1.0) (- 1.0 x)))))
                                          double code(double x) {
                                          	double tmp;
                                          	if (x <= -5e-310) {
                                          		tmp = fmod(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, (x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0);
                                          	} else if (x <= 400.0) {
                                          		tmp = exp(-x) * fmod(fma(x, (x * fma(x, 0.16666666666666666, 0.5)), x), 1.0);
                                          	} else {
                                          		tmp = fmod(1.0, 1.0) * (1.0 - x);
                                          	}
                                          	return tmp;
                                          }
                                          
                                          function code(x)
                                          	tmp = 0.0
                                          	if (x <= -5e-310)
                                          		tmp = Float64(rem(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, Float64(x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0));
                                          	elseif (x <= 400.0)
                                          		tmp = Float64(exp(Float64(-x)) * rem(fma(x, Float64(x * fma(x, 0.16666666666666666, 0.5)), x), 1.0));
                                          	else
                                          		tmp = Float64(rem(1.0, 1.0) * Float64(1.0 - x));
                                          	end
                                          	return tmp
                                          end
                                          
                                          code[x_] := If[LessEqual[x, -5e-310], N[(N[With[{TMP1 = N[(x * N[(x * 0.5 + 1.0), $MachinePrecision] + 1.0), $MachinePrecision], TMP2 = N[(x * N[(x * -0.25), $MachinePrecision] + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(x * N[(x * 0.5 + -1.0), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 400.0], N[(N[Exp[(-x)], $MachinePrecision] * N[With[{TMP1 = N[(x * N[(x * N[(x * 0.16666666666666666 + 0.5), $MachinePrecision]), $MachinePrecision] + x), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision]), $MachinePrecision], N[(N[With[{TMP1 = 1.0, TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]]]
                                          
                                          \begin{array}{l}
                                          
                                          \\
                                          \begin{array}{l}
                                          \mathbf{if}\;x \leq -5 \cdot 10^{-310}:\\
                                          \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\
                                          
                                          \mathbf{elif}\;x \leq 400:\\
                                          \;\;\;\;e^{-x} \cdot \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)\\
                                          
                                          \mathbf{else}:\\
                                          \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\
                                          
                                          
                                          \end{array}
                                          \end{array}
                                          
                                          Derivation
                                          1. Split input into 3 regimes
                                          2. if x < -4.999999999999985e-310

                                            1. Initial program 11.2%

                                              \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                            2. Add Preprocessing
                                            3. Taylor expanded in x around 0

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

                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right)} \]
                                              2. *-rgt-identityN/A

                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1} + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \]
                                              3. *-commutativeN/A

                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \cdot x} \]
                                              4. +-commutativeN/A

                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)} \cdot x \]
                                              5. associate-*r*N/A

                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \left(\color{blue}{\left(\frac{1}{2} \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) \cdot x \]
                                              6. distribute-rgt-outN/A

                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\frac{1}{2} \cdot x + -1\right)\right)} \cdot x \]
                                              7. associate-*l*N/A

                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                                              8. distribute-lft-outN/A

                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 + \left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                                            5. Applied rewrites10.3%

                                              \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)} \]
                                            6. Taylor expanded in x around 0

                                              \[\leadsto \left(\left(e^{x}\right) \bmod \left(1 + \frac{-1}{4} \cdot {x}^{2}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                                            7. Step-by-step derivation
                                              1. Applied rewrites10.3%

                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]
                                              2. Taylor expanded in x around 0

                                                \[\leadsto \left(\left(1 + x \cdot \left(1 + \frac{1}{2} \cdot x\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot \frac{-1}{4}, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                                              3. Step-by-step derivation
                                                1. Applied rewrites10.7%

                                                  \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]

                                                if -4.999999999999985e-310 < x < 400

                                                1. Initial program 8.0%

                                                  \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                                2. Add Preprocessing
                                                3. Taylor expanded in x around 0

                                                  \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{1}\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                4. Step-by-step derivation
                                                  1. Applied rewrites7.3%

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

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

                                                      \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right)\right) + 1\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                    2. lower-fma.f64N/A

                                                      \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, 1 + x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right), 1\right)\right)} \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                    3. +-commutativeN/A

                                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot x\right) + 1}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                    4. lower-fma.f64N/A

                                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, \frac{1}{2} + \frac{1}{6} \cdot x, 1\right)}, 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                    5. +-commutativeN/A

                                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\frac{1}{6} \cdot x + \frac{1}{2}}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                    6. *-commutativeN/A

                                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{x \cdot \frac{1}{6}} + \frac{1}{2}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                    7. lower-fma.f647.3

                                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \color{blue}{\mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, 1\right), 1\right)\right) \bmod 1\right) \cdot e^{-x} \]
                                                  4. Applied rewrites7.3%

                                                    \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), 1\right), 1\right)\right)} \bmod 1\right) \cdot e^{-x} \]
                                                  5. Taylor expanded in x around inf

                                                    \[\leadsto \left(\left({x}^{3} \cdot \color{blue}{\left(\frac{1}{6} + \left(\frac{1}{2} \cdot \frac{1}{x} + \frac{1}{{x}^{2}}\right)\right)}\right) \bmod 1\right) \cdot e^{\mathsf{neg}\left(x\right)} \]
                                                  6. Step-by-step derivation
                                                    1. Applied rewrites98.3%

                                                      \[\leadsto \left(\left(\mathsf{fma}\left(x, \color{blue}{x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right)}, x\right)\right) \bmod 1\right) \cdot e^{-x} \]

                                                    if 400 < x

                                                    1. Initial program 0.0%

                                                      \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                                    2. Add Preprocessing
                                                    3. Taylor expanded in x around 0

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

                                                        \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                      2. neg-mul-1N/A

                                                        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                      3. distribute-lft1-inN/A

                                                        \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
                                                      4. *-commutativeN/A

                                                        \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                      5. lower-*.f64N/A

                                                        \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                      6. lower-fmod.f64N/A

                                                        \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                      7. lower-exp.f64N/A

                                                        \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                      8. lower-sqrt.f64N/A

                                                        \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                      9. lower-cos.f64N/A

                                                        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                      10. +-commutativeN/A

                                                        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
                                                      11. unsub-negN/A

                                                        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                      12. lower--.f640.0

                                                        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                    5. Applied rewrites0.0%

                                                      \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
                                                    6. Taylor expanded in x around 0

                                                      \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                    7. Step-by-step derivation
                                                      1. Applied rewrites0.0%

                                                        \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                      2. Taylor expanded in x around 0

                                                        \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                                      3. Step-by-step derivation
                                                        1. Applied rewrites100.0%

                                                          \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                                      4. Recombined 3 regimes into one program.
                                                      5. Final simplification62.3%

                                                        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -5 \cdot 10^{-310}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\ \mathbf{elif}\;x \leq 400:\\ \;\;\;\;e^{-x} \cdot \left(\left(\mathsf{fma}\left(x, x \cdot \mathsf{fma}\left(x, 0.16666666666666666, 0.5\right), x\right)\right) \bmod 1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \]
                                                      6. Add Preprocessing

                                                      Alternative 5: 25.7% accurate, 2.8× speedup?

                                                      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq 400:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\ \end{array} \end{array} \]
                                                      (FPCore (x)
                                                       :precision binary64
                                                       (if (<= x 400.0)
                                                         (*
                                                          (fmod (fma x (fma x 0.5 1.0) 1.0) (fma x (* x -0.25) 1.0))
                                                          (fma x (fma x 0.5 -1.0) 1.0))
                                                         (* (fmod 1.0 1.0) (- 1.0 x))))
                                                      double code(double x) {
                                                      	double tmp;
                                                      	if (x <= 400.0) {
                                                      		tmp = fmod(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, (x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0);
                                                      	} else {
                                                      		tmp = fmod(1.0, 1.0) * (1.0 - x);
                                                      	}
                                                      	return tmp;
                                                      }
                                                      
                                                      function code(x)
                                                      	tmp = 0.0
                                                      	if (x <= 400.0)
                                                      		tmp = Float64(rem(fma(x, fma(x, 0.5, 1.0), 1.0), fma(x, Float64(x * -0.25), 1.0)) * fma(x, fma(x, 0.5, -1.0), 1.0));
                                                      	else
                                                      		tmp = Float64(rem(1.0, 1.0) * Float64(1.0 - x));
                                                      	end
                                                      	return tmp
                                                      end
                                                      
                                                      code[x_] := If[LessEqual[x, 400.0], N[(N[With[{TMP1 = N[(x * N[(x * 0.5 + 1.0), $MachinePrecision] + 1.0), $MachinePrecision], TMP2 = N[(x * N[(x * -0.25), $MachinePrecision] + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(x * N[(x * 0.5 + -1.0), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], N[(N[With[{TMP1 = 1.0, TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]]
                                                      
                                                      \begin{array}{l}
                                                      
                                                      \\
                                                      \begin{array}{l}
                                                      \mathbf{if}\;x \leq 400:\\
                                                      \;\;\;\;\left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)\\
                                                      
                                                      \mathbf{else}:\\
                                                      \;\;\;\;\left(1 \bmod 1\right) \cdot \left(1 - x\right)\\
                                                      
                                                      
                                                      \end{array}
                                                      \end{array}
                                                      
                                                      Derivation
                                                      1. Split input into 2 regimes
                                                      2. if x < 400

                                                        1. Initial program 9.6%

                                                          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                                        2. Add Preprocessing
                                                        3. Taylor expanded in x around 0

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

                                                            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right)} \]
                                                          2. *-rgt-identityN/A

                                                            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1} + x \cdot \left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \]
                                                          3. *-commutativeN/A

                                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(-1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)\right) \cdot x} \]
                                                          4. +-commutativeN/A

                                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\frac{1}{2} \cdot \left(x \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right)} \cdot x \]
                                                          5. associate-*r*N/A

                                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \left(\color{blue}{\left(\frac{1}{2} \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + -1 \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)\right) \cdot x \]
                                                          6. distribute-rgt-outN/A

                                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\frac{1}{2} \cdot x + -1\right)\right)} \cdot x \]
                                                          7. associate-*l*N/A

                                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot 1 + \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                                                          8. distribute-lft-outN/A

                                                            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 + \left(\frac{1}{2} \cdot x + -1\right) \cdot x\right)} \]
                                                        5. Applied rewrites9.1%

                                                          \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right)} \]
                                                        6. Taylor expanded in x around 0

                                                          \[\leadsto \left(\left(e^{x}\right) \bmod \left(1 + \frac{-1}{4} \cdot {x}^{2}\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                                                        7. Step-by-step derivation
                                                          1. Applied rewrites9.0%

                                                            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]
                                                          2. Taylor expanded in x around 0

                                                            \[\leadsto \left(\left(1 + x \cdot \left(1 + \frac{1}{2} \cdot x\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot \frac{-1}{4}, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, \frac{1}{2}, -1\right), 1\right) \]
                                                          3. Step-by-step derivation
                                                            1. Applied rewrites9.2%

                                                              \[\leadsto \left(\left(\mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, 1\right), 1\right)\right) \bmod \left(\mathsf{fma}\left(x, x \cdot -0.25, 1\right)\right)\right) \cdot \mathsf{fma}\left(x, \mathsf{fma}\left(x, 0.5, -1\right), 1\right) \]

                                                            if 400 < x

                                                            1. Initial program 0.0%

                                                              \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                                            2. Add Preprocessing
                                                            3. Taylor expanded in x around 0

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

                                                                \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                              2. neg-mul-1N/A

                                                                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                              3. distribute-lft1-inN/A

                                                                \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
                                                              4. *-commutativeN/A

                                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                              5. lower-*.f64N/A

                                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                              6. lower-fmod.f64N/A

                                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                              7. lower-exp.f64N/A

                                                                \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                              8. lower-sqrt.f64N/A

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                              9. lower-cos.f64N/A

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                              10. +-commutativeN/A

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
                                                              11. unsub-negN/A

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                              12. lower--.f640.0

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                            5. Applied rewrites0.0%

                                                              \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
                                                            6. Taylor expanded in x around 0

                                                              \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                            7. Step-by-step derivation
                                                              1. Applied rewrites0.0%

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                              2. Taylor expanded in x around 0

                                                                \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                                              3. Step-by-step derivation
                                                                1. Applied rewrites100.0%

                                                                  \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                                              4. Recombined 2 regimes into one program.
                                                              5. Add Preprocessing

                                                              Alternative 6: 24.3% accurate, 3.7× speedup?

                                                              \[\begin{array}{l} \\ \left(1 - x\right) \cdot \left(\left(x + 1\right) \bmod 1\right) \end{array} \]
                                                              (FPCore (x) :precision binary64 (* (- 1.0 x) (fmod (+ x 1.0) 1.0)))
                                                              double code(double x) {
                                                              	return (1.0 - x) * fmod((x + 1.0), 1.0);
                                                              }
                                                              
                                                              real(8) function code(x)
                                                                  real(8), intent (in) :: x
                                                                  code = (1.0d0 - x) * mod((x + 1.0d0), 1.0d0)
                                                              end function
                                                              
                                                              def code(x):
                                                              	return (1.0 - x) * math.fmod((x + 1.0), 1.0)
                                                              
                                                              function code(x)
                                                              	return Float64(Float64(1.0 - x) * rem(Float64(x + 1.0), 1.0))
                                                              end
                                                              
                                                              code[x_] := N[(N[(1.0 - x), $MachinePrecision] * N[With[{TMP1 = N[(x + 1.0), $MachinePrecision], TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision]), $MachinePrecision]
                                                              
                                                              \begin{array}{l}
                                                              
                                                              \\
                                                              \left(1 - x\right) \cdot \left(\left(x + 1\right) \bmod 1\right)
                                                              \end{array}
                                                              
                                                              Derivation
                                                              1. Initial program 7.9%

                                                                \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                                              2. Add Preprocessing
                                                              3. Taylor expanded in x around 0

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

                                                                  \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                                2. neg-mul-1N/A

                                                                  \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                                3. distribute-lft1-inN/A

                                                                  \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
                                                                4. *-commutativeN/A

                                                                  \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                                5. lower-*.f64N/A

                                                                  \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                                6. lower-fmod.f64N/A

                                                                  \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                7. lower-exp.f64N/A

                                                                  \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                8. lower-sqrt.f64N/A

                                                                  \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                9. lower-cos.f64N/A

                                                                  \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                10. +-commutativeN/A

                                                                  \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
                                                                11. unsub-negN/A

                                                                  \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                                12. lower--.f647.2

                                                                  \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                              5. Applied rewrites7.2%

                                                                \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
                                                              6. Taylor expanded in x around 0

                                                                \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                              7. Step-by-step derivation
                                                                1. Applied rewrites7.1%

                                                                  \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                2. Taylor expanded in x around 0

                                                                  \[\leadsto \left(\left(1 + x\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                3. Step-by-step derivation
                                                                  1. Applied rewrites23.5%

                                                                    \[\leadsto \left(\left(x + 1\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                  2. Final simplification23.5%

                                                                    \[\leadsto \left(1 - x\right) \cdot \left(\left(x + 1\right) \bmod 1\right) \]
                                                                  3. Add Preprocessing

                                                                  Alternative 7: 23.0% accurate, 3.8× speedup?

                                                                  \[\begin{array}{l} \\ \left(1 \bmod 1\right) \cdot \left(1 - x\right) \end{array} \]
                                                                  (FPCore (x) :precision binary64 (* (fmod 1.0 1.0) (- 1.0 x)))
                                                                  double code(double x) {
                                                                  	return fmod(1.0, 1.0) * (1.0 - x);
                                                                  }
                                                                  
                                                                  real(8) function code(x)
                                                                      real(8), intent (in) :: x
                                                                      code = mod(1.0d0, 1.0d0) * (1.0d0 - x)
                                                                  end function
                                                                  
                                                                  def code(x):
                                                                  	return math.fmod(1.0, 1.0) * (1.0 - x)
                                                                  
                                                                  function code(x)
                                                                  	return Float64(rem(1.0, 1.0) * Float64(1.0 - x))
                                                                  end
                                                                  
                                                                  code[x_] := N[(N[With[{TMP1 = 1.0, TMP2 = 1.0}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]
                                                                  
                                                                  \begin{array}{l}
                                                                  
                                                                  \\
                                                                  \left(1 \bmod 1\right) \cdot \left(1 - x\right)
                                                                  \end{array}
                                                                  
                                                                  Derivation
                                                                  1. Initial program 7.9%

                                                                    \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
                                                                  2. Add Preprocessing
                                                                  3. Taylor expanded in x around 0

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

                                                                      \[\leadsto \color{blue}{\left(-1 \cdot x\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                                    2. neg-mul-1N/A

                                                                      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(x\right)\right)} \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) + \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \]
                                                                    3. distribute-lft1-inN/A

                                                                      \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \cdot \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \]
                                                                    4. *-commutativeN/A

                                                                      \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                                    5. lower-*.f64N/A

                                                                      \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right)} \]
                                                                    6. lower-fmod.f64N/A

                                                                      \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)} \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                    7. lower-exp.f64N/A

                                                                      \[\leadsto \left(\color{blue}{\left(e^{x}\right)} \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                    8. lower-sqrt.f64N/A

                                                                      \[\leadsto \left(\left(e^{x}\right) \bmod \color{blue}{\left(\sqrt{\cos x}\right)}\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                    9. lower-cos.f64N/A

                                                                      \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\color{blue}{\cos x}}\right)\right) \cdot \left(\left(\mathsf{neg}\left(x\right)\right) + 1\right) \]
                                                                    10. +-commutativeN/A

                                                                      \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 + \left(\mathsf{neg}\left(x\right)\right)\right)} \]
                                                                    11. unsub-negN/A

                                                                      \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                                    12. lower--.f647.2

                                                                      \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\left(1 - x\right)} \]
                                                                  5. Applied rewrites7.2%

                                                                    \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \left(1 - x\right)} \]
                                                                  6. Taylor expanded in x around 0

                                                                    \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                  7. Step-by-step derivation
                                                                    1. Applied rewrites7.1%

                                                                      \[\leadsto \left(\left(e^{x}\right) \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                    2. Taylor expanded in x around 0

                                                                      \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                    3. Step-by-step derivation
                                                                      1. Applied rewrites21.0%

                                                                        \[\leadsto \left(1 \bmod 1\right) \cdot \left(1 - x\right) \]
                                                                      2. Add Preprocessing

                                                                      Reproduce

                                                                      ?
                                                                      herbie shell --seed 2024219 
                                                                      (FPCore (x)
                                                                        :name "expfmod (used to be hard to sample)"
                                                                        :precision binary64
                                                                        (* (fmod (exp x) (sqrt (cos x))) (exp (- x))))