Main:z from

Percentage Accurate: 91.8% → 99.2%

Time: 17.9s

Alternatives: 5

Speedup: N/A×

Specification

Math

\[\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

(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))))

C

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));
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z, t)
use fmin_fmax_functions
    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

Java

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));
}

Python

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))

Julia

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

MATLAB

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

Wolfram

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]

Initial Program: 91.8% accurate, 1.0× speedup

Math

\[\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

(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))))

C

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));
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z, t)
use fmin_fmax_functions
    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

Java

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));
}

Python

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))

Julia

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

MATLAB

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

Wolfram

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]

Alternative 1: 99.2% accurate, N/A× speedup

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{z + 1} - \sqrt{z}\\ t_2 := \sqrt{t + 1} - \sqrt{t}\\ t_3 := \left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + t\_1\right) + t\_2\\ t_4 := {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\\ \mathbf{if}\;t\_3 \leq 0.0001:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, t\_4\right)\right) + t\_1\right) + t\_2\\ \mathbf{elif}\;t\_3 \leq 2.01:\\ \;\;\;\;\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, t\_4\right)\right)\right)\right) - {x}^{0.5}\right) + t\_2\\ \mathbf{else}:\\ \;\;\;\;t\_3\\ \end{array} \end{array} \]

FPCore

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 (+ z 1.0)) (sqrt z)))
        (t_2 (- (sqrt (+ t 1.0)) (sqrt t)))
        (t_3
         (+
          (+
           (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
           t_1)
          t_2))
        (t_4 (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0)))
   (if (<= t_3 0.0001)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow x 3.0) -1.0) 0.5)
        (fma 0.5 (pow (pow x -1.0) 0.5) t_4))
       t_1)
      t_2)
     (if (<= t_3 2.01)
       (+
        (-
         (+
          (pow (+ 1.0 x) 0.5)
          (fma
           -0.125
           (pow (pow (pow z 3.0) -1.0) 0.5)
           (fma
            0.0625
            (pow (pow (pow z 5.0) -1.0) 0.5)
            (fma 0.5 (pow (pow z -1.0) 0.5) t_4))))
         (pow x 0.5))
        t_2)
       t_3))))

C

assert(x < y && y < z && z < t);
double code(double x, double y, double z, double t) {
	double t_1 = sqrt((z + 1.0)) - sqrt(z);
	double t_2 = sqrt((t + 1.0)) - sqrt(t);
	double t_3 = (((sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + t_1) + t_2;
	double t_4 = pow((pow(y, 0.5) + pow((1.0 + y), 0.5)), -1.0);
	double tmp;
	if (t_3 <= 0.0001) {
		tmp = (fma(-0.125, pow(pow(pow(x, 3.0), -1.0), 0.5), fma(0.5, pow(pow(x, -1.0), 0.5), t_4)) + t_1) + t_2;
	} else if (t_3 <= 2.01) {
		tmp = ((pow((1.0 + x), 0.5) + fma(-0.125, pow(pow(pow(z, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(z, 5.0), -1.0), 0.5), fma(0.5, pow(pow(z, -1.0), 0.5), t_4)))) - pow(x, 0.5)) + t_2;
	} else {
		tmp = t_3;
	}
	return tmp;
}

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	t_1 = Float64(sqrt(Float64(z + 1.0)) - sqrt(z))
	t_2 = Float64(sqrt(Float64(t + 1.0)) - sqrt(t))
	t_3 = Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y))) + t_1) + t_2)
	t_4 = Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0
	tmp = 0.0
	if (t_3 <= 0.0001)
		tmp = Float64(Float64(fma(-0.125, (((x ^ 3.0) ^ -1.0) ^ 0.5), fma(0.5, ((x ^ -1.0) ^ 0.5), t_4)) + t_1) + t_2);
	elseif (t_3 <= 2.01)
		tmp = Float64(Float64(Float64((Float64(1.0 + x) ^ 0.5) + fma(-0.125, (((z ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((z ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((z ^ -1.0) ^ 0.5), t_4)))) - (x ^ 0.5)) + t_2);
	else
		tmp = t_3;
	end
	return tmp
end

Wolfram

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[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = 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] + t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision]}, Block[{t$95$4 = N[Power[N[(N[Power[y, 0.5], $MachinePrecision] + N[Power[N[(1.0 + y), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]}, If[LessEqual[t$95$3, 0.0001], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + t$95$4), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision], If[LessEqual[t$95$3, 2.01], N[(N[(N[(N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.125 * N[Power[N[Power[N[Power[z, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[z, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[z, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + t$95$4), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Power[x, 0.5], $MachinePrecision]), $MachinePrecision] + t$95$2), $MachinePrecision], t$95$3]]]]]]

Derivation

1. Split input into 3 regimes

2. if (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t))) < 1.00000000000000005e-4

   1. Initial program 12.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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 12.2%

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

   5. Taylor expanded in x around inf

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

      1. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, \color{blue}{\sqrt{\frac{1}{{x}^{3}}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      2. pow1/2 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      3. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      4. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      6. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{\frac{1}{x}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      8. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      10. pow1/2 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      12. inv-pow N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      13. lower-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 49.0%

      \[\leadsto \left(\color{blue}{\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)} + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 1.00000000000000005e-4 < (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t))) < 2.0099999999999998

   1. Initial program 96.8%

      \[\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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 96.9%

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

   5. Taylor expanded in z around inf

      \[\leadsto \color{blue}{\left(\left(\sqrt{1 + x} + \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{{z}^{3}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{z}^{5}}} + \left(\frac{1}{2} \cdot \sqrt{\frac{1}{z}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right)\right)\right) - \sqrt{x}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 37.6%

      \[\leadsto \color{blue}{\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right) - {x}^{0.5}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 2.0099999999999998 < (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t)))

   1. Initial program 98.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. Add Preprocessing
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 2: 98.0% accurate, N/A× speedup

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{z + 1} - \sqrt{z}\\ t_2 := \left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\\ t_3 := \sqrt{t + 1} - \sqrt{t}\\ \mathbf{if}\;\left(t\_2 + t\_1\right) + t\_3 \leq 0.0001:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right) + t\_1\right) + t\_3\\ \mathbf{else}:\\ \;\;\;\;\left(t\_2 + \frac{1}{{\left(z + 1\right)}^{0.5} + {z}^{0.5}}\right) + t\_3\\ \end{array} \end{array} \]

FPCore

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 (+ z 1.0)) (sqrt z)))
        (t_2 (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y))))
        (t_3 (- (sqrt (+ t 1.0)) (sqrt t))))
   (if (<= (+ (+ t_2 t_1) t_3) 0.0001)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow x 3.0) -1.0) 0.5)
        (fma
         0.5
         (pow (pow x -1.0) 0.5)
         (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0)))
       t_1)
      t_3)
     (+ (+ t_2 (/ 1.0 (+ (pow (+ z 1.0) 0.5) (pow z 0.5)))) t_3))))

C

assert(x < y && y < z && z < t);
double code(double x, double y, double z, double t) {
	double t_1 = sqrt((z + 1.0)) - sqrt(z);
	double t_2 = (sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y));
	double t_3 = sqrt((t + 1.0)) - sqrt(t);
	double tmp;
	if (((t_2 + t_1) + t_3) <= 0.0001) {
		tmp = (fma(-0.125, pow(pow(pow(x, 3.0), -1.0), 0.5), fma(0.5, pow(pow(x, -1.0), 0.5), pow((pow(y, 0.5) + pow((1.0 + y), 0.5)), -1.0))) + t_1) + t_3;
	} else {
		tmp = (t_2 + (1.0 / (pow((z + 1.0), 0.5) + pow(z, 0.5)))) + t_3;
	}
	return tmp;
}

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	t_1 = Float64(sqrt(Float64(z + 1.0)) - sqrt(z))
	t_2 = Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y)))
	t_3 = Float64(sqrt(Float64(t + 1.0)) - sqrt(t))
	tmp = 0.0
	if (Float64(Float64(t_2 + t_1) + t_3) <= 0.0001)
		tmp = Float64(Float64(fma(-0.125, (((x ^ 3.0) ^ -1.0) ^ 0.5), fma(0.5, ((x ^ -1.0) ^ 0.5), (Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0))) + t_1) + t_3);
	else
		tmp = Float64(Float64(t_2 + Float64(1.0 / Float64((Float64(z + 1.0) ^ 0.5) + (z ^ 0.5)))) + t_3);
	end
	return tmp
end

Wolfram

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[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = 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]}, Block[{t$95$3 = N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(t$95$2 + t$95$1), $MachinePrecision] + t$95$3), $MachinePrecision], 0.0001], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[Power[N[(N[Power[y, 0.5], $MachinePrecision] + N[Power[N[(1.0 + y), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$3), $MachinePrecision], N[(N[(t$95$2 + N[(1.0 / N[(N[Power[N[(z + 1.0), $MachinePrecision], 0.5], $MachinePrecision] + N[Power[z, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$3), $MachinePrecision]]]]]

Derivation

1. Split input into 2 regimes

2. if (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t))) < 1.00000000000000005e-4

   1. Initial program 12.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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 12.2%

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

   5. Taylor expanded in x around inf

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

      1. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, \color{blue}{\sqrt{\frac{1}{{x}^{3}}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      2. pow1/2 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      3. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      4. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      6. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{\frac{1}{x}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      8. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      10. pow1/2 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      12. inv-pow N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      13. lower-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 49.0%

      \[\leadsto \left(\color{blue}{\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)} + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 1.00000000000000005e-4 < (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t)))

   1. Initial program 97.3%

      \[\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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. flip-- N/A

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

      6. lower-/.f64 N/A

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

   4. Applied rewrites 97.5%

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

   5. Taylor expanded in z around 0

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

   7. Applied rewrites 98.0%

      \[\leadsto \left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \frac{\color{blue}{1}}{{\left(z + 1\right)}^{0.5} + {z}^{0.5}}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 93.2% accurate, N/A× speedup

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{z + 1} - \sqrt{z}\\ t_2 := \left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + t\_1\\ t_3 := \sqrt{t + 1} - \sqrt{t}\\ t_4 := t\_2 + t\_3\\ t_5 := {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\\ \mathbf{if}\;t\_4 \leq 0.0001:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, t\_5\right)\right) + t\_1\right) + t\_3\\ \mathbf{elif}\;t\_4 \leq 2.01:\\ \;\;\;\;\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, t\_5\right)\right)\right)\right) - {x}^{0.5}\right) + t\_3\\ \mathbf{else}:\\ \;\;\;\;t\_2 + \frac{\mathsf{fma}\left({\left({t}^{-1}\right)}^{0.5}, -0.125, \mathsf{fma}\left({\left({\left({t}^{5}\right)}^{-1}\right)}^{0.5}, -0.0390625, \mathsf{fma}\left({\left({\left({t}^{3}\right)}^{-1}\right)}^{0.5}, 0.0625, 0.5 \cdot {t}^{0.5}\right)\right)\right)}{t}\\ \end{array} \end{array} \]

FPCore

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 (+ z 1.0)) (sqrt z)))
        (t_2
         (+
          (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
          t_1))
        (t_3 (- (sqrt (+ t 1.0)) (sqrt t)))
        (t_4 (+ t_2 t_3))
        (t_5 (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0)))
   (if (<= t_4 0.0001)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow x 3.0) -1.0) 0.5)
        (fma 0.5 (pow (pow x -1.0) 0.5) t_5))
       t_1)
      t_3)
     (if (<= t_4 2.01)
       (+
        (-
         (+
          (pow (+ 1.0 x) 0.5)
          (fma
           -0.125
           (pow (pow (pow z 3.0) -1.0) 0.5)
           (fma
            0.0625
            (pow (pow (pow z 5.0) -1.0) 0.5)
            (fma 0.5 (pow (pow z -1.0) 0.5) t_5))))
         (pow x 0.5))
        t_3)
       (+
        t_2
        (/
         (fma
          (pow (pow t -1.0) 0.5)
          -0.125
          (fma
           (pow (pow (pow t 5.0) -1.0) 0.5)
           -0.0390625
           (fma (pow (pow (pow t 3.0) -1.0) 0.5) 0.0625 (* 0.5 (pow t 0.5)))))
         t))))))

C

assert(x < y && y < z && z < t);
double code(double x, double y, double z, double t) {
	double t_1 = sqrt((z + 1.0)) - sqrt(z);
	double t_2 = ((sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + t_1;
	double t_3 = sqrt((t + 1.0)) - sqrt(t);
	double t_4 = t_2 + t_3;
	double t_5 = pow((pow(y, 0.5) + pow((1.0 + y), 0.5)), -1.0);
	double tmp;
	if (t_4 <= 0.0001) {
		tmp = (fma(-0.125, pow(pow(pow(x, 3.0), -1.0), 0.5), fma(0.5, pow(pow(x, -1.0), 0.5), t_5)) + t_1) + t_3;
	} else if (t_4 <= 2.01) {
		tmp = ((pow((1.0 + x), 0.5) + fma(-0.125, pow(pow(pow(z, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(z, 5.0), -1.0), 0.5), fma(0.5, pow(pow(z, -1.0), 0.5), t_5)))) - pow(x, 0.5)) + t_3;
	} else {
		tmp = t_2 + (fma(pow(pow(t, -1.0), 0.5), -0.125, fma(pow(pow(pow(t, 5.0), -1.0), 0.5), -0.0390625, fma(pow(pow(pow(t, 3.0), -1.0), 0.5), 0.0625, (0.5 * pow(t, 0.5))))) / t);
	}
	return tmp;
}

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	t_1 = Float64(sqrt(Float64(z + 1.0)) - sqrt(z))
	t_2 = Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y))) + t_1)
	t_3 = Float64(sqrt(Float64(t + 1.0)) - sqrt(t))
	t_4 = Float64(t_2 + t_3)
	t_5 = Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0
	tmp = 0.0
	if (t_4 <= 0.0001)
		tmp = Float64(Float64(fma(-0.125, (((x ^ 3.0) ^ -1.0) ^ 0.5), fma(0.5, ((x ^ -1.0) ^ 0.5), t_5)) + t_1) + t_3);
	elseif (t_4 <= 2.01)
		tmp = Float64(Float64(Float64((Float64(1.0 + x) ^ 0.5) + fma(-0.125, (((z ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((z ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((z ^ -1.0) ^ 0.5), t_5)))) - (x ^ 0.5)) + t_3);
	else
		tmp = Float64(t_2 + Float64(fma(((t ^ -1.0) ^ 0.5), -0.125, fma((((t ^ 5.0) ^ -1.0) ^ 0.5), -0.0390625, fma((((t ^ 3.0) ^ -1.0) ^ 0.5), 0.0625, Float64(0.5 * (t ^ 0.5))))) / t));
	end
	return tmp
end

Wolfram

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[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = 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] + t$95$1), $MachinePrecision]}, Block[{t$95$3 = N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$4 = N[(t$95$2 + t$95$3), $MachinePrecision]}, Block[{t$95$5 = N[Power[N[(N[Power[y, 0.5], $MachinePrecision] + N[Power[N[(1.0 + y), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]}, If[LessEqual[t$95$4, 0.0001], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + t$95$5), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$3), $MachinePrecision], If[LessEqual[t$95$4, 2.01], N[(N[(N[(N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.125 * N[Power[N[Power[N[Power[z, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[z, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[z, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + t$95$5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Power[x, 0.5], $MachinePrecision]), $MachinePrecision] + t$95$3), $MachinePrecision], N[(t$95$2 + N[(N[(N[Power[N[Power[t, -1.0], $MachinePrecision], 0.5], $MachinePrecision] * -0.125 + N[(N[Power[N[Power[N[Power[t, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] * -0.0390625 + N[(N[Power[N[Power[N[Power[t, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] * 0.0625 + N[(0.5 * N[Power[t, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision]]]]]]]]

Derivation

1. Split input into 3 regimes

2. if (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t))) < 1.00000000000000005e-4

   1. Initial program 12.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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 12.2%

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

   5. Taylor expanded in x around inf

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

      1. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, \color{blue}{\sqrt{\frac{1}{{x}^{3}}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      2. pow1/2 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      3. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      4. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      6. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{\frac{1}{x}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      8. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      10. pow1/2 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      12. inv-pow N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      13. lower-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 49.0%

      \[\leadsto \left(\color{blue}{\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)} + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 1.00000000000000005e-4 < (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t))) < 2.0099999999999998

   1. Initial program 96.8%

      \[\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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 96.9%

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

   5. Taylor expanded in z around inf

      \[\leadsto \color{blue}{\left(\left(\sqrt{1 + x} + \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{{z}^{3}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{z}^{5}}} + \left(\frac{1}{2} \cdot \sqrt{\frac{1}{z}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right)\right)\right) - \sqrt{x}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 37.6%

      \[\leadsto \color{blue}{\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right) - {x}^{0.5}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 2.0099999999999998 < (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t)))

   1. Initial program 98.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. Add Preprocessing

   3. Taylor expanded in t around inf

      \[\leadsto \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) + \color{blue}{\frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{t}} + \left(\frac{-5}{128} \cdot \sqrt{\frac{1}{{t}^{5}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{t}^{3}}} + \frac{1}{2} \cdot \sqrt{t}\right)\right)}{t}} \]
   4. Step-by-step derivation

      1. lower-/.f64 N/A

         \[\leadsto \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) + \frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{t}} + \left(\frac{-5}{128} \cdot \sqrt{\frac{1}{{t}^{5}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{t}^{3}}} + \frac{1}{2} \cdot \sqrt{t}\right)\right)}{\color{blue}{t}} \]

   5. Applied rewrites 22.0%

      \[\leadsto \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) + \color{blue}{\frac{\mathsf{fma}\left({\left({t}^{-1}\right)}^{0.5}, -0.125, \mathsf{fma}\left({\left({\left({t}^{5}\right)}^{-1}\right)}^{0.5}, -0.0390625, \mathsf{fma}\left({\left({\left({t}^{3}\right)}^{-1}\right)}^{0.5}, 0.0625, 0.5 \cdot {t}^{0.5}\right)\right)\right)}{t}} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 4: 69.1% accurate, N/A× speedup

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := \sqrt{z + 1} - \sqrt{z}\\ t_2 := \sqrt{t + 1} - \sqrt{t}\\ t_3 := {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\\ \mathbf{if}\;\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + t\_1\right) + t\_2 \leq 0.0001:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, t\_3\right)\right) + t\_1\right) + t\_2\\ \mathbf{else}:\\ \;\;\;\;\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, t\_3\right)\right)\right)\right) - {x}^{0.5}\right) + t\_2\\ \end{array} \end{array} \]

FPCore

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 (+ z 1.0)) (sqrt z)))
        (t_2 (- (sqrt (+ t 1.0)) (sqrt t)))
        (t_3 (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0)))
   (if (<=
        (+
         (+
          (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
          t_1)
         t_2)
        0.0001)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow x 3.0) -1.0) 0.5)
        (fma 0.5 (pow (pow x -1.0) 0.5) t_3))
       t_1)
      t_2)
     (+
      (-
       (+
        (pow (+ 1.0 x) 0.5)
        (fma
         -0.125
         (pow (pow (pow z 3.0) -1.0) 0.5)
         (fma
          0.0625
          (pow (pow (pow z 5.0) -1.0) 0.5)
          (fma 0.5 (pow (pow z -1.0) 0.5) t_3))))
       (pow x 0.5))
      t_2))))

C

assert(x < y && y < z && z < t);
double code(double x, double y, double z, double t) {
	double t_1 = sqrt((z + 1.0)) - sqrt(z);
	double t_2 = sqrt((t + 1.0)) - sqrt(t);
	double t_3 = pow((pow(y, 0.5) + pow((1.0 + y), 0.5)), -1.0);
	double tmp;
	if (((((sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + t_1) + t_2) <= 0.0001) {
		tmp = (fma(-0.125, pow(pow(pow(x, 3.0), -1.0), 0.5), fma(0.5, pow(pow(x, -1.0), 0.5), t_3)) + t_1) + t_2;
	} else {
		tmp = ((pow((1.0 + x), 0.5) + fma(-0.125, pow(pow(pow(z, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(z, 5.0), -1.0), 0.5), fma(0.5, pow(pow(z, -1.0), 0.5), t_3)))) - pow(x, 0.5)) + t_2;
	}
	return tmp;
}

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	t_1 = Float64(sqrt(Float64(z + 1.0)) - sqrt(z))
	t_2 = Float64(sqrt(Float64(t + 1.0)) - sqrt(t))
	t_3 = Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0
	tmp = 0.0
	if (Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y))) + t_1) + t_2) <= 0.0001)
		tmp = Float64(Float64(fma(-0.125, (((x ^ 3.0) ^ -1.0) ^ 0.5), fma(0.5, ((x ^ -1.0) ^ 0.5), t_3)) + t_1) + t_2);
	else
		tmp = Float64(Float64(Float64((Float64(1.0 + x) ^ 0.5) + fma(-0.125, (((z ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((z ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((z ^ -1.0) ^ 0.5), t_3)))) - (x ^ 0.5)) + t_2);
	end
	return tmp
end

Wolfram

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[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[Power[N[(N[Power[y, 0.5], $MachinePrecision] + N[Power[N[(1.0 + y), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]}, If[LessEqual[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] + t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision], 0.0001], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + t$95$3), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision], N[(N[(N[(N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.125 * N[Power[N[Power[N[Power[z, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[z, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[z, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Power[x, 0.5], $MachinePrecision]), $MachinePrecision] + t$95$2), $MachinePrecision]]]]]

Derivation

1. Split input into 2 regimes

2. if (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t))) < 1.00000000000000005e-4

   1. Initial program 12.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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 12.2%

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

   5. Taylor expanded in x around inf

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

      1. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, \color{blue}{\sqrt{\frac{1}{{x}^{3}}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      2. pow1/2 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      3. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left(\frac{1}{{x}^{3}}\right)}^{\color{blue}{\frac{1}{2}}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      4. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      6. lower-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot \sqrt{\frac{1}{x}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{\frac{1}{x}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      8. inv-pow N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, \sqrt{{x}^{-1}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      10. pow1/2 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      12. inv-pow N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      13. lower-pow.f64 N/A

          \[\leadsto \left(\mathsf{fma}\left(\frac{-1}{8}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{2}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, {\left(\sqrt{y} + \sqrt{1 + y}\right)}^{-1}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 49.0%

      \[\leadsto \left(\color{blue}{\mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({x}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)} + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 1.00000000000000005e-4 < (+.f64 (+.f64 (+.f64 (-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))) (-.f64 (sqrt.f64 (+.f64 z #s(literal 1 binary64))) (sqrt.f64 z))) (-.f64 (sqrt.f64 (+.f64 t #s(literal 1 binary64))) (sqrt.f64 t)))

   1. Initial program 97.3%

      \[\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. Add Preprocessing
   3. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-+.f64 N/A

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

      3. lift-sqrt.f64 N/A

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

      4. lift-sqrt.f64 N/A

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

      5. +-commutative N/A

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

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   4. Applied rewrites 97.4%

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

   5. Taylor expanded in z around inf

      \[\leadsto \color{blue}{\left(\left(\sqrt{1 + x} + \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{{z}^{3}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{z}^{5}}} + \left(\frac{1}{2} \cdot \sqrt{\frac{1}{z}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right)\right)\right) - \sqrt{x}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   7. Applied rewrites 30.2%

      \[\leadsto \color{blue}{\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right) - {x}^{0.5}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 64.1% accurate, N/A× speedup

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right) - {x}^{0.5}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \end{array} \]

FPCore

NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
(FPCore (x y z t)
 :precision binary64
 (+
  (-
   (+
    (pow (+ 1.0 x) 0.5)
    (fma
     -0.125
     (pow (pow (pow z 3.0) -1.0) 0.5)
     (fma
      0.0625
      (pow (pow (pow z 5.0) -1.0) 0.5)
      (fma
       0.5
       (pow (pow z -1.0) 0.5)
       (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0)))))
   (pow x 0.5))
  (- (sqrt (+ t 1.0)) (sqrt t))))

C

assert(x < y && y < z && z < t);
double code(double x, double y, double z, double t) {
	return ((pow((1.0 + x), 0.5) + fma(-0.125, pow(pow(pow(z, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(z, 5.0), -1.0), 0.5), fma(0.5, pow(pow(z, -1.0), 0.5), pow((pow(y, 0.5) + pow((1.0 + y), 0.5)), -1.0))))) - pow(x, 0.5)) + (sqrt((t + 1.0)) - sqrt(t));
}

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	return Float64(Float64(Float64((Float64(1.0 + x) ^ 0.5) + fma(-0.125, (((z ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((z ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((z ^ -1.0) ^ 0.5), (Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0))))) - (x ^ 0.5)) + Float64(sqrt(Float64(t + 1.0)) - sqrt(t)))
end

Wolfram

NOTE: x, y, z, and t should be sorted in increasing order before calling this function.
code[x_, y_, z_, t_] := N[(N[(N[(N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.125 * N[Power[N[Power[N[Power[z, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[z, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[z, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[Power[N[(N[Power[y, 0.5], $MachinePrecision] + N[Power[N[(1.0 + y), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Power[x, 0.5], $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 92.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. Add Preprocessing
3. Step-by-step derivation

   1. lift--.f64 N/A

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

   2. lift-+.f64 N/A

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

   3. lift-sqrt.f64 N/A

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

   4. lift-sqrt.f64 N/A

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

   5. +-commutative N/A

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

   6. flip-- N/A

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

   7. lower-/.f64 N/A

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

4. Applied rewrites 92.7%

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

5. Taylor expanded in z around inf

   \[\leadsto \color{blue}{\left(\left(\sqrt{1 + x} + \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{{z}^{3}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{z}^{5}}} + \left(\frac{1}{2} \cdot \sqrt{\frac{1}{z}} + \frac{1}{\sqrt{y} + \sqrt{1 + y}}\right)\right)\right)\right) - \sqrt{x}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

7. Applied rewrites 29.1%

   \[\leadsto \color{blue}{\left(\left({\left(1 + x\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({z}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({z}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({z}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right) - {x}^{0.5}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
8. Add Preprocessing

Reproduce

herbie shell --seed 2025064 
(FPCore (x y z t)
  :name "Main:z from "
  :precision binary64

  :alt
  (! :herbie-platform default (+ (+ (+ (/ 1 (+ (sqrt (+ x 1)) (sqrt x))) (/ 1 (+ (sqrt (+ y 1)) (sqrt y)))) (/ 1 (+ (sqrt (+ z 1)) (sqrt z)))) (- (sqrt (+ t 1)) (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))))