Average Error: 15.7 → 15.2
Time: 26.4s
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{\sqrt{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}} \cdot \sqrt{\frac{\log \left(e^{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{\sqrt{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}} \cdot \sqrt{\frac{\log \left(e^{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}
double f(double x) {
        double r185198 = 1.0;
        double r185199 = 0.5;
        double r185200 = x;
        double r185201 = hypot(r185198, r185200);
        double r185202 = r185198 / r185201;
        double r185203 = r185198 + r185202;
        double r185204 = r185199 * r185203;
        double r185205 = sqrt(r185204);
        double r185206 = r185198 - r185205;
        return r185206;
}
↓
double f(double x) {
        double r185207 = 1.0;
        double r185208 = r185207 * r185207;
        double r185209 = x;
        double r185210 = hypot(r185207, r185209);
        double r185211 = r185207 / r185210;
        double r185212 = r185207 + r185211;
        double r185213 = 0.5;
        double r185214 = r185212 * r185213;
        double r185215 = r185208 - r185214;
        double r185216 = sqrt(r185215);
        double r185217 = r185213 * r185212;
        double r185218 = sqrt(r185217);
        double r185219 = r185207 + r185218;
        double r185220 = sqrt(r185219);
        double r185221 = r185216 / r185220;
        double r185222 = exp(r185215);
        double r185223 = log(r185222);
        double r185224 = r185223 / r185219;
        double r185225 = sqrt(r185224);
        double r185226 = r185221 * r185225;
        return r185226;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.7

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

  3. Applied flip--15.7

    \[\leadsto \color{blue}{\frac{1 \cdot 1 - \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 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\]

  4. Simplified15.2

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

  6. Applied add-sqr-sqrt15.7

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

  7. Applied add-sqr-sqrt15.7

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

  8. Applied times-frac15.2

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

  10. Applied sqrt-undiv15.2

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

  12. Applied add-log-exp15.2

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

  13. Applied add-log-exp15.2

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

  14. Applied diff-log15.7

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

  15. Simplified15.2

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

  16. Final simplification15.2

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

Reproduce

herbie shell --seed 2019347 +o rules:numerics
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  :precision binary64
  (- 1 (sqrt (* 0.5 (+ 1 (/ 1 (hypot 1 x)))))))