Numeric.Log:$clog1p from log-domain-0.10.2.1, B

Percentage Accurate: 99.7% → 99.8%
Time: 5.6s
Alternatives: 10
Speedup: 1.0×

Specification

?
\[\begin{array}{l} \\ \frac{x}{1 + \sqrt{x + 1}} \end{array} \]
(FPCore (x) :precision binary64 (/ x (+ 1.0 (sqrt (+ x 1.0)))))
double code(double x) {
	return x / (1.0 + sqrt((x + 1.0)));
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = x / (1.0d0 + sqrt((x + 1.0d0)))
end function
public static double code(double x) {
	return x / (1.0 + Math.sqrt((x + 1.0)));
}
def code(x):
	return x / (1.0 + math.sqrt((x + 1.0)))
function code(x)
	return Float64(x / Float64(1.0 + sqrt(Float64(x + 1.0))))
end
function tmp = code(x)
	tmp = x / (1.0 + sqrt((x + 1.0)));
end
code[x_] := N[(x / N[(1.0 + N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{x}{1 + \sqrt{x + 1}}
\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 10 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.7% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{x}{1 + \sqrt{x + 1}} \end{array} \]
(FPCore (x) :precision binary64 (/ x (+ 1.0 (sqrt (+ x 1.0)))))
double code(double x) {
	return x / (1.0 + sqrt((x + 1.0)));
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = x / (1.0d0 + sqrt((x + 1.0d0)))
end function
public static double code(double x) {
	return x / (1.0 + Math.sqrt((x + 1.0)));
}
def code(x):
	return x / (1.0 + math.sqrt((x + 1.0)))
function code(x)
	return Float64(x / Float64(1.0 + sqrt(Float64(x + 1.0))))
end
function tmp = code(x)
	tmp = x / (1.0 + sqrt((x + 1.0)));
end
code[x_] := N[(x / N[(1.0 + N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{x}{1 + \sqrt{x + 1}}
\end{array}

Alternative 1: 99.8% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \sqrt{1 + x}\\ \mathbf{if}\;\frac{x}{t\_0 + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.0390625, x, 0.0625\right), x, -0.125\right), x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;t\_0 - 1\\ \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (let* ((t_0 (sqrt (+ 1.0 x))))
   (if (<= (/ x (+ t_0 1.0)) 0.0002)
     (* (fma (fma (fma -0.0390625 x 0.0625) x -0.125) x 0.5) x)
     (- t_0 1.0))))
double code(double x) {
	double t_0 = sqrt((1.0 + x));
	double tmp;
	if ((x / (t_0 + 1.0)) <= 0.0002) {
		tmp = fma(fma(fma(-0.0390625, x, 0.0625), x, -0.125), x, 0.5) * x;
	} else {
		tmp = t_0 - 1.0;
	}
	return tmp;
}
function code(x)
	t_0 = sqrt(Float64(1.0 + x))
	tmp = 0.0
	if (Float64(x / Float64(t_0 + 1.0)) <= 0.0002)
		tmp = Float64(fma(fma(fma(-0.0390625, x, 0.0625), x, -0.125), x, 0.5) * x);
	else
		tmp = Float64(t_0 - 1.0);
	end
	return tmp
end
code[x_] := Block[{t$95$0 = N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[N[(x / N[(t$95$0 + 1.0), $MachinePrecision]), $MachinePrecision], 0.0002], N[(N[(N[(N[(-0.0390625 * x + 0.0625), $MachinePrecision] * x + -0.125), $MachinePrecision] * x + 0.5), $MachinePrecision] * x), $MachinePrecision], N[(t$95$0 - 1.0), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \sqrt{1 + x}\\
\mathbf{if}\;\frac{x}{t\_0 + 1} \leq 0.0002:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.0390625, x, 0.0625\right), x, -0.125\right), x, 0.5\right) \cdot x\\

\mathbf{else}:\\
\;\;\;\;t\_0 - 1\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2.0000000000000001e-4

    1. Initial program 100.0%

      \[\frac{x}{1 + \sqrt{x + 1}} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \color{blue}{x \cdot \left(\frac{1}{2} + x \cdot \left(x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) - \frac{1}{8}\right)\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\frac{1}{2} + x \cdot \left(x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) - \frac{1}{8}\right)\right) \cdot x} \]
      2. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\frac{1}{2} + x \cdot \left(x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) - \frac{1}{8}\right)\right) \cdot x} \]
      3. +-commutativeN/A

        \[\leadsto \color{blue}{\left(x \cdot \left(x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) - \frac{1}{8}\right) + \frac{1}{2}\right)} \cdot x \]
      4. *-commutativeN/A

        \[\leadsto \left(\color{blue}{\left(x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) - \frac{1}{8}\right) \cdot x} + \frac{1}{2}\right) \cdot x \]
      5. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) - \frac{1}{8}, x, \frac{1}{2}\right)} \cdot x \]
      6. sub-negN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{x \cdot \left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) + \left(\mathsf{neg}\left(\frac{1}{8}\right)\right)}, x, \frac{1}{2}\right) \cdot x \]
      7. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) \cdot x} + \left(\mathsf{neg}\left(\frac{1}{8}\right)\right), x, \frac{1}{2}\right) \cdot x \]
      8. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\left(\frac{1}{16} + \frac{-5}{128} \cdot x\right) \cdot x + \color{blue}{\frac{-1}{8}}, x, \frac{1}{2}\right) \cdot x \]
      9. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{1}{16} + \frac{-5}{128} \cdot x, x, \frac{-1}{8}\right)}, x, \frac{1}{2}\right) \cdot x \]
      10. +-commutativeN/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\frac{-5}{128} \cdot x + \frac{1}{16}}, x, \frac{-1}{8}\right), x, \frac{1}{2}\right) \cdot x \]
      11. lower-fma.f6499.8

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(-0.0390625, x, 0.0625\right)}, x, -0.125\right), x, 0.5\right) \cdot x \]
    5. Applied rewrites99.8%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.0390625, x, 0.0625\right), x, -0.125\right), x, 0.5\right) \cdot x} \]

    if 2.0000000000000001e-4 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

    1. Initial program 99.2%

      \[\frac{x}{1 + \sqrt{x + 1}} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{x}{1 + \sqrt{x + 1}}} \]
      2. lift-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{1 + \sqrt{x + 1}}} \]
      3. +-commutativeN/A

        \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1} + 1}} \]
      4. flip-+N/A

        \[\leadsto \frac{x}{\color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}{\sqrt{x + 1} - 1}}} \]
      5. associate-/r/N/A

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

        \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right)} \]
      7. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      8. lift-sqrt.f64N/A

        \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1}} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      9. lift-sqrt.f64N/A

        \[\leadsto \frac{x}{\sqrt{x + 1} \cdot \color{blue}{\sqrt{x + 1}} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      10. rem-square-sqrtN/A

        \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      11. lift-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      12. metadata-evalN/A

        \[\leadsto \frac{x}{\left(x + 1\right) - \color{blue}{1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      13. associate--l+N/A

        \[\leadsto \frac{x}{\color{blue}{x + \left(1 - 1\right)}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      14. metadata-evalN/A

        \[\leadsto \frac{x}{x + \color{blue}{0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      15. lower-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      16. rem-exp-logN/A

        \[\leadsto \frac{x}{x + 0} \cdot \left(\color{blue}{e^{\log \left(\sqrt{x + 1}\right)}} - 1\right) \]
      17. lower-expm1.f64N/A

        \[\leadsto \frac{x}{x + 0} \cdot \color{blue}{\mathsf{expm1}\left(\log \left(\sqrt{x + 1}\right)\right)} \]
      18. lift-sqrt.f64N/A

        \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(\sqrt{x + 1}\right)}\right) \]
      19. pow1/2N/A

        \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left({\left(x + 1\right)}^{\frac{1}{2}}\right)}\right) \]
      20. pow-to-expN/A

        \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(e^{\log \left(x + 1\right) \cdot \frac{1}{2}}\right)}\right) \]
    4. Applied rewrites92.5%

      \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot 0.5\right)} \]
    5. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right)} \]
      2. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{x}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      3. lift-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      4. +-rgt-identityN/A

        \[\leadsto \frac{x}{\color{blue}{x}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      5. *-inversesN/A

        \[\leadsto \color{blue}{1} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      6. lift-expm1.f64N/A

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

        \[\leadsto 1 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right)} \]
      8. lift-*.f64N/A

        \[\leadsto 1 \cdot \left(e^{\color{blue}{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      9. lift-log1p.f64N/A

        \[\leadsto 1 \cdot \left(e^{\color{blue}{\log \left(1 + x\right)} \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      10. exp-to-powN/A

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

        \[\leadsto 1 \cdot \left({\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      12. pow1/2N/A

        \[\leadsto 1 \cdot \left(\color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      13. distribute-rgt-inN/A

        \[\leadsto \color{blue}{\sqrt{x + 1} \cdot 1 + \left(\mathsf{neg}\left(1\right)\right) \cdot 1} \]
      14. metadata-evalN/A

        \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \cdot 1 \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \]
      16. metadata-evalN/A

        \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \]
      17. *-rgt-identityN/A

        \[\leadsto \color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right) \]
      18. sub-negN/A

        \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
      19. lower--.f64N/A

        \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
      20. lower-sqrt.f64N/A

        \[\leadsto \color{blue}{\sqrt{x + 1}} - 1 \]
      21. +-commutativeN/A

        \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
      22. lower-+.f64100.0

        \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
    6. Applied rewrites100.0%

      \[\leadsto \color{blue}{\sqrt{1 + x} - 1} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification99.9%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.0390625, x, 0.0625\right), x, -0.125\right), x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1 + x} - 1\\ \end{array} \]
  5. Add Preprocessing

Alternative 2: 99.2% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \sqrt{1 + x}\\ \mathbf{if}\;\frac{x}{t\_0 + 1} \leq 2 \cdot 10^{-14}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.0625, x, -0.125\right), x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;t\_0 - 1\\ \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (let* ((t_0 (sqrt (+ 1.0 x))))
   (if (<= (/ x (+ t_0 1.0)) 2e-14)
     (* (fma (fma 0.0625 x -0.125) x 0.5) x)
     (- t_0 1.0))))
double code(double x) {
	double t_0 = sqrt((1.0 + x));
	double tmp;
	if ((x / (t_0 + 1.0)) <= 2e-14) {
		tmp = fma(fma(0.0625, x, -0.125), x, 0.5) * x;
	} else {
		tmp = t_0 - 1.0;
	}
	return tmp;
}
function code(x)
	t_0 = sqrt(Float64(1.0 + x))
	tmp = 0.0
	if (Float64(x / Float64(t_0 + 1.0)) <= 2e-14)
		tmp = Float64(fma(fma(0.0625, x, -0.125), x, 0.5) * x);
	else
		tmp = Float64(t_0 - 1.0);
	end
	return tmp
end
code[x_] := Block[{t$95$0 = N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[N[(x / N[(t$95$0 + 1.0), $MachinePrecision]), $MachinePrecision], 2e-14], N[(N[(N[(0.0625 * x + -0.125), $MachinePrecision] * x + 0.5), $MachinePrecision] * x), $MachinePrecision], N[(t$95$0 - 1.0), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \sqrt{1 + x}\\
\mathbf{if}\;\frac{x}{t\_0 + 1} \leq 2 \cdot 10^{-14}:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.0625, x, -0.125\right), x, 0.5\right) \cdot x\\

\mathbf{else}:\\
\;\;\;\;t\_0 - 1\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2e-14

    1. Initial program 100.0%

      \[\frac{x}{1 + \sqrt{x + 1}} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \color{blue}{x \cdot \left(\frac{1}{2} + x \cdot \left(\frac{1}{16} \cdot x - \frac{1}{8}\right)\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\frac{1}{2} + x \cdot \left(\frac{1}{16} \cdot x - \frac{1}{8}\right)\right) \cdot x} \]
      2. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\frac{1}{2} + x \cdot \left(\frac{1}{16} \cdot x - \frac{1}{8}\right)\right) \cdot x} \]
      3. +-commutativeN/A

        \[\leadsto \color{blue}{\left(x \cdot \left(\frac{1}{16} \cdot x - \frac{1}{8}\right) + \frac{1}{2}\right)} \cdot x \]
      4. *-commutativeN/A

        \[\leadsto \left(\color{blue}{\left(\frac{1}{16} \cdot x - \frac{1}{8}\right) \cdot x} + \frac{1}{2}\right) \cdot x \]
      5. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{16} \cdot x - \frac{1}{8}, x, \frac{1}{2}\right)} \cdot x \]
      6. sub-negN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{1}{16} \cdot x + \left(\mathsf{neg}\left(\frac{1}{8}\right)\right)}, x, \frac{1}{2}\right) \cdot x \]
      7. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{16} \cdot x + \color{blue}{\frac{-1}{8}}, x, \frac{1}{2}\right) \cdot x \]
      8. lower-fma.f6499.7

        \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(0.0625, x, -0.125\right)}, x, 0.5\right) \cdot x \]
    5. Applied rewrites99.7%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(0.0625, x, -0.125\right), x, 0.5\right) \cdot x} \]

    if 2e-14 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

    1. Initial program 99.2%

      \[\frac{x}{1 + \sqrt{x + 1}} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{x}{1 + \sqrt{x + 1}}} \]
      2. lift-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{1 + \sqrt{x + 1}}} \]
      3. +-commutativeN/A

        \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1} + 1}} \]
      4. flip-+N/A

        \[\leadsto \frac{x}{\color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}{\sqrt{x + 1} - 1}}} \]
      5. associate-/r/N/A

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

        \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right)} \]
      7. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      8. lift-sqrt.f64N/A

        \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1}} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      9. lift-sqrt.f64N/A

        \[\leadsto \frac{x}{\sqrt{x + 1} \cdot \color{blue}{\sqrt{x + 1}} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      10. rem-square-sqrtN/A

        \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      11. lift-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
      12. metadata-evalN/A

        \[\leadsto \frac{x}{\left(x + 1\right) - \color{blue}{1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      13. associate--l+N/A

        \[\leadsto \frac{x}{\color{blue}{x + \left(1 - 1\right)}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      14. metadata-evalN/A

        \[\leadsto \frac{x}{x + \color{blue}{0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      15. lower-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
      16. rem-exp-logN/A

        \[\leadsto \frac{x}{x + 0} \cdot \left(\color{blue}{e^{\log \left(\sqrt{x + 1}\right)}} - 1\right) \]
      17. lower-expm1.f64N/A

        \[\leadsto \frac{x}{x + 0} \cdot \color{blue}{\mathsf{expm1}\left(\log \left(\sqrt{x + 1}\right)\right)} \]
      18. lift-sqrt.f64N/A

        \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(\sqrt{x + 1}\right)}\right) \]
      19. pow1/2N/A

        \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left({\left(x + 1\right)}^{\frac{1}{2}}\right)}\right) \]
      20. pow-to-expN/A

        \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(e^{\log \left(x + 1\right) \cdot \frac{1}{2}}\right)}\right) \]
    4. Applied rewrites92.6%

      \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot 0.5\right)} \]
    5. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right)} \]
      2. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{x}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      3. lift-+.f64N/A

        \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      4. +-rgt-identityN/A

        \[\leadsto \frac{x}{\color{blue}{x}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      5. *-inversesN/A

        \[\leadsto \color{blue}{1} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
      6. lift-expm1.f64N/A

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

        \[\leadsto 1 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right)} \]
      8. lift-*.f64N/A

        \[\leadsto 1 \cdot \left(e^{\color{blue}{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      9. lift-log1p.f64N/A

        \[\leadsto 1 \cdot \left(e^{\color{blue}{\log \left(1 + x\right)} \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      10. exp-to-powN/A

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

        \[\leadsto 1 \cdot \left({\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      12. pow1/2N/A

        \[\leadsto 1 \cdot \left(\color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
      13. distribute-rgt-inN/A

        \[\leadsto \color{blue}{\sqrt{x + 1} \cdot 1 + \left(\mathsf{neg}\left(1\right)\right) \cdot 1} \]
      14. metadata-evalN/A

        \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \cdot 1 \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \]
      16. metadata-evalN/A

        \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \]
      17. *-rgt-identityN/A

        \[\leadsto \color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right) \]
      18. sub-negN/A

        \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
      19. lower--.f64N/A

        \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
      20. lower-sqrt.f64N/A

        \[\leadsto \color{blue}{\sqrt{x + 1}} - 1 \]
      21. +-commutativeN/A

        \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
      22. lower-+.f6499.8

        \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
    6. Applied rewrites99.8%

      \[\leadsto \color{blue}{\sqrt{1 + x} - 1} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification99.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 2 \cdot 10^{-14}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.0625, x, -0.125\right), x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1 + x} - 1\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 99.0% accurate, 0.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \sqrt{1 + x}\\ \mathbf{if}\;\frac{x}{t\_0 + 1} \leq 2 \cdot 10^{-14}:\\ \;\;\;\;\mathsf{fma}\left(-0.125 \cdot x, x, 0.5 \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0 - 1\\ \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (let* ((t_0 (sqrt (+ 1.0 x))))
   (if (<= (/ x (+ t_0 1.0)) 2e-14)
     (fma (* -0.125 x) x (* 0.5 x))
     (- t_0 1.0))))
double code(double x) {
	double t_0 = sqrt((1.0 + x));
	double tmp;
	if ((x / (t_0 + 1.0)) <= 2e-14) {
		tmp = fma((-0.125 * x), x, (0.5 * x));
	} else {
		tmp = t_0 - 1.0;
	}
	return tmp;
}
function code(x)
	t_0 = sqrt(Float64(1.0 + x))
	tmp = 0.0
	if (Float64(x / Float64(t_0 + 1.0)) <= 2e-14)
		tmp = fma(Float64(-0.125 * x), x, Float64(0.5 * x));
	else
		tmp = Float64(t_0 - 1.0);
	end
	return tmp
end
code[x_] := Block[{t$95$0 = N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[N[(x / N[(t$95$0 + 1.0), $MachinePrecision]), $MachinePrecision], 2e-14], N[(N[(-0.125 * x), $MachinePrecision] * x + N[(0.5 * x), $MachinePrecision]), $MachinePrecision], N[(t$95$0 - 1.0), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \sqrt{1 + x}\\
\mathbf{if}\;\frac{x}{t\_0 + 1} \leq 2 \cdot 10^{-14}:\\
\;\;\;\;\mathsf{fma}\left(-0.125 \cdot x, x, 0.5 \cdot x\right)\\

\mathbf{else}:\\
\;\;\;\;t\_0 - 1\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2e-14

    1. Initial program 100.0%

      \[\frac{x}{1 + \sqrt{x + 1}} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

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

        \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
      2. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
      3. +-commutativeN/A

        \[\leadsto \color{blue}{\left(\frac{-1}{8} \cdot x + \frac{1}{2}\right)} \cdot x \]
      4. lower-fma.f6499.5

        \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right)} \cdot x \]
    5. Applied rewrites99.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x} \]
    6. Step-by-step derivation
      1. Applied rewrites99.5%

        \[\leadsto \mathsf{fma}\left(-0.125 \cdot x, \color{blue}{x}, 0.5 \cdot x\right) \]

      if 2e-14 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

      1. Initial program 99.2%

        \[\frac{x}{1 + \sqrt{x + 1}} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{x}{1 + \sqrt{x + 1}}} \]
        2. lift-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{1 + \sqrt{x + 1}}} \]
        3. +-commutativeN/A

          \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1} + 1}} \]
        4. flip-+N/A

          \[\leadsto \frac{x}{\color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}{\sqrt{x + 1} - 1}}} \]
        5. associate-/r/N/A

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

          \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right)} \]
        7. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        8. lift-sqrt.f64N/A

          \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1}} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        9. lift-sqrt.f64N/A

          \[\leadsto \frac{x}{\sqrt{x + 1} \cdot \color{blue}{\sqrt{x + 1}} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        10. rem-square-sqrtN/A

          \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        11. lift-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        12. metadata-evalN/A

          \[\leadsto \frac{x}{\left(x + 1\right) - \color{blue}{1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        13. associate--l+N/A

          \[\leadsto \frac{x}{\color{blue}{x + \left(1 - 1\right)}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        14. metadata-evalN/A

          \[\leadsto \frac{x}{x + \color{blue}{0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        15. lower-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        16. rem-exp-logN/A

          \[\leadsto \frac{x}{x + 0} \cdot \left(\color{blue}{e^{\log \left(\sqrt{x + 1}\right)}} - 1\right) \]
        17. lower-expm1.f64N/A

          \[\leadsto \frac{x}{x + 0} \cdot \color{blue}{\mathsf{expm1}\left(\log \left(\sqrt{x + 1}\right)\right)} \]
        18. lift-sqrt.f64N/A

          \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(\sqrt{x + 1}\right)}\right) \]
        19. pow1/2N/A

          \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left({\left(x + 1\right)}^{\frac{1}{2}}\right)}\right) \]
        20. pow-to-expN/A

          \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(e^{\log \left(x + 1\right) \cdot \frac{1}{2}}\right)}\right) \]
      4. Applied rewrites92.6%

        \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot 0.5\right)} \]
      5. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right)} \]
        2. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{x}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        3. lift-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        4. +-rgt-identityN/A

          \[\leadsto \frac{x}{\color{blue}{x}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        5. *-inversesN/A

          \[\leadsto \color{blue}{1} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        6. lift-expm1.f64N/A

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

          \[\leadsto 1 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right)} \]
        8. lift-*.f64N/A

          \[\leadsto 1 \cdot \left(e^{\color{blue}{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        9. lift-log1p.f64N/A

          \[\leadsto 1 \cdot \left(e^{\color{blue}{\log \left(1 + x\right)} \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        10. exp-to-powN/A

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

          \[\leadsto 1 \cdot \left({\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        12. pow1/2N/A

          \[\leadsto 1 \cdot \left(\color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        13. distribute-rgt-inN/A

          \[\leadsto \color{blue}{\sqrt{x + 1} \cdot 1 + \left(\mathsf{neg}\left(1\right)\right) \cdot 1} \]
        14. metadata-evalN/A

          \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \cdot 1 \]
        15. metadata-evalN/A

          \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \]
        16. metadata-evalN/A

          \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \]
        17. *-rgt-identityN/A

          \[\leadsto \color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right) \]
        18. sub-negN/A

          \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
        19. lower--.f64N/A

          \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
        20. lower-sqrt.f64N/A

          \[\leadsto \color{blue}{\sqrt{x + 1}} - 1 \]
        21. +-commutativeN/A

          \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
        22. lower-+.f6499.8

          \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
      6. Applied rewrites99.8%

        \[\leadsto \color{blue}{\sqrt{1 + x} - 1} \]
    7. Recombined 2 regimes into one program.
    8. Final simplification99.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 2 \cdot 10^{-14}:\\ \;\;\;\;\mathsf{fma}\left(-0.125 \cdot x, x, 0.5 \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1 + x} - 1\\ \end{array} \]
    9. Add Preprocessing

    Alternative 4: 98.5% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(-0.125 \cdot x, x, 0.5 \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x} - 1\\ \end{array} \end{array} \]
    (FPCore (x)
     :precision binary64
     (if (<= (/ x (+ (sqrt (+ 1.0 x)) 1.0)) 0.0002)
       (fma (* -0.125 x) x (* 0.5 x))
       (- (sqrt x) 1.0)))
    double code(double x) {
    	double tmp;
    	if ((x / (sqrt((1.0 + x)) + 1.0)) <= 0.0002) {
    		tmp = fma((-0.125 * x), x, (0.5 * x));
    	} else {
    		tmp = sqrt(x) - 1.0;
    	}
    	return tmp;
    }
    
    function code(x)
    	tmp = 0.0
    	if (Float64(x / Float64(sqrt(Float64(1.0 + x)) + 1.0)) <= 0.0002)
    		tmp = fma(Float64(-0.125 * x), x, Float64(0.5 * x));
    	else
    		tmp = Float64(sqrt(x) - 1.0);
    	end
    	return tmp
    end
    
    code[x_] := If[LessEqual[N[(x / N[(N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], 0.0002], N[(N[(-0.125 * x), $MachinePrecision] * x + N[(0.5 * x), $MachinePrecision]), $MachinePrecision], N[(N[Sqrt[x], $MachinePrecision] - 1.0), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\
    \;\;\;\;\mathsf{fma}\left(-0.125 \cdot x, x, 0.5 \cdot x\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{x} - 1\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2.0000000000000001e-4

      1. Initial program 100.0%

        \[\frac{x}{1 + \sqrt{x + 1}} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

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

          \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
        2. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
        3. +-commutativeN/A

          \[\leadsto \color{blue}{\left(\frac{-1}{8} \cdot x + \frac{1}{2}\right)} \cdot x \]
        4. lower-fma.f6499.2

          \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right)} \cdot x \]
      5. Applied rewrites99.2%

        \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x} \]
      6. Step-by-step derivation
        1. Applied rewrites99.2%

          \[\leadsto \mathsf{fma}\left(-0.125 \cdot x, \color{blue}{x}, 0.5 \cdot x\right) \]

        if 2.0000000000000001e-4 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

        1. Initial program 99.2%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto \color{blue}{\sqrt{x} - 1} \]
        4. Step-by-step derivation
          1. lower--.f64N/A

            \[\leadsto \color{blue}{\sqrt{x} - 1} \]
          2. lower-sqrt.f6497.2

            \[\leadsto \color{blue}{\sqrt{x}} - 1 \]
        5. Applied rewrites97.2%

          \[\leadsto \color{blue}{\sqrt{x} - 1} \]
      7. Recombined 2 regimes into one program.
      8. Final simplification98.6%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(-0.125 \cdot x, x, 0.5 \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x} - 1\\ \end{array} \]
      9. Add Preprocessing

      Alternative 5: 98.5% accurate, 0.6× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x} - 1\\ \end{array} \end{array} \]
      (FPCore (x)
       :precision binary64
       (if (<= (/ x (+ (sqrt (+ 1.0 x)) 1.0)) 0.0002)
         (* (fma -0.125 x 0.5) x)
         (- (sqrt x) 1.0)))
      double code(double x) {
      	double tmp;
      	if ((x / (sqrt((1.0 + x)) + 1.0)) <= 0.0002) {
      		tmp = fma(-0.125, x, 0.5) * x;
      	} else {
      		tmp = sqrt(x) - 1.0;
      	}
      	return tmp;
      }
      
      function code(x)
      	tmp = 0.0
      	if (Float64(x / Float64(sqrt(Float64(1.0 + x)) + 1.0)) <= 0.0002)
      		tmp = Float64(fma(-0.125, x, 0.5) * x);
      	else
      		tmp = Float64(sqrt(x) - 1.0);
      	end
      	return tmp
      end
      
      code[x_] := If[LessEqual[N[(x / N[(N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], 0.0002], N[(N[(-0.125 * x + 0.5), $MachinePrecision] * x), $MachinePrecision], N[(N[Sqrt[x], $MachinePrecision] - 1.0), $MachinePrecision]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\
      \;\;\;\;\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x\\
      
      \mathbf{else}:\\
      \;\;\;\;\sqrt{x} - 1\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2.0000000000000001e-4

        1. Initial program 100.0%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

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

            \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
          2. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
          3. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\frac{-1}{8} \cdot x + \frac{1}{2}\right)} \cdot x \]
          4. lower-fma.f6499.2

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right)} \cdot x \]
        5. Applied rewrites99.2%

          \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x} \]

        if 2.0000000000000001e-4 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

        1. Initial program 99.2%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto \color{blue}{\sqrt{x} - 1} \]
        4. Step-by-step derivation
          1. lower--.f64N/A

            \[\leadsto \color{blue}{\sqrt{x} - 1} \]
          2. lower-sqrt.f6497.2

            \[\leadsto \color{blue}{\sqrt{x}} - 1 \]
        5. Applied rewrites97.2%

          \[\leadsto \color{blue}{\sqrt{x} - 1} \]
      3. Recombined 2 regimes into one program.
      4. Final simplification98.6%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x} - 1\\ \end{array} \]
      5. Add Preprocessing

      Alternative 6: 97.8% accurate, 0.6× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x}\\ \end{array} \end{array} \]
      (FPCore (x)
       :precision binary64
       (if (<= (/ x (+ (sqrt (+ 1.0 x)) 1.0)) 0.0002)
         (* (fma -0.125 x 0.5) x)
         (sqrt x)))
      double code(double x) {
      	double tmp;
      	if ((x / (sqrt((1.0 + x)) + 1.0)) <= 0.0002) {
      		tmp = fma(-0.125, x, 0.5) * x;
      	} else {
      		tmp = sqrt(x);
      	}
      	return tmp;
      }
      
      function code(x)
      	tmp = 0.0
      	if (Float64(x / Float64(sqrt(Float64(1.0 + x)) + 1.0)) <= 0.0002)
      		tmp = Float64(fma(-0.125, x, 0.5) * x);
      	else
      		tmp = sqrt(x);
      	end
      	return tmp
      end
      
      code[x_] := If[LessEqual[N[(x / N[(N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], 0.0002], N[(N[(-0.125 * x + 0.5), $MachinePrecision] * x), $MachinePrecision], N[Sqrt[x], $MachinePrecision]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\
      \;\;\;\;\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x\\
      
      \mathbf{else}:\\
      \;\;\;\;\sqrt{x}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2.0000000000000001e-4

        1. Initial program 100.0%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

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

            \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
          2. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\frac{1}{2} + \frac{-1}{8} \cdot x\right) \cdot x} \]
          3. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\frac{-1}{8} \cdot x + \frac{1}{2}\right)} \cdot x \]
          4. lower-fma.f6499.2

            \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right)} \cdot x \]
        5. Applied rewrites99.2%

          \[\leadsto \color{blue}{\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x} \]

        if 2.0000000000000001e-4 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

        1. Initial program 99.2%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto \color{blue}{\sqrt{x}} \]
        4. Step-by-step derivation
          1. lower-sqrt.f6495.8

            \[\leadsto \color{blue}{\sqrt{x}} \]
        5. Applied rewrites95.8%

          \[\leadsto \color{blue}{\sqrt{x}} \]
      3. Recombined 2 regimes into one program.
      4. Final simplification98.1%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;\mathsf{fma}\left(-0.125, x, 0.5\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x}\\ \end{array} \]
      5. Add Preprocessing

      Alternative 7: 97.1% accurate, 0.6× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x}\\ \end{array} \end{array} \]
      (FPCore (x)
       :precision binary64
       (if (<= (/ x (+ (sqrt (+ 1.0 x)) 1.0)) 0.0002) (* 0.5 x) (sqrt x)))
      double code(double x) {
      	double tmp;
      	if ((x / (sqrt((1.0 + x)) + 1.0)) <= 0.0002) {
      		tmp = 0.5 * x;
      	} else {
      		tmp = sqrt(x);
      	}
      	return tmp;
      }
      
      real(8) function code(x)
          real(8), intent (in) :: x
          real(8) :: tmp
          if ((x / (sqrt((1.0d0 + x)) + 1.0d0)) <= 0.0002d0) then
              tmp = 0.5d0 * x
          else
              tmp = sqrt(x)
          end if
          code = tmp
      end function
      
      public static double code(double x) {
      	double tmp;
      	if ((x / (Math.sqrt((1.0 + x)) + 1.0)) <= 0.0002) {
      		tmp = 0.5 * x;
      	} else {
      		tmp = Math.sqrt(x);
      	}
      	return tmp;
      }
      
      def code(x):
      	tmp = 0
      	if (x / (math.sqrt((1.0 + x)) + 1.0)) <= 0.0002:
      		tmp = 0.5 * x
      	else:
      		tmp = math.sqrt(x)
      	return tmp
      
      function code(x)
      	tmp = 0.0
      	if (Float64(x / Float64(sqrt(Float64(1.0 + x)) + 1.0)) <= 0.0002)
      		tmp = Float64(0.5 * x);
      	else
      		tmp = sqrt(x);
      	end
      	return tmp
      end
      
      function tmp_2 = code(x)
      	tmp = 0.0;
      	if ((x / (sqrt((1.0 + x)) + 1.0)) <= 0.0002)
      		tmp = 0.5 * x;
      	else
      		tmp = sqrt(x);
      	end
      	tmp_2 = tmp;
      end
      
      code[x_] := If[LessEqual[N[(x / N[(N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision], 0.0002], N[(0.5 * x), $MachinePrecision], N[Sqrt[x], $MachinePrecision]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\
      \;\;\;\;0.5 \cdot x\\
      
      \mathbf{else}:\\
      \;\;\;\;\sqrt{x}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) < 2.0000000000000001e-4

        1. Initial program 100.0%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \color{blue}{\frac{1}{2} \cdot x} \]
        4. Step-by-step derivation
          1. lower-*.f6498.8

            \[\leadsto \color{blue}{0.5 \cdot x} \]
        5. Applied rewrites98.8%

          \[\leadsto \color{blue}{0.5 \cdot x} \]

        if 2.0000000000000001e-4 < (/.f64 x (+.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))

        1. Initial program 99.2%

          \[\frac{x}{1 + \sqrt{x + 1}} \]
        2. Add Preprocessing
        3. Taylor expanded in x around inf

          \[\leadsto \color{blue}{\sqrt{x}} \]
        4. Step-by-step derivation
          1. lower-sqrt.f6495.8

            \[\leadsto \color{blue}{\sqrt{x}} \]
        5. Applied rewrites95.8%

          \[\leadsto \color{blue}{\sqrt{x}} \]
      3. Recombined 2 regimes into one program.
      4. Final simplification97.9%

        \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x}{\sqrt{1 + x} + 1} \leq 0.0002:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x}\\ \end{array} \]
      5. Add Preprocessing

      Alternative 8: 99.7% accurate, 1.0× speedup?

      \[\begin{array}{l} \\ \frac{x}{\sqrt{1 + x} + 1} \end{array} \]
      (FPCore (x) :precision binary64 (/ x (+ (sqrt (+ 1.0 x)) 1.0)))
      double code(double x) {
      	return x / (sqrt((1.0 + x)) + 1.0);
      }
      
      real(8) function code(x)
          real(8), intent (in) :: x
          code = x / (sqrt((1.0d0 + x)) + 1.0d0)
      end function
      
      public static double code(double x) {
      	return x / (Math.sqrt((1.0 + x)) + 1.0);
      }
      
      def code(x):
      	return x / (math.sqrt((1.0 + x)) + 1.0)
      
      function code(x)
      	return Float64(x / Float64(sqrt(Float64(1.0 + x)) + 1.0))
      end
      
      function tmp = code(x)
      	tmp = x / (sqrt((1.0 + x)) + 1.0);
      end
      
      code[x_] := N[(x / N[(N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision]
      
      \begin{array}{l}
      
      \\
      \frac{x}{\sqrt{1 + x} + 1}
      \end{array}
      
      Derivation
      1. Initial program 99.7%

        \[\frac{x}{1 + \sqrt{x + 1}} \]
      2. Add Preprocessing
      3. Final simplification99.7%

        \[\leadsto \frac{x}{\sqrt{1 + x} + 1} \]
      4. Add Preprocessing

      Alternative 9: 68.0% accurate, 4.7× speedup?

      \[\begin{array}{l} \\ 0.5 \cdot x \end{array} \]
      (FPCore (x) :precision binary64 (* 0.5 x))
      double code(double x) {
      	return 0.5 * x;
      }
      
      real(8) function code(x)
          real(8), intent (in) :: x
          code = 0.5d0 * x
      end function
      
      public static double code(double x) {
      	return 0.5 * x;
      }
      
      def code(x):
      	return 0.5 * x
      
      function code(x)
      	return Float64(0.5 * x)
      end
      
      function tmp = code(x)
      	tmp = 0.5 * x;
      end
      
      code[x_] := N[(0.5 * x), $MachinePrecision]
      
      \begin{array}{l}
      
      \\
      0.5 \cdot x
      \end{array}
      
      Derivation
      1. Initial program 99.7%

        \[\frac{x}{1 + \sqrt{x + 1}} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

        \[\leadsto \color{blue}{\frac{1}{2} \cdot x} \]
      4. Step-by-step derivation
        1. lower-*.f6469.5

          \[\leadsto \color{blue}{0.5 \cdot x} \]
      5. Applied rewrites69.5%

        \[\leadsto \color{blue}{0.5 \cdot x} \]
      6. Add Preprocessing

      Alternative 10: 4.5% accurate, 7.0× speedup?

      \[\begin{array}{l} \\ 1 - 1 \end{array} \]
      (FPCore (x) :precision binary64 (- 1.0 1.0))
      double code(double x) {
      	return 1.0 - 1.0;
      }
      
      real(8) function code(x)
          real(8), intent (in) :: x
          code = 1.0d0 - 1.0d0
      end function
      
      public static double code(double x) {
      	return 1.0 - 1.0;
      }
      
      def code(x):
      	return 1.0 - 1.0
      
      function code(x)
      	return Float64(1.0 - 1.0)
      end
      
      function tmp = code(x)
      	tmp = 1.0 - 1.0;
      end
      
      code[x_] := N[(1.0 - 1.0), $MachinePrecision]
      
      \begin{array}{l}
      
      \\
      1 - 1
      \end{array}
      
      Derivation
      1. Initial program 99.7%

        \[\frac{x}{1 + \sqrt{x + 1}} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{x}{1 + \sqrt{x + 1}}} \]
        2. lift-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{1 + \sqrt{x + 1}}} \]
        3. +-commutativeN/A

          \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1} + 1}} \]
        4. flip-+N/A

          \[\leadsto \frac{x}{\color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}{\sqrt{x + 1} - 1}}} \]
        5. associate-/r/N/A

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

          \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right)} \]
        7. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{x}{\sqrt{x + 1} \cdot \sqrt{x + 1} - 1 \cdot 1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        8. lift-sqrt.f64N/A

          \[\leadsto \frac{x}{\color{blue}{\sqrt{x + 1}} \cdot \sqrt{x + 1} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        9. lift-sqrt.f64N/A

          \[\leadsto \frac{x}{\sqrt{x + 1} \cdot \color{blue}{\sqrt{x + 1}} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        10. rem-square-sqrtN/A

          \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        11. lift-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{\left(x + 1\right)} - 1 \cdot 1} \cdot \left(\sqrt{x + 1} - 1\right) \]
        12. metadata-evalN/A

          \[\leadsto \frac{x}{\left(x + 1\right) - \color{blue}{1}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        13. associate--l+N/A

          \[\leadsto \frac{x}{\color{blue}{x + \left(1 - 1\right)}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        14. metadata-evalN/A

          \[\leadsto \frac{x}{x + \color{blue}{0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        15. lower-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \left(\sqrt{x + 1} - 1\right) \]
        16. rem-exp-logN/A

          \[\leadsto \frac{x}{x + 0} \cdot \left(\color{blue}{e^{\log \left(\sqrt{x + 1}\right)}} - 1\right) \]
        17. lower-expm1.f64N/A

          \[\leadsto \frac{x}{x + 0} \cdot \color{blue}{\mathsf{expm1}\left(\log \left(\sqrt{x + 1}\right)\right)} \]
        18. lift-sqrt.f64N/A

          \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(\sqrt{x + 1}\right)}\right) \]
        19. pow1/2N/A

          \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left({\left(x + 1\right)}^{\frac{1}{2}}\right)}\right) \]
        20. pow-to-expN/A

          \[\leadsto \frac{x}{x + 0} \cdot \mathsf{expm1}\left(\log \color{blue}{\left(e^{\log \left(x + 1\right) \cdot \frac{1}{2}}\right)}\right) \]
      4. Applied rewrites97.6%

        \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot 0.5\right)} \]
      5. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \color{blue}{\frac{x}{x + 0} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right)} \]
        2. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{x}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        3. lift-+.f64N/A

          \[\leadsto \frac{x}{\color{blue}{x + 0}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        4. +-rgt-identityN/A

          \[\leadsto \frac{x}{\color{blue}{x}} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        5. *-inversesN/A

          \[\leadsto \color{blue}{1} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}\right) \]
        6. lift-expm1.f64N/A

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

          \[\leadsto 1 \cdot \color{blue}{\left(e^{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right)} \]
        8. lift-*.f64N/A

          \[\leadsto 1 \cdot \left(e^{\color{blue}{\mathsf{log1p}\left(x\right) \cdot \frac{1}{2}}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        9. lift-log1p.f64N/A

          \[\leadsto 1 \cdot \left(e^{\color{blue}{\log \left(1 + x\right)} \cdot \frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        10. exp-to-powN/A

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

          \[\leadsto 1 \cdot \left({\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        12. pow1/2N/A

          \[\leadsto 1 \cdot \left(\color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right)\right) \]
        13. distribute-rgt-inN/A

          \[\leadsto \color{blue}{\sqrt{x + 1} \cdot 1 + \left(\mathsf{neg}\left(1\right)\right) \cdot 1} \]
        14. metadata-evalN/A

          \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \cdot 1 \]
        15. metadata-evalN/A

          \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{-1} \]
        16. metadata-evalN/A

          \[\leadsto \sqrt{x + 1} \cdot 1 + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} \]
        17. *-rgt-identityN/A

          \[\leadsto \color{blue}{\sqrt{x + 1}} + \left(\mathsf{neg}\left(1\right)\right) \]
        18. sub-negN/A

          \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
        19. lower--.f64N/A

          \[\leadsto \color{blue}{\sqrt{x + 1} - 1} \]
        20. lower-sqrt.f64N/A

          \[\leadsto \color{blue}{\sqrt{x + 1}} - 1 \]
        21. +-commutativeN/A

          \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
        22. lower-+.f6437.0

          \[\leadsto \sqrt{\color{blue}{1 + x}} - 1 \]
      6. Applied rewrites37.0%

        \[\leadsto \color{blue}{\sqrt{1 + x} - 1} \]
      7. Taylor expanded in x around 0

        \[\leadsto \color{blue}{1} - 1 \]
      8. Step-by-step derivation
        1. Applied rewrites4.5%

          \[\leadsto \color{blue}{1} - 1 \]
        2. Add Preprocessing

        Reproduce

        ?
        herbie shell --seed 2024276 
        (FPCore (x)
          :name "Numeric.Log:$clog1p from log-domain-0.10.2.1, B"
          :precision binary64
          (/ x (+ 1.0 (sqrt (+ x 1.0)))))