Main:z from

Percentage Accurate: 91.7% → 96.2%
Time: 24.8s
Alternatives: 16
Speedup: 1.3×

Specification

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

\\
\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)
\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 16 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: 91.7% accurate, 1.0× speedup?

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

\\
\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)
\end{array}

Alternative 1: 96.2% accurate, 0.6× speedup?

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{y + 1} + \sqrt{y}\\ t_2 := \sqrt{1 + t} - \sqrt{t}\\ t_3 := \frac{-1}{t_1}\\ t_4 := \sqrt{x + 1}\\ t_5 := \frac{1}{t_1} - \sqrt{x}\\ t_6 := \sqrt{1 + z}\\ \mathbf{if}\;y \leq 5.5 \cdot 10^{+40}:\\ \;\;\;\;\left(t_4 + t_5\right) + \left(t_2 + \frac{1}{\sqrt{z} + t_6}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 + \left(x + \left(\sqrt{x} + t_3\right) \cdot t_5\right)}{\sqrt{x} + \left(t_4 + t_3\right)} + \left(t_2 + \left(t_6 - \sqrt{z}\right)\right)\\ \end{array} \end{array} \]
NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
(FPCore (x y z t)
 :precision binary64
 (let* ((t_1 (+ (sqrt (+ y 1.0)) (sqrt y)))
        (t_2 (- (sqrt (+ 1.0 t)) (sqrt t)))
        (t_3 (/ -1.0 t_1))
        (t_4 (sqrt (+ x 1.0)))
        (t_5 (- (/ 1.0 t_1) (sqrt x)))
        (t_6 (sqrt (+ 1.0 z))))
   (if (<= y 5.5e+40)
     (+ (+ t_4 t_5) (+ t_2 (/ 1.0 (+ (sqrt z) t_6))))
     (+
      (/ (+ 1.0 (+ x (* (+ (sqrt x) t_3) t_5))) (+ (sqrt x) (+ t_4 t_3)))
      (+ t_2 (- t_6 (sqrt z)))))))
assert(x < y && y < z && z < t);
double code(double x, double y, double z, double t) {
	double t_1 = sqrt((y + 1.0)) + sqrt(y);
	double t_2 = sqrt((1.0 + t)) - sqrt(t);
	double t_3 = -1.0 / t_1;
	double t_4 = sqrt((x + 1.0));
	double t_5 = (1.0 / t_1) - sqrt(x);
	double t_6 = sqrt((1.0 + z));
	double tmp;
	if (y <= 5.5e+40) {
		tmp = (t_4 + t_5) + (t_2 + (1.0 / (sqrt(z) + t_6)));
	} else {
		tmp = ((1.0 + (x + ((sqrt(x) + t_3) * t_5))) / (sqrt(x) + (t_4 + t_3))) + (t_2 + (t_6 - sqrt(z)));
	}
	return tmp;
}
NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
real(8) function code(x, y, z, t)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: t_3
    real(8) :: t_4
    real(8) :: t_5
    real(8) :: t_6
    real(8) :: tmp
    t_1 = sqrt((y + 1.0d0)) + sqrt(y)
    t_2 = sqrt((1.0d0 + t)) - sqrt(t)
    t_3 = (-1.0d0) / t_1
    t_4 = sqrt((x + 1.0d0))
    t_5 = (1.0d0 / t_1) - sqrt(x)
    t_6 = sqrt((1.0d0 + z))
    if (y <= 5.5d+40) then
        tmp = (t_4 + t_5) + (t_2 + (1.0d0 / (sqrt(z) + t_6)))
    else
        tmp = ((1.0d0 + (x + ((sqrt(x) + t_3) * t_5))) / (sqrt(x) + (t_4 + t_3))) + (t_2 + (t_6 - sqrt(z)))
    end if
    code = tmp
end function
assert x < y && y < z && z < t;
public static double code(double x, double y, double z, double t) {
	double t_1 = Math.sqrt((y + 1.0)) + Math.sqrt(y);
	double t_2 = Math.sqrt((1.0 + t)) - Math.sqrt(t);
	double t_3 = -1.0 / t_1;
	double t_4 = Math.sqrt((x + 1.0));
	double t_5 = (1.0 / t_1) - Math.sqrt(x);
	double t_6 = Math.sqrt((1.0 + z));
	double tmp;
	if (y <= 5.5e+40) {
		tmp = (t_4 + t_5) + (t_2 + (1.0 / (Math.sqrt(z) + t_6)));
	} else {
		tmp = ((1.0 + (x + ((Math.sqrt(x) + t_3) * t_5))) / (Math.sqrt(x) + (t_4 + t_3))) + (t_2 + (t_6 - Math.sqrt(z)));
	}
	return tmp;
}
[x, y, z, t] = sort([x, y, z, t])
def code(x, y, z, t):
	t_1 = math.sqrt((y + 1.0)) + math.sqrt(y)
	t_2 = math.sqrt((1.0 + t)) - math.sqrt(t)
	t_3 = -1.0 / t_1
	t_4 = math.sqrt((x + 1.0))
	t_5 = (1.0 / t_1) - math.sqrt(x)
	t_6 = math.sqrt((1.0 + z))
	tmp = 0
	if y <= 5.5e+40:
		tmp = (t_4 + t_5) + (t_2 + (1.0 / (math.sqrt(z) + t_6)))
	else:
		tmp = ((1.0 + (x + ((math.sqrt(x) + t_3) * t_5))) / (math.sqrt(x) + (t_4 + t_3))) + (t_2 + (t_6 - math.sqrt(z)))
	return tmp
x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	t_1 = Float64(sqrt(Float64(y + 1.0)) + sqrt(y))
	t_2 = Float64(sqrt(Float64(1.0 + t)) - sqrt(t))
	t_3 = Float64(-1.0 / t_1)
	t_4 = sqrt(Float64(x + 1.0))
	t_5 = Float64(Float64(1.0 / t_1) - sqrt(x))
	t_6 = sqrt(Float64(1.0 + z))
	tmp = 0.0
	if (y <= 5.5e+40)
		tmp = Float64(Float64(t_4 + t_5) + Float64(t_2 + Float64(1.0 / Float64(sqrt(z) + t_6))));
	else
		tmp = Float64(Float64(Float64(1.0 + Float64(x + Float64(Float64(sqrt(x) + t_3) * t_5))) / Float64(sqrt(x) + Float64(t_4 + t_3))) + Float64(t_2 + Float64(t_6 - sqrt(z))));
	end
	return tmp
end
x, y, z, t = num2cell(sort([x, y, z, t])){:}
function tmp_2 = code(x, y, z, t)
	t_1 = sqrt((y + 1.0)) + sqrt(y);
	t_2 = sqrt((1.0 + t)) - sqrt(t);
	t_3 = -1.0 / t_1;
	t_4 = sqrt((x + 1.0));
	t_5 = (1.0 / t_1) - sqrt(x);
	t_6 = sqrt((1.0 + z));
	tmp = 0.0;
	if (y <= 5.5e+40)
		tmp = (t_4 + t_5) + (t_2 + (1.0 / (sqrt(z) + t_6)));
	else
		tmp = ((1.0 + (x + ((sqrt(x) + t_3) * t_5))) / (sqrt(x) + (t_4 + t_3))) + (t_2 + (t_6 - sqrt(z)));
	end
	tmp_2 = tmp;
end
NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(-1.0 / t$95$1), $MachinePrecision]}, Block[{t$95$4 = N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$5 = N[(N[(1.0 / t$95$1), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$6 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[y, 5.5e+40], N[(N[(t$95$4 + t$95$5), $MachinePrecision] + N[(t$95$2 + N[(1.0 / N[(N[Sqrt[z], $MachinePrecision] + t$95$6), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[(1.0 + N[(x + N[(N[(N[Sqrt[x], $MachinePrecision] + t$95$3), $MachinePrecision] * t$95$5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[Sqrt[x], $MachinePrecision] + N[(t$95$4 + t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(t$95$2 + N[(t$95$6 - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]]]]
\begin{array}{l}
[x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
\\
\begin{array}{l}
t_1 := \sqrt{y + 1} + \sqrt{y}\\
t_2 := \sqrt{1 + t} - \sqrt{t}\\
t_3 := \frac{-1}{t_1}\\
t_4 := \sqrt{x + 1}\\
t_5 := \frac{1}{t_1} - \sqrt{x}\\
t_6 := \sqrt{1 + z}\\
\mathbf{if}\;y \leq 5.5 \cdot 10^{+40}:\\
\;\;\;\;\left(t_4 + t_5\right) + \left(t_2 + \frac{1}{\sqrt{z} + t_6}\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{1 + \left(x + \left(\sqrt{x} + t_3\right) \cdot t_5\right)}{\sqrt{x} + \left(t_4 + t_3\right)} + \left(t_2 + \left(t_6 - \sqrt{z}\right)\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if y < 5.49999999999999974e40

    1. Initial program 95.2%

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Step-by-step derivation
      1. associate-+l+95.2%

        \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
      2. associate-+l-66.0%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      3. +-commutative66.0%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      4. sub-neg66.0%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      5. sub-neg66.0%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      6. +-commutative66.0%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      7. +-commutative66.0%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
    3. Simplified66.0%

      \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
    4. Step-by-step derivation
      1. flip--66.0%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt65.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. add-sqr-sqrt66.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    5. Applied egg-rr66.6%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    6. Step-by-step derivation
      1. associate--l+66.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. +-inverses66.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. metadata-eval66.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    7. Simplified66.8%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    8. Step-by-step derivation
      1. flip--66.9%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt56.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(1 + z\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. +-commutative56.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(z + 1\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      4. add-sqr-sqrt67.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - \color{blue}{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      5. +-commutative67.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - z}{\sqrt{\color{blue}{z + 1}} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    9. Applied egg-rr67.3%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\left(z + 1\right) - z}{\sqrt{z + 1} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    10. Taylor expanded in z around 0 67.8%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{1}}{\sqrt{z + 1} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]

    if 5.49999999999999974e40 < y

    1. Initial program 86.4%

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Step-by-step derivation
      1. associate-+l+86.4%

        \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
      2. associate-+l-86.4%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      3. +-commutative86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      4. sub-neg86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      5. sub-neg86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      6. +-commutative86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      7. +-commutative86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
    3. Simplified86.4%

      \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
    4. Step-by-step derivation
      1. flip--86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt58.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. add-sqr-sqrt86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    5. Applied egg-rr86.4%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    6. Step-by-step derivation
      1. associate--l+86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. +-inverses86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. metadata-eval86.4%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    7. Simplified86.4%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    8. Step-by-step derivation
      1. flip--86.4%

        \[\leadsto \color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right) \cdot \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)}{\sqrt{x + 1} + \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt70.1%

        \[\leadsto \frac{\color{blue}{\left(x + 1\right)} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right) \cdot \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)}{\sqrt{x + 1} + \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    9. Applied egg-rr70.1%

      \[\leadsto \color{blue}{\frac{\left(x + 1\right) - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right) \cdot \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)}{\sqrt{x + 1} + \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    10. Step-by-step derivation
      1. Simplified70.2%

        \[\leadsto \color{blue}{\frac{1 + \left(x - \left(\sqrt{x} + \frac{-1}{\sqrt{1 + y} + \sqrt{y}}\right) \cdot \left(\sqrt{x} + \frac{-1}{\sqrt{1 + y} + \sqrt{y}}\right)\right)}{\sqrt{x} + \left(\sqrt{1 + x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    11. Recombined 2 regimes into one program.
    12. Final simplification68.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq 5.5 \cdot 10^{+40}:\\ \;\;\;\;\left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 + \left(x + \left(\sqrt{x} + \frac{-1}{\sqrt{y + 1} + \sqrt{y}}\right) \cdot \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right)}{\sqrt{x} + \left(\sqrt{x + 1} + \frac{-1}{\sqrt{y + 1} + \sqrt{y}}\right)} + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right)\\ \end{array} \]

    Alternative 2: 94.3% accurate, 1.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right) \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (+
      (+ (sqrt (+ x 1.0)) (- (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y))) (sqrt x)))
      (+ (- (sqrt (+ 1.0 t)) (sqrt t)) (/ 1.0 (+ (sqrt z) (sqrt (+ 1.0 z)))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	return (sqrt((x + 1.0)) + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) - sqrt(x))) + ((sqrt((1.0 + t)) - sqrt(t)) + (1.0 / (sqrt(z) + sqrt((1.0 + z)))));
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        code = (sqrt((x + 1.0d0)) + ((1.0d0 / (sqrt((y + 1.0d0)) + sqrt(y))) - sqrt(x))) + ((sqrt((1.0d0 + t)) - sqrt(t)) + (1.0d0 / (sqrt(z) + sqrt((1.0d0 + z)))))
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	return (Math.sqrt((x + 1.0)) + ((1.0 / (Math.sqrt((y + 1.0)) + Math.sqrt(y))) - Math.sqrt(x))) + ((Math.sqrt((1.0 + t)) - Math.sqrt(t)) + (1.0 / (Math.sqrt(z) + Math.sqrt((1.0 + z)))));
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	return (math.sqrt((x + 1.0)) + ((1.0 / (math.sqrt((y + 1.0)) + math.sqrt(y))) - math.sqrt(x))) + ((math.sqrt((1.0 + t)) - math.sqrt(t)) + (1.0 / (math.sqrt(z) + math.sqrt((1.0 + z)))))
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	return Float64(Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(1.0 / Float64(sqrt(Float64(y + 1.0)) + sqrt(y))) - sqrt(x))) + Float64(Float64(sqrt(Float64(1.0 + t)) - sqrt(t)) + Float64(1.0 / Float64(sqrt(z) + sqrt(Float64(1.0 + z))))))
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp = code(x, y, z, t)
    	tmp = (sqrt((x + 1.0)) + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) - sqrt(x))) + ((sqrt((1.0 + t)) - sqrt(t)) + (1.0 / (sqrt(z) + sqrt((1.0 + z)))));
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(1.0 / N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision] + N[(1.0 / N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)
    \end{array}
    
    Derivation
    1. Initial program 91.6%

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Step-by-step derivation
      1. associate-+l+91.6%

        \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
      2. associate-+l-74.3%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      3. +-commutative74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      4. sub-neg74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      5. sub-neg74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      6. +-commutative74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      7. +-commutative74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
    3. Simplified74.3%

      \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
    4. Step-by-step derivation
      1. flip--74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt62.9%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. add-sqr-sqrt74.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    5. Applied egg-rr74.7%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    6. Step-by-step derivation
      1. associate--l+74.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. +-inverses74.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. metadata-eval74.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    7. Simplified74.8%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    8. Step-by-step derivation
      1. flip--75.1%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt61.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(1 + z\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. +-commutative61.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(z + 1\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      4. add-sqr-sqrt75.5%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - \color{blue}{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      5. +-commutative75.5%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - z}{\sqrt{\color{blue}{z + 1}} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    9. Applied egg-rr75.5%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\left(z + 1\right) - z}{\sqrt{z + 1} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    10. Taylor expanded in z around 0 77.3%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{1}}{\sqrt{z + 1} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    11. Final simplification77.3%

      \[\leadsto \left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right) \]

    Alternative 3: 94.3% accurate, 1.3× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{1 + z}\\ \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \frac{1}{\sqrt{z} + t_1}\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (sqrt (+ 1.0 z))))
       (if (<= t 2.5e+14)
         (+ 2.0 (+ t_1 (- (sqrt (+ 1.0 t)) (+ (sqrt z) (sqrt t)))))
         (+
          (+ (sqrt (+ x 1.0)) (- (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y))) (sqrt x)))
          (/ 1.0 (+ (sqrt z) t_1))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	} else {
    		tmp = (sqrt((x + 1.0)) + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) - sqrt(x))) + (1.0 / (sqrt(z) + t_1));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: tmp
        t_1 = sqrt((1.0d0 + z))
        if (t <= 2.5d+14) then
            tmp = 2.0d0 + (t_1 + (sqrt((1.0d0 + t)) - (sqrt(z) + sqrt(t))))
        else
            tmp = (sqrt((x + 1.0d0)) + ((1.0d0 / (sqrt((y + 1.0d0)) + sqrt(y))) - sqrt(x))) + (1.0d0 / (sqrt(z) + t_1))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = 2.0 + (t_1 + (Math.sqrt((1.0 + t)) - (Math.sqrt(z) + Math.sqrt(t))));
    	} else {
    		tmp = (Math.sqrt((x + 1.0)) + ((1.0 / (Math.sqrt((y + 1.0)) + Math.sqrt(y))) - Math.sqrt(x))) + (1.0 / (Math.sqrt(z) + t_1));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((1.0 + z))
    	tmp = 0
    	if t <= 2.5e+14:
    		tmp = 2.0 + (t_1 + (math.sqrt((1.0 + t)) - (math.sqrt(z) + math.sqrt(t))))
    	else:
    		tmp = (math.sqrt((x + 1.0)) + ((1.0 / (math.sqrt((y + 1.0)) + math.sqrt(y))) - math.sqrt(x))) + (1.0 / (math.sqrt(z) + t_1))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = sqrt(Float64(1.0 + z))
    	tmp = 0.0
    	if (t <= 2.5e+14)
    		tmp = Float64(2.0 + Float64(t_1 + Float64(sqrt(Float64(1.0 + t)) - Float64(sqrt(z) + sqrt(t)))));
    	else
    		tmp = Float64(Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(1.0 / Float64(sqrt(Float64(y + 1.0)) + sqrt(y))) - sqrt(x))) + Float64(1.0 / Float64(sqrt(z) + t_1)));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((1.0 + z));
    	tmp = 0.0;
    	if (t <= 2.5e+14)
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	else
    		tmp = (sqrt((x + 1.0)) + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) - sqrt(x))) + (1.0 / (sqrt(z) + t_1));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[t, 2.5e+14], N[(2.0 + N[(t$95$1 + N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(1.0 / N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(1.0 / N[(N[Sqrt[z], $MachinePrecision] + t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{1 + z}\\
    \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\
    \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \frac{1}{\sqrt{z} + t_1}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if t < 2.5e14

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. sub-neg96.2%

          \[\leadsto \left(\color{blue}{\left(\sqrt{x + 1} + \left(-\sqrt{x}\right)\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+l+81.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l+56.4%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.4%

          \[\leadsto \sqrt{x + 1} + \color{blue}{\left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} \]
        6. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\color{blue}{\left(0 - \sqrt{x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right) \]
        7. associate-+l-56.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(0 - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
        8. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(-\left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
      3. Simplified38.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{y} + \left(\sqrt{x} - \sqrt{1 + y}\right)\right)\right)} \]
      4. Taylor expanded in y around 0 35.3%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \color{blue}{\left(\sqrt{x} - 1\right)}\right) \]
      5. Taylor expanded in x around 0 25.9%

        \[\leadsto \color{blue}{\left(2 + \left(\sqrt{1 + z} + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \sqrt{t}\right)} \]
      6. Step-by-step derivation
        1. associate--l+45.3%

          \[\leadsto \color{blue}{2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \left(\sqrt{z} + \sqrt{t}\right)\right)} \]
        2. +-commutative45.3%

          \[\leadsto 2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \color{blue}{\left(\sqrt{t} + \sqrt{z}\right)}\right) \]
        3. associate--l+45.3%

          \[\leadsto 2 + \color{blue}{\left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{t} + \sqrt{z}\right)\right)\right)} \]
        4. +-commutative45.3%

          \[\leadsto 2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \color{blue}{\left(\sqrt{z} + \sqrt{t}\right)}\right)\right) \]
      7. Simplified45.3%

        \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)} \]

      if 2.5e14 < t

      1. Initial program 86.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. associate-+l-65.5%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. +-commutative65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. sub-neg65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        5. sub-neg65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        6. +-commutative65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        7. +-commutative65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
      3. Simplified65.5%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
      4. Step-by-step derivation
        1. flip--65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. add-sqr-sqrt55.9%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. add-sqr-sqrt65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      5. Applied egg-rr65.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      6. Step-by-step derivation
        1. associate--l+65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. +-inverses65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. metadata-eval65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      7. Simplified65.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      8. Step-by-step derivation
        1. flip--66.0%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. add-sqr-sqrt56.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(1 + z\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. +-commutative56.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(z + 1\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        4. add-sqr-sqrt66.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - \color{blue}{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        5. +-commutative66.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - z}{\sqrt{\color{blue}{z + 1}} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      9. Applied egg-rr66.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\left(z + 1\right) - z}{\sqrt{z + 1} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      10. Taylor expanded in z around 0 70.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{1}}{\sqrt{z + 1} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      11. Taylor expanded in t around inf 70.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \color{blue}{\frac{1}{\sqrt{z} + \sqrt{1 + z}}} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification56.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} - \sqrt{x}\right)\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\\ \end{array} \]

    Alternative 4: 94.4% accurate, 1.3× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{1 + z}\\ \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\frac{1}{\sqrt{z} + t_1} + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (sqrt (+ 1.0 z))))
       (if (<= t 2.5e+14)
         (+ 2.0 (+ t_1 (- (sqrt (+ 1.0 t)) (+ (sqrt z) (sqrt t)))))
         (+
          (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))
          (+ (/ 1.0 (+ (sqrt z) t_1)) (- (sqrt (+ x 1.0)) (sqrt x)))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	} else {
    		tmp = (1.0 / (sqrt((y + 1.0)) + sqrt(y))) + ((1.0 / (sqrt(z) + t_1)) + (sqrt((x + 1.0)) - sqrt(x)));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: tmp
        t_1 = sqrt((1.0d0 + z))
        if (t <= 2.5d+14) then
            tmp = 2.0d0 + (t_1 + (sqrt((1.0d0 + t)) - (sqrt(z) + sqrt(t))))
        else
            tmp = (1.0d0 / (sqrt((y + 1.0d0)) + sqrt(y))) + ((1.0d0 / (sqrt(z) + t_1)) + (sqrt((x + 1.0d0)) - sqrt(x)))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = 2.0 + (t_1 + (Math.sqrt((1.0 + t)) - (Math.sqrt(z) + Math.sqrt(t))));
    	} else {
    		tmp = (1.0 / (Math.sqrt((y + 1.0)) + Math.sqrt(y))) + ((1.0 / (Math.sqrt(z) + t_1)) + (Math.sqrt((x + 1.0)) - Math.sqrt(x)));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((1.0 + z))
    	tmp = 0
    	if t <= 2.5e+14:
    		tmp = 2.0 + (t_1 + (math.sqrt((1.0 + t)) - (math.sqrt(z) + math.sqrt(t))))
    	else:
    		tmp = (1.0 / (math.sqrt((y + 1.0)) + math.sqrt(y))) + ((1.0 / (math.sqrt(z) + t_1)) + (math.sqrt((x + 1.0)) - math.sqrt(x)))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = sqrt(Float64(1.0 + z))
    	tmp = 0.0
    	if (t <= 2.5e+14)
    		tmp = Float64(2.0 + Float64(t_1 + Float64(sqrt(Float64(1.0 + t)) - Float64(sqrt(z) + sqrt(t)))));
    	else
    		tmp = Float64(Float64(1.0 / Float64(sqrt(Float64(y + 1.0)) + sqrt(y))) + Float64(Float64(1.0 / Float64(sqrt(z) + t_1)) + Float64(sqrt(Float64(x + 1.0)) - sqrt(x))));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((1.0 + z));
    	tmp = 0.0;
    	if (t <= 2.5e+14)
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	else
    		tmp = (1.0 / (sqrt((y + 1.0)) + sqrt(y))) + ((1.0 / (sqrt(z) + t_1)) + (sqrt((x + 1.0)) - sqrt(x)));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[t, 2.5e+14], N[(2.0 + N[(t$95$1 + N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(1.0 / N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(1.0 / N[(N[Sqrt[z], $MachinePrecision] + t$95$1), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{1 + z}\\
    \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\
    \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\frac{1}{\sqrt{z} + t_1} + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if t < 2.5e14

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. sub-neg96.2%

          \[\leadsto \left(\color{blue}{\left(\sqrt{x + 1} + \left(-\sqrt{x}\right)\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+l+81.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l+56.4%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.4%

          \[\leadsto \sqrt{x + 1} + \color{blue}{\left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} \]
        6. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\color{blue}{\left(0 - \sqrt{x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right) \]
        7. associate-+l-56.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(0 - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
        8. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(-\left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
      3. Simplified38.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{y} + \left(\sqrt{x} - \sqrt{1 + y}\right)\right)\right)} \]
      4. Taylor expanded in y around 0 35.3%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \color{blue}{\left(\sqrt{x} - 1\right)}\right) \]
      5. Taylor expanded in x around 0 25.9%

        \[\leadsto \color{blue}{\left(2 + \left(\sqrt{1 + z} + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \sqrt{t}\right)} \]
      6. Step-by-step derivation
        1. associate--l+45.3%

          \[\leadsto \color{blue}{2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \left(\sqrt{z} + \sqrt{t}\right)\right)} \]
        2. +-commutative45.3%

          \[\leadsto 2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \color{blue}{\left(\sqrt{t} + \sqrt{z}\right)}\right) \]
        3. associate--l+45.3%

          \[\leadsto 2 + \color{blue}{\left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{t} + \sqrt{z}\right)\right)\right)} \]
        4. +-commutative45.3%

          \[\leadsto 2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \color{blue}{\left(\sqrt{z} + \sqrt{t}\right)}\right)\right) \]
      7. Simplified45.3%

        \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)} \]

      if 2.5e14 < t

      1. Initial program 86.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. associate-+l-65.5%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. +-commutative65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. sub-neg65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        5. sub-neg65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        6. +-commutative65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        7. +-commutative65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
      3. Simplified65.5%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
      4. Step-by-step derivation
        1. flip--65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. add-sqr-sqrt55.9%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. add-sqr-sqrt65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      5. Applied egg-rr65.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      6. Step-by-step derivation
        1. associate--l+65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. +-inverses65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. metadata-eval65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      7. Simplified65.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      8. Step-by-step derivation
        1. flip--66.0%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. add-sqr-sqrt56.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(1 + z\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. +-commutative56.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(z + 1\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        4. add-sqr-sqrt66.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - \color{blue}{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        5. +-commutative66.8%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - z}{\sqrt{\color{blue}{z + 1}} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      9. Applied egg-rr66.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\left(z + 1\right) - z}{\sqrt{z + 1} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      10. Taylor expanded in z around 0 70.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{1}}{\sqrt{z + 1} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      11. Taylor expanded in t around inf 54.0%

        \[\leadsto \color{blue}{\left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\sqrt{1 + x} + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\right) - \sqrt{x}} \]
      12. Step-by-step derivation
        1. associate--l+66.3%

          \[\leadsto \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\left(\sqrt{1 + x} + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right) - \sqrt{x}\right)} \]
        2. +-commutative66.3%

          \[\leadsto \frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\color{blue}{\left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \sqrt{1 + x}\right)} - \sqrt{x}\right) \]
        3. +-commutative66.3%

          \[\leadsto \frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \sqrt{\color{blue}{x + 1}}\right) - \sqrt{x}\right) \]
        4. associate--l+93.8%

          \[\leadsto \frac{1}{\sqrt{1 + y} + \sqrt{y}} + \color{blue}{\left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} \]
        5. +-commutative93.8%

          \[\leadsto \frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \left(\sqrt{\color{blue}{1 + x}} - \sqrt{x}\right)\right) \]
      13. Simplified93.8%

        \[\leadsto \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \left(\sqrt{1 + x} - \sqrt{x}\right)\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification67.5%

      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)\\ \end{array} \]

    Alternative 5: 92.7% accurate, 1.3× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ 1 + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\right) \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (+
      1.0
      (+
       (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))
       (+ (- (sqrt (+ 1.0 t)) (sqrt t)) (/ 1.0 (+ (sqrt z) (sqrt (+ 1.0 z))))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	return 1.0 + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) + ((sqrt((1.0 + t)) - sqrt(t)) + (1.0 / (sqrt(z) + sqrt((1.0 + z))))));
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        code = 1.0d0 + ((1.0d0 / (sqrt((y + 1.0d0)) + sqrt(y))) + ((sqrt((1.0d0 + t)) - sqrt(t)) + (1.0d0 / (sqrt(z) + sqrt((1.0d0 + z))))))
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	return 1.0 + ((1.0 / (Math.sqrt((y + 1.0)) + Math.sqrt(y))) + ((Math.sqrt((1.0 + t)) - Math.sqrt(t)) + (1.0 / (Math.sqrt(z) + Math.sqrt((1.0 + z))))));
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	return 1.0 + ((1.0 / (math.sqrt((y + 1.0)) + math.sqrt(y))) + ((math.sqrt((1.0 + t)) - math.sqrt(t)) + (1.0 / (math.sqrt(z) + math.sqrt((1.0 + z))))))
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	return Float64(1.0 + Float64(Float64(1.0 / Float64(sqrt(Float64(y + 1.0)) + sqrt(y))) + Float64(Float64(sqrt(Float64(1.0 + t)) - sqrt(t)) + Float64(1.0 / Float64(sqrt(z) + sqrt(Float64(1.0 + z)))))))
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp = code(x, y, z, t)
    	tmp = 1.0 + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) + ((sqrt((1.0 + t)) - sqrt(t)) + (1.0 / (sqrt(z) + sqrt((1.0 + z))))));
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := N[(1.0 + N[(N[(1.0 / N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision] + N[(1.0 / N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    1 + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\right)
    \end{array}
    
    Derivation
    1. Initial program 91.6%

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Step-by-step derivation
      1. associate-+l+91.6%

        \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
      2. associate-+l-74.3%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      3. +-commutative74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      4. sub-neg74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      5. sub-neg74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      6. +-commutative74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      7. +-commutative74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
    3. Simplified74.3%

      \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
    4. Step-by-step derivation
      1. flip--74.3%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt62.9%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. add-sqr-sqrt74.7%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    5. Applied egg-rr74.7%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    6. Step-by-step derivation
      1. associate--l+74.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. +-inverses74.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. metadata-eval74.8%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    7. Simplified74.8%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    8. Step-by-step derivation
      1. flip--75.1%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      2. add-sqr-sqrt61.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(1 + z\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      3. +-commutative61.6%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{\left(z + 1\right)} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      4. add-sqr-sqrt75.5%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - \color{blue}{z}}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      5. +-commutative75.5%

        \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\left(z + 1\right) - z}{\sqrt{\color{blue}{z + 1}} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    9. Applied egg-rr75.5%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\color{blue}{\frac{\left(z + 1\right) - z}{\sqrt{z + 1} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    10. Taylor expanded in z around 0 77.3%

      \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\frac{\color{blue}{1}}{\sqrt{z + 1} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
    11. Taylor expanded in x around 0 35.0%

      \[\leadsto \color{blue}{\left(1 + \left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\sqrt{1 + t} + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\right)\right) - \sqrt{t}} \]
    12. Step-by-step derivation
      1. associate--l+51.3%

        \[\leadsto \color{blue}{1 + \left(\left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\sqrt{1 + t} + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\right) - \sqrt{t}\right)} \]
      2. associate--l+58.1%

        \[\leadsto 1 + \color{blue}{\left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\left(\sqrt{1 + t} + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right) - \sqrt{t}\right)\right)} \]
      3. +-commutative58.1%

        \[\leadsto 1 + \left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\color{blue}{\left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \sqrt{1 + t}\right)} - \sqrt{t}\right)\right) \]
      4. associate-+r-58.6%

        \[\leadsto 1 + \left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \color{blue}{\left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)}\right) \]
    13. Simplified58.6%

      \[\leadsto \color{blue}{1 + \left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(\frac{1}{\sqrt{z} + \sqrt{1 + z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)\right)} \]
    14. Final simplification58.6%

      \[\leadsto 1 + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \frac{1}{\sqrt{z} + \sqrt{1 + z}}\right)\right) \]

    Alternative 6: 92.8% accurate, 1.3× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{1 + z}\\ \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(t_1 - \sqrt{z}\right) - \sqrt{x}\right)\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (sqrt (+ 1.0 z))))
       (if (<= t 2.5e+14)
         (+ 2.0 (+ t_1 (- (sqrt (+ 1.0 t)) (+ (sqrt z) (sqrt t)))))
         (+
          (sqrt (+ x 1.0))
          (+
           (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))
           (- (- t_1 (sqrt z)) (sqrt x)))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	} else {
    		tmp = sqrt((x + 1.0)) + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) + ((t_1 - sqrt(z)) - sqrt(x)));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: tmp
        t_1 = sqrt((1.0d0 + z))
        if (t <= 2.5d+14) then
            tmp = 2.0d0 + (t_1 + (sqrt((1.0d0 + t)) - (sqrt(z) + sqrt(t))))
        else
            tmp = sqrt((x + 1.0d0)) + ((1.0d0 / (sqrt((y + 1.0d0)) + sqrt(y))) + ((t_1 - sqrt(z)) - sqrt(x)))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = 2.0 + (t_1 + (Math.sqrt((1.0 + t)) - (Math.sqrt(z) + Math.sqrt(t))));
    	} else {
    		tmp = Math.sqrt((x + 1.0)) + ((1.0 / (Math.sqrt((y + 1.0)) + Math.sqrt(y))) + ((t_1 - Math.sqrt(z)) - Math.sqrt(x)));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((1.0 + z))
    	tmp = 0
    	if t <= 2.5e+14:
    		tmp = 2.0 + (t_1 + (math.sqrt((1.0 + t)) - (math.sqrt(z) + math.sqrt(t))))
    	else:
    		tmp = math.sqrt((x + 1.0)) + ((1.0 / (math.sqrt((y + 1.0)) + math.sqrt(y))) + ((t_1 - math.sqrt(z)) - math.sqrt(x)))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = sqrt(Float64(1.0 + z))
    	tmp = 0.0
    	if (t <= 2.5e+14)
    		tmp = Float64(2.0 + Float64(t_1 + Float64(sqrt(Float64(1.0 + t)) - Float64(sqrt(z) + sqrt(t)))));
    	else
    		tmp = Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(1.0 / Float64(sqrt(Float64(y + 1.0)) + sqrt(y))) + Float64(Float64(t_1 - sqrt(z)) - sqrt(x))));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((1.0 + z));
    	tmp = 0.0;
    	if (t <= 2.5e+14)
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	else
    		tmp = sqrt((x + 1.0)) + ((1.0 / (sqrt((y + 1.0)) + sqrt(y))) + ((t_1 - sqrt(z)) - sqrt(x)));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[t, 2.5e+14], N[(2.0 + N[(t$95$1 + N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(1.0 / N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(t$95$1 - N[Sqrt[z], $MachinePrecision]), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{1 + z}\\
    \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\
    \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(t_1 - \sqrt{z}\right) - \sqrt{x}\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if t < 2.5e14

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. sub-neg96.2%

          \[\leadsto \left(\color{blue}{\left(\sqrt{x + 1} + \left(-\sqrt{x}\right)\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+l+81.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l+56.4%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.4%

          \[\leadsto \sqrt{x + 1} + \color{blue}{\left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} \]
        6. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\color{blue}{\left(0 - \sqrt{x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right) \]
        7. associate-+l-56.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(0 - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
        8. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(-\left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
      3. Simplified38.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{y} + \left(\sqrt{x} - \sqrt{1 + y}\right)\right)\right)} \]
      4. Taylor expanded in y around 0 35.3%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \color{blue}{\left(\sqrt{x} - 1\right)}\right) \]
      5. Taylor expanded in x around 0 25.9%

        \[\leadsto \color{blue}{\left(2 + \left(\sqrt{1 + z} + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \sqrt{t}\right)} \]
      6. Step-by-step derivation
        1. associate--l+45.3%

          \[\leadsto \color{blue}{2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \left(\sqrt{z} + \sqrt{t}\right)\right)} \]
        2. +-commutative45.3%

          \[\leadsto 2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \color{blue}{\left(\sqrt{t} + \sqrt{z}\right)}\right) \]
        3. associate--l+45.3%

          \[\leadsto 2 + \color{blue}{\left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{t} + \sqrt{z}\right)\right)\right)} \]
        4. +-commutative45.3%

          \[\leadsto 2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \color{blue}{\left(\sqrt{z} + \sqrt{t}\right)}\right)\right) \]
      7. Simplified45.3%

        \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)} \]

      if 2.5e14 < t

      1. Initial program 86.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-65.5%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-53.1%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative53.1%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+53.1%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified36.4%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 50.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified53.1%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Step-by-step derivation
        1. flip--65.5%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. add-sqr-sqrt55.9%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. add-sqr-sqrt65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      8. Applied egg-rr53.3%

        \[\leadsto \sqrt{x + 1} + \left(\color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}} - \left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)\right) \]
      9. Step-by-step derivation
        1. associate--l+65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. +-inverses65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. metadata-eval65.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      10. Simplified53.3%

        \[\leadsto \sqrt{x + 1} + \left(\color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}} - \left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)\right) \]
    3. Recombined 2 regimes into one program.
    4. Final simplification49.0%

      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{x}\right)\right)\\ \end{array} \]

    Alternative 7: 92.7% accurate, 1.3× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{1 + z} - \sqrt{z}\\ t_2 := \sqrt{y + 1}\\ \mathbf{if}\;y \leq 1.4:\\ \;\;\;\;\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + t_1\right) + \left(\left(1 + t_2\right) - \sqrt{y}\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\frac{1}{t_2 + \sqrt{y}} + \left(t_1 - \sqrt{x}\right)\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (- (sqrt (+ 1.0 z)) (sqrt z))) (t_2 (sqrt (+ y 1.0))))
       (if (<= y 1.4)
         (+ (+ (- (sqrt (+ 1.0 t)) (sqrt t)) t_1) (- (+ 1.0 t_2) (sqrt y)))
         (+ (sqrt (+ x 1.0)) (+ (/ 1.0 (+ t_2 (sqrt y))) (- t_1 (sqrt x)))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((1.0 + z)) - sqrt(z);
    	double t_2 = sqrt((y + 1.0));
    	double tmp;
    	if (y <= 1.4) {
    		tmp = ((sqrt((1.0 + t)) - sqrt(t)) + t_1) + ((1.0 + t_2) - sqrt(y));
    	} else {
    		tmp = sqrt((x + 1.0)) + ((1.0 / (t_2 + sqrt(y))) + (t_1 - sqrt(x)));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: t_2
        real(8) :: tmp
        t_1 = sqrt((1.0d0 + z)) - sqrt(z)
        t_2 = sqrt((y + 1.0d0))
        if (y <= 1.4d0) then
            tmp = ((sqrt((1.0d0 + t)) - sqrt(t)) + t_1) + ((1.0d0 + t_2) - sqrt(y))
        else
            tmp = sqrt((x + 1.0d0)) + ((1.0d0 / (t_2 + sqrt(y))) + (t_1 - sqrt(x)))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((1.0 + z)) - Math.sqrt(z);
    	double t_2 = Math.sqrt((y + 1.0));
    	double tmp;
    	if (y <= 1.4) {
    		tmp = ((Math.sqrt((1.0 + t)) - Math.sqrt(t)) + t_1) + ((1.0 + t_2) - Math.sqrt(y));
    	} else {
    		tmp = Math.sqrt((x + 1.0)) + ((1.0 / (t_2 + Math.sqrt(y))) + (t_1 - Math.sqrt(x)));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((1.0 + z)) - math.sqrt(z)
    	t_2 = math.sqrt((y + 1.0))
    	tmp = 0
    	if y <= 1.4:
    		tmp = ((math.sqrt((1.0 + t)) - math.sqrt(t)) + t_1) + ((1.0 + t_2) - math.sqrt(y))
    	else:
    		tmp = math.sqrt((x + 1.0)) + ((1.0 / (t_2 + math.sqrt(y))) + (t_1 - math.sqrt(x)))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = Float64(sqrt(Float64(1.0 + z)) - sqrt(z))
    	t_2 = sqrt(Float64(y + 1.0))
    	tmp = 0.0
    	if (y <= 1.4)
    		tmp = Float64(Float64(Float64(sqrt(Float64(1.0 + t)) - sqrt(t)) + t_1) + Float64(Float64(1.0 + t_2) - sqrt(y)));
    	else
    		tmp = Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(1.0 / Float64(t_2 + sqrt(y))) + Float64(t_1 - sqrt(x))));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((1.0 + z)) - sqrt(z);
    	t_2 = sqrt((y + 1.0));
    	tmp = 0.0;
    	if (y <= 1.4)
    		tmp = ((sqrt((1.0 + t)) - sqrt(t)) + t_1) + ((1.0 + t_2) - sqrt(y));
    	else
    		tmp = sqrt((x + 1.0)) + ((1.0 / (t_2 + sqrt(y))) + (t_1 - sqrt(x)));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[y, 1.4], N[(N[(N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + N[(N[(1.0 + t$95$2), $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(1.0 / N[(t$95$2 + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(t$95$1 - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{1 + z} - \sqrt{z}\\
    t_2 := \sqrt{y + 1}\\
    \mathbf{if}\;y \leq 1.4:\\
    \;\;\;\;\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + t_1\right) + \left(\left(1 + t_2\right) - \sqrt{y}\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{x + 1} + \left(\frac{1}{t_2 + \sqrt{y}} + \left(t_1 - \sqrt{x}\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if y < 1.3999999999999999

      1. Initial program 97.5%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+97.5%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. associate-+l-64.6%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. +-commutative64.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. sub-neg64.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        5. sub-neg64.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        6. +-commutative64.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        7. +-commutative64.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right) \]
      3. Simplified64.6%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)} \]
      4. Taylor expanded in x around 0 61.4%

        \[\leadsto \color{blue}{\left(\left(1 + \sqrt{1 + y}\right) - \sqrt{y}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]

      if 1.3999999999999999 < y

      1. Initial program 85.4%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+85.4%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative85.4%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-84.7%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-50.5%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative50.5%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+50.5%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative50.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified32.8%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 28.1%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative28.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative28.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+28.2%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified28.2%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Step-by-step derivation
        1. flip--84.7%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. add-sqr-sqrt61.0%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. add-sqr-sqrt85.4%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\left(1 + y\right) - \color{blue}{y}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      8. Applied egg-rr28.4%

        \[\leadsto \sqrt{x + 1} + \left(\color{blue}{\frac{\left(1 + y\right) - y}{\sqrt{1 + y} + \sqrt{y}}} - \left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)\right) \]
      9. Step-by-step derivation
        1. associate--l+85.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1 + \left(y - y\right)}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        2. +-inverses85.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{1 + \color{blue}{0}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
        3. metadata-eval85.6%

          \[\leadsto \left(\sqrt{x + 1} - \left(\sqrt{x} - \frac{\color{blue}{1}}{\sqrt{1 + y} + \sqrt{y}}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \]
      10. Simplified28.4%

        \[\leadsto \sqrt{x + 1} + \left(\color{blue}{\frac{1}{\sqrt{1 + y} + \sqrt{y}}} - \left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)\right) \]
    3. Recombined 2 regimes into one program.
    4. Final simplification45.4%

      \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq 1.4:\\ \;\;\;\;\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) + \left(\left(1 + \sqrt{y + 1}\right) - \sqrt{y}\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\frac{1}{\sqrt{y + 1} + \sqrt{y}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{x}\right)\right)\\ \end{array} \]

    Alternative 8: 91.7% accurate, 1.3× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{1 + z}\\ \mathbf{if}\;t \leq 1.16 \cdot 10^{+15}:\\ \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\left(t_1 - \sqrt{z}\right) - \sqrt{x}\right)\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (sqrt (+ 1.0 z))))
       (if (<= t 1.16e+15)
         (+ 2.0 (+ t_1 (- (sqrt (+ 1.0 t)) (+ (sqrt z) (sqrt t)))))
         (+
          (sqrt (+ x 1.0))
          (+ (- (sqrt (+ y 1.0)) (sqrt y)) (- (- t_1 (sqrt z)) (sqrt x)))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((1.0 + z));
    	double tmp;
    	if (t <= 1.16e+15) {
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	} else {
    		tmp = sqrt((x + 1.0)) + ((sqrt((y + 1.0)) - sqrt(y)) + ((t_1 - sqrt(z)) - sqrt(x)));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: tmp
        t_1 = sqrt((1.0d0 + z))
        if (t <= 1.16d+15) then
            tmp = 2.0d0 + (t_1 + (sqrt((1.0d0 + t)) - (sqrt(z) + sqrt(t))))
        else
            tmp = sqrt((x + 1.0d0)) + ((sqrt((y + 1.0d0)) - sqrt(y)) + ((t_1 - sqrt(z)) - sqrt(x)))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((1.0 + z));
    	double tmp;
    	if (t <= 1.16e+15) {
    		tmp = 2.0 + (t_1 + (Math.sqrt((1.0 + t)) - (Math.sqrt(z) + Math.sqrt(t))));
    	} else {
    		tmp = Math.sqrt((x + 1.0)) + ((Math.sqrt((y + 1.0)) - Math.sqrt(y)) + ((t_1 - Math.sqrt(z)) - Math.sqrt(x)));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((1.0 + z))
    	tmp = 0
    	if t <= 1.16e+15:
    		tmp = 2.0 + (t_1 + (math.sqrt((1.0 + t)) - (math.sqrt(z) + math.sqrt(t))))
    	else:
    		tmp = math.sqrt((x + 1.0)) + ((math.sqrt((y + 1.0)) - math.sqrt(y)) + ((t_1 - math.sqrt(z)) - math.sqrt(x)))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = sqrt(Float64(1.0 + z))
    	tmp = 0.0
    	if (t <= 1.16e+15)
    		tmp = Float64(2.0 + Float64(t_1 + Float64(sqrt(Float64(1.0 + t)) - Float64(sqrt(z) + sqrt(t)))));
    	else
    		tmp = Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(sqrt(Float64(y + 1.0)) - sqrt(y)) + Float64(Float64(t_1 - sqrt(z)) - sqrt(x))));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((1.0 + z));
    	tmp = 0.0;
    	if (t <= 1.16e+15)
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	else
    		tmp = sqrt((x + 1.0)) + ((sqrt((y + 1.0)) - sqrt(y)) + ((t_1 - sqrt(z)) - sqrt(x)));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[t, 1.16e+15], N[(2.0 + N[(t$95$1 + N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision] + N[(N[(t$95$1 - N[Sqrt[z], $MachinePrecision]), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{1 + z}\\
    \mathbf{if}\;t \leq 1.16 \cdot 10^{+15}:\\
    \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\left(t_1 - \sqrt{z}\right) - \sqrt{x}\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if t < 1.16e15

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. sub-neg96.2%

          \[\leadsto \left(\color{blue}{\left(\sqrt{x + 1} + \left(-\sqrt{x}\right)\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+l+81.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l+56.4%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.4%

          \[\leadsto \sqrt{x + 1} + \color{blue}{\left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} \]
        6. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\color{blue}{\left(0 - \sqrt{x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right) \]
        7. associate-+l-56.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(0 - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
        8. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(-\left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
      3. Simplified38.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{y} + \left(\sqrt{x} - \sqrt{1 + y}\right)\right)\right)} \]
      4. Taylor expanded in y around 0 35.3%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \color{blue}{\left(\sqrt{x} - 1\right)}\right) \]
      5. Taylor expanded in x around 0 25.9%

        \[\leadsto \color{blue}{\left(2 + \left(\sqrt{1 + z} + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \sqrt{t}\right)} \]
      6. Step-by-step derivation
        1. associate--l+45.3%

          \[\leadsto \color{blue}{2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \left(\sqrt{z} + \sqrt{t}\right)\right)} \]
        2. +-commutative45.3%

          \[\leadsto 2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \color{blue}{\left(\sqrt{t} + \sqrt{z}\right)}\right) \]
        3. associate--l+45.3%

          \[\leadsto 2 + \color{blue}{\left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{t} + \sqrt{z}\right)\right)\right)} \]
        4. +-commutative45.3%

          \[\leadsto 2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \color{blue}{\left(\sqrt{z} + \sqrt{t}\right)}\right)\right) \]
      7. Simplified45.3%

        \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)} \]

      if 1.16e15 < t

      1. Initial program 86.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-65.5%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-53.1%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative53.1%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+53.1%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified36.4%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 50.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified53.1%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
    3. Recombined 2 regimes into one program.
    4. Final simplification48.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 1.16 \cdot 10^{+15}:\\ \;\;\;\;2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{x}\right)\right)\\ \end{array} \]

    Alternative 9: 86.2% accurate, 2.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{y + 1}\\ \mathbf{if}\;z \leq 2.5 \cdot 10^{+16}:\\ \;\;\;\;1 + \left(t_1 - \left(\left(\sqrt{y} + \sqrt{z}\right) - \sqrt{1 + z}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\left(t_1 - \sqrt{y}\right) - \sqrt{x}\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (sqrt (+ y 1.0))))
       (if (<= z 2.5e+16)
         (+ 1.0 (- t_1 (- (+ (sqrt y) (sqrt z)) (sqrt (+ 1.0 z)))))
         (+ (sqrt (+ x 1.0)) (- (- t_1 (sqrt y)) (sqrt x))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((y + 1.0));
    	double tmp;
    	if (z <= 2.5e+16) {
    		tmp = 1.0 + (t_1 - ((sqrt(y) + sqrt(z)) - sqrt((1.0 + z))));
    	} else {
    		tmp = sqrt((x + 1.0)) + ((t_1 - sqrt(y)) - sqrt(x));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: tmp
        t_1 = sqrt((y + 1.0d0))
        if (z <= 2.5d+16) then
            tmp = 1.0d0 + (t_1 - ((sqrt(y) + sqrt(z)) - sqrt((1.0d0 + z))))
        else
            tmp = sqrt((x + 1.0d0)) + ((t_1 - sqrt(y)) - sqrt(x))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((y + 1.0));
    	double tmp;
    	if (z <= 2.5e+16) {
    		tmp = 1.0 + (t_1 - ((Math.sqrt(y) + Math.sqrt(z)) - Math.sqrt((1.0 + z))));
    	} else {
    		tmp = Math.sqrt((x + 1.0)) + ((t_1 - Math.sqrt(y)) - Math.sqrt(x));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((y + 1.0))
    	tmp = 0
    	if z <= 2.5e+16:
    		tmp = 1.0 + (t_1 - ((math.sqrt(y) + math.sqrt(z)) - math.sqrt((1.0 + z))))
    	else:
    		tmp = math.sqrt((x + 1.0)) + ((t_1 - math.sqrt(y)) - math.sqrt(x))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = sqrt(Float64(y + 1.0))
    	tmp = 0.0
    	if (z <= 2.5e+16)
    		tmp = Float64(1.0 + Float64(t_1 - Float64(Float64(sqrt(y) + sqrt(z)) - sqrt(Float64(1.0 + z)))));
    	else
    		tmp = Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(t_1 - sqrt(y)) - sqrt(x)));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((y + 1.0));
    	tmp = 0.0;
    	if (z <= 2.5e+16)
    		tmp = 1.0 + (t_1 - ((sqrt(y) + sqrt(z)) - sqrt((1.0 + z))));
    	else
    		tmp = sqrt((x + 1.0)) + ((t_1 - sqrt(y)) - sqrt(x));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[z, 2.5e+16], N[(1.0 + N[(t$95$1 - N[(N[(N[Sqrt[y], $MachinePrecision] + N[Sqrt[z], $MachinePrecision]), $MachinePrecision] - N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(t$95$1 - N[Sqrt[y], $MachinePrecision]), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{y + 1}\\
    \mathbf{if}\;z \leq 2.5 \cdot 10^{+16}:\\
    \;\;\;\;1 + \left(t_1 - \left(\left(\sqrt{y} + \sqrt{z}\right) - \sqrt{1 + z}\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{x + 1} + \left(\left(t_1 - \sqrt{y}\right) - \sqrt{x}\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if z < 2.5e16

      1. Initial program 96.0%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.0%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative96.0%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-76.1%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-56.6%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.6%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+56.6%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative56.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified52.6%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 33.5%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative33.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative33.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+33.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified33.5%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around 0 35.4%

        \[\leadsto \color{blue}{\left(1 + \left(\sqrt{1 + z} + \sqrt{1 + y}\right)\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Step-by-step derivation
        1. associate--l+46.9%

          \[\leadsto \color{blue}{1 + \left(\left(\sqrt{1 + z} + \sqrt{1 + y}\right) - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
        2. +-commutative46.9%

          \[\leadsto 1 + \left(\color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right)} - \left(\sqrt{z} + \sqrt{y}\right)\right) \]
        3. associate--l+46.9%

          \[\leadsto 1 + \color{blue}{\left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{z} + \sqrt{y}\right)\right)\right)} \]
        4. +-commutative46.9%

          \[\leadsto 1 + \left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right)\right) \]
      9. Simplified46.9%

        \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)\right)} \]

      if 2.5e16 < z

      1. Initial program 86.1%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.1%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative86.1%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-72.1%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-52.8%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative52.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+52.8%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative52.8%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified18.8%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 26.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+28.7%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified28.7%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in z around inf 28.7%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\sqrt{x}}\right) \]
    3. Recombined 2 regimes into one program.
    4. Final simplification38.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq 2.5 \cdot 10^{+16}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\left(\sqrt{y} + \sqrt{z}\right) - \sqrt{1 + z}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \sqrt{x}\right)\\ \end{array} \]

    Alternative 10: 90.2% accurate, 2.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;\left(\sqrt{1 + t} + 3\right) - \left(\sqrt{z} + \sqrt{t}\right)\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\sqrt{y} + \left(\sqrt{z} - \sqrt{1 + z}\right)\right)\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (if (<= t 2.5e+14)
       (- (+ (sqrt (+ 1.0 t)) 3.0) (+ (sqrt z) (sqrt t)))
       (+ 1.0 (- (sqrt (+ y 1.0)) (+ (sqrt y) (- (sqrt z) (sqrt (+ 1.0 z))))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = (sqrt((1.0 + t)) + 3.0) - (sqrt(z) + sqrt(t));
    	} else {
    		tmp = 1.0 + (sqrt((y + 1.0)) - (sqrt(y) + (sqrt(z) - sqrt((1.0 + z)))));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: tmp
        if (t <= 2.5d+14) then
            tmp = (sqrt((1.0d0 + t)) + 3.0d0) - (sqrt(z) + sqrt(t))
        else
            tmp = 1.0d0 + (sqrt((y + 1.0d0)) - (sqrt(y) + (sqrt(z) - sqrt((1.0d0 + z)))))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double tmp;
    	if (t <= 2.5e+14) {
    		tmp = (Math.sqrt((1.0 + t)) + 3.0) - (Math.sqrt(z) + Math.sqrt(t));
    	} else {
    		tmp = 1.0 + (Math.sqrt((y + 1.0)) - (Math.sqrt(y) + (Math.sqrt(z) - Math.sqrt((1.0 + z)))));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	tmp = 0
    	if t <= 2.5e+14:
    		tmp = (math.sqrt((1.0 + t)) + 3.0) - (math.sqrt(z) + math.sqrt(t))
    	else:
    		tmp = 1.0 + (math.sqrt((y + 1.0)) - (math.sqrt(y) + (math.sqrt(z) - math.sqrt((1.0 + z)))))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	tmp = 0.0
    	if (t <= 2.5e+14)
    		tmp = Float64(Float64(sqrt(Float64(1.0 + t)) + 3.0) - Float64(sqrt(z) + sqrt(t)));
    	else
    		tmp = Float64(1.0 + Float64(sqrt(Float64(y + 1.0)) - Float64(sqrt(y) + Float64(sqrt(z) - sqrt(Float64(1.0 + z))))));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	tmp = 0.0;
    	if (t <= 2.5e+14)
    		tmp = (sqrt((1.0 + t)) + 3.0) - (sqrt(z) + sqrt(t));
    	else
    		tmp = 1.0 + (sqrt((y + 1.0)) - (sqrt(y) + (sqrt(z) - sqrt((1.0 + z)))));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := If[LessEqual[t, 2.5e+14], N[(N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] + 3.0), $MachinePrecision] - N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1.0 + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[y], $MachinePrecision] + N[(N[Sqrt[z], $MachinePrecision] - N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\
    \;\;\;\;\left(\sqrt{1 + t} + 3\right) - \left(\sqrt{z} + \sqrt{t}\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\sqrt{y} + \left(\sqrt{z} - \sqrt{1 + z}\right)\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if t < 2.5e14

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. sub-neg96.2%

          \[\leadsto \left(\color{blue}{\left(\sqrt{x + 1} + \left(-\sqrt{x}\right)\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+l+81.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l+56.4%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.4%

          \[\leadsto \sqrt{x + 1} + \color{blue}{\left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} \]
        6. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\color{blue}{\left(0 - \sqrt{x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right) \]
        7. associate-+l-56.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(0 - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
        8. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(-\left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
      3. Simplified38.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{y} + \left(\sqrt{x} - \sqrt{1 + y}\right)\right)\right)} \]
      4. Taylor expanded in y around 0 35.3%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \color{blue}{\left(\sqrt{x} - 1\right)}\right) \]
      5. Taylor expanded in z around 0 21.8%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\color{blue}{\left(1 + \sqrt{1 + t}\right)} - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{x} - 1\right)\right) \]
      6. Taylor expanded in x around 0 23.6%

        \[\leadsto \color{blue}{\left(3 + \sqrt{1 + t}\right) - \left(\sqrt{z} + \sqrt{t}\right)} \]

      if 2.5e14 < t

      1. Initial program 86.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-65.5%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-53.1%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative53.1%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+53.1%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified36.4%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 50.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified53.1%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around 0 25.0%

        \[\leadsto \color{blue}{\left(1 + \left(\sqrt{1 + z} + \sqrt{1 + y}\right)\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Step-by-step derivation
        1. associate--l+53.4%

          \[\leadsto \color{blue}{1 + \left(\left(\sqrt{1 + z} + \sqrt{1 + y}\right) - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
        2. +-commutative53.4%

          \[\leadsto 1 + \left(\color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right)} - \left(\sqrt{z} + \sqrt{y}\right)\right) \]
        3. +-commutative53.4%

          \[\leadsto 1 + \left(\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right) \]
      9. Applied egg-rr53.4%

        \[\leadsto \color{blue}{1 + \left(\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \left(\sqrt{y} + \sqrt{z}\right)\right)} \]
      10. Step-by-step derivation
        1. associate--l+49.8%

          \[\leadsto 1 + \color{blue}{\left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)\right)} \]
        2. +-commutative49.8%

          \[\leadsto 1 + \left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{z} + \sqrt{y}\right)}\right)\right) \]
        3. associate--r+54.8%

          \[\leadsto 1 + \left(\sqrt{1 + y} + \color{blue}{\left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{y}\right)}\right) \]
      11. Simplified54.8%

        \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{y}\right)\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification37.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 2.5 \cdot 10^{+14}:\\ \;\;\;\;\left(\sqrt{1 + t} + 3\right) - \left(\sqrt{z} + \sqrt{t}\right)\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\sqrt{y} + \left(\sqrt{z} - \sqrt{1 + z}\right)\right)\right)\\ \end{array} \]

    Alternative 11: 90.4% accurate, 2.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{1 + z}\\ \mathbf{if}\;t \leq 2.55 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\sqrt{y} + \left(\sqrt{z} - t_1\right)\right)\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (let* ((t_1 (sqrt (+ 1.0 z))))
       (if (<= t 2.55e+14)
         (+ 2.0 (+ t_1 (- (sqrt (+ 1.0 t)) (+ (sqrt z) (sqrt t)))))
         (+ 1.0 (- (sqrt (+ y 1.0)) (+ (sqrt y) (- (sqrt z) t_1)))))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double t_1 = sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.55e+14) {
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	} else {
    		tmp = 1.0 + (sqrt((y + 1.0)) - (sqrt(y) + (sqrt(z) - t_1)));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: t_1
        real(8) :: tmp
        t_1 = sqrt((1.0d0 + z))
        if (t <= 2.55d+14) then
            tmp = 2.0d0 + (t_1 + (sqrt((1.0d0 + t)) - (sqrt(z) + sqrt(t))))
        else
            tmp = 1.0d0 + (sqrt((y + 1.0d0)) - (sqrt(y) + (sqrt(z) - t_1)))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double t_1 = Math.sqrt((1.0 + z));
    	double tmp;
    	if (t <= 2.55e+14) {
    		tmp = 2.0 + (t_1 + (Math.sqrt((1.0 + t)) - (Math.sqrt(z) + Math.sqrt(t))));
    	} else {
    		tmp = 1.0 + (Math.sqrt((y + 1.0)) - (Math.sqrt(y) + (Math.sqrt(z) - t_1)));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	t_1 = math.sqrt((1.0 + z))
    	tmp = 0
    	if t <= 2.55e+14:
    		tmp = 2.0 + (t_1 + (math.sqrt((1.0 + t)) - (math.sqrt(z) + math.sqrt(t))))
    	else:
    		tmp = 1.0 + (math.sqrt((y + 1.0)) - (math.sqrt(y) + (math.sqrt(z) - t_1)))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	t_1 = sqrt(Float64(1.0 + z))
    	tmp = 0.0
    	if (t <= 2.55e+14)
    		tmp = Float64(2.0 + Float64(t_1 + Float64(sqrt(Float64(1.0 + t)) - Float64(sqrt(z) + sqrt(t)))));
    	else
    		tmp = Float64(1.0 + Float64(sqrt(Float64(y + 1.0)) - Float64(sqrt(y) + Float64(sqrt(z) - t_1))));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	t_1 = sqrt((1.0 + z));
    	tmp = 0.0;
    	if (t <= 2.55e+14)
    		tmp = 2.0 + (t_1 + (sqrt((1.0 + t)) - (sqrt(z) + sqrt(t))));
    	else
    		tmp = 1.0 + (sqrt((y + 1.0)) - (sqrt(y) + (sqrt(z) - t_1)));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := Block[{t$95$1 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[t, 2.55e+14], N[(2.0 + N[(t$95$1 + N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[z], $MachinePrecision] + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1.0 + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[(N[Sqrt[y], $MachinePrecision] + N[(N[Sqrt[z], $MachinePrecision] - t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    t_1 := \sqrt{1 + z}\\
    \mathbf{if}\;t \leq 2.55 \cdot 10^{+14}:\\
    \;\;\;\;2 + \left(t_1 + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\sqrt{y} + \left(\sqrt{z} - t_1\right)\right)\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if t < 2.55e14

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. sub-neg96.2%

          \[\leadsto \left(\color{blue}{\left(\sqrt{x + 1} + \left(-\sqrt{x}\right)\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+l+81.8%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l+56.4%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.4%

          \[\leadsto \sqrt{x + 1} + \color{blue}{\left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\left(-\sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} \]
        6. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \left(\color{blue}{\left(0 - \sqrt{x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right) \]
        7. associate-+l-56.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(0 - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
        8. neg-sub056.4%

          \[\leadsto \sqrt{x + 1} + \left(\left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) + \color{blue}{\left(-\left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)}\right) \]
      3. Simplified38.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \left(\sqrt{y} + \left(\sqrt{x} - \sqrt{1 + y}\right)\right)\right)} \]
      4. Taylor expanded in y around 0 35.3%

        \[\leadsto \sqrt{x + 1} + \left(\left(\left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \sqrt{t}\right) - \sqrt{z}\right) - \color{blue}{\left(\sqrt{x} - 1\right)}\right) \]
      5. Taylor expanded in x around 0 25.9%

        \[\leadsto \color{blue}{\left(2 + \left(\sqrt{1 + z} + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \sqrt{t}\right)} \]
      6. Step-by-step derivation
        1. associate--l+45.3%

          \[\leadsto \color{blue}{2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \left(\sqrt{z} + \sqrt{t}\right)\right)} \]
        2. +-commutative45.3%

          \[\leadsto 2 + \left(\left(\sqrt{1 + z} + \sqrt{1 + t}\right) - \color{blue}{\left(\sqrt{t} + \sqrt{z}\right)}\right) \]
        3. associate--l+45.3%

          \[\leadsto 2 + \color{blue}{\left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{t} + \sqrt{z}\right)\right)\right)} \]
        4. +-commutative45.3%

          \[\leadsto 2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \color{blue}{\left(\sqrt{z} + \sqrt{t}\right)}\right)\right) \]
      7. Simplified45.3%

        \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)} \]

      if 2.55e14 < t

      1. Initial program 86.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative86.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-65.5%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-53.1%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative53.1%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+53.1%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified36.4%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 50.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative50.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+53.1%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified53.1%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around 0 25.0%

        \[\leadsto \color{blue}{\left(1 + \left(\sqrt{1 + z} + \sqrt{1 + y}\right)\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Step-by-step derivation
        1. associate--l+53.4%

          \[\leadsto \color{blue}{1 + \left(\left(\sqrt{1 + z} + \sqrt{1 + y}\right) - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
        2. +-commutative53.4%

          \[\leadsto 1 + \left(\color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right)} - \left(\sqrt{z} + \sqrt{y}\right)\right) \]
        3. +-commutative53.4%

          \[\leadsto 1 + \left(\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right) \]
      9. Applied egg-rr53.4%

        \[\leadsto \color{blue}{1 + \left(\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \left(\sqrt{y} + \sqrt{z}\right)\right)} \]
      10. Step-by-step derivation
        1. associate--l+49.8%

          \[\leadsto 1 + \color{blue}{\left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)\right)} \]
        2. +-commutative49.8%

          \[\leadsto 1 + \left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{z} + \sqrt{y}\right)}\right)\right) \]
        3. associate--r+54.8%

          \[\leadsto 1 + \left(\sqrt{1 + y} + \color{blue}{\left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{y}\right)}\right) \]
      11. Simplified54.8%

        \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) - \sqrt{y}\right)\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification49.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq 2.55 \cdot 10^{+14}:\\ \;\;\;\;2 + \left(\sqrt{1 + z} + \left(\sqrt{1 + t} - \left(\sqrt{z} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \left(\sqrt{y} + \left(\sqrt{z} - \sqrt{1 + z}\right)\right)\right)\\ \end{array} \]

    Alternative 12: 85.7% accurate, 2.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\ \;\;\;\;\left(\sqrt{1 + z} + 2\right) - \sqrt{z}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \sqrt{x}\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (if (<= z 1.85e+15)
       (- (+ (sqrt (+ 1.0 z)) 2.0) (sqrt z))
       (+ (sqrt (+ x 1.0)) (- (- (sqrt (+ y 1.0)) (sqrt y)) (sqrt x)))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double tmp;
    	if (z <= 1.85e+15) {
    		tmp = (sqrt((1.0 + z)) + 2.0) - sqrt(z);
    	} else {
    		tmp = sqrt((x + 1.0)) + ((sqrt((y + 1.0)) - sqrt(y)) - sqrt(x));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: tmp
        if (z <= 1.85d+15) then
            tmp = (sqrt((1.0d0 + z)) + 2.0d0) - sqrt(z)
        else
            tmp = sqrt((x + 1.0d0)) + ((sqrt((y + 1.0d0)) - sqrt(y)) - sqrt(x))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double tmp;
    	if (z <= 1.85e+15) {
    		tmp = (Math.sqrt((1.0 + z)) + 2.0) - Math.sqrt(z);
    	} else {
    		tmp = Math.sqrt((x + 1.0)) + ((Math.sqrt((y + 1.0)) - Math.sqrt(y)) - Math.sqrt(x));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	tmp = 0
    	if z <= 1.85e+15:
    		tmp = (math.sqrt((1.0 + z)) + 2.0) - math.sqrt(z)
    	else:
    		tmp = math.sqrt((x + 1.0)) + ((math.sqrt((y + 1.0)) - math.sqrt(y)) - math.sqrt(x))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	tmp = 0.0
    	if (z <= 1.85e+15)
    		tmp = Float64(Float64(sqrt(Float64(1.0 + z)) + 2.0) - sqrt(z));
    	else
    		tmp = Float64(sqrt(Float64(x + 1.0)) + Float64(Float64(sqrt(Float64(y + 1.0)) - sqrt(y)) - sqrt(x)));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	tmp = 0.0;
    	if (z <= 1.85e+15)
    		tmp = (sqrt((1.0 + z)) + 2.0) - sqrt(z);
    	else
    		tmp = sqrt((x + 1.0)) + ((sqrt((y + 1.0)) - sqrt(y)) - sqrt(x));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := If[LessEqual[z, 1.85e+15], N[(N[(N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision] + 2.0), $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision], N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] + N[(N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\
    \;\;\;\;\left(\sqrt{1 + z} + 2\right) - \sqrt{z}\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \sqrt{x}\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if z < 1.85e15

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-76.2%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-56.5%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.5%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+56.5%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative56.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified52.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 33.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified33.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around 0 35.6%

        \[\leadsto \color{blue}{\left(1 + \left(\sqrt{1 + z} + \sqrt{1 + y}\right)\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Taylor expanded in y around 0 46.5%

        \[\leadsto \color{blue}{\left(2 + \sqrt{1 + z}\right) - \sqrt{z}} \]

      if 1.85e15 < z

      1. Initial program 85.9%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+85.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative85.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-72.0%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-52.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative52.9%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+52.9%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative52.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified19.2%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 26.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+28.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified28.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in z around inf 28.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\sqrt{x}}\right) \]
    3. Recombined 2 regimes into one program.
    4. Final simplification38.5%

      \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\ \;\;\;\;\left(\sqrt{1 + z} + 2\right) - \sqrt{z}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \sqrt{x}\right)\\ \end{array} \]

    Alternative 13: 84.4% accurate, 3.9× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\ \;\;\;\;2 - \left(\sqrt{z} - \sqrt{1 + z}\right)\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \sqrt{y}\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (if (<= z 1.85e+15)
       (- 2.0 (- (sqrt z) (sqrt (+ 1.0 z))))
       (+ 1.0 (- (sqrt (+ y 1.0)) (sqrt y)))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double tmp;
    	if (z <= 1.85e+15) {
    		tmp = 2.0 - (sqrt(z) - sqrt((1.0 + z)));
    	} else {
    		tmp = 1.0 + (sqrt((y + 1.0)) - sqrt(y));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: tmp
        if (z <= 1.85d+15) then
            tmp = 2.0d0 - (sqrt(z) - sqrt((1.0d0 + z)))
        else
            tmp = 1.0d0 + (sqrt((y + 1.0d0)) - sqrt(y))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double tmp;
    	if (z <= 1.85e+15) {
    		tmp = 2.0 - (Math.sqrt(z) - Math.sqrt((1.0 + z)));
    	} else {
    		tmp = 1.0 + (Math.sqrt((y + 1.0)) - Math.sqrt(y));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	tmp = 0
    	if z <= 1.85e+15:
    		tmp = 2.0 - (math.sqrt(z) - math.sqrt((1.0 + z)))
    	else:
    		tmp = 1.0 + (math.sqrt((y + 1.0)) - math.sqrt(y))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	tmp = 0.0
    	if (z <= 1.85e+15)
    		tmp = Float64(2.0 - Float64(sqrt(z) - sqrt(Float64(1.0 + z))));
    	else
    		tmp = Float64(1.0 + Float64(sqrt(Float64(y + 1.0)) - sqrt(y)));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	tmp = 0.0;
    	if (z <= 1.85e+15)
    		tmp = 2.0 - (sqrt(z) - sqrt((1.0 + z)));
    	else
    		tmp = 1.0 + (sqrt((y + 1.0)) - sqrt(y));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := If[LessEqual[z, 1.85e+15], N[(2.0 - N[(N[Sqrt[z], $MachinePrecision] - N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1.0 + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\
    \;\;\;\;2 - \left(\sqrt{z} - \sqrt{1 + z}\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;1 + \left(\sqrt{y + 1} - \sqrt{y}\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if z < 1.85e15

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-76.2%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-56.5%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.5%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+56.5%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative56.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified52.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 33.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified33.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around 0 35.6%

        \[\leadsto \color{blue}{\left(1 + \left(\sqrt{1 + z} + \sqrt{1 + y}\right)\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Taylor expanded in y around 0 46.5%

        \[\leadsto \color{blue}{\left(2 + \sqrt{1 + z}\right) - \sqrt{z}} \]
      9. Step-by-step derivation
        1. associate--l+46.5%

          \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} - \sqrt{z}\right)} \]
      10. Simplified46.5%

        \[\leadsto \color{blue}{2 + \left(\sqrt{1 + z} - \sqrt{z}\right)} \]

      if 1.85e15 < z

      1. Initial program 85.9%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+85.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative85.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-72.0%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-52.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative52.9%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+52.9%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative52.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified19.2%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 26.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+28.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified28.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around inf 4.0%

        \[\leadsto \color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Step-by-step derivation
        1. associate--l+17.9%

          \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
        2. +-commutative17.9%

          \[\leadsto \sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right) \]
      9. Simplified17.9%

        \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)} \]
      10. Taylor expanded in z around 0 27.6%

        \[\leadsto \color{blue}{\left(1 + \sqrt{1 + y}\right) - \sqrt{y}} \]
      11. Step-by-step derivation
        1. associate--l+55.3%

          \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} - \sqrt{y}\right)} \]
      12. Simplified55.3%

        \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} - \sqrt{y}\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification50.4%

      \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\ \;\;\;\;2 - \left(\sqrt{z} - \sqrt{1 + z}\right)\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \sqrt{y}\right)\\ \end{array} \]

    Alternative 14: 84.4% accurate, 3.9× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\ \;\;\;\;\left(\sqrt{1 + z} + 2\right) - \sqrt{z}\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \sqrt{y}\right)\\ \end{array} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t)
     :precision binary64
     (if (<= z 1.85e+15)
       (- (+ (sqrt (+ 1.0 z)) 2.0) (sqrt z))
       (+ 1.0 (- (sqrt (+ y 1.0)) (sqrt y)))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	double tmp;
    	if (z <= 1.85e+15) {
    		tmp = (sqrt((1.0 + z)) + 2.0) - sqrt(z);
    	} else {
    		tmp = 1.0 + (sqrt((y + 1.0)) - sqrt(y));
    	}
    	return tmp;
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        real(8) :: tmp
        if (z <= 1.85d+15) then
            tmp = (sqrt((1.0d0 + z)) + 2.0d0) - sqrt(z)
        else
            tmp = 1.0d0 + (sqrt((y + 1.0d0)) - sqrt(y))
        end if
        code = tmp
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	double tmp;
    	if (z <= 1.85e+15) {
    		tmp = (Math.sqrt((1.0 + z)) + 2.0) - Math.sqrt(z);
    	} else {
    		tmp = 1.0 + (Math.sqrt((y + 1.0)) - Math.sqrt(y));
    	}
    	return tmp;
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	tmp = 0
    	if z <= 1.85e+15:
    		tmp = (math.sqrt((1.0 + z)) + 2.0) - math.sqrt(z)
    	else:
    		tmp = 1.0 + (math.sqrt((y + 1.0)) - math.sqrt(y))
    	return tmp
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	tmp = 0.0
    	if (z <= 1.85e+15)
    		tmp = Float64(Float64(sqrt(Float64(1.0 + z)) + 2.0) - sqrt(z));
    	else
    		tmp = Float64(1.0 + Float64(sqrt(Float64(y + 1.0)) - sqrt(y)));
    	end
    	return tmp
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp_2 = code(x, y, z, t)
    	tmp = 0.0;
    	if (z <= 1.85e+15)
    		tmp = (sqrt((1.0 + z)) + 2.0) - sqrt(z);
    	else
    		tmp = 1.0 + (sqrt((y + 1.0)) - sqrt(y));
    	end
    	tmp_2 = tmp;
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := If[LessEqual[z, 1.85e+15], N[(N[(N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision] + 2.0), $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision], N[(1.0 + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \begin{array}{l}
    \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\
    \;\;\;\;\left(\sqrt{1 + z} + 2\right) - \sqrt{z}\\
    
    \mathbf{else}:\\
    \;\;\;\;1 + \left(\sqrt{y + 1} - \sqrt{y}\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if z < 1.85e15

      1. Initial program 96.2%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative96.2%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-76.2%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-56.5%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative56.5%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+56.5%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative56.5%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified52.5%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 33.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+33.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified33.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around 0 35.6%

        \[\leadsto \color{blue}{\left(1 + \left(\sqrt{1 + z} + \sqrt{1 + y}\right)\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Taylor expanded in y around 0 46.5%

        \[\leadsto \color{blue}{\left(2 + \sqrt{1 + z}\right) - \sqrt{z}} \]

      if 1.85e15 < z

      1. Initial program 85.9%

        \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
      2. Step-by-step derivation
        1. associate-+l+85.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
        2. +-commutative85.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        3. associate-+r-72.0%

          \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
        4. associate-+l-52.9%

          \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
        5. +-commutative52.9%

          \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
        6. associate--l+52.9%

          \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
        7. +-commutative52.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
      3. Simplified19.2%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
      4. Taylor expanded in t around inf 26.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
      5. Step-by-step derivation
        1. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
        2. +-commutative26.9%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
        3. associate--l+28.6%

          \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      6. Simplified28.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
      7. Taylor expanded in x around inf 4.0%

        \[\leadsto \color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
      8. Step-by-step derivation
        1. associate--l+17.9%

          \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
        2. +-commutative17.9%

          \[\leadsto \sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right) \]
      9. Simplified17.9%

        \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)} \]
      10. Taylor expanded in z around 0 27.6%

        \[\leadsto \color{blue}{\left(1 + \sqrt{1 + y}\right) - \sqrt{y}} \]
      11. Step-by-step derivation
        1. associate--l+55.3%

          \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} - \sqrt{y}\right)} \]
      12. Simplified55.3%

        \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} - \sqrt{y}\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification50.4%

      \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq 1.85 \cdot 10^{+15}:\\ \;\;\;\;\left(\sqrt{1 + z} + 2\right) - \sqrt{z}\\ \mathbf{else}:\\ \;\;\;\;1 + \left(\sqrt{y + 1} - \sqrt{y}\right)\\ \end{array} \]

    Alternative 15: 64.0% accurate, 4.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ 1 + \left(\sqrt{y + 1} - \sqrt{y}\right) \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t) :precision binary64 (+ 1.0 (- (sqrt (+ y 1.0)) (sqrt y))))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	return 1.0 + (sqrt((y + 1.0)) - sqrt(y));
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        code = 1.0d0 + (sqrt((y + 1.0d0)) - sqrt(y))
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	return 1.0 + (Math.sqrt((y + 1.0)) - Math.sqrt(y));
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	return 1.0 + (math.sqrt((y + 1.0)) - math.sqrt(y))
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	return Float64(1.0 + Float64(sqrt(Float64(y + 1.0)) - sqrt(y)))
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp = code(x, y, z, t)
    	tmp = 1.0 + (sqrt((y + 1.0)) - sqrt(y));
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := N[(1.0 + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    1 + \left(\sqrt{y + 1} - \sqrt{y}\right)
    \end{array}
    
    Derivation
    1. Initial program 91.6%

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Step-by-step derivation
      1. associate-+l+91.6%

        \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
      2. +-commutative91.6%

        \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      3. associate-+r-74.3%

        \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      4. associate-+l-54.9%

        \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
      5. +-commutative54.9%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
      6. associate--l+54.9%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
      7. +-commutative54.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
    3. Simplified37.7%

      \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
    4. Taylor expanded in t around inf 30.6%

      \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
    5. Step-by-step derivation
      1. +-commutative30.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
      2. +-commutative30.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
      3. associate--l+31.4%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
    6. Simplified31.4%

      \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
    7. Taylor expanded in x around inf 16.3%

      \[\leadsto \color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
    8. Step-by-step derivation
      1. associate--l+22.4%

        \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
      2. +-commutative22.4%

        \[\leadsto \sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right) \]
    9. Simplified22.4%

      \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)} \]
    10. Taylor expanded in z around 0 27.0%

      \[\leadsto \color{blue}{\left(1 + \sqrt{1 + y}\right) - \sqrt{y}} \]
    11. Step-by-step derivation
      1. associate--l+45.7%

        \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} - \sqrt{y}\right)} \]
    12. Simplified45.7%

      \[\leadsto \color{blue}{1 + \left(\sqrt{1 + y} - \sqrt{y}\right)} \]
    13. Final simplification45.7%

      \[\leadsto 1 + \left(\sqrt{y + 1} - \sqrt{y}\right) \]

    Alternative 16: 13.9% accurate, 4.0× speedup?

    \[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \sqrt{y + 1} - \sqrt{y} \end{array} \]
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    (FPCore (x y z t) :precision binary64 (- (sqrt (+ y 1.0)) (sqrt y)))
    assert(x < y && y < z && z < t);
    double code(double x, double y, double z, double t) {
    	return sqrt((y + 1.0)) - sqrt(y);
    }
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    real(8) function code(x, y, z, t)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8), intent (in) :: z
        real(8), intent (in) :: t
        code = sqrt((y + 1.0d0)) - sqrt(y)
    end function
    
    assert x < y && y < z && z < t;
    public static double code(double x, double y, double z, double t) {
    	return Math.sqrt((y + 1.0)) - Math.sqrt(y);
    }
    
    [x, y, z, t] = sort([x, y, z, t])
    def code(x, y, z, t):
    	return math.sqrt((y + 1.0)) - math.sqrt(y)
    
    x, y, z, t = sort([x, y, z, t])
    function code(x, y, z, t)
    	return Float64(sqrt(Float64(y + 1.0)) - sqrt(y))
    end
    
    x, y, z, t = num2cell(sort([x, y, z, t])){:}
    function tmp = code(x, y, z, t)
    	tmp = sqrt((y + 1.0)) - sqrt(y);
    end
    
    NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
    code[x_, y_, z_, t_] := N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]
    
    \begin{array}{l}
    [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\
    \\
    \sqrt{y + 1} - \sqrt{y}
    \end{array}
    
    Derivation
    1. Initial program 91.6%

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Step-by-step derivation
      1. associate-+l+91.6%

        \[\leadsto \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)} \]
      2. +-commutative91.6%

        \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{x + 1} - \sqrt{x}\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      3. associate-+r-74.3%

        \[\leadsto \color{blue}{\left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \sqrt{x}\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right) \]
      4. associate-+l-54.9%

        \[\leadsto \color{blue}{\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \sqrt{x + 1}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)} \]
      5. +-commutative54.9%

        \[\leadsto \color{blue}{\left(\sqrt{x + 1} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right)} - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right) \]
      6. associate--l+54.9%

        \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{y + 1} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right)} \]
      7. +-commutative54.9%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right) - \left(\sqrt{x} - \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)\right)\right) \]
    3. Simplified37.7%

      \[\leadsto \color{blue}{\sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} - \sqrt{1 + z}\right) + \left(\sqrt{t} + \left(\sqrt{z} - \sqrt{1 + t}\right)\right)\right)\right)} \]
    4. Taylor expanded in t around inf 30.6%

      \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\left(\sqrt{z} + \sqrt{x}\right) - \sqrt{1 + z}\right)}\right) \]
    5. Step-by-step derivation
      1. +-commutative30.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\color{blue}{\left(\sqrt{x} + \sqrt{z}\right)} - \sqrt{1 + z}\right)\right) \]
      2. +-commutative30.6%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \left(\left(\sqrt{x} + \sqrt{z}\right) - \sqrt{\color{blue}{z + 1}}\right)\right) \]
      3. associate--l+31.4%

        \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
    6. Simplified31.4%

      \[\leadsto \sqrt{x + 1} + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) - \color{blue}{\left(\sqrt{x} + \left(\sqrt{z} - \sqrt{z + 1}\right)\right)}\right) \]
    7. Taylor expanded in x around inf 16.3%

      \[\leadsto \color{blue}{\left(\sqrt{1 + y} + \sqrt{1 + z}\right) - \left(\sqrt{z} + \sqrt{y}\right)} \]
    8. Step-by-step derivation
      1. associate--l+22.4%

        \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{z} + \sqrt{y}\right)\right)} \]
      2. +-commutative22.4%

        \[\leadsto \sqrt{1 + y} + \left(\sqrt{1 + z} - \color{blue}{\left(\sqrt{y} + \sqrt{z}\right)}\right) \]
    9. Simplified22.4%

      \[\leadsto \color{blue}{\sqrt{1 + y} + \left(\sqrt{1 + z} - \left(\sqrt{y} + \sqrt{z}\right)\right)} \]
    10. Taylor expanded in z around inf 14.4%

      \[\leadsto \color{blue}{\sqrt{1 + y} - \sqrt{y}} \]
    11. Final simplification14.4%

      \[\leadsto \sqrt{y + 1} - \sqrt{y} \]

    Developer target: 99.3% accurate, 1.0× speedup?

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

    Reproduce

    ?
    herbie shell --seed 2023229 
    (FPCore (x y z t)
      :name "Main:z from "
      :precision binary64
    
      :herbie-target
      (+ (+ (+ (/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x))) (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))) (/ 1.0 (+ (sqrt (+ z 1.0)) (sqrt z)))) (- (sqrt (+ t 1.0)) (sqrt t)))
    
      (+ (+ (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y))) (- (sqrt (+ z 1.0)) (sqrt z))) (- (sqrt (+ t 1.0)) (sqrt t))))