Average Error: 15.1 → 14.6
Time: 2.8m
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{\left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} + \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right) \cdot \left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} - \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right)}{\mathsf{fma}\left(\sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}, 1, \mathsf{fma}\left(1, 1, \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5} + \left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)\right)}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{\left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} + \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right) \cdot \left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} - \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right)}{\mathsf{fma}\left(\sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}, 1, \mathsf{fma}\left(1, 1, \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5} + \left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)\right)}
double f(double x) {
        double r10001571 = 1.0;
        double r10001572 = 0.5;
        double r10001573 = x;
        double r10001574 = hypot(r10001571, r10001573);
        double r10001575 = r10001571 / r10001574;
        double r10001576 = r10001571 + r10001575;
        double r10001577 = r10001572 * r10001576;
        double r10001578 = sqrt(r10001577);
        double r10001579 = r10001571 - r10001578;
        return r10001579;
}
↓
double f(double x) {
        double r10001580 = 1.0;
        double r10001581 = r10001580 * r10001580;
        double r10001582 = r10001581 * r10001580;
        double r10001583 = 3.0;
        double r10001584 = pow(r10001582, r10001583);
        double r10001585 = sqrt(r10001584);
        double r10001586 = x;
        double r10001587 = hypot(r10001580, r10001586);
        double r10001588 = r10001580 / r10001587;
        double r10001589 = r10001588 + r10001580;
        double r10001590 = 0.5;
        double r10001591 = r10001589 * r10001590;
        double r10001592 = sqrt(r10001591);
        double r10001593 = r10001591 * r10001592;
        double r10001594 = pow(r10001593, r10001583);
        double r10001595 = sqrt(r10001594);
        double r10001596 = r10001585 + r10001595;
        double r10001597 = r10001585 - r10001595;
        double r10001598 = r10001596 * r10001597;
        double r10001599 = fma(r10001580, r10001580, r10001591);
        double r10001600 = fma(r10001592, r10001580, r10001599);
        double r10001601 = r10001593 + r10001582;
        double r10001602 = r10001601 * r10001593;
        double r10001603 = fma(r10001582, r10001582, r10001602);
        double r10001604 = r10001600 * r10001603;
        double r10001605 = r10001598 / r10001604;
        return r10001605;
}

Error

Bits error versus x

Derivation

  1. Initial program 15.1

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

  3. Applied flip3--15.3

    \[\leadsto \color{blue}{\frac{{1}^{3} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{1 \cdot 1 + \left(\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 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}}\]

  4. Simplified15.1

    \[\leadsto \frac{\color{blue}{\left(1 \cdot 1\right) \cdot 1 - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}{1 \cdot 1 + \left(\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 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}\]

  5. Simplified14.6

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

  7. Applied flip3--15.1

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

  8. Applied associate-/l/15.1

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

  9. Simplified14.6

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

  11. Applied add-sqr-sqrt14.6

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

  12. Applied add-sqr-sqrt14.6

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

  13. Applied difference-of-squares14.6

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

  14. Final simplification14.6

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

Reproduce

herbie shell --seed 2019200 +o rules:numerics
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))