Average Error: 15.1 → 14.6
Time: 24.9s
Precision: 64
\[1 - \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\sqrt{1 - \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}} \cdot \frac{\sqrt{1 - \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}}}{1 + \left(\left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right)}\]
1 - \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\sqrt{1 - \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}} \cdot \frac{\sqrt{1 - \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}}}{1 + \left(\left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right)}
double f(double x) {
        double r4400723 = 1.0;
        double r4400724 = 0.5;
        double r4400725 = x;
        double r4400726 = hypot(r4400723, r4400725);
        double r4400727 = r4400723 / r4400726;
        double r4400728 = r4400723 + r4400727;
        double r4400729 = r4400724 * r4400728;
        double r4400730 = sqrt(r4400729);
        double r4400731 = r4400723 - r4400730;
        return r4400731;
}
↓
double f(double x) {
        double r4400732 = 1.0;
        double r4400733 = 0.5;
        double r4400734 = x;
        double r4400735 = hypot(r4400732, r4400734);
        double r4400736 = r4400733 / r4400735;
        double r4400737 = r4400733 + r4400736;
        double r4400738 = sqrt(r4400737);
        double r4400739 = r4400737 * r4400738;
        double r4400740 = r4400732 - r4400739;
        double r4400741 = sqrt(r4400740);
        double r4400742 = r4400737 + r4400738;
        double r4400743 = r4400732 + r4400742;
        double r4400744 = r4400741 / r4400743;
        double r4400745 = r4400741 * r4400744;
        return r4400745;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.1

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

  2. Simplified15.1

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

  4. Applied flip3--15.4

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

  5. Simplified15.1

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

  6. Simplified14.6

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

  8. Applied *-un-lft-identity14.6

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

  9. Applied *-un-lft-identity14.6

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

  10. Applied distribute-lft-out14.6

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

  11. Applied add-sqr-sqrt14.6

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

  12. Applied times-frac14.6

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

  13. Simplified14.6

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

  14. Final simplification14.6

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

Reproduce

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