Average Error: 0.0 → 0.0
Time: 15.5s
Precision: 64
\[\Re(\left(\frac{e^{x} + e^{-x}}{2} \cdot \cos y + \frac{e^{x} - e^{-x}}{2} \cdot \sin y i\right))\]
↓
\[\left(\frac{1}{e^{x}} \cdot \cos y + \cos y \cdot e^{x}\right) \cdot \frac{1}{2}\]
\Re(\left(\frac{e^{x} + e^{-x}}{2} \cdot \cos y + \frac{e^{x} - e^{-x}}{2} \cdot \sin y i\right))
↓
\left(\frac{1}{e^{x}} \cdot \cos y + \cos y \cdot e^{x}\right) \cdot \frac{1}{2}
double f(double x, double y) {
        double r688224 = x;
        double r688225 = exp(r688224);
        double r688226 = -r688224;
        double r688227 = exp(r688226);
        double r688228 = r688225 + r688227;
        double r688229 = 2.0;
        double r688230 = r688228 / r688229;
        double r688231 = y;
        double r688232 = cos(r688231);
        double r688233 = r688230 * r688232;
        double r688234 = r688225 - r688227;
        double r688235 = r688234 / r688229;
        double r688236 = sin(r688231);
        double r688237 = r688235 * r688236;
        double r688238 = /* ERROR: no complex support in C */;
        double r688239 = /* ERROR: no complex support in C */;
        return r688239;
}
↓
double f(double x, double y) {
        double r688240 = 1.0;
        double r688241 = x;
        double r688242 = exp(r688241);
        double r688243 = r688240 / r688242;
        double r688244 = y;
        double r688245 = cos(r688244);
        double r688246 = r688243 * r688245;
        double r688247 = r688245 * r688242;
        double r688248 = r688246 + r688247;
        double r688249 = 0.5;
        double r688250 = r688248 * r688249;
        return r688250;
}

Error

Bits error versus x

Bits error versus y

Derivation

  1. Initial program 0.0

    \[\Re(\left(\frac{e^{x} + e^{-x}}{2} \cdot \cos y + \frac{e^{x} - e^{-x}}{2} \cdot \sin y i\right))\]

  2. Simplified0.0

    \[\leadsto \color{blue}{\frac{1}{2} \cdot \left(\frac{\cos y}{e^{x}} + \cos y \cdot e^{x}\right)}\]
  3. Using strategy rm

  4. Applied div-inv0.0

    \[\leadsto \frac{1}{2} \cdot \left(\color{blue}{\cos y \cdot \frac{1}{e^{x}}} + \cos y \cdot e^{x}\right)\]

  5. Final simplification0.0

    \[\leadsto \left(\frac{1}{e^{x}} \cdot \cos y + \cos y \cdot e^{x}\right) \cdot \frac{1}{2}\]

Reproduce

herbie shell --seed 2019135 
(FPCore (x y)
  :name "Euler formula real part (p55)"
  (re (complex (* (/ (+ (exp x) (exp (- x))) 2) (cos y)) (* (/ (- (exp x) (exp (- x))) 2) (sin y)))))