Main:z from

Percentage Accurate: 91.0% → 99.2%

Time: 19.4s

Alternatives: 6

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.0% 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{y + 1} - \sqrt{y}\\ t_2 := \sqrt{t + 1} - \sqrt{t}\\ \mathbf{if}\;t\_1 \leq 0.0005:\\ \;\;\;\;\left(\left(\frac{1}{{\left(1 + x\right)}^{0.5} + {x}^{0.5}} + \frac{\mathsf{fma}\left(-0.125, {\left({y}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({y}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {y}^{0.5}\right)\right)}{y}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + t\_2\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + t\_1\right) + \frac{1}{{\left(z + 1\right)}^{0.5} + {z}^{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 (+ y 1.0)) (sqrt y)))
        (t_2 (- (sqrt (+ t 1.0)) (sqrt t))))
   (if (<= t_1 0.0005)
     (+
      (+
       (+
        (/ 1.0 (+ (pow (+ 1.0 x) 0.5) (pow x 0.5)))
        (/
         (fma
          -0.125
          (pow (pow y -1.0) 0.5)
          (fma 0.0625 (pow (pow (pow y 3.0) -1.0) 0.5) (* 0.5 (pow y 0.5))))
         y))
       (- (sqrt (+ z 1.0)) (sqrt z)))
      t_2)
     (+
      (+
       (+ (- (sqrt (+ x 1.0)) (sqrt x)) t_1)
       (/ 1.0 (+ (pow (+ z 1.0) 0.5) (pow z 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((y + 1.0)) - sqrt(y);
	double t_2 = sqrt((t + 1.0)) - sqrt(t);
	double tmp;
	if (t_1 <= 0.0005) {
		tmp = (((1.0 / (pow((1.0 + x), 0.5) + pow(x, 0.5))) + (fma(-0.125, pow(pow(y, -1.0), 0.5), fma(0.0625, pow(pow(pow(y, 3.0), -1.0), 0.5), (0.5 * pow(y, 0.5)))) / y)) + (sqrt((z + 1.0)) - sqrt(z))) + t_2;
	} else {
		tmp = (((sqrt((x + 1.0)) - sqrt(x)) + t_1) + (1.0 / (pow((z + 1.0), 0.5) + pow(z, 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(y + 1.0)) - sqrt(y))
	t_2 = Float64(sqrt(Float64(t + 1.0)) - sqrt(t))
	tmp = 0.0
	if (t_1 <= 0.0005)
		tmp = Float64(Float64(Float64(Float64(1.0 / Float64((Float64(1.0 + x) ^ 0.5) + (x ^ 0.5))) + Float64(fma(-0.125, ((y ^ -1.0) ^ 0.5), fma(0.0625, (((y ^ 3.0) ^ -1.0) ^ 0.5), Float64(0.5 * (y ^ 0.5)))) / y)) + Float64(sqrt(Float64(z + 1.0)) - sqrt(z))) + t_2);
	else
		tmp = Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + t_1) + Float64(1.0 / Float64((Float64(z + 1.0) ^ 0.5) + (z ^ 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[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, 0.0005], N[(N[(N[(N[(1.0 / N[(N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision] + N[Power[x, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(-0.125 * N[Power[N[Power[y, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[y, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[y, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$2), $MachinePrecision], N[(N[(N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + 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$2), $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y)) < 5.0000000000000001e-4

   1. Initial program 76.7%

      \[\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. lift--.f64 N/A

         \[\leadsto \left(\left(\color{blue}{\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. lift-+.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{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) \]

      3. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{\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) \]

      4. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{x + 1} - \color{blue}{\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) \]

      5. +-commutative N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{1 + x}} - \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) \]

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 77.2%

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

   4. Taylor expanded in x around 0

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

   6. Applied rewrites 92.8%

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

   7. Taylor expanded in y around inf

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

      1. lower-/.f64 N/A

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

      2. lower-fma.f64 N/A

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

      3. pow1/2 N/A

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

      4. lower-pow.f64 N/A

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

      5. inv-pow N/A

         \[\leadsto \left(\left(\frac{1}{{\left(1 + x\right)}^{\frac{1}{2}} + {x}^{\frac{1}{2}}} + \frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({y}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{16} \cdot \sqrt{\frac{1}{{y}^{3}}} + \frac{1}{2} \cdot \sqrt{y}\right)}{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(\left(\frac{1}{{\left(1 + x\right)}^{\frac{1}{2}} + {x}^{\frac{1}{2}}} + \frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({y}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{16} \cdot \sqrt{\frac{1}{{y}^{3}}} + \frac{1}{2} \cdot \sqrt{y}\right)}{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(\left(\frac{1}{{\left(1 + x\right)}^{\frac{1}{2}} + {x}^{\frac{1}{2}}} + \frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({y}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, \sqrt{\frac{1}{{y}^{3}}}, \frac{1}{2} \cdot \sqrt{y}\right)\right)}{y}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

      8. pow1/2 N/A

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

      9. lower-pow.f64 N/A

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

      10. inv-pow N/A

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

      11. lower-pow.f64 N/A

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

      12. lower-pow.f64 N/A

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

      13. lower-*.f64 N/A

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

      14. pow1/2 N/A

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

      15. lift-pow.f64 99.4

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

   9. Applied rewrites 99.4%

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

   if 5.0000000000000001e-4 < (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))

   1. Initial program 97.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. 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) \]

   3. Applied rewrites 97.6%

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

   4. 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) \]
   5. Step-by-step derivation

   6. Applied rewrites 99.1%

      \[\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 2: 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{y + 1} - \sqrt{y}\\ t_2 := \sqrt{t + 1} - \sqrt{t}\\ \mathbf{if}\;t\_1 \leq 0.0005:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({y}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({y}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({y}^{-1}\right)}^{0.5}, {\left({x}^{0.5} + {\left(1 + x\right)}^{0.5}\right)}^{-1}\right)\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + t\_2\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + t\_1\right) + \frac{1}{{\left(z + 1\right)}^{0.5} + {z}^{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 (+ y 1.0)) (sqrt y)))
        (t_2 (- (sqrt (+ t 1.0)) (sqrt t))))
   (if (<= t_1 0.0005)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow y 3.0) -1.0) 0.5)
        (fma
         0.0625
         (pow (pow (pow y 5.0) -1.0) 0.5)
         (fma
          0.5
          (pow (pow y -1.0) 0.5)
          (pow (+ (pow x 0.5) (pow (+ 1.0 x) 0.5)) -1.0))))
       (- (sqrt (+ z 1.0)) (sqrt z)))
      t_2)
     (+
      (+
       (+ (- (sqrt (+ x 1.0)) (sqrt x)) t_1)
       (/ 1.0 (+ (pow (+ z 1.0) 0.5) (pow z 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((y + 1.0)) - sqrt(y);
	double t_2 = sqrt((t + 1.0)) - sqrt(t);
	double tmp;
	if (t_1 <= 0.0005) {
		tmp = (fma(-0.125, pow(pow(pow(y, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(y, 5.0), -1.0), 0.5), fma(0.5, pow(pow(y, -1.0), 0.5), pow((pow(x, 0.5) + pow((1.0 + x), 0.5)), -1.0)))) + (sqrt((z + 1.0)) - sqrt(z))) + t_2;
	} else {
		tmp = (((sqrt((x + 1.0)) - sqrt(x)) + t_1) + (1.0 / (pow((z + 1.0), 0.5) + pow(z, 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(y + 1.0)) - sqrt(y))
	t_2 = Float64(sqrt(Float64(t + 1.0)) - sqrt(t))
	tmp = 0.0
	if (t_1 <= 0.0005)
		tmp = Float64(Float64(fma(-0.125, (((y ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((y ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((y ^ -1.0) ^ 0.5), (Float64((x ^ 0.5) + (Float64(1.0 + x) ^ 0.5)) ^ -1.0)))) + Float64(sqrt(Float64(z + 1.0)) - sqrt(z))) + t_2);
	else
		tmp = Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + t_1) + Float64(1.0 / Float64((Float64(z + 1.0) ^ 0.5) + (z ^ 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[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, 0.0005], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[y, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[y, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[y, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[Power[N[(N[Power[x, 0.5], $MachinePrecision] + N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$2), $MachinePrecision], N[(N[(N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + 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$2), $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y)) < 5.0000000000000001e-4

   1. Initial program 76.7%

      \[\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. lift--.f64 N/A

         \[\leadsto \left(\left(\color{blue}{\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. lift-+.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{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) \]

      3. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{\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) \]

      4. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{x + 1} - \color{blue}{\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) \]

      5. +-commutative N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{1 + x}} - \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) \]

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 77.2%

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

   4. Taylor expanded in y around inf

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

      1. lower-fma.f64 N/A

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

   6. Applied rewrites 99.3%

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

   if 5.0000000000000001e-4 < (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))

   1. Initial program 97.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. 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) \]

   3. Applied rewrites 97.6%

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

   4. 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) \]
   5. Step-by-step derivation

   6. Applied rewrites 99.1%

      \[\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: 98.5% accurate, N/A× speedup

Math

\[\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{z + 1} - \sqrt{z}\\ \mathbf{if}\;t\_1 \leq 0.0005:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({y}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({y}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({y}^{-1}\right)}^{0.5}, {\left({x}^{0.5} + {\left(1 + x\right)}^{0.5}\right)}^{-1}\right)\right)\right) + t\_2\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + t\_1\right) + t\_2\right) + \frac{1}{{\left(t + 1\right)}^{0.5} + {t}^{0.5}}\\ \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 (+ y 1.0)) (sqrt y)))
        (t_2 (- (sqrt (+ z 1.0)) (sqrt z))))
   (if (<= t_1 0.0005)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow y 3.0) -1.0) 0.5)
        (fma
         0.0625
         (pow (pow (pow y 5.0) -1.0) 0.5)
         (fma
          0.5
          (pow (pow y -1.0) 0.5)
          (pow (+ (pow x 0.5) (pow (+ 1.0 x) 0.5)) -1.0))))
       t_2)
      (- (sqrt (+ t 1.0)) (sqrt t)))
     (+
      (+ (+ (- (sqrt (+ x 1.0)) (sqrt x)) t_1) t_2)
      (/ 1.0 (+ (pow (+ t 1.0) 0.5) (pow t 0.5)))))))

C

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((z + 1.0)) - sqrt(z);
	double tmp;
	if (t_1 <= 0.0005) {
		tmp = (fma(-0.125, pow(pow(pow(y, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(y, 5.0), -1.0), 0.5), fma(0.5, pow(pow(y, -1.0), 0.5), pow((pow(x, 0.5) + pow((1.0 + x), 0.5)), -1.0)))) + t_2) + (sqrt((t + 1.0)) - sqrt(t));
	} else {
		tmp = (((sqrt((x + 1.0)) - sqrt(x)) + t_1) + t_2) + (1.0 / (pow((t + 1.0), 0.5) + pow(t, 0.5)));
	}
	return tmp;
}

Julia

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(z + 1.0)) - sqrt(z))
	tmp = 0.0
	if (t_1 <= 0.0005)
		tmp = Float64(Float64(fma(-0.125, (((y ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((y ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((y ^ -1.0) ^ 0.5), (Float64((x ^ 0.5) + (Float64(1.0 + x) ^ 0.5)) ^ -1.0)))) + t_2) + Float64(sqrt(Float64(t + 1.0)) - sqrt(t)));
	else
		tmp = Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + t_1) + t_2) + Float64(1.0 / Float64((Float64(t + 1.0) ^ 0.5) + (t ^ 0.5))));
	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[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, 0.0005], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[y, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[y, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[y, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[Power[N[(N[Power[x, 0.5], $MachinePrecision] + N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$2), $MachinePrecision] + N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision] + N[(1.0 / N[(N[Power[N[(t + 1.0), $MachinePrecision], 0.5], $MachinePrecision] + N[Power[t, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y)) < 5.0000000000000001e-4

   1. Initial program 76.7%

      \[\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. lift--.f64 N/A

         \[\leadsto \left(\left(\color{blue}{\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. lift-+.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{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) \]

      3. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{\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) \]

      4. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{x + 1} - \color{blue}{\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) \]

      5. +-commutative N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{1 + x}} - \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) \]

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 77.2%

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

   4. Taylor expanded in y around inf

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

      1. lower-fma.f64 N/A

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

   6. Applied rewrites 99.3%

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

   if 5.0000000000000001e-4 < (-.f64 (sqrt.f64 (+.f64 y #s(literal 1 binary64))) (sqrt.f64 y))

   1. Initial program 97.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. lift--.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) + \color{blue}{\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{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{\color{blue}{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(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\color{blue}{\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} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \color{blue}{\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) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \color{blue}{\frac{\sqrt{t + 1} \cdot \sqrt{t + 1} - \sqrt{t} \cdot \sqrt{t}}{\sqrt{t + 1} + \sqrt{t}}} \]

      6. 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) + \color{blue}{\frac{\sqrt{t + 1} \cdot \sqrt{t + 1} - \sqrt{t} \cdot \sqrt{t}}{\sqrt{t + 1} + \sqrt{t}}} \]

   3. Applied rewrites 97.5%

      \[\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{{\left(t + 1\right)}^{0.5} \cdot {\left(t + 1\right)}^{0.5} - {t}^{0.5} \cdot {t}^{0.5}}{{\left(t + 1\right)}^{0.5} + {t}^{0.5}}} \]

   4. Taylor expanded in t around 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) + \frac{\color{blue}{1}}{{\left(t + 1\right)}^{\frac{1}{2}} + {t}^{\frac{1}{2}}} \]
   5. Step-by-step derivation

   6. Applied rewrites 98.1%

      \[\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{\color{blue}{1}}{{\left(t + 1\right)}^{0.5} + {t}^{0.5}} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 98.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}\\ \mathbf{if}\;y \leq 5000:\\ \;\;\;\;\left(\left(\left(e^{\mathsf{log1p}\left(x\right) \cdot 0.5} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + t\_1\right) + t\_2\\ \mathbf{else}:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({y}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({y}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({y}^{-1}\right)}^{0.5}, {\left({x}^{0.5} + {\left(1 + x\right)}^{0.5}\right)}^{-1}\right)\right)\right) + t\_1\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))))
   (if (<= y 5000.0)
     (+
      (+
       (+ (- (exp (* (log1p x) 0.5)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
       t_1)
      t_2)
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow y 3.0) -1.0) 0.5)
        (fma
         0.0625
         (pow (pow (pow y 5.0) -1.0) 0.5)
         (fma
          0.5
          (pow (pow y -1.0) 0.5)
          (pow (+ (pow x 0.5) (pow (+ 1.0 x) 0.5)) -1.0))))
       t_1)
      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 tmp;
	if (y <= 5000.0) {
		tmp = (((exp((log1p(x) * 0.5)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + t_1) + t_2;
	} else {
		tmp = (fma(-0.125, pow(pow(pow(y, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(y, 5.0), -1.0), 0.5), fma(0.5, pow(pow(y, -1.0), 0.5), pow((pow(x, 0.5) + pow((1.0 + x), 0.5)), -1.0)))) + t_1) + 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))
	tmp = 0.0
	if (y <= 5000.0)
		tmp = Float64(Float64(Float64(Float64(exp(Float64(log1p(x) * 0.5)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y))) + t_1) + t_2);
	else
		tmp = Float64(Float64(fma(-0.125, (((y ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((y ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((y ^ -1.0) ^ 0.5), (Float64((x ^ 0.5) + (Float64(1.0 + x) ^ 0.5)) ^ -1.0)))) + t_1) + 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]}, If[LessEqual[y, 5000.0], N[(N[(N[(N[(N[Exp[N[(N[Log[1 + x], $MachinePrecision] * 0.5), $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], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[y, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[y, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[y, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[Power[N[(N[Power[x, 0.5], $MachinePrecision] + N[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if y < 5e3

   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. lift-+.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{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. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{\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) \]

      3. pow1/2 N/A

         \[\leadsto \left(\left(\left(\color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}} - \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) \]

      4. pow-to-exp N/A

         \[\leadsto \left(\left(\left(\color{blue}{e^{\log \left(x + 1\right) \cdot \frac{1}{2}}} - \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) \]

      5. lower-exp.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{e^{\log \left(x + 1\right) \cdot \frac{1}{2}}} - \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) \]

      6. lower-*.f64 N/A

         \[\leadsto \left(\left(\left(e^{\color{blue}{\log \left(x + 1\right) \cdot \frac{1}{2}}} - \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) \]

      7. +-commutative N/A

         \[\leadsto \left(\left(\left(e^{\log \color{blue}{\left(1 + x\right)} \cdot \frac{1}{2}} - \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) \]

      8. lower-log1p.f64 97.5

         \[\leadsto \left(\left(\left(e^{\color{blue}{\mathsf{log1p}\left(x\right)} \cdot 0.5} - \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) \]

   3. Applied rewrites 97.5%

      \[\leadsto \left(\left(\left(\color{blue}{e^{\mathsf{log1p}\left(x\right) \cdot 0.5}} - \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) \]

   if 5e3 < y

   1. Initial program 76.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. lift--.f64 N/A

         \[\leadsto \left(\left(\color{blue}{\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. lift-+.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{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) \]

      3. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{\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) \]

      4. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{x + 1} - \color{blue}{\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) \]

      5. +-commutative N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{1 + x}} - \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) \]

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 77.4%

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

   4. Taylor expanded in y around inf

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

      1. lower-fma.f64 N/A

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

   6. Applied rewrites 99.3%

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

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

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \begin{array}{l} t_1 := {\left(1 + x\right)}^{0.5}\\ \mathbf{if}\;y \leq 6.2 \cdot 10^{-10}:\\ \;\;\;\;\left(t\_1 + \left({\left(1 + z\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({t}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({t}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({t}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right)\right) - \left({x}^{0.5} + {z}^{0.5}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\mathsf{fma}\left(-0.125, {\left({\left({y}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({y}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({y}^{-1}\right)}^{0.5}, {\left({x}^{0.5} + t\_1\right)}^{-1}\right)\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\\ \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 (pow (+ 1.0 x) 0.5)))
   (if (<= y 6.2e-10)
     (-
      (+
       t_1
       (+
        (pow (+ 1.0 z) 0.5)
        (fma
         -0.125
         (pow (pow (pow t 3.0) -1.0) 0.5)
         (fma
          0.0625
          (pow (pow (pow t 5.0) -1.0) 0.5)
          (fma
           0.5
           (pow (pow t -1.0) 0.5)
           (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0))))))
      (+ (pow x 0.5) (pow z 0.5)))
     (+
      (+
       (fma
        -0.125
        (pow (pow (pow y 3.0) -1.0) 0.5)
        (fma
         0.0625
         (pow (pow (pow y 5.0) -1.0) 0.5)
         (fma 0.5 (pow (pow y -1.0) 0.5) (pow (+ (pow x 0.5) t_1) -1.0))))
       (- (sqrt (+ z 1.0)) (sqrt z)))
      (- (sqrt (+ t 1.0)) (sqrt t))))))

C

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

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	t_1 = Float64(1.0 + x) ^ 0.5
	tmp = 0.0
	if (y <= 6.2e-10)
		tmp = Float64(Float64(t_1 + Float64((Float64(1.0 + z) ^ 0.5) + fma(-0.125, (((t ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((t ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((t ^ -1.0) ^ 0.5), (Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0)))))) - Float64((x ^ 0.5) + (z ^ 0.5)));
	else
		tmp = Float64(Float64(fma(-0.125, (((y ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((y ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((y ^ -1.0) ^ 0.5), (Float64((x ^ 0.5) + t_1) ^ -1.0)))) + Float64(sqrt(Float64(z + 1.0)) - sqrt(z))) + Float64(sqrt(Float64(t + 1.0)) - sqrt(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[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision]}, If[LessEqual[y, 6.2e-10], N[(N[(t$95$1 + N[(N[Power[N[(1.0 + z), $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.125 * N[Power[N[Power[N[Power[t, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[t, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[t, -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]), $MachinePrecision] - N[(N[Power[x, 0.5], $MachinePrecision] + N[Power[z, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[(-0.125 * N[Power[N[Power[N[Power[y, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[y, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[y, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[Power[N[(N[Power[x, 0.5], $MachinePrecision] + t$95$1), $MachinePrecision], -1.0], $MachinePrecision]), $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]]]

Derivation

1. Split input into 2 regimes

2. if y < 6.2000000000000003e-10

   1. Initial program 97.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. 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) \]

   3. Applied rewrites 97.6%

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

   4. Taylor expanded in t around inf

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

   6. Applied rewrites 46.5%

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

   if 6.2000000000000003e-10 < y

   1. Initial program 78.7%

      \[\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. lift--.f64 N/A

         \[\leadsto \left(\left(\color{blue}{\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. lift-+.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{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) \]

      3. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\color{blue}{\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) \]

      4. lift-sqrt.f64 N/A

         \[\leadsto \left(\left(\left(\sqrt{x + 1} - \color{blue}{\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) \]

      5. +-commutative N/A

         \[\leadsto \left(\left(\left(\sqrt{\color{blue}{1 + x}} - \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) \]

      6. flip-- N/A

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

      7. lower-/.f64 N/A

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

   3. Applied rewrites 79.2%

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

   4. Taylor expanded in y around inf

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

      1. lower-fma.f64 N/A

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

   6. Applied rewrites 92.2%

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

Alternative 6: 32.1% accurate, N/A× speedup

Math

\[\begin{array}{l} [x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \\ \left({\left(1 + x\right)}^{0.5} + \left({\left(1 + z\right)}^{0.5} + \mathsf{fma}\left(-0.125, {\left({\left({t}^{3}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({t}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.5, {\left({t}^{-1}\right)}^{0.5}, {\left({y}^{0.5} + {\left(1 + y\right)}^{0.5}\right)}^{-1}\right)\right)\right)\right)\right) - \left({x}^{0.5} + {z}^{0.5}\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)
   (+
    (pow (+ 1.0 z) 0.5)
    (fma
     -0.125
     (pow (pow (pow t 3.0) -1.0) 0.5)
     (fma
      0.0625
      (pow (pow (pow t 5.0) -1.0) 0.5)
      (fma
       0.5
       (pow (pow t -1.0) 0.5)
       (pow (+ (pow y 0.5) (pow (+ 1.0 y) 0.5)) -1.0))))))
  (+ (pow x 0.5) (pow z 0.5))))

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) + (pow((1.0 + z), 0.5) + fma(-0.125, pow(pow(pow(t, 3.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(t, 5.0), -1.0), 0.5), fma(0.5, pow(pow(t, -1.0), 0.5), pow((pow(y, 0.5) + pow((1.0 + y), 0.5)), -1.0)))))) - (pow(x, 0.5) + pow(z, 0.5));
}

Julia

x, y, z, t = sort([x, y, z, t])
function code(x, y, z, t)
	return Float64(Float64((Float64(1.0 + x) ^ 0.5) + Float64((Float64(1.0 + z) ^ 0.5) + fma(-0.125, (((t ^ 3.0) ^ -1.0) ^ 0.5), fma(0.0625, (((t ^ 5.0) ^ -1.0) ^ 0.5), fma(0.5, ((t ^ -1.0) ^ 0.5), (Float64((y ^ 0.5) + (Float64(1.0 + y) ^ 0.5)) ^ -1.0)))))) - Float64((x ^ 0.5) + (z ^ 0.5)))
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[Power[N[(1.0 + x), $MachinePrecision], 0.5], $MachinePrecision] + N[(N[Power[N[(1.0 + z), $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.125 * N[Power[N[Power[N[Power[t, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[t, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[N[Power[t, -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]), $MachinePrecision] - N[(N[Power[x, 0.5], $MachinePrecision] + N[Power[z, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 91.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. 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) \]

3. Applied rewrites 91.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) \]

4. Taylor expanded in t around inf

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

6. Applied rewrites 32.1%

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

Reproduce

herbie shell --seed 2025093 
(FPCore (x y z t)
  :name "Main:z from "
  :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))))