Average Error: 15.4 → 14.9
Time: 4.1s
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 r180157 = 1.0;
        double r180158 = 0.5;
        double r180159 = x;
        double r180160 = hypot(r180157, r180159);
        double r180161 = r180157 / r180160;
        double r180162 = r180157 + r180161;
        double r180163 = r180158 * r180162;
        double r180164 = sqrt(r180163);
        double r180165 = r180157 - r180164;
        return r180165;
}
↓
double f(double x) {
        double r180166 = 1.0;
        double r180167 = r180166 * r180166;
        double r180168 = 0.5;
        double r180169 = r180168 * r180168;
        double r180170 = r180167 - r180169;
        double r180171 = x;
        double r180172 = hypot(r180166, r180171);
        double r180173 = r180170 * r180172;
        double r180174 = r180168 + r180166;
        double r180175 = r180168 * r180174;
        double r180176 = r180173 - r180175;
        double r180177 = r180166 * r180176;
        double r180178 = r180166 + r180168;
        double r180179 = r180178 * r180172;
        double r180180 = r180177 / r180179;
        double r180181 = log(r180180);
        double r180182 = exp(r180181);
        double r180183 = r180166 / r180172;
        double r180184 = r180166 + r180183;
        double r180185 = r180168 * r180184;
        double r180186 = sqrt(r180185);
        double r180187 = r180166 + r180186;
        double r180188 = r180182 / r180187;
        return r180188;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.4

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

  3. Applied flip--15.4

    \[\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. Simplified14.9

    \[\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/14.9

    \[\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--14.9

    \[\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/14.9

    \[\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-sub14.9

    \[\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. Simplified14.9

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

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

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

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

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

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

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

    \[\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. Simplified14.9

    \[\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 simplification14.9

    \[\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 2020049 
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  :precision binary64
  (- 1 (sqrt (* 0.5 (+ 1 (/ 1 (hypot 1 x)))))))