# ?

Average Error: 0.2 → 0.0
Time: 2.1s
Precision: binary64
Cost: 6528

# ?

$1.79 \cdot 10^{-308} \leq x \land x \leq 1.79 \cdot 10^{+308}$
$\frac{1}{\sqrt{x}}$
${x}^{-0.5}$
(FPCore (x) :precision binary64 (/ 1.0 (sqrt x)))
(FPCore (x) :precision binary64 (pow x -0.5))
double code(double x) {
return 1.0 / sqrt(x);
}

double code(double x) {
return pow(x, -0.5);
}

real(8) function code(x)
real(8), intent (in) :: x
code = 1.0d0 / sqrt(x)
end function

real(8) function code(x)
real(8), intent (in) :: x
code = x ** (-0.5d0)
end function

public static double code(double x) {
return 1.0 / Math.sqrt(x);
}

public static double code(double x) {
return Math.pow(x, -0.5);
}

def code(x):
return 1.0 / math.sqrt(x)

def code(x):
return math.pow(x, -0.5)

function code(x)
return Float64(1.0 / sqrt(x))
end

function code(x)
return x ^ -0.5
end

function tmp = code(x)
tmp = 1.0 / sqrt(x);
end

function tmp = code(x)
tmp = x ^ -0.5;
end

code[x_] := N[(1.0 / N[Sqrt[x], $MachinePrecision]),$MachinePrecision]

code[x_] := N[Power[x, -0.5], \$MachinePrecision]

\frac{1}{\sqrt{x}}

{x}^{-0.5}


# Try it out?

Results

 In Out
Enter valid numbers for all inputs

# Derivation?

1. Initial program 0.2

$\frac{1}{\sqrt{x}}$
2. Applied egg-rr29.1

$\leadsto \color{blue}{\left(1 + {x}^{-0.5}\right) - 1}$
3. Simplified0.0

$\leadsto \color{blue}{{x}^{-0.5}}$
Proof
[Start]29.1 $\left(1 + {x}^{-0.5}\right) - 1$ $\color{blue}{\left({x}^{-0.5} + 1\right)} - 1$ $\color{blue}{{x}^{-0.5} + \left(1 - 1\right)}$ ${x}^{-0.5} + \color{blue}{0}$ $\color{blue}{{x}^{-0.5}}$
4. Final simplification0.0

$\leadsto {x}^{-0.5}$

# Reproduce?

herbie shell --seed 1
(FPCore (x)
:name "1 / sqrt(x)"
:precision binary64
:pre (and (<= 1.79e-308 x) (<= x 1.79e+308))
(/ 1.0 (sqrt x)))