Average Error: 15.5 → 15.0
Time: 3.4s
Precision: binary64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[{e}^{\left(\log \left(\frac{1}{1 + \sqrt{1 \cdot \left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}} \cdot \frac{\mathsf{hypot}\left(1, x\right) \cdot \left(1 - 0.5\right) - 0.5}{\mathsf{hypot}\left(1, x\right)}\right)\right)}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
{e}^{\left(\log \left(\frac{1}{1 + \sqrt{1 \cdot \left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}} \cdot \frac{\mathsf{hypot}\left(1, x\right) \cdot \left(1 - 0.5\right) - 0.5}{\mathsf{hypot}\left(1, x\right)}\right)\right)}
double code(double x) {
	return ((double) (1.0 - ((double) sqrt(((double) (0.5 * ((double) (1.0 + (1.0 / ((double) hypot(1.0, x)))))))))));
}
↓
double code(double x) {
	return ((double) pow(((double) M_E), ((double) log(((double) ((1.0 / ((double) (1.0 + ((double) sqrt(((double) (1.0 * ((double) (0.5 + (0.5 / ((double) hypot(1.0, x)))))))))))) * (((double) (((double) (((double) hypot(1.0, x)) * ((double) (1.0 - 0.5)))) - 0.5)) / ((double) hypot(1.0, x)))))))));
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.5

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

  3. Applied flip--15.5

    \[\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.0

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

  5. Simplified15.0

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

  7. Applied flip--15.0

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

  8. Applied frac-sub15.0

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

  9. Simplified15.0

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

  10. Simplified15.0

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

  12. Applied add-exp-log15.0

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

  13. Applied add-exp-log15.0

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

  14. Applied add-exp-log17.7

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

  15. Applied prod-exp17.7

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

  16. Applied add-exp-log17.5

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

  17. Applied add-exp-log17.5

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

  18. Applied prod-exp17.4

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

  19. Applied div-exp17.4

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

  20. Applied add-exp-log17.4

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

  21. Applied prod-exp17.4

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

  22. Applied div-exp17.4

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

  23. Simplified15.0

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

  25. Applied pow115.0

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

  26. Applied pow115.0

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

  27. Applied pow-prod-down15.0

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

  28. Applied pow115.0

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

  29. Applied pow-prod-down15.0

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

  30. Applied log-pow15.0

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

  31. Applied exp-prod15.0

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

  32. Simplified15.0

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

  33. Final simplification15.0

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

Reproduce

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