?

?

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

(FPCore (x) :precision binary64 (/ (* 2.0 (sinh x)) 2.0))

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

double code(double x) {
	return (2.0 * sinh(x)) / 2.0;
}

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

public static double code(double x) {
	return (2.0 * Math.sinh(x)) / 2.0;
}

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

def code(x):
	return (2.0 * math.sinh(x)) / 2.0

function code(x)
	return Float64(Float64((exp(1) ^ x) - Float64(1.0 / (exp(1) ^ x))) / 2.0)
end

function code(x)
	return Float64(Float64(2.0 * sinh(x)) / 2.0)
end

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

function tmp = code(x)
	tmp = (2.0 * sinh(x)) / 2.0;
end

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

code[x_] := N[(N[(2.0 * N[Sinh[x], $MachinePrecision]), $MachinePrecision] / 2.0), $MachinePrecision]

\frac{{e}^{x} - \frac{1}{{e}^{x}}}{2}

\frac{2 \cdot \sinh x}{2}

Error?

Try it out?

Derivation?

1. Initial program 58.0

   \[\frac{{e}^{x} - \frac{1}{{e}^{x}}}{2} \]

2. Taylor expanded in x around inf 58.0

   \[\leadsto \frac{\color{blue}{e^{\log e \cdot x} - \frac{1}{e^{\log e \cdot x}}}}{2} \]

3. Simplified57.9

   \[\leadsto \frac{\color{blue}{e^{x} - e^{-x}}}{2} \]
   Proof

   [Start]58.0	\[ \frac{e^{\log e \cdot x} - \frac{1}{e^{\log e \cdot x}}}{2} \]
   log-E [=>]58.0	\[ \frac{e^{\color{blue}{1} \cdot x} - \frac{1}{e^{\log e \cdot x}}}{2} \]
   *-lft-identity [=>]58.0	\[ \frac{e^{\color{blue}{x}} - \frac{1}{e^{\log e \cdot x}}}{2} \]
   remove-double-neg [<=]58.0	\[ \frac{e^{\color{blue}{-\left(-x\right)}} - \frac{1}{e^{\log e \cdot x}}}{2} \]
   remove-double-neg [=>]58.0	\[ \frac{e^{\color{blue}{x}} - \frac{1}{e^{\log e \cdot x}}}{2} \]
   rec-exp [=>]57.9	\[ \frac{e^{x} - \color{blue}{e^{-\log e \cdot x}}}{2} \]
   log-E [=>]57.9	\[ \frac{e^{x} - e^{-\color{blue}{1} \cdot x}}{2} \]
   distribute-lft-neg-in [=>]57.9	\[ \frac{e^{x} - e^{\color{blue}{\left(-1\right) \cdot x}}}{2} \]
   metadata-eval [=>]57.9	\[ \frac{e^{x} - e^{\color{blue}{-1} \cdot x}}{2} \]
   neg-mul-1 [<=]57.9	\[ \frac{e^{x} - e^{\color{blue}{-x}}}{2} \]

4. Taylor expanded in x around -inf 57.9

   \[\leadsto \frac{\color{blue}{e^{x} - e^{-1 \cdot x}}}{2} \]

5. Simplified0.0

   \[\leadsto \frac{\color{blue}{2 \cdot \sinh x}}{2} \]
   Proof

   [Start]57.9	\[ \frac{e^{x} - e^{-1 \cdot x}}{2} \]
   mul-1-neg [=>]57.9	\[ \frac{e^{x} - e^{\color{blue}{-x}}}{2} \]
   *-lft-identity [<=]57.9	\[ \frac{\color{blue}{1 \cdot e^{x}} - e^{-x}}{2} \]
   *-lft-identity [<=]57.9	\[ \frac{1 \cdot e^{x} - \color{blue}{1 \cdot e^{-x}}}{2} \]
   distribute-lft-out-- [=>]57.9	\[ \frac{\color{blue}{1 \cdot \left(e^{x} - e^{-x}\right)}}{2} \]
   metadata-eval [<=]57.9	\[ \frac{\color{blue}{\frac{2}{2}} \cdot \left(e^{x} - e^{-x}\right)}{2} \]
   associate-/r/ [<=]57.9	\[ \frac{\color{blue}{\frac{2}{\frac{2}{e^{x} - e^{-x}}}}}{2} \]
   associate-/l* [<=]57.9	\[ \frac{\color{blue}{\frac{2 \cdot \left(e^{x} - e^{-x}\right)}{2}}}{2} \]
   associate-*r/ [<=]57.9	\[ \frac{\color{blue}{2 \cdot \frac{e^{x} - e^{-x}}{2}}}{2} \]
   sinh-def [<=]0.0	\[ \frac{2 \cdot \color{blue}{\sinh x}}{2} \]

6. Final simplification0.0

   \[\leadsto \frac{2 \cdot \sinh x}{2} \]

Alternatives

Error

Reproduce?

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