?

Average Accuracy: 91.6% → 99.3%
Time: 35.3s
Precision: binary64
Cost: 85824

?

\[ \begin{array}{c}[x, y, z, t] = \mathsf{sort}([x, y, z, t])\\ \end{array} \]
\[\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) \]
↓
\[\begin{array}{l} t_1 := \sqrt{x} + \sqrt{1 + x}\\ t_2 := \sqrt{1 + y} + \sqrt{y}\\ \frac{\mathsf{fma}\left(t_2, 1 + \left(x - x\right), t_1\right)}{t_2 \cdot t_1} + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) \end{array} \]
(FPCore (x y z t)
 :precision binary64
 (+
  (+
   (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
   (- (sqrt (+ z 1.0)) (sqrt z)))
  (- (sqrt (+ t 1.0)) (sqrt t))))
↓
(FPCore (x y z t)
 :precision binary64
 (let* ((t_1 (+ (sqrt x) (sqrt (+ 1.0 x))))
        (t_2 (+ (sqrt (+ 1.0 y)) (sqrt y))))
   (+
    (/ (fma t_2 (+ 1.0 (- x x)) t_1) (* t_2 t_1))
    (+ (/ 1.0 (+ (sqrt (+ 1.0 z)) (sqrt z))) (- (sqrt (+ 1.0 t)) (sqrt t))))))
double code(double x, double y, double z, double t) {
	return (((sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + (sqrt((z + 1.0)) - sqrt(z))) + (sqrt((t + 1.0)) - sqrt(t));
}
↓
double code(double x, double y, double z, double t) {
	double t_1 = sqrt(x) + sqrt((1.0 + x));
	double t_2 = sqrt((1.0 + y)) + sqrt(y);
	return (fma(t_2, (1.0 + (x - x)), t_1) / (t_2 * t_1)) + ((1.0 / (sqrt((1.0 + z)) + sqrt(z))) + (sqrt((1.0 + t)) - sqrt(t)));
}

function code(x, y, z, t)
	return Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y))) + Float64(sqrt(Float64(z + 1.0)) - sqrt(z))) + Float64(sqrt(Float64(t + 1.0)) - sqrt(t)))
end
↓
function code(x, y, z, t)
	t_1 = Float64(sqrt(x) + sqrt(Float64(1.0 + x)))
	t_2 = Float64(sqrt(Float64(1.0 + y)) + sqrt(y))
	return Float64(Float64(fma(t_2, Float64(1.0 + Float64(x - x)), t_1) / Float64(t_2 * t_1)) + Float64(Float64(1.0 / Float64(sqrt(Float64(1.0 + z)) + sqrt(z))) + Float64(sqrt(Float64(1.0 + t)) - sqrt(t))))
end

code[x_, y_, z_, t_] := N[(N[(N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
↓
code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[Sqrt[x], $MachinePrecision] + N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[Sqrt[N[(1.0 + y), $MachinePrecision]], $MachinePrecision] + N[Sqrt[y], $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(t$95$2 * N[(1.0 + N[(x - x), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision] / N[(t$95$2 * t$95$1), $MachinePrecision]), $MachinePrecision] + N[(N[(1.0 / N[(N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision] + N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]

\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)
↓
\begin{array}{l}
t_1 := \sqrt{x} + \sqrt{1 + x}\\
t_2 := \sqrt{1 + y} + \sqrt{y}\\
\frac{\mathsf{fma}\left(t_2, 1 + \left(x - x\right), t_1\right)}{t_2 \cdot t_1} + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\end{array}

Error?

Target

Original91.6%
Target99.4%
Herbie99.3%
\[\left(\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}} + \frac{1}{\sqrt{y + 1} + \sqrt{y}}\right) + \frac{1}{\sqrt{z + 1} + \sqrt{z}}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

Derivation?

  1. Initial program 91.6%

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

  2. Simplified91.6%

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

    [Start]91.6

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

    associate-+l+ [=>]91.6

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

    associate-+l- [=>]91.6

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

    +-commutative [=>]91.6

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

    sub-neg [=>]91.6

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

    sub-neg [<=]91.6

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

    +-commutative [=>]91.6

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

    +-commutative [=>]91.6

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

  3. Applied egg-rr92.2%

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

    [Start]91.6

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

    flip-- [=>]91.8

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

    add-sqr-sqrt [<=]82.8

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

    add-sqr-sqrt [<=]92.2

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

  4. Simplified92.7%

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

    [Start]92.2

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

    associate--l+ [=>]92.7

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

    +-inverses [=>]92.7

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

    metadata-eval [=>]92.7

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

  5. Applied egg-rr93.0%

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

    [Start]92.7

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

    add-cbrt-cube [=>]92.7

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

    pow1/3 [=>]92.7

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

    pow3 [=>]92.7

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

    associate--r- [=>]93.0

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

    +-commutative [=>]93.0

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

  6. Applied egg-rr93.5%

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

    [Start]93.0

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

    unpow1/3 [=>]93.0

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

    rem-cbrt-cube [=>]93.1

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

    +-commutative [=>]93.1

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

    flip-- [=>]93.2

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

    frac-add [=>]93.1

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

    add-sqr-sqrt [<=]93.1

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

    add-sqr-sqrt [<=]93.5

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

  7. Simplified97.9%

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

    [Start]93.5

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

    *-commutative [=>]93.5

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

    *-rgt-identity [=>]93.5

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

    fma-def [=>]93.5

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

    +-commutative [<=]93.5

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

    associate--l+ [=>]97.9

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

    +-commutative [=>]97.9

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

    +-commutative [<=]97.9

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

    *-commutative [=>]97.9

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

    +-commutative [=>]97.9

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

    +-commutative [<=]97.9

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

  8. Applied egg-rr99.3%

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

    [Start]97.9

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

    flip-- [=>]98.1

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

    div-inv [=>]98.1

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

    add-sqr-sqrt [<=]68.0

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

    add-sqr-sqrt [<=]98.5

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

    associate--l+ [=>]99.3

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

  9. Simplified99.3%

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

    [Start]99.3

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

    +-inverses [=>]99.3

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

    metadata-eval [=>]99.3

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

    *-lft-identity [=>]99.3

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

  10. Final simplification99.3%

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

Alternatives

Alternative 1
Accuracy98.0%
Cost72384
\[\begin{array}{l} t_1 := \sqrt{x} + \sqrt{1 + x}\\ \frac{\mathsf{fma}\left(t_1, \frac{1}{\sqrt{1 + y} + \sqrt{y}}, 1\right)}{t_1} + \left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) \end{array} \]
Alternative 2
Accuracy96.3%
Cost66116
\[\begin{array}{l} t_1 := \sqrt{1 + y}\\ t_2 := \sqrt{1 + x}\\ \mathbf{if}\;\left(t_2 - \sqrt{x}\right) - \left(\sqrt{y} - t_1\right) \leq 1:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_2}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) + \left(1 + \frac{1}{t_1 + \sqrt{y}}\right)\\ \end{array} \]
Alternative 3
Accuracy96.4%
Cost65988
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ t_2 := \sqrt{1 + y} - \sqrt{y}\\ \mathbf{if}\;t_2 \leq 0:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \mathbf{else}:\\ \;\;\;\;\left(t_1 + \left(t_2 - \sqrt{x}\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)\\ \end{array} \]
Alternative 4
Accuracy97.2%
Cost65988
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ t_2 := \sqrt{1 + y} - \sqrt{y}\\ \mathbf{if}\;t_2 \leq 0:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) + \left(t_1 + \left(t_2 - \sqrt{x}\right)\right)\\ \end{array} \]
Alternative 5
Accuracy97.7%
Cost65984
\[\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) + e^{\log \left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \frac{1 + \left(x - x\right)}{\sqrt{x} + \sqrt{1 + x}}\right)} \]
Alternative 6
Accuracy98.4%
Cost53060
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ \mathbf{if}\;y \leq 3.5 \cdot 10^{+31}:\\ \;\;\;\;\left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) + \left(\left(t_1 - \sqrt{x}\right) - \frac{-1}{\sqrt{1 + y} + \sqrt{y}}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \end{array} \]
Alternative 7
Accuracy97.0%
Cost52932
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ \mathbf{if}\;y \leq 3.5 \cdot 10^{+31}:\\ \;\;\;\;\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) + \left(t_1 - \left(\sqrt{x} + \frac{-1}{\sqrt{1 + y} + \sqrt{y}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \end{array} \]
Alternative 8
Accuracy96.9%
Cost39876
\[\begin{array}{l} \mathbf{if}\;y \leq 2.6 \cdot 10^{+18}:\\ \;\;\;\;\left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right) + \left(1 - \left(\sqrt{y} - \sqrt{1 + y}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + \sqrt{1 + x}}\\ \end{array} \]
Alternative 9
Accuracy90.2%
Cost39748
\[\begin{array}{l} t_1 := \sqrt{1 + z}\\ t_2 := \sqrt{1 + x}\\ \mathbf{if}\;t \leq 1.5 \cdot 10^{+27}:\\ \;\;\;\;1 + \left(\left(t_2 + \left(t_1 + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \left(\sqrt{x} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_2 + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) + \left(t_1 - \left(\sqrt{x} + \sqrt{z}\right)\right)\right)\\ \end{array} \]
Alternative 10
Accuracy91.2%
Cost39748
\[\begin{array}{l} t_1 := \sqrt{1 + z}\\ t_2 := \sqrt{1 + x}\\ \mathbf{if}\;t \leq 1.5 \cdot 10^{+27}:\\ \;\;\;\;1 + \left(\left(t_2 + \left(t_1 + \sqrt{1 + t}\right)\right) - \left(\sqrt{z} + \left(\sqrt{x} + \sqrt{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_2 + \left(\frac{1}{\sqrt{1 + y} + \sqrt{y}} + \left(t_1 - \left(\sqrt{x} + \sqrt{z}\right)\right)\right)\\ \end{array} \]
Alternative 11
Accuracy95.7%
Cost39748
\[\begin{array}{l} \mathbf{if}\;y \leq 2.6 \cdot 10^{+18}:\\ \;\;\;\;\left(\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) + \left(\left(1 + \sqrt{1 + y}\right) - \sqrt{y}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + \sqrt{1 + x}}\\ \end{array} \]
Alternative 12
Accuracy90.0%
Cost39620
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ \mathbf{if}\;y \leq 2.6 \cdot 10^{+18}:\\ \;\;\;\;t_1 + \left(\left(\sqrt{1 + y} - \sqrt{y}\right) + \left(\sqrt{1 + z} - \left(\sqrt{x} + \sqrt{z}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \end{array} \]
Alternative 13
Accuracy80.7%
Cost26564
\[\begin{array}{l} t_1 := \sqrt{y} + \sqrt{x}\\ t_2 := \sqrt{1 + y}\\ t_3 := \sqrt{1 + x}\\ \mathbf{if}\;z \leq 1.25:\\ \;\;\;\;1 + \left(t_2 + \left(t_3 - t_1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_3 + \left(t_2 - t_1\right)\\ \end{array} \]
Alternative 14
Accuracy90.0%
Cost26564
\[\begin{array}{l} \mathbf{if}\;y \leq 2.6 \cdot 10^{+18}:\\ \;\;\;\;1 + \left(\left(\sqrt{1 + y} + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) - \sqrt{y}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + \sqrt{1 + x}}\\ \end{array} \]
Alternative 15
Accuracy69.8%
Cost26436
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ \mathbf{if}\;y \leq 1.55 \cdot 10^{+16}:\\ \;\;\;\;t_1 + \left(\sqrt{1 + y} - \left(\sqrt{y} + \sqrt{x}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \end{array} \]
Alternative 16
Accuracy69.8%
Cost26436
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ \mathbf{if}\;y \leq 4.8 \cdot 10^{+15}:\\ \;\;\;\;\left(\sqrt{1 + y} + t_1\right) - \left(\sqrt{y} + \sqrt{x}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + t_1}\\ \end{array} \]
Alternative 17
Accuracy69.7%
Cost20164
\[\begin{array}{l} \mathbf{if}\;y \leq 3 \cdot 10^{+15}:\\ \;\;\;\;\left(\sqrt{1 + y} - \left(\sqrt{y} + \sqrt{x}\right)\right) + \left(1 + x \cdot 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + \sqrt{1 + x}}\\ \end{array} \]
Alternative 18
Accuracy69.6%
Cost19908
\[\begin{array}{l} \mathbf{if}\;y \leq 4 \cdot 10^{+15}:\\ \;\;\;\;1 + \left(\sqrt{1 + y} - \left(\sqrt{y} + \sqrt{x}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + \sqrt{1 + x}}\\ \end{array} \]
Alternative 19
Accuracy61.4%
Cost13380
\[\begin{array}{l} t_1 := \sqrt{1 + x} - \sqrt{x}\\ \mathbf{if}\;y \leq 30:\\ \;\;\;\;1 + t_1\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 20
Accuracy65.2%
Cost13380
\[\begin{array}{l} \mathbf{if}\;y \leq 4.5 \cdot 10^{+15}:\\ \;\;\;\;1 - \left(\sqrt{y} - \sqrt{1 + y}\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1 + x} - \sqrt{x}\\ \end{array} \]
Alternative 21
Accuracy65.2%
Cost13380
\[\begin{array}{l} \mathbf{if}\;y \leq 4 \cdot 10^{+15}:\\ \;\;\;\;\left(1 + \sqrt{1 + y}\right) - \sqrt{y}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1 + x} - \sqrt{x}\\ \end{array} \]
Alternative 22
Accuracy69.6%
Cost13380
\[\begin{array}{l} \mathbf{if}\;y \leq 5.4 \cdot 10^{+15}:\\ \;\;\;\;\left(1 + \sqrt{1 + y}\right) - \sqrt{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{x} + \sqrt{1 + x}}\\ \end{array} \]
Alternative 23
Accuracy35.5%
Cost13120
\[\sqrt{1 + x} - \sqrt{x} \]
Alternative 24
Accuracy35.0%
Cost6848
\[\left(1 + x \cdot 0.5\right) - \sqrt{x} \]
Alternative 25
Accuracy34.4%
Cost6592
\[1 - \sqrt{x} \]
Alternative 26
Accuracy34.5%
Cost64
\[1 \]

Error

Reproduce?

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

  :herbie-target
  (+ (+ (+ (/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x))) (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))) (/ 1.0 (+ (sqrt (+ z 1.0)) (sqrt z)))) (- (sqrt (+ t 1.0)) (sqrt t)))

  (+ (+ (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y))) (- (sqrt (+ z 1.0)) (sqrt z))) (- (sqrt (+ t 1.0)) (sqrt t))))