Average Error: 29.5 → 0.6
Time: 11.0s
Precision: binary64
Cost: 13504
\[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
\[\frac{\frac{2 + x}{e^{x}} + \frac{x}{e^{x}}}{2} \]
(FPCore (x eps)
 :precision binary64
 (/
  (-
   (* (+ 1.0 (/ 1.0 eps)) (exp (- (* (- 1.0 eps) x))))
   (* (- (/ 1.0 eps) 1.0) (exp (- (* (+ 1.0 eps) x)))))
  2.0))
(FPCore (x eps)
 :precision binary64
 (/ (+ (/ (+ 2.0 x) (exp x)) (/ x (exp x))) 2.0))
double code(double x, double eps) {
	return (((1.0 + (1.0 / eps)) * exp(-((1.0 - eps) * x))) - (((1.0 / eps) - 1.0) * exp(-((1.0 + eps) * x)))) / 2.0;
}
double code(double x, double eps) {
	return (((2.0 + x) / exp(x)) + (x / exp(x))) / 2.0;
}
real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = (((1.0d0 + (1.0d0 / eps)) * exp(-((1.0d0 - eps) * x))) - (((1.0d0 / eps) - 1.0d0) * exp(-((1.0d0 + eps) * x)))) / 2.0d0
end function
real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = (((2.0d0 + x) / exp(x)) + (x / exp(x))) / 2.0d0
end function
public static double code(double x, double eps) {
	return (((1.0 + (1.0 / eps)) * Math.exp(-((1.0 - eps) * x))) - (((1.0 / eps) - 1.0) * Math.exp(-((1.0 + eps) * x)))) / 2.0;
}
public static double code(double x, double eps) {
	return (((2.0 + x) / Math.exp(x)) + (x / Math.exp(x))) / 2.0;
}
def code(x, eps):
	return (((1.0 + (1.0 / eps)) * math.exp(-((1.0 - eps) * x))) - (((1.0 / eps) - 1.0) * math.exp(-((1.0 + eps) * x)))) / 2.0
def code(x, eps):
	return (((2.0 + x) / math.exp(x)) + (x / math.exp(x))) / 2.0
function code(x, eps)
	return Float64(Float64(Float64(Float64(1.0 + Float64(1.0 / eps)) * exp(Float64(-Float64(Float64(1.0 - eps) * x)))) - Float64(Float64(Float64(1.0 / eps) - 1.0) * exp(Float64(-Float64(Float64(1.0 + eps) * x))))) / 2.0)
end
function code(x, eps)
	return Float64(Float64(Float64(Float64(2.0 + x) / exp(x)) + Float64(x / exp(x))) / 2.0)
end
function tmp = code(x, eps)
	tmp = (((1.0 + (1.0 / eps)) * exp(-((1.0 - eps) * x))) - (((1.0 / eps) - 1.0) * exp(-((1.0 + eps) * x)))) / 2.0;
end
function tmp = code(x, eps)
	tmp = (((2.0 + x) / exp(x)) + (x / exp(x))) / 2.0;
end
code[x_, eps_] := N[(N[(N[(N[(1.0 + N[(1.0 / eps), $MachinePrecision]), $MachinePrecision] * N[Exp[(-N[(N[(1.0 - eps), $MachinePrecision] * x), $MachinePrecision])], $MachinePrecision]), $MachinePrecision] - N[(N[(N[(1.0 / eps), $MachinePrecision] - 1.0), $MachinePrecision] * N[Exp[(-N[(N[(1.0 + eps), $MachinePrecision] * x), $MachinePrecision])], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / 2.0), $MachinePrecision]
code[x_, eps_] := N[(N[(N[(N[(2.0 + x), $MachinePrecision] / N[Exp[x], $MachinePrecision]), $MachinePrecision] + N[(x / N[Exp[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / 2.0), $MachinePrecision]
\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2}
\frac{\frac{2 + x}{e^{x}} + \frac{x}{e^{x}}}{2}

Error

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 29.5

    \[\frac{\left(1 + \frac{1}{\varepsilon}\right) \cdot e^{-\left(1 - \varepsilon\right) \cdot x} - \left(\frac{1}{\varepsilon} - 1\right) \cdot e^{-\left(1 + \varepsilon\right) \cdot x}}{2} \]
  2. Simplified43.9

    \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{\varepsilon + -1}\right)}^{x}, \frac{1 - \frac{1}{\varepsilon}}{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}{2}} \]
    Proof
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (+.f64 eps -1)) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (Rewrite<= +-commutative_binary64 (+.f64 -1 eps))) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) eps)) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 eps)))) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (pow.f64 (exp.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 eps)))) x) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (neg.f64 (-.f64 1 eps)) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 1 points increase in error, 54 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 (-.f64 1 eps) x)))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (fma.f64 eps x (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)))))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 eps x) (*.f64 1 x)))))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 x (+.f64 eps 1)))))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 1 eps)))))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (-.f64 1 (/.f64 1 eps)) (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 1 eps) x))))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (/.f64 1 eps)))) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 1 eps)) 1)) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 1 eps))) 1) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 1 eps) 1))) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (/.f64 1 eps) 1))) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) 1)) (exp.f64 (*.f64 (+.f64 1 eps) x)))) 2): 0 points increase in error, 0 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) (/.f64 1 (exp.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 1 points increase in error, 1 points decrease in error
    (/.f64 (fma.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x))) (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) (Rewrite<= exp-neg_binary64 (exp.f64 (neg.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 2 points increase in error, 1 points decrease in error
    (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x)))) (*.f64 (neg.f64 (-.f64 (/.f64 1 eps) 1)) (exp.f64 (neg.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 2 points increase in error, 7 points decrease in error
    (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 (+.f64 1 (/.f64 1 eps)) (exp.f64 (neg.f64 (*.f64 (-.f64 1 eps) x)))) (*.f64 (-.f64 (/.f64 1 eps) 1) (exp.f64 (neg.f64 (*.f64 (+.f64 1 eps) x)))))) 2): 0 points increase in error, 0 points decrease in error
  3. Applied egg-rr43.9

    \[\leadsto \frac{\mathsf{fma}\left(1 + \frac{1}{\varepsilon}, {\left(e^{\varepsilon + -1}\right)}^{x}, \frac{1 - \frac{1}{\varepsilon}}{\color{blue}{{\left(\sqrt[3]{e^{\mathsf{fma}\left(\varepsilon, x, x\right)}}\right)}^{3}}}\right)}{2} \]
  4. Taylor expanded in eps around 0 30.1

    \[\leadsto \frac{\color{blue}{\left(\frac{e^{-1 \cdot x}}{\varepsilon} + \left(e^{-1 \cdot x} \cdot x + \left(\frac{1}{e^{x}} + e^{-1 \cdot x}\right)\right)\right) - \left(\frac{1}{\varepsilon \cdot e^{x}} + -1 \cdot \frac{x}{e^{x}}\right)}}{2} \]
  5. Simplified0.6

    \[\leadsto \frac{\color{blue}{\left(2 \cdot e^{-x} + \frac{x}{e^{x}}\right) + \frac{x}{e^{x}}}}{2} \]
    Proof
    (+.f64 (+.f64 (*.f64 2 (exp.f64 (neg.f64 x))) (/.f64 x (exp.f64 x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (*.f64 2 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x)))) (/.f64 x (exp.f64 x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (Rewrite<= count-2_binary64 (+.f64 (exp.f64 (*.f64 -1 x)) (exp.f64 (*.f64 -1 x)))) (/.f64 x (exp.f64 x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite=> associate-+l+_binary64 (+.f64 (exp.f64 (*.f64 -1 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 x (exp.f64 x))))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 x))) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 x (exp.f64 x)))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 x (exp.f64 x)))) (/.f64 x (exp.f64 x))): 1 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 x)) (exp.f64 x)))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (exp.f64 x)) x)))) (/.f64 x (exp.f64 x))): 1 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (*.f64 (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 x))) x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (exp.f64 (*.f64 -1 x)) (*.f64 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) x))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x))))) (/.f64 x (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 x (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (*.f64 -1 (/.f64 x (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) 0)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (Rewrite<= +-inverses_binary64 (-.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (/.f64 (exp.f64 (*.f64 -1 x)) eps)))) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (/.f64 (exp.f64 (*.f64 -1 x)) eps))) (*.f64 -1 (/.f64 x (exp.f64 x)))): 127 points increase in error, 1 points decrease in error
    (-.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (/.f64 1 (exp.f64 x)) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x)))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (*.f64 -1 x))) (/.f64 1 (exp.f64 x))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 x)))) (/.f64 1 (exp.f64 x)))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x)))) (/.f64 1 (exp.f64 x)))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (/.f64 1 (exp.f64 x))) (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 x))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (/.f64 1 (exp.f64 x))) (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x)))))) (/.f64 (exp.f64 (*.f64 -1 x)) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (/.f64 (exp.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 x))) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (/.f64 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))) eps)) (*.f64 -1 (/.f64 x (exp.f64 x)))): 1 points increase in error, 1 points decrease in error
    (-.f64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (Rewrite=> associate-/l/_binary64 (/.f64 1 (*.f64 eps (exp.f64 x))))) (*.f64 -1 (/.f64 x (exp.f64 x)))): 2 points increase in error, 0 points decrease in error
    (Rewrite<= associate--r+_binary64 (-.f64 (+.f64 (/.f64 (exp.f64 (*.f64 -1 x)) eps) (+.f64 (*.f64 (exp.f64 (*.f64 -1 x)) x) (+.f64 (/.f64 1 (exp.f64 x)) (exp.f64 (*.f64 -1 x))))) (+.f64 (/.f64 1 (*.f64 eps (exp.f64 x))) (*.f64 -1 (/.f64 x (exp.f64 x)))))): 63 points increase in error, 62 points decrease in error
  6. Taylor expanded in x around inf 0.6

    \[\leadsto \frac{\color{blue}{\left(\frac{x}{e^{x}} + 2 \cdot e^{-x}\right)} + \frac{x}{e^{x}}}{2} \]
  7. Simplified0.6

    \[\leadsto \frac{\color{blue}{\left(\frac{x}{e^{x}} + \frac{2}{e^{x}}\right)} + \frac{x}{e^{x}}}{2} \]
    Proof
    (+.f64 (/.f64 x (exp.f64 x)) (/.f64 2 (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 x (exp.f64 x)) (/.f64 (Rewrite<= metadata-eval (*.f64 2 1)) (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 x (exp.f64 x)) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 1 (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 x (exp.f64 x)) (*.f64 2 (Rewrite<= exp-neg_binary64 (exp.f64 (neg.f64 x))))): 1 points increase in error, 1 points decrease in error
  8. Taylor expanded in x around inf 0.6

    \[\leadsto \frac{\color{blue}{\left(2 \cdot \frac{1}{e^{x}} + \frac{x}{e^{x}}\right)} + \frac{x}{e^{x}}}{2} \]
  9. Simplified0.6

    \[\leadsto \frac{\color{blue}{\frac{2 + x}{e^{x}}} + \frac{x}{e^{x}}}{2} \]
    Proof
    (/.f64 (+.f64 2 x) (exp.f64 x)): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 2 x))) (exp.f64 x)): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (exp.f64 x)) (+.f64 2 x))): 2 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> rec-exp_binary64 (exp.f64 (neg.f64 x))) (+.f64 2 x)): 1 points increase in error, 1 points decrease in error
    (Rewrite=> distribute-rgt-in_binary64 (+.f64 (*.f64 2 (exp.f64 (neg.f64 x))) (*.f64 x (exp.f64 (neg.f64 x))))): 1 points increase in error, 1 points decrease in error
    (Rewrite=> fma-def_binary64 (fma.f64 2 (exp.f64 (neg.f64 x)) (*.f64 x (exp.f64 (neg.f64 x))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 2 (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))) (*.f64 x (exp.f64 (neg.f64 x)))): 1 points increase in error, 1 points decrease in error
    (fma.f64 2 (/.f64 1 (exp.f64 x)) (*.f64 x (Rewrite<= rec-exp_binary64 (/.f64 1 (exp.f64 x))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 2 (/.f64 1 (exp.f64 x)) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 x 1) (exp.f64 x)))): 1 points increase in error, 0 points decrease in error
    (fma.f64 2 (/.f64 1 (exp.f64 x)) (/.f64 (Rewrite=> *-rgt-identity_binary64 x) (exp.f64 x))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (/.f64 1 (exp.f64 x))) (/.f64 x (exp.f64 x)))): 0 points increase in error, 0 points decrease in error
  10. Final simplification0.6

    \[\leadsto \frac{\frac{2 + x}{e^{x}} + \frac{x}{e^{x}}}{2} \]

Alternatives

Alternative 1
Error1.0
Cost7108
\[\begin{array}{l} \mathbf{if}\;x \leq 2.25:\\ \;\;\;\;\frac{\frac{x}{e^{x}} + \left(2 - x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
Alternative 2
Error1.1
Cost836
\[\begin{array}{l} \mathbf{if}\;x \leq 1.4:\\ \;\;\;\;\frac{\left(2 - x\right) + \left(x - x \cdot x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
Alternative 3
Error1.2
Cost580
\[\begin{array}{l} \mathbf{if}\;x \leq 360:\\ \;\;\;\;\frac{x + \left(2 - x\right)}{2}\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
Alternative 4
Error1.2
Cost196
\[\begin{array}{l} \mathbf{if}\;x \leq 370:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
Alternative 5
Error46.9
Cost64
\[0 \]

Error

Reproduce

herbie shell --seed 2022325 
(FPCore (x eps)
  :name "NMSE Section 6.1 mentioned, A"
  :precision binary64
  (/ (- (* (+ 1.0 (/ 1.0 eps)) (exp (- (* (- 1.0 eps) x)))) (* (- (/ 1.0 eps) 1.0) (exp (- (* (+ 1.0 eps) x))))) 2.0))