Quotient of sum of exps

Percentage Accurate: 99.1% → 99.1%
Time: 5.9s
Alternatives: 12
Speedup: 1.0×

Specification

?
\[\begin{array}{l} \\ \frac{e^{a}}{e^{a} + e^{b}} \end{array} \]
(FPCore (a b) :precision binary64 (/ (exp a) (+ (exp a) (exp b))))
double code(double a, double b) {
	return exp(a) / (exp(a) + exp(b));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = exp(a) / (exp(a) + exp(b))
end function
public static double code(double a, double b) {
	return Math.exp(a) / (Math.exp(a) + Math.exp(b));
}
def code(a, b):
	return math.exp(a) / (math.exp(a) + math.exp(b))
function code(a, b)
	return Float64(exp(a) / Float64(exp(a) + exp(b)))
end
function tmp = code(a, b)
	tmp = exp(a) / (exp(a) + exp(b));
end
code[a_, b_] := N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[a], $MachinePrecision] + N[Exp[b], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{e^{a}}{e^{a} + e^{b}}
\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 12 alternatives:

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

Initial Program: 99.1% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{e^{a}}{e^{a} + e^{b}} \end{array} \]
(FPCore (a b) :precision binary64 (/ (exp a) (+ (exp a) (exp b))))
double code(double a, double b) {
	return exp(a) / (exp(a) + exp(b));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = exp(a) / (exp(a) + exp(b))
end function
public static double code(double a, double b) {
	return Math.exp(a) / (Math.exp(a) + Math.exp(b));
}
def code(a, b):
	return math.exp(a) / (math.exp(a) + math.exp(b))
function code(a, b)
	return Float64(exp(a) / Float64(exp(a) + exp(b)))
end
function tmp = code(a, b)
	tmp = exp(a) / (exp(a) + exp(b));
end
code[a_, b_] := N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[a], $MachinePrecision] + N[Exp[b], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{e^{a}}{e^{a} + e^{b}}
\end{array}

Alternative 1: 99.1% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{e^{a}}{e^{b} + e^{a}} \end{array} \]
(FPCore (a b) :precision binary64 (/ (exp a) (+ (exp b) (exp a))))
double code(double a, double b) {
	return exp(a) / (exp(b) + exp(a));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = exp(a) / (exp(b) + exp(a))
end function
public static double code(double a, double b) {
	return Math.exp(a) / (Math.exp(b) + Math.exp(a));
}
def code(a, b):
	return math.exp(a) / (math.exp(b) + math.exp(a))
function code(a, b)
	return Float64(exp(a) / Float64(exp(b) + exp(a)))
end
function tmp = code(a, b)
	tmp = exp(a) / (exp(b) + exp(a));
end
code[a_, b_] := N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{e^{a}}{e^{b} + e^{a}}
\end{array}
Derivation
  1. Initial program 99.2%

    \[\frac{e^{a}}{e^{a} + e^{b}} \]
  2. Add Preprocessing
  3. Final simplification99.2%

    \[\leadsto \frac{e^{a}}{e^{b} + e^{a}} \]
  4. Add Preprocessing

Alternative 2: 72.8% accurate, 0.9× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666, b, 0.5\right), b, 1\right), b, 2\right)}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
(FPCore (a b)
 :precision binary64
 (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.508817835104878)
   (/ 1.0 (fma (fma (fma 0.16666666666666666 b 0.5) b 1.0) b 2.0))
   1.0))
double code(double a, double b) {
	double tmp;
	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878) {
		tmp = 1.0 / fma(fma(fma(0.16666666666666666, b, 0.5), b, 1.0), b, 2.0);
	} else {
		tmp = 1.0;
	}
	return tmp;
}
function code(a, b)
	tmp = 0.0
	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.508817835104878)
		tmp = Float64(1.0 / fma(fma(fma(0.16666666666666666, b, 0.5), b, 1.0), b, 2.0));
	else
		tmp = 1.0;
	end
	return tmp
end
code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.508817835104878], N[(1.0 / N[(N[(N[(0.16666666666666666 * b + 0.5), $MachinePrecision] * b + 1.0), $MachinePrecision] * b + 2.0), $MachinePrecision]), $MachinePrecision], 1.0]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\
\;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666, b, 0.5\right), b, 1\right), b, 2\right)}\\

\mathbf{else}:\\
\;\;\;\;1\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.50881783510487799

    1. Initial program 100.0%

      \[\frac{e^{a}}{e^{a} + e^{b}} \]
    2. Add Preprocessing
    3. Taylor expanded in a around 0

      \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
    4. Step-by-step derivation
      1. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
      2. +-commutativeN/A

        \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
      3. lower-+.f64N/A

        \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
      4. lower-exp.f6474.7

        \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
    5. Applied rewrites74.7%

      \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
    6. Taylor expanded in b around 0

      \[\leadsto \frac{1}{2 + \color{blue}{b \cdot \left(1 + b \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot b\right)\right)}} \]
    7. Step-by-step derivation
      1. Applied rewrites64.1%

        \[\leadsto \frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666, b, 0.5\right), b, 1\right), \color{blue}{b}, 2\right)} \]

      if 0.50881783510487799 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

      1. Initial program 95.0%

        \[\frac{e^{a}}{e^{a} + e^{b}} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. /-rgt-identityN/A

          \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
        2. clear-numN/A

          \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
        3. inv-powN/A

          \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
        4. pow-flipN/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
        5. metadata-evalN/A

          \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
        6. metadata-evalN/A

          \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
        7. pow-powN/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
        8. sqr-powN/A

          \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
        9. unpow-prod-downN/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
        10. lower-*.f64N/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
        11. lower-pow.f64N/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
        12. lower-pow.f64N/A

          \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
        13. lift-+.f64N/A

          \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
        14. +-commutativeN/A

          \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
        15. lower-+.f64N/A

          \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
        16. metadata-evalN/A

          \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
        17. lower-pow.f64N/A

          \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
      4. Applied rewrites95.0%

        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
      5. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
        3. lift-exp.f64N/A

          \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
        4. pow2N/A

          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
        5. lift-pow.f64N/A

          \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
        6. pow-to-expN/A

          \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
        7. pow-expN/A

          \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
        8. div-expN/A

          \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
        9. lower-exp.f64N/A

          \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
        10. lower--.f64N/A

          \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
        11. lower-*.f64N/A

          \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
      6. Applied rewrites95.1%

        \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
      7. Step-by-step derivation
        1. lift-exp.f64N/A

          \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
        2. lift--.f64N/A

          \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
        3. flip--N/A

          \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
        4. div-invN/A

          \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
        5. exp-prodN/A

          \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
        6. lower-pow.f64N/A

          \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
      8. Applied rewrites97.6%

        \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
      9. Taylor expanded in a around inf

        \[\leadsto \color{blue}{1} \]
      10. Step-by-step derivation
        1. Applied rewrites97.6%

          \[\leadsto \color{blue}{1} \]
      11. Recombined 2 regimes into one program.
      12. Final simplification69.3%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666, b, 0.5\right), b, 1\right), b, 2\right)}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
      13. Add Preprocessing

      Alternative 3: 72.6% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666 \cdot b, b, 1\right), b, 2\right)}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
      (FPCore (a b)
       :precision binary64
       (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.508817835104878)
         (/ 1.0 (fma (fma (* 0.16666666666666666 b) b 1.0) b 2.0))
         1.0))
      double code(double a, double b) {
      	double tmp;
      	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878) {
      		tmp = 1.0 / fma(fma((0.16666666666666666 * b), b, 1.0), b, 2.0);
      	} else {
      		tmp = 1.0;
      	}
      	return tmp;
      }
      
      function code(a, b)
      	tmp = 0.0
      	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.508817835104878)
      		tmp = Float64(1.0 / fma(fma(Float64(0.16666666666666666 * b), b, 1.0), b, 2.0));
      	else
      		tmp = 1.0;
      	end
      	return tmp
      end
      
      code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.508817835104878], N[(1.0 / N[(N[(N[(0.16666666666666666 * b), $MachinePrecision] * b + 1.0), $MachinePrecision] * b + 2.0), $MachinePrecision]), $MachinePrecision], 1.0]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\
      \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666 \cdot b, b, 1\right), b, 2\right)}\\
      
      \mathbf{else}:\\
      \;\;\;\;1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.50881783510487799

        1. Initial program 100.0%

          \[\frac{e^{a}}{e^{a} + e^{b}} \]
        2. Add Preprocessing
        3. Taylor expanded in a around 0

          \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
        4. Step-by-step derivation
          1. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
          2. +-commutativeN/A

            \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
          3. lower-+.f64N/A

            \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
          4. lower-exp.f6474.7

            \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
        5. Applied rewrites74.7%

          \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
        6. Taylor expanded in b around 0

          \[\leadsto \frac{1}{2 + \color{blue}{b \cdot \left(1 + b \cdot \left(\frac{1}{2} + \frac{1}{6} \cdot b\right)\right)}} \]
        7. Step-by-step derivation
          1. Applied rewrites64.1%

            \[\leadsto \frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666, b, 0.5\right), b, 1\right), \color{blue}{b}, 2\right)} \]
          2. Taylor expanded in b around inf

            \[\leadsto \frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{1}{6} \cdot b, b, 1\right), b, 2\right)} \]
          3. Step-by-step derivation
            1. Applied rewrites63.6%

              \[\leadsto \frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666 \cdot b, b, 1\right), b, 2\right)} \]

            if 0.50881783510487799 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

            1. Initial program 95.0%

              \[\frac{e^{a}}{e^{a} + e^{b}} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. /-rgt-identityN/A

                \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
              2. clear-numN/A

                \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
              3. inv-powN/A

                \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
              4. pow-flipN/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
              5. metadata-evalN/A

                \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
              6. metadata-evalN/A

                \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
              7. pow-powN/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
              8. sqr-powN/A

                \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
              9. unpow-prod-downN/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
              10. lower-*.f64N/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
              11. lower-pow.f64N/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
              12. lower-pow.f64N/A

                \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
              13. lift-+.f64N/A

                \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
              14. +-commutativeN/A

                \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
              15. lower-+.f64N/A

                \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
              16. metadata-evalN/A

                \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
              17. lower-pow.f64N/A

                \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
            4. Applied rewrites95.0%

              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
            5. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
              2. lift-*.f64N/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
              3. lift-exp.f64N/A

                \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
              4. pow2N/A

                \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
              5. lift-pow.f64N/A

                \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
              6. pow-to-expN/A

                \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
              7. pow-expN/A

                \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
              8. div-expN/A

                \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
              9. lower-exp.f64N/A

                \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
              10. lower--.f64N/A

                \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
              11. lower-*.f64N/A

                \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
            6. Applied rewrites95.1%

              \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
            7. Step-by-step derivation
              1. lift-exp.f64N/A

                \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
              2. lift--.f64N/A

                \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
              3. flip--N/A

                \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
              4. div-invN/A

                \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
              5. exp-prodN/A

                \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
              6. lower-pow.f64N/A

                \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
            8. Applied rewrites97.6%

              \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
            9. Taylor expanded in a around inf

              \[\leadsto \color{blue}{1} \]
            10. Step-by-step derivation
              1. Applied rewrites97.6%

                \[\leadsto \color{blue}{1} \]
            11. Recombined 2 regimes into one program.
            12. Final simplification68.9%

              \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.16666666666666666 \cdot b, b, 1\right), b, 2\right)}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
            13. Add Preprocessing

            Alternative 4: 68.2% accurate, 0.9× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.5, b, 1\right), b, 2\right)}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
            (FPCore (a b)
             :precision binary64
             (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.508817835104878)
               (/ 1.0 (fma (fma 0.5 b 1.0) b 2.0))
               1.0))
            double code(double a, double b) {
            	double tmp;
            	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878) {
            		tmp = 1.0 / fma(fma(0.5, b, 1.0), b, 2.0);
            	} else {
            		tmp = 1.0;
            	}
            	return tmp;
            }
            
            function code(a, b)
            	tmp = 0.0
            	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.508817835104878)
            		tmp = Float64(1.0 / fma(fma(0.5, b, 1.0), b, 2.0));
            	else
            		tmp = 1.0;
            	end
            	return tmp
            end
            
            code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.508817835104878], N[(1.0 / N[(N[(0.5 * b + 1.0), $MachinePrecision] * b + 2.0), $MachinePrecision]), $MachinePrecision], 1.0]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\
            \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.5, b, 1\right), b, 2\right)}\\
            
            \mathbf{else}:\\
            \;\;\;\;1\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.50881783510487799

              1. Initial program 100.0%

                \[\frac{e^{a}}{e^{a} + e^{b}} \]
              2. Add Preprocessing
              3. Taylor expanded in a around 0

                \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
              4. Step-by-step derivation
                1. lower-/.f64N/A

                  \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                2. +-commutativeN/A

                  \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                3. lower-+.f64N/A

                  \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                4. lower-exp.f6474.7

                  \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
              5. Applied rewrites74.7%

                \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
              6. Taylor expanded in b around 0

                \[\leadsto \frac{1}{2 + \color{blue}{b \cdot \left(1 + \frac{1}{2} \cdot b\right)}} \]
              7. Step-by-step derivation
                1. Applied rewrites60.0%

                  \[\leadsto \frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.5, b, 1\right), \color{blue}{b}, 2\right)} \]

                if 0.50881783510487799 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

                1. Initial program 95.0%

                  \[\frac{e^{a}}{e^{a} + e^{b}} \]
                2. Add Preprocessing
                3. Step-by-step derivation
                  1. /-rgt-identityN/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
                  2. clear-numN/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
                  3. inv-powN/A

                    \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
                  4. pow-flipN/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
                  5. metadata-evalN/A

                    \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
                  6. metadata-evalN/A

                    \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
                  7. pow-powN/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
                  8. sqr-powN/A

                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
                  9. unpow-prod-downN/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                  10. lower-*.f64N/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                  11. lower-pow.f64N/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                  12. lower-pow.f64N/A

                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                  13. lift-+.f64N/A

                    \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                  14. +-commutativeN/A

                    \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                  15. lower-+.f64N/A

                    \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                  16. metadata-evalN/A

                    \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                  17. lower-pow.f64N/A

                    \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                4. Applied rewrites95.0%

                  \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
                5. Step-by-step derivation
                  1. lift-/.f64N/A

                    \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                  2. lift-*.f64N/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                  3. lift-exp.f64N/A

                    \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
                  4. pow2N/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
                  5. lift-pow.f64N/A

                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
                  6. pow-to-expN/A

                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
                  7. pow-expN/A

                    \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
                  8. div-expN/A

                    \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                  9. lower-exp.f64N/A

                    \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                  10. lower--.f64N/A

                    \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                  11. lower-*.f64N/A

                    \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                6. Applied rewrites95.1%

                  \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                7. Step-by-step derivation
                  1. lift-exp.f64N/A

                    \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                  2. lift--.f64N/A

                    \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                  3. flip--N/A

                    \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                  4. div-invN/A

                    \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                  5. exp-prodN/A

                    \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                  6. lower-pow.f64N/A

                    \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                8. Applied rewrites97.6%

                  \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
                9. Taylor expanded in a around inf

                  \[\leadsto \color{blue}{1} \]
                10. Step-by-step derivation
                  1. Applied rewrites97.6%

                    \[\leadsto \color{blue}{1} \]
                11. Recombined 2 regimes into one program.
                12. Final simplification65.9%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(0.5, b, 1\right), b, 2\right)}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
                13. Add Preprocessing

                Alternative 5: 55.5% accurate, 0.9× speedup?

                \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{2 + b}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
                (FPCore (a b)
                 :precision binary64
                 (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.508817835104878)
                   (/ 1.0 (+ 2.0 b))
                   1.0))
                double code(double a, double b) {
                	double tmp;
                	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878) {
                		tmp = 1.0 / (2.0 + b);
                	} else {
                		tmp = 1.0;
                	}
                	return tmp;
                }
                
                real(8) function code(a, b)
                    real(8), intent (in) :: a
                    real(8), intent (in) :: b
                    real(8) :: tmp
                    if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878d0) then
                        tmp = 1.0d0 / (2.0d0 + b)
                    else
                        tmp = 1.0d0
                    end if
                    code = tmp
                end function
                
                public static double code(double a, double b) {
                	double tmp;
                	if ((Math.exp(a) / (Math.exp(b) + Math.exp(a))) <= 0.508817835104878) {
                		tmp = 1.0 / (2.0 + b);
                	} else {
                		tmp = 1.0;
                	}
                	return tmp;
                }
                
                def code(a, b):
                	tmp = 0
                	if (math.exp(a) / (math.exp(b) + math.exp(a))) <= 0.508817835104878:
                		tmp = 1.0 / (2.0 + b)
                	else:
                		tmp = 1.0
                	return tmp
                
                function code(a, b)
                	tmp = 0.0
                	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.508817835104878)
                		tmp = Float64(1.0 / Float64(2.0 + b));
                	else
                		tmp = 1.0;
                	end
                	return tmp
                end
                
                function tmp_2 = code(a, b)
                	tmp = 0.0;
                	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878)
                		tmp = 1.0 / (2.0 + b);
                	else
                		tmp = 1.0;
                	end
                	tmp_2 = tmp;
                end
                
                code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.508817835104878], N[(1.0 / N[(2.0 + b), $MachinePrecision]), $MachinePrecision], 1.0]
                
                \begin{array}{l}
                
                \\
                \begin{array}{l}
                \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\
                \;\;\;\;\frac{1}{2 + b}\\
                
                \mathbf{else}:\\
                \;\;\;\;1\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 2 regimes
                2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.50881783510487799

                  1. Initial program 100.0%

                    \[\frac{e^{a}}{e^{a} + e^{b}} \]
                  2. Add Preprocessing
                  3. Taylor expanded in a around 0

                    \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                  4. Step-by-step derivation
                    1. lower-/.f64N/A

                      \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                    2. +-commutativeN/A

                      \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                    3. lower-+.f64N/A

                      \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                    4. lower-exp.f6474.7

                      \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                  5. Applied rewrites74.7%

                    \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                  6. Taylor expanded in b around 0

                    \[\leadsto \frac{1}{2 + \color{blue}{b}} \]
                  7. Step-by-step derivation
                    1. Applied rewrites43.9%

                      \[\leadsto \frac{1}{2 + \color{blue}{b}} \]

                    if 0.50881783510487799 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

                    1. Initial program 95.0%

                      \[\frac{e^{a}}{e^{a} + e^{b}} \]
                    2. Add Preprocessing
                    3. Step-by-step derivation
                      1. /-rgt-identityN/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
                      2. clear-numN/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
                      3. inv-powN/A

                        \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
                      4. pow-flipN/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
                      5. metadata-evalN/A

                        \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
                      6. metadata-evalN/A

                        \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
                      7. pow-powN/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
                      8. sqr-powN/A

                        \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
                      9. unpow-prod-downN/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                      10. lower-*.f64N/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                      11. lower-pow.f64N/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                      12. lower-pow.f64N/A

                        \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                      13. lift-+.f64N/A

                        \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                      14. +-commutativeN/A

                        \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                      15. lower-+.f64N/A

                        \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                      16. metadata-evalN/A

                        \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                      17. lower-pow.f64N/A

                        \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                    4. Applied rewrites95.0%

                      \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
                    5. Step-by-step derivation
                      1. lift-/.f64N/A

                        \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                      2. lift-*.f64N/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                      3. lift-exp.f64N/A

                        \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
                      4. pow2N/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
                      5. lift-pow.f64N/A

                        \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
                      6. pow-to-expN/A

                        \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
                      7. pow-expN/A

                        \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
                      8. div-expN/A

                        \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                      9. lower-exp.f64N/A

                        \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                      10. lower--.f64N/A

                        \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                      11. lower-*.f64N/A

                        \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                    6. Applied rewrites95.1%

                      \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                    7. Step-by-step derivation
                      1. lift-exp.f64N/A

                        \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                      2. lift--.f64N/A

                        \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                      3. flip--N/A

                        \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                      4. div-invN/A

                        \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                      5. exp-prodN/A

                        \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                      6. lower-pow.f64N/A

                        \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                    8. Applied rewrites97.6%

                      \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
                    9. Taylor expanded in a around inf

                      \[\leadsto \color{blue}{1} \]
                    10. Step-by-step derivation
                      1. Applied rewrites97.6%

                        \[\leadsto \color{blue}{1} \]
                    11. Recombined 2 regimes into one program.
                    12. Final simplification52.3%

                      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\frac{1}{2 + b}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
                    13. Add Preprocessing

                    Alternative 6: 55.1% accurate, 0.9× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\mathsf{fma}\left(0.25, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
                    (FPCore (a b)
                     :precision binary64
                     (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.508817835104878)
                       (fma 0.25 a (fma -0.25 b 0.5))
                       1.0))
                    double code(double a, double b) {
                    	double tmp;
                    	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878) {
                    		tmp = fma(0.25, a, fma(-0.25, b, 0.5));
                    	} else {
                    		tmp = 1.0;
                    	}
                    	return tmp;
                    }
                    
                    function code(a, b)
                    	tmp = 0.0
                    	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.508817835104878)
                    		tmp = fma(0.25, a, fma(-0.25, b, 0.5));
                    	else
                    		tmp = 1.0;
                    	end
                    	return tmp
                    end
                    
                    code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.508817835104878], N[(0.25 * a + N[(-0.25 * b + 0.5), $MachinePrecision]), $MachinePrecision], 1.0]
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\
                    \;\;\;\;\mathsf{fma}\left(0.25, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right)\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;1\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.50881783510487799

                      1. Initial program 100.0%

                        \[\frac{e^{a}}{e^{a} + e^{b}} \]
                      2. Add Preprocessing
                      3. Taylor expanded in b around 0

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

                          \[\leadsto \color{blue}{\frac{-1 \cdot \left(b \cdot e^{a}\right)}{{\left(1 + e^{a}\right)}^{2}}} + \frac{e^{a}}{1 + e^{a}} \]
                        2. unpow2N/A

                          \[\leadsto \frac{-1 \cdot \left(b \cdot e^{a}\right)}{\color{blue}{\left(1 + e^{a}\right) \cdot \left(1 + e^{a}\right)}} + \frac{e^{a}}{1 + e^{a}} \]
                        3. associate-*r*N/A

                          \[\leadsto \frac{\color{blue}{\left(-1 \cdot b\right) \cdot e^{a}}}{\left(1 + e^{a}\right) \cdot \left(1 + e^{a}\right)} + \frac{e^{a}}{1 + e^{a}} \]
                        4. times-fracN/A

                          \[\leadsto \color{blue}{\frac{-1 \cdot b}{1 + e^{a}} \cdot \frac{e^{a}}{1 + e^{a}}} + \frac{e^{a}}{1 + e^{a}} \]
                        5. distribute-lft1-inN/A

                          \[\leadsto \color{blue}{\left(\frac{-1 \cdot b}{1 + e^{a}} + 1\right) \cdot \frac{e^{a}}{1 + e^{a}}} \]
                        6. lower-*.f64N/A

                          \[\leadsto \color{blue}{\left(\frac{-1 \cdot b}{1 + e^{a}} + 1\right) \cdot \frac{e^{a}}{1 + e^{a}}} \]
                      5. Applied rewrites79.8%

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

                        \[\leadsto \frac{1}{2} \cdot \left(1 + \frac{-1}{2} \cdot b\right) + \color{blue}{a \cdot \left(\frac{1}{2} \cdot \left(1 + \left(\frac{-1}{2} \cdot b + \frac{1}{4} \cdot b\right)\right) - \frac{1}{4} \cdot \left(1 + \frac{-1}{2} \cdot b\right)\right)} \]
                      7. Applied rewrites43.4%

                        \[\leadsto \mathsf{fma}\left(0.25, \color{blue}{a}, \mathsf{fma}\left(-0.25, b, 0.5\right)\right) \]

                      if 0.50881783510487799 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

                      1. Initial program 95.0%

                        \[\frac{e^{a}}{e^{a} + e^{b}} \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. /-rgt-identityN/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
                        2. clear-numN/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
                        3. inv-powN/A

                          \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
                        4. pow-flipN/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
                        5. metadata-evalN/A

                          \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
                        6. metadata-evalN/A

                          \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
                        7. pow-powN/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
                        8. sqr-powN/A

                          \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
                        9. unpow-prod-downN/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                        10. lower-*.f64N/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                        11. lower-pow.f64N/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                        12. lower-pow.f64N/A

                          \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                        13. lift-+.f64N/A

                          \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                        14. +-commutativeN/A

                          \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                        15. lower-+.f64N/A

                          \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                        16. metadata-evalN/A

                          \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                        17. lower-pow.f64N/A

                          \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                      4. Applied rewrites95.0%

                        \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
                      5. Step-by-step derivation
                        1. lift-/.f64N/A

                          \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                        2. lift-*.f64N/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                        3. lift-exp.f64N/A

                          \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
                        4. pow2N/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
                        5. lift-pow.f64N/A

                          \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
                        6. pow-to-expN/A

                          \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
                        7. pow-expN/A

                          \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
                        8. div-expN/A

                          \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                        9. lower-exp.f64N/A

                          \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                        10. lower--.f64N/A

                          \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                        11. lower-*.f64N/A

                          \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                      6. Applied rewrites95.1%

                        \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                      7. Step-by-step derivation
                        1. lift-exp.f64N/A

                          \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                        2. lift--.f64N/A

                          \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                        3. flip--N/A

                          \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                        4. div-invN/A

                          \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                        5. exp-prodN/A

                          \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                        6. lower-pow.f64N/A

                          \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                      8. Applied rewrites97.6%

                        \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
                      9. Taylor expanded in a around inf

                        \[\leadsto \color{blue}{1} \]
                      10. Step-by-step derivation
                        1. Applied rewrites97.6%

                          \[\leadsto \color{blue}{1} \]
                      11. Recombined 2 regimes into one program.
                      12. Final simplification51.8%

                        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\mathsf{fma}\left(0.25, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
                      13. Add Preprocessing

                      Alternative 7: 54.8% accurate, 1.0× speedup?

                      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\mathsf{fma}\left(-0.25, b, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
                      (FPCore (a b)
                       :precision binary64
                       (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.508817835104878)
                         (fma -0.25 b 0.5)
                         1.0))
                      double code(double a, double b) {
                      	double tmp;
                      	if ((exp(a) / (exp(b) + exp(a))) <= 0.508817835104878) {
                      		tmp = fma(-0.25, b, 0.5);
                      	} else {
                      		tmp = 1.0;
                      	}
                      	return tmp;
                      }
                      
                      function code(a, b)
                      	tmp = 0.0
                      	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.508817835104878)
                      		tmp = fma(-0.25, b, 0.5);
                      	else
                      		tmp = 1.0;
                      	end
                      	return tmp
                      end
                      
                      code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.508817835104878], N[(-0.25 * b + 0.5), $MachinePrecision], 1.0]
                      
                      \begin{array}{l}
                      
                      \\
                      \begin{array}{l}
                      \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\
                      \;\;\;\;\mathsf{fma}\left(-0.25, b, 0.5\right)\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;1\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.50881783510487799

                        1. Initial program 100.0%

                          \[\frac{e^{a}}{e^{a} + e^{b}} \]
                        2. Add Preprocessing
                        3. Taylor expanded in a around 0

                          \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                        4. Step-by-step derivation
                          1. lower-/.f64N/A

                            \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                          2. +-commutativeN/A

                            \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                          3. lower-+.f64N/A

                            \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                          4. lower-exp.f6474.7

                            \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                        5. Applied rewrites74.7%

                          \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                        6. Taylor expanded in b around 0

                          \[\leadsto \frac{1}{2} + \color{blue}{\frac{-1}{4} \cdot b} \]
                        7. Step-by-step derivation
                          1. Applied rewrites43.3%

                            \[\leadsto \mathsf{fma}\left(-0.25, \color{blue}{b}, 0.5\right) \]

                          if 0.50881783510487799 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

                          1. Initial program 95.0%

                            \[\frac{e^{a}}{e^{a} + e^{b}} \]
                          2. Add Preprocessing
                          3. Step-by-step derivation
                            1. /-rgt-identityN/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
                            2. clear-numN/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
                            3. inv-powN/A

                              \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
                            4. pow-flipN/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
                            5. metadata-evalN/A

                              \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
                            6. metadata-evalN/A

                              \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
                            7. pow-powN/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
                            8. sqr-powN/A

                              \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
                            9. unpow-prod-downN/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                            10. lower-*.f64N/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                            11. lower-pow.f64N/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                            12. lower-pow.f64N/A

                              \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                            13. lift-+.f64N/A

                              \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                            14. +-commutativeN/A

                              \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                            15. lower-+.f64N/A

                              \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                            16. metadata-evalN/A

                              \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                            17. lower-pow.f64N/A

                              \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                          4. Applied rewrites95.0%

                            \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
                          5. Step-by-step derivation
                            1. lift-/.f64N/A

                              \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                            2. lift-*.f64N/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                            3. lift-exp.f64N/A

                              \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
                            4. pow2N/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
                            5. lift-pow.f64N/A

                              \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
                            6. pow-to-expN/A

                              \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
                            7. pow-expN/A

                              \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
                            8. div-expN/A

                              \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                            9. lower-exp.f64N/A

                              \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                            10. lower--.f64N/A

                              \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                            11. lower-*.f64N/A

                              \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                          6. Applied rewrites95.1%

                            \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                          7. Step-by-step derivation
                            1. lift-exp.f64N/A

                              \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                            2. lift--.f64N/A

                              \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                            3. flip--N/A

                              \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                            4. div-invN/A

                              \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                            5. exp-prodN/A

                              \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                            6. lower-pow.f64N/A

                              \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                          8. Applied rewrites97.6%

                            \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
                          9. Taylor expanded in a around inf

                            \[\leadsto \color{blue}{1} \]
                          10. Step-by-step derivation
                            1. Applied rewrites97.6%

                              \[\leadsto \color{blue}{1} \]
                          11. Recombined 2 regimes into one program.
                          12. Final simplification51.8%

                            \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.508817835104878:\\ \;\;\;\;\mathsf{fma}\left(-0.25, b, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
                          13. Add Preprocessing

                          Alternative 8: 98.6% accurate, 1.0× speedup?

                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;e^{a} \leq 10^{-13}:\\ \;\;\;\;\frac{e^{a}}{1 + e^{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + e^{b}}\\ \end{array} \end{array} \]
                          (FPCore (a b)
                           :precision binary64
                           (if (<= (exp a) 1e-13) (/ (exp a) (+ 1.0 (exp a))) (/ 1.0 (+ 1.0 (exp b)))))
                          double code(double a, double b) {
                          	double tmp;
                          	if (exp(a) <= 1e-13) {
                          		tmp = exp(a) / (1.0 + exp(a));
                          	} else {
                          		tmp = 1.0 / (1.0 + exp(b));
                          	}
                          	return tmp;
                          }
                          
                          real(8) function code(a, b)
                              real(8), intent (in) :: a
                              real(8), intent (in) :: b
                              real(8) :: tmp
                              if (exp(a) <= 1d-13) then
                                  tmp = exp(a) / (1.0d0 + exp(a))
                              else
                                  tmp = 1.0d0 / (1.0d0 + exp(b))
                              end if
                              code = tmp
                          end function
                          
                          public static double code(double a, double b) {
                          	double tmp;
                          	if (Math.exp(a) <= 1e-13) {
                          		tmp = Math.exp(a) / (1.0 + Math.exp(a));
                          	} else {
                          		tmp = 1.0 / (1.0 + Math.exp(b));
                          	}
                          	return tmp;
                          }
                          
                          def code(a, b):
                          	tmp = 0
                          	if math.exp(a) <= 1e-13:
                          		tmp = math.exp(a) / (1.0 + math.exp(a))
                          	else:
                          		tmp = 1.0 / (1.0 + math.exp(b))
                          	return tmp
                          
                          function code(a, b)
                          	tmp = 0.0
                          	if (exp(a) <= 1e-13)
                          		tmp = Float64(exp(a) / Float64(1.0 + exp(a)));
                          	else
                          		tmp = Float64(1.0 / Float64(1.0 + exp(b)));
                          	end
                          	return tmp
                          end
                          
                          function tmp_2 = code(a, b)
                          	tmp = 0.0;
                          	if (exp(a) <= 1e-13)
                          		tmp = exp(a) / (1.0 + exp(a));
                          	else
                          		tmp = 1.0 / (1.0 + exp(b));
                          	end
                          	tmp_2 = tmp;
                          end
                          
                          code[a_, b_] := If[LessEqual[N[Exp[a], $MachinePrecision], 1e-13], N[(N[Exp[a], $MachinePrecision] / N[(1.0 + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1.0 / N[(1.0 + N[Exp[b], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
                          
                          \begin{array}{l}
                          
                          \\
                          \begin{array}{l}
                          \mathbf{if}\;e^{a} \leq 10^{-13}:\\
                          \;\;\;\;\frac{e^{a}}{1 + e^{a}}\\
                          
                          \mathbf{else}:\\
                          \;\;\;\;\frac{1}{1 + e^{b}}\\
                          
                          
                          \end{array}
                          \end{array}
                          
                          Derivation
                          1. Split input into 2 regimes
                          2. if (exp.f64 a) < 1e-13

                            1. Initial program 98.8%

                              \[\frac{e^{a}}{e^{a} + e^{b}} \]
                            2. Add Preprocessing
                            3. Taylor expanded in b around 0

                              \[\leadsto \frac{e^{a}}{e^{a} + \color{blue}{1}} \]
                            4. Step-by-step derivation
                              1. Applied rewrites100.0%

                                \[\leadsto \frac{e^{a}}{e^{a} + \color{blue}{1}} \]

                              if 1e-13 < (exp.f64 a)

                              1. Initial program 99.4%

                                \[\frac{e^{a}}{e^{a} + e^{b}} \]
                              2. Add Preprocessing
                              3. Taylor expanded in a around 0

                                \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                              4. Step-by-step derivation
                                1. lower-/.f64N/A

                                  \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                2. +-commutativeN/A

                                  \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                3. lower-+.f64N/A

                                  \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                4. lower-exp.f6498.8

                                  \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                              5. Applied rewrites98.8%

                                \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                            5. Recombined 2 regimes into one program.
                            6. Final simplification99.2%

                              \[\leadsto \begin{array}{l} \mathbf{if}\;e^{a} \leq 10^{-13}:\\ \;\;\;\;\frac{e^{a}}{1 + e^{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + e^{b}}\\ \end{array} \]
                            7. Add Preprocessing

                            Alternative 9: 54.6% accurate, 1.0× speedup?

                            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.75:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \end{array} \]
                            (FPCore (a b)
                             :precision binary64
                             (if (<= (/ (exp a) (+ (exp b) (exp a))) 0.75) 0.5 1.0))
                            double code(double a, double b) {
                            	double tmp;
                            	if ((exp(a) / (exp(b) + exp(a))) <= 0.75) {
                            		tmp = 0.5;
                            	} else {
                            		tmp = 1.0;
                            	}
                            	return tmp;
                            }
                            
                            real(8) function code(a, b)
                                real(8), intent (in) :: a
                                real(8), intent (in) :: b
                                real(8) :: tmp
                                if ((exp(a) / (exp(b) + exp(a))) <= 0.75d0) then
                                    tmp = 0.5d0
                                else
                                    tmp = 1.0d0
                                end if
                                code = tmp
                            end function
                            
                            public static double code(double a, double b) {
                            	double tmp;
                            	if ((Math.exp(a) / (Math.exp(b) + Math.exp(a))) <= 0.75) {
                            		tmp = 0.5;
                            	} else {
                            		tmp = 1.0;
                            	}
                            	return tmp;
                            }
                            
                            def code(a, b):
                            	tmp = 0
                            	if (math.exp(a) / (math.exp(b) + math.exp(a))) <= 0.75:
                            		tmp = 0.5
                            	else:
                            		tmp = 1.0
                            	return tmp
                            
                            function code(a, b)
                            	tmp = 0.0
                            	if (Float64(exp(a) / Float64(exp(b) + exp(a))) <= 0.75)
                            		tmp = 0.5;
                            	else
                            		tmp = 1.0;
                            	end
                            	return tmp
                            end
                            
                            function tmp_2 = code(a, b)
                            	tmp = 0.0;
                            	if ((exp(a) / (exp(b) + exp(a))) <= 0.75)
                            		tmp = 0.5;
                            	else
                            		tmp = 1.0;
                            	end
                            	tmp_2 = tmp;
                            end
                            
                            code[a_, b_] := If[LessEqual[N[(N[Exp[a], $MachinePrecision] / N[(N[Exp[b], $MachinePrecision] + N[Exp[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 0.75], 0.5, 1.0]
                            
                            \begin{array}{l}
                            
                            \\
                            \begin{array}{l}
                            \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.75:\\
                            \;\;\;\;0.5\\
                            
                            \mathbf{else}:\\
                            \;\;\;\;1\\
                            
                            
                            \end{array}
                            \end{array}
                            
                            Derivation
                            1. Split input into 2 regimes
                            2. if (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b))) < 0.75

                              1. Initial program 100.0%

                                \[\frac{e^{a}}{e^{a} + e^{b}} \]
                              2. Add Preprocessing
                              3. Taylor expanded in a around 0

                                \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                              4. Step-by-step derivation
                                1. lower-/.f64N/A

                                  \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                2. +-commutativeN/A

                                  \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                3. lower-+.f64N/A

                                  \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                4. lower-exp.f6474.7

                                  \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                              5. Applied rewrites74.7%

                                \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                              6. Taylor expanded in b around 0

                                \[\leadsto \frac{1}{2} \]
                              7. Step-by-step derivation
                                1. Applied rewrites42.5%

                                  \[\leadsto 0.5 \]

                                if 0.75 < (/.f64 (exp.f64 a) (+.f64 (exp.f64 a) (exp.f64 b)))

                                1. Initial program 95.0%

                                  \[\frac{e^{a}}{e^{a} + e^{b}} \]
                                2. Add Preprocessing
                                3. Step-by-step derivation
                                  1. /-rgt-identityN/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{\frac{e^{a} + e^{b}}{1}}} \]
                                  2. clear-numN/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{\frac{1}{\frac{1}{e^{a} + e^{b}}}}} \]
                                  3. inv-powN/A

                                    \[\leadsto \frac{e^{a}}{\frac{1}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{-1}}}} \]
                                  4. pow-flipN/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left(e^{a} + e^{b}\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}}} \]
                                  5. metadata-evalN/A

                                    \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{1}}} \]
                                  6. metadata-evalN/A

                                    \[\leadsto \frac{e^{a}}{{\left(e^{a} + e^{b}\right)}^{\color{blue}{\left(-1 \cdot -1\right)}}} \]
                                  7. pow-powN/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{-1}\right)}^{-1}}} \]
                                  8. sqr-powN/A

                                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)} \cdot {\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1}} \]
                                  9. unpow-prod-downN/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                                  10. lower-*.f64N/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                                  11. lower-pow.f64N/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                                  12. lower-pow.f64N/A

                                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                                  13. lift-+.f64N/A

                                    \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{a} + e^{b}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                                  14. +-commutativeN/A

                                    \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                                  15. lower-+.f64N/A

                                    \[\leadsto \frac{e^{a}}{{\left({\color{blue}{\left(e^{b} + e^{a}\right)}}^{\left(\frac{-1}{2}\right)}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                                  16. metadata-evalN/A

                                    \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\color{blue}{\frac{-1}{2}}}\right)}^{-1} \cdot {\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}} \]
                                  17. lower-pow.f64N/A

                                    \[\leadsto \frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot \color{blue}{{\left({\left(e^{a} + e^{b}\right)}^{\left(\frac{-1}{2}\right)}\right)}^{-1}}} \]
                                4. Applied rewrites95.0%

                                  \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{-0.5}\right)}^{-1}}} \]
                                5. Step-by-step derivation
                                  1. lift-/.f64N/A

                                    \[\leadsto \color{blue}{\frac{e^{a}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                                  2. lift-*.f64N/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}}} \]
                                  3. lift-exp.f64N/A

                                    \[\leadsto \frac{\color{blue}{e^{a}}}{{\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1} \cdot {\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}} \]
                                  4. pow2N/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}^{2}}} \]
                                  5. lift-pow.f64N/A

                                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left({\left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right)}^{-1}\right)}}^{2}} \]
                                  6. pow-to-expN/A

                                    \[\leadsto \frac{e^{a}}{{\color{blue}{\left(e^{\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1}\right)}}^{2}} \]
                                  7. pow-expN/A

                                    \[\leadsto \frac{e^{a}}{\color{blue}{e^{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}}} \]
                                  8. div-expN/A

                                    \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                                  9. lower-exp.f64N/A

                                    \[\leadsto \color{blue}{e^{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                                  10. lower--.f64N/A

                                    \[\leadsto e^{\color{blue}{a - \left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                                  11. lower-*.f64N/A

                                    \[\leadsto e^{a - \color{blue}{\left(\log \left({\left(e^{b} + e^{a}\right)}^{\frac{-1}{2}}\right) \cdot -1\right) \cdot 2}} \]
                                6. Applied rewrites95.1%

                                  \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                                7. Step-by-step derivation
                                  1. lift-exp.f64N/A

                                    \[\leadsto \color{blue}{e^{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                                  2. lift--.f64N/A

                                    \[\leadsto e^{\color{blue}{a - \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}} \]
                                  3. flip--N/A

                                    \[\leadsto e^{\color{blue}{\frac{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                                  4. div-invN/A

                                    \[\leadsto e^{\color{blue}{\left(a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)\right) \cdot \frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}}} \]
                                  5. exp-prodN/A

                                    \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                                  6. lower-pow.f64N/A

                                    \[\leadsto \color{blue}{{\left(e^{a \cdot a - \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right) \cdot \left(\log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2\right)}\right)}^{\left(\frac{1}{a + \log \left(\sqrt{e^{b} + e^{a}}\right) \cdot 2}\right)}} \]
                                8. Applied rewrites97.6%

                                  \[\leadsto \color{blue}{{\left(e^{a \cdot a - {\log \left(\sqrt{e^{b} + e^{a}}\right)}^{2} \cdot 4}\right)}^{\left({\left(\mathsf{fma}\left(2, \log \left(\sqrt{e^{b} + e^{a}}\right), a\right)\right)}^{-1}\right)}} \]
                                9. Taylor expanded in a around inf

                                  \[\leadsto \color{blue}{1} \]
                                10. Step-by-step derivation
                                  1. Applied rewrites97.6%

                                    \[\leadsto \color{blue}{1} \]
                                11. Recombined 2 regimes into one program.
                                12. Final simplification51.1%

                                  \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{a}}{e^{b} + e^{a}} \leq 0.75:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]
                                13. Add Preprocessing

                                Alternative 10: 98.4% accurate, 1.4× speedup?

                                \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;e^{a} \leq 10^{-13}:\\ \;\;\;\;\frac{e^{a}}{1 + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + e^{b}}\\ \end{array} \end{array} \]
                                (FPCore (a b)
                                 :precision binary64
                                 (if (<= (exp a) 1e-13) (/ (exp a) (+ 1.0 1.0)) (/ 1.0 (+ 1.0 (exp b)))))
                                double code(double a, double b) {
                                	double tmp;
                                	if (exp(a) <= 1e-13) {
                                		tmp = exp(a) / (1.0 + 1.0);
                                	} else {
                                		tmp = 1.0 / (1.0 + exp(b));
                                	}
                                	return tmp;
                                }
                                
                                real(8) function code(a, b)
                                    real(8), intent (in) :: a
                                    real(8), intent (in) :: b
                                    real(8) :: tmp
                                    if (exp(a) <= 1d-13) then
                                        tmp = exp(a) / (1.0d0 + 1.0d0)
                                    else
                                        tmp = 1.0d0 / (1.0d0 + exp(b))
                                    end if
                                    code = tmp
                                end function
                                
                                public static double code(double a, double b) {
                                	double tmp;
                                	if (Math.exp(a) <= 1e-13) {
                                		tmp = Math.exp(a) / (1.0 + 1.0);
                                	} else {
                                		tmp = 1.0 / (1.0 + Math.exp(b));
                                	}
                                	return tmp;
                                }
                                
                                def code(a, b):
                                	tmp = 0
                                	if math.exp(a) <= 1e-13:
                                		tmp = math.exp(a) / (1.0 + 1.0)
                                	else:
                                		tmp = 1.0 / (1.0 + math.exp(b))
                                	return tmp
                                
                                function code(a, b)
                                	tmp = 0.0
                                	if (exp(a) <= 1e-13)
                                		tmp = Float64(exp(a) / Float64(1.0 + 1.0));
                                	else
                                		tmp = Float64(1.0 / Float64(1.0 + exp(b)));
                                	end
                                	return tmp
                                end
                                
                                function tmp_2 = code(a, b)
                                	tmp = 0.0;
                                	if (exp(a) <= 1e-13)
                                		tmp = exp(a) / (1.0 + 1.0);
                                	else
                                		tmp = 1.0 / (1.0 + exp(b));
                                	end
                                	tmp_2 = tmp;
                                end
                                
                                code[a_, b_] := If[LessEqual[N[Exp[a], $MachinePrecision], 1e-13], N[(N[Exp[a], $MachinePrecision] / N[(1.0 + 1.0), $MachinePrecision]), $MachinePrecision], N[(1.0 / N[(1.0 + N[Exp[b], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
                                
                                \begin{array}{l}
                                
                                \\
                                \begin{array}{l}
                                \mathbf{if}\;e^{a} \leq 10^{-13}:\\
                                \;\;\;\;\frac{e^{a}}{1 + 1}\\
                                
                                \mathbf{else}:\\
                                \;\;\;\;\frac{1}{1 + e^{b}}\\
                                
                                
                                \end{array}
                                \end{array}
                                
                                Derivation
                                1. Split input into 2 regimes
                                2. if (exp.f64 a) < 1e-13

                                  1. Initial program 98.8%

                                    \[\frac{e^{a}}{e^{a} + e^{b}} \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in b around 0

                                    \[\leadsto \frac{e^{a}}{e^{a} + \color{blue}{1}} \]
                                  4. Step-by-step derivation
                                    1. Applied rewrites100.0%

                                      \[\leadsto \frac{e^{a}}{e^{a} + \color{blue}{1}} \]
                                    2. Taylor expanded in a around 0

                                      \[\leadsto \frac{e^{a}}{\color{blue}{1} + 1} \]
                                    3. Step-by-step derivation
                                      1. Applied rewrites99.0%

                                        \[\leadsto \frac{e^{a}}{\color{blue}{1} + 1} \]

                                      if 1e-13 < (exp.f64 a)

                                      1. Initial program 99.4%

                                        \[\frac{e^{a}}{e^{a} + e^{b}} \]
                                      2. Add Preprocessing
                                      3. Taylor expanded in a around 0

                                        \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                      4. Step-by-step derivation
                                        1. lower-/.f64N/A

                                          \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                        2. +-commutativeN/A

                                          \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                        3. lower-+.f64N/A

                                          \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                        4. lower-exp.f6498.8

                                          \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                                      5. Applied rewrites98.8%

                                        \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                                    4. Recombined 2 regimes into one program.
                                    5. Final simplification98.8%

                                      \[\leadsto \begin{array}{l} \mathbf{if}\;e^{a} \leq 10^{-13}:\\ \;\;\;\;\frac{e^{a}}{1 + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + e^{b}}\\ \end{array} \]
                                    6. Add Preprocessing

                                    Alternative 11: 86.1% accurate, 2.6× speedup?

                                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \leq -7.8 \cdot 10^{+23}:\\ \;\;\;\;-0.0020833333333333333 \cdot {b}^{5}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + e^{b}}\\ \end{array} \end{array} \]
                                    (FPCore (a b)
                                     :precision binary64
                                     (if (<= a -7.8e+23)
                                       (* -0.0020833333333333333 (pow b 5.0))
                                       (/ 1.0 (+ 1.0 (exp b)))))
                                    double code(double a, double b) {
                                    	double tmp;
                                    	if (a <= -7.8e+23) {
                                    		tmp = -0.0020833333333333333 * pow(b, 5.0);
                                    	} else {
                                    		tmp = 1.0 / (1.0 + exp(b));
                                    	}
                                    	return tmp;
                                    }
                                    
                                    real(8) function code(a, b)
                                        real(8), intent (in) :: a
                                        real(8), intent (in) :: b
                                        real(8) :: tmp
                                        if (a <= (-7.8d+23)) then
                                            tmp = (-0.0020833333333333333d0) * (b ** 5.0d0)
                                        else
                                            tmp = 1.0d0 / (1.0d0 + exp(b))
                                        end if
                                        code = tmp
                                    end function
                                    
                                    public static double code(double a, double b) {
                                    	double tmp;
                                    	if (a <= -7.8e+23) {
                                    		tmp = -0.0020833333333333333 * Math.pow(b, 5.0);
                                    	} else {
                                    		tmp = 1.0 / (1.0 + Math.exp(b));
                                    	}
                                    	return tmp;
                                    }
                                    
                                    def code(a, b):
                                    	tmp = 0
                                    	if a <= -7.8e+23:
                                    		tmp = -0.0020833333333333333 * math.pow(b, 5.0)
                                    	else:
                                    		tmp = 1.0 / (1.0 + math.exp(b))
                                    	return tmp
                                    
                                    function code(a, b)
                                    	tmp = 0.0
                                    	if (a <= -7.8e+23)
                                    		tmp = Float64(-0.0020833333333333333 * (b ^ 5.0));
                                    	else
                                    		tmp = Float64(1.0 / Float64(1.0 + exp(b)));
                                    	end
                                    	return tmp
                                    end
                                    
                                    function tmp_2 = code(a, b)
                                    	tmp = 0.0;
                                    	if (a <= -7.8e+23)
                                    		tmp = -0.0020833333333333333 * (b ^ 5.0);
                                    	else
                                    		tmp = 1.0 / (1.0 + exp(b));
                                    	end
                                    	tmp_2 = tmp;
                                    end
                                    
                                    code[a_, b_] := If[LessEqual[a, -7.8e+23], N[(-0.0020833333333333333 * N[Power[b, 5.0], $MachinePrecision]), $MachinePrecision], N[(1.0 / N[(1.0 + N[Exp[b], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
                                    
                                    \begin{array}{l}
                                    
                                    \\
                                    \begin{array}{l}
                                    \mathbf{if}\;a \leq -7.8 \cdot 10^{+23}:\\
                                    \;\;\;\;-0.0020833333333333333 \cdot {b}^{5}\\
                                    
                                    \mathbf{else}:\\
                                    \;\;\;\;\frac{1}{1 + e^{b}}\\
                                    
                                    
                                    \end{array}
                                    \end{array}
                                    
                                    Derivation
                                    1. Split input into 2 regimes
                                    2. if a < -7.8000000000000001e23

                                      1. Initial program 98.7%

                                        \[\frac{e^{a}}{e^{a} + e^{b}} \]
                                      2. Add Preprocessing
                                      3. Taylor expanded in a around 0

                                        \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                      4. Step-by-step derivation
                                        1. lower-/.f64N/A

                                          \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                        2. +-commutativeN/A

                                          \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                        3. lower-+.f64N/A

                                          \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                        4. lower-exp.f6432.8

                                          \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                                      5. Applied rewrites32.8%

                                        \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                                      6. Taylor expanded in b around 0

                                        \[\leadsto \frac{1}{2} + \color{blue}{b \cdot \left({b}^{2} \cdot \left(\frac{1}{48} + \frac{-1}{480} \cdot {b}^{2}\right) - \frac{1}{4}\right)} \]
                                      7. Step-by-step derivation
                                        1. Applied rewrites2.7%

                                          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.0020833333333333333, b \cdot b, 0.020833333333333332\right), b \cdot b, -0.25\right), \color{blue}{b}, 0.5\right) \]
                                        2. Taylor expanded in b around inf

                                          \[\leadsto \frac{-1}{480} \cdot {b}^{\color{blue}{5}} \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites55.9%

                                            \[\leadsto {b}^{5} \cdot -0.0020833333333333333 \]

                                          if -7.8000000000000001e23 < a

                                          1. Initial program 99.4%

                                            \[\frac{e^{a}}{e^{a} + e^{b}} \]
                                          2. Add Preprocessing
                                          3. Taylor expanded in a around 0

                                            \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                          4. Step-by-step derivation
                                            1. lower-/.f64N/A

                                              \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                            2. +-commutativeN/A

                                              \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                            3. lower-+.f64N/A

                                              \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                            4. lower-exp.f6496.7

                                              \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                                          5. Applied rewrites96.7%

                                            \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                                        4. Recombined 2 regimes into one program.
                                        5. Final simplification84.7%

                                          \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -7.8 \cdot 10^{+23}:\\ \;\;\;\;-0.0020833333333333333 \cdot {b}^{5}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + e^{b}}\\ \end{array} \]
                                        6. Add Preprocessing

                                        Alternative 12: 39.4% accurate, 315.0× speedup?

                                        \[\begin{array}{l} \\ 0.5 \end{array} \]
                                        (FPCore (a b) :precision binary64 0.5)
                                        double code(double a, double b) {
                                        	return 0.5;
                                        }
                                        
                                        real(8) function code(a, b)
                                            real(8), intent (in) :: a
                                            real(8), intent (in) :: b
                                            code = 0.5d0
                                        end function
                                        
                                        public static double code(double a, double b) {
                                        	return 0.5;
                                        }
                                        
                                        def code(a, b):
                                        	return 0.5
                                        
                                        function code(a, b)
                                        	return 0.5
                                        end
                                        
                                        function tmp = code(a, b)
                                        	tmp = 0.5;
                                        end
                                        
                                        code[a_, b_] := 0.5
                                        
                                        \begin{array}{l}
                                        
                                        \\
                                        0.5
                                        \end{array}
                                        
                                        Derivation
                                        1. Initial program 99.2%

                                          \[\frac{e^{a}}{e^{a} + e^{b}} \]
                                        2. Add Preprocessing
                                        3. Taylor expanded in a around 0

                                          \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                        4. Step-by-step derivation
                                          1. lower-/.f64N/A

                                            \[\leadsto \color{blue}{\frac{1}{1 + e^{b}}} \]
                                          2. +-commutativeN/A

                                            \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                          3. lower-+.f64N/A

                                            \[\leadsto \frac{1}{\color{blue}{e^{b} + 1}} \]
                                          4. lower-exp.f6478.0

                                            \[\leadsto \frac{1}{\color{blue}{e^{b}} + 1} \]
                                        5. Applied rewrites78.0%

                                          \[\leadsto \color{blue}{\frac{1}{e^{b} + 1}} \]
                                        6. Taylor expanded in b around 0

                                          \[\leadsto \frac{1}{2} \]
                                        7. Step-by-step derivation
                                          1. Applied rewrites38.8%

                                            \[\leadsto 0.5 \]
                                          2. Add Preprocessing

                                          Developer Target 1: 100.0% accurate, 2.7× speedup?

                                          \[\begin{array}{l} \\ \frac{1}{1 + e^{b - a}} \end{array} \]
                                          (FPCore (a b) :precision binary64 (/ 1.0 (+ 1.0 (exp (- b a)))))
                                          double code(double a, double b) {
                                          	return 1.0 / (1.0 + exp((b - a)));
                                          }
                                          
                                          real(8) function code(a, b)
                                              real(8), intent (in) :: a
                                              real(8), intent (in) :: b
                                              code = 1.0d0 / (1.0d0 + exp((b - a)))
                                          end function
                                          
                                          public static double code(double a, double b) {
                                          	return 1.0 / (1.0 + Math.exp((b - a)));
                                          }
                                          
                                          def code(a, b):
                                          	return 1.0 / (1.0 + math.exp((b - a)))
                                          
                                          function code(a, b)
                                          	return Float64(1.0 / Float64(1.0 + exp(Float64(b - a))))
                                          end
                                          
                                          function tmp = code(a, b)
                                          	tmp = 1.0 / (1.0 + exp((b - a)));
                                          end
                                          
                                          code[a_, b_] := N[(1.0 / N[(1.0 + N[Exp[N[(b - a), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
                                          
                                          \begin{array}{l}
                                          
                                          \\
                                          \frac{1}{1 + e^{b - a}}
                                          \end{array}
                                          

                                          Reproduce

                                          ?
                                          herbie shell --seed 2024284 
                                          (FPCore (a b)
                                            :name "Quotient of sum of exps"
                                            :precision binary64
                                          
                                            :alt
                                            (! :herbie-platform default (/ 1 (+ 1 (exp (- b a)))))
                                          
                                            (/ (exp a) (+ (exp a) (exp b))))