Average Error: 15.1 → 14.6
Time: 40.9s
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{\log \left(e^{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot \left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)\right)}\right)}{1 \cdot \left(\sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} + 1\right) + 0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{\log \left(e^{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot \left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)\right)}\right)}{1 \cdot \left(\sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} + 1\right) + 0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}
double f(double x) {
        double r7852398 = 1.0;
        double r7852399 = 0.5;
        double r7852400 = x;
        double r7852401 = hypot(r7852398, r7852400);
        double r7852402 = r7852398 / r7852401;
        double r7852403 = r7852398 + r7852402;
        double r7852404 = r7852399 * r7852403;
        double r7852405 = sqrt(r7852404);
        double r7852406 = r7852398 - r7852405;
        return r7852406;
}
↓
double f(double x) {
        double r7852407 = 1.0;
        double r7852408 = r7852407 * r7852407;
        double r7852409 = r7852407 * r7852408;
        double r7852410 = 0.5;
        double r7852411 = x;
        double r7852412 = hypot(r7852407, r7852411);
        double r7852413 = r7852407 / r7852412;
        double r7852414 = r7852413 + r7852407;
        double r7852415 = r7852410 * r7852414;
        double r7852416 = sqrt(r7852415);
        double r7852417 = r7852416 * r7852415;
        double r7852418 = r7852409 - r7852417;
        double r7852419 = exp(r7852418);
        double r7852420 = log(r7852419);
        double r7852421 = r7852416 + r7852407;
        double r7852422 = r7852407 * r7852421;
        double r7852423 = r7852422 + r7852415;
        double r7852424 = r7852420 / r7852423;
        return r7852424;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.1

    \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
  2. Using strategy rm

  3. Applied flip3--15.4

    \[\leadsto \color{blue}{\frac{{1}^{3} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{1 \cdot 1 + \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}}\]

  4. Simplified15.1

    \[\leadsto \frac{\color{blue}{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}}{1 \cdot 1 + \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}\]

  5. Simplified14.6

    \[\leadsto \frac{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}{\color{blue}{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5 + 1 \cdot \left(1 + \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}}\]
  6. Using strategy rm

  7. Applied add-log-exp14.6

    \[\leadsto \frac{\color{blue}{\log \left(e^{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}\right)}}{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5 + 1 \cdot \left(1 + \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}\]
  8. Using strategy rm

  9. Applied *-un-lft-identity14.6

    \[\leadsto \frac{\log \left(e^{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}\right)}{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5 + 1 \cdot \left(1 + \sqrt{\left(1 + \frac{1}{\color{blue}{1 \cdot \mathsf{hypot}\left(1, x\right)}}\right) \cdot 0.5}\right)}\]

  10. Applied *-un-lft-identity14.6

    \[\leadsto \frac{\log \left(e^{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}\right)}{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5 + 1 \cdot \left(1 + \sqrt{\left(1 + \frac{\color{blue}{1 \cdot 1}}{1 \cdot \mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}\]

  11. Applied times-frac14.6

    \[\leadsto \frac{\log \left(e^{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}\right)}{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5 + 1 \cdot \left(1 + \sqrt{\left(1 + \color{blue}{\frac{1}{1} \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}\right) \cdot 0.5}\right)}\]

  12. Simplified14.6

    \[\leadsto \frac{\log \left(e^{\left(1 \cdot 1\right) \cdot 1 - \left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right) \cdot \sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}\right)}{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5 + 1 \cdot \left(1 + \sqrt{\left(1 + \color{blue}{1} \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}\]

  13. Final simplification14.6

    \[\leadsto \frac{\log \left(e^{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot \left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)\right)}\right)}{1 \cdot \left(\sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} + 1\right) + 0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}\]

Reproduce

herbie shell --seed 2019168 
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))