1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\frac{0.25 - \frac{0.5}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{\left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}\right)}(FPCore (x) :precision binary64 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))
(FPCore (x) :precision binary64 (/ (- 0.25 (* (/ 0.5 (hypot 1.0 x)) (/ 0.5 (hypot 1.0 x)))) (* (+ 0.5 (/ 0.5 (hypot 1.0 x))) (+ 1.0 (sqrt (+ 0.5 (/ 0.5 (hypot 1.0 x))))))))
double code(double x) {
return 1.0 - sqrt(0.5 * (1.0 + (1.0 / hypot(1.0, x))));
}
double code(double x) {
return (0.25 - ((0.5 / hypot(1.0, x)) * (0.5 / hypot(1.0, x)))) / ((0.5 + (0.5 / hypot(1.0, x))) * (1.0 + sqrt(0.5 + (0.5 / hypot(1.0, x)))));
}



Bits error versus x
Results
Initial program 15.3
Simplified15.3
rmApplied flip--_binary6415.3
Simplified14.8
rmApplied flip--_binary6414.8
Applied associate-/l/_binary6414.8
Final simplification14.8
herbie shell --seed 2021174
(FPCore (x)
:name "Given's Rotation SVD example, simplified"
:precision binary64
(- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))