?

?

(FPCore (x) :precision binary64 (/ (sqrt (- 1.0 (pow x 2.0))) (+ 1.0 x)))

(FPCore (x) :precision binary64 (sqrt (/ (- 1.0 x) (+ 1.0 x))))

double code(double x) {
	return sqrt((1.0 - pow(x, 2.0))) / (1.0 + x);
}

double code(double x) {
	return sqrt(((1.0 - x) / (1.0 + x)));
}

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

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

public static double code(double x) {
	return Math.sqrt((1.0 - Math.pow(x, 2.0))) / (1.0 + x);
}

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

def code(x):
	return math.sqrt((1.0 - math.pow(x, 2.0))) / (1.0 + x)

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

function code(x)
	return Float64(sqrt(Float64(1.0 - (x ^ 2.0))) / Float64(1.0 + x))
end

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

function tmp = code(x)
	tmp = sqrt((1.0 - (x ^ 2.0))) / (1.0 + x);
end

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

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

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

\frac{\sqrt{1 - {x}^{2}}}{1 + x}

\sqrt{\frac{1 - x}{1 + x}}

Error?

Try it out?

Derivation?

1. Initial program 13.1

   \[\frac{\sqrt{1 - {x}^{2}}}{1 + x} \]

2. Simplified13.1

   \[\leadsto \color{blue}{\frac{\sqrt{1 - x \cdot x}}{x - -1}} \]
   Proof

   [Start]13.1	\[ \frac{\sqrt{1 - {x}^{2}}}{1 + x} \]
   unpow2 [=>]13.1	\[ \frac{\sqrt{1 - \color{blue}{x \cdot x}}}{1 + x} \]
   +-commutative [=>]13.1	\[ \frac{\sqrt{1 - x \cdot x}}{\color{blue}{x + 1}} \]
   metadata-eval [<=]13.1	\[ \frac{\sqrt{1 - x \cdot x}}{x + \color{blue}{\left(--1\right)}} \]
   sub-neg [<=]13.1	\[ \frac{\sqrt{1 - x \cdot x}}{\color{blue}{x - -1}} \]

3. Applied egg-rr13.1

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

4. Simplified0.3

   \[\leadsto \color{blue}{\sqrt{\frac{-\mathsf{fma}\left(x, x, -1\right)}{{\left(1 + x\right)}^{2}}}} \]
   Proof

   [Start]13.1	\[ \sqrt{\frac{1 - x \cdot x}{{\left(1 + x\right)}^{2}}} \]
   cancel-sign-sub-inv [=>]13.1	\[ \sqrt{\frac{\color{blue}{1 + \left(-x\right) \cdot x}}{{\left(1 + x\right)}^{2}}} \]
   *-commutative [<=]13.1	\[ \sqrt{\frac{1 + \color{blue}{x \cdot \left(-x\right)}}{{\left(1 + x\right)}^{2}}} \]
   +-commutative [=>]13.1	\[ \sqrt{\frac{\color{blue}{x \cdot \left(-x\right) + 1}}{{\left(1 + x\right)}^{2}}} \]
   distribute-rgt-neg-out [=>]13.1	\[ \sqrt{\frac{\color{blue}{\left(-x \cdot x\right)} + 1}{{\left(1 + x\right)}^{2}}} \]
   metadata-eval [<=]13.1	\[ \sqrt{\frac{\left(-x \cdot x\right) + \color{blue}{\left(--1\right)}}{{\left(1 + x\right)}^{2}}} \]
   distribute-neg-in [<=]13.1	\[ \sqrt{\frac{\color{blue}{-\left(x \cdot x + -1\right)}}{{\left(1 + x\right)}^{2}}} \]
   fma-udef [<=]0.3	\[ \sqrt{\frac{-\color{blue}{\mathsf{fma}\left(x, x, -1\right)}}{{\left(1 + x\right)}^{2}}} \]

5. Applied egg-rr0.2

   \[\leadsto \sqrt{\color{blue}{0 + \frac{1 - x}{1 + x}}} \]

6. Simplified0.2

   \[\leadsto \sqrt{\color{blue}{\frac{1 - x}{1 + x}}} \]
   Proof

   [Start]0.2	\[ \sqrt{0 + \frac{1 - x}{1 + x}} \]
   +-lft-identity [=>]0.2	\[ \sqrt{\color{blue}{\frac{1 - x}{1 + x}}} \]

7. Final simplification0.2

   \[\leadsto \sqrt{\frac{1 - x}{1 + x}} \]

Alternatives

Error

Reproduce?

herbie shell --seed 1 
(FPCore (x)
  :name "sqrt(1-x^2)/(1+x)"
  :precision binary64
  :pre (and (<= 0.99999 x) (<= x 1.0))
  (/ (sqrt (- 1.0 (pow x 2.0))) (+ 1.0 x)))