1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\frac{1 \cdot \frac{\left({1}^{3} - {0.5}^{3}\right) \cdot \mathsf{hypot}\left(1, x\right) - \left(1 \cdot 1 + \left(0.5 \cdot 0.5 + 1 \cdot 0.5\right)\right) \cdot 0.5}{\mathsf{hypot}\left(1, x\right) \cdot \left(0.5 \cdot \left(0.5 + 1\right) + 1 \cdot 1\right)}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}double f(double x) {
double r269767 = 1.0;
double r269768 = 0.5;
double r269769 = x;
double r269770 = hypot(r269767, r269769);
double r269771 = r269767 / r269770;
double r269772 = r269767 + r269771;
double r269773 = r269768 * r269772;
double r269774 = sqrt(r269773);
double r269775 = r269767 - r269774;
return r269775;
}
double f(double x) {
double r269776 = 1.0;
double r269777 = 3.0;
double r269778 = pow(r269776, r269777);
double r269779 = 0.5;
double r269780 = pow(r269779, r269777);
double r269781 = r269778 - r269780;
double r269782 = x;
double r269783 = hypot(r269776, r269782);
double r269784 = r269781 * r269783;
double r269785 = r269776 * r269776;
double r269786 = r269779 * r269779;
double r269787 = r269776 * r269779;
double r269788 = r269786 + r269787;
double r269789 = r269785 + r269788;
double r269790 = r269789 * r269779;
double r269791 = r269784 - r269790;
double r269792 = r269779 + r269776;
double r269793 = r269779 * r269792;
double r269794 = r269793 + r269785;
double r269795 = r269783 * r269794;
double r269796 = r269791 / r269795;
double r269797 = r269776 * r269796;
double r269798 = r269776 / r269783;
double r269799 = r269776 + r269798;
double r269800 = r269779 * r269799;
double r269801 = sqrt(r269800);
double r269802 = r269776 + r269801;
double r269803 = r269797 / r269802;
return r269803;
}



Bits error versus x
Results
Initial program 15.3
rmApplied flip--15.3
Simplified14.8
rmApplied flip3--14.8
Applied frac-sub14.9
Simplified14.9
Final simplification14.9
herbie shell --seed 2020033
(FPCore (x)
:name "Given's Rotation SVD example, simplified"
:precision binary64
(- 1 (sqrt (* 0.5 (+ 1 (/ 1 (hypot 1 x)))))))