Average Error: 15.7 → 15.3
Time: 4.0s
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{e^{\log \left(\frac{1 \cdot \left(\left(1 \cdot 1 - 0.5 \cdot 0.5\right) \cdot \mathsf{hypot}\left(1, x\right) - 0.5 \cdot \left(0.5 + 1\right)\right)}{\left(1 + 0.5\right) \cdot \mathsf{hypot}\left(1, x\right)}\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{e^{\log \left(\frac{1 \cdot \left(\left(1 \cdot 1 - 0.5 \cdot 0.5\right) \cdot \mathsf{hypot}\left(1, x\right) - 0.5 \cdot \left(0.5 + 1\right)\right)}{\left(1 + 0.5\right) \cdot \mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}
double f(double x) {
        double r179818 = 1.0;
        double r179819 = 0.5;
        double r179820 = x;
        double r179821 = hypot(r179818, r179820);
        double r179822 = r179818 / r179821;
        double r179823 = r179818 + r179822;
        double r179824 = r179819 * r179823;
        double r179825 = sqrt(r179824);
        double r179826 = r179818 - r179825;
        return r179826;
}
↓
double f(double x) {
        double r179827 = 1.0;
        double r179828 = r179827 * r179827;
        double r179829 = 0.5;
        double r179830 = r179829 * r179829;
        double r179831 = r179828 - r179830;
        double r179832 = x;
        double r179833 = hypot(r179827, r179832);
        double r179834 = r179831 * r179833;
        double r179835 = r179829 + r179827;
        double r179836 = r179829 * r179835;
        double r179837 = r179834 - r179836;
        double r179838 = r179827 * r179837;
        double r179839 = r179827 + r179829;
        double r179840 = r179839 * r179833;
        double r179841 = r179838 / r179840;
        double r179842 = log(r179841);
        double r179843 = exp(r179842);
        double r179844 = r179827 / r179833;
        double r179845 = r179827 + r179844;
        double r179846 = r179829 * r179845;
        double r179847 = sqrt(r179846);
        double r179848 = r179827 + r179847;
        double r179849 = r179843 / r179848;
        return r179849;
}

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.3

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

  6. Applied associate-*r/15.3

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

  7. Applied flip--15.3

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

  8. Applied associate-*r/15.3

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

  9. Applied frac-sub15.3

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

  10. Simplified15.3

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

  12. Applied add-exp-log18.0

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

  13. Applied add-exp-log18.0

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

  14. Applied prod-exp18.0

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

  15. Applied add-exp-log17.8

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

  16. Applied add-exp-log17.8

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

  17. Applied prod-exp17.8

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

  18. Applied div-exp17.8

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

  19. Simplified15.3

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

  20. Final simplification15.3

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

Reproduce

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